Introduction to Programming in ATS

Hongwei Xi

ATS Trustful Software, Inc.

As a programming language, ATS is both syntax-rich and feature-rich. This book introduces the reader to some core features of ATS, including basic functional programming, simple types, (recursively defined) datatypes, polymorphic types, dependent types, linear types, theorem-proving, programming with theorem-proving (PwTP), and template-based programming. Although the reader is not assumed to be familiar with programming in general, the book is likely to be rather dense for someone without considerable programming experience.

All rights are reserved. Permission is granted to print this document for personal use.


To Jinning, Zoe, and Chloe.

Table of Contents
I. Basic Functional Programming
1. Preparation for Starting
A Running Program
A Template for Single-File Programs
A Makefile Template
2. Elements of Programming
Expressions and Values
Names and Bindings
Scopes for Bindings
Environments for Evaluation
Static Semantics
Primitive Types
Tuples and Tuple Types
Records and Record Types
Conditional Expressions
Sequence Expressions
Comments in Code
3. Functions
Functions as a Simple Form of Abstraction
Function Arity
Function Interface
Evaluation of Function Calls
Recursive Functions
Evaluation of Recursive Function Calls
Example: Coin Changes for Fun
Tail-Call and Tail-Recursion
Example: The Eight-Queens Puzzle
Mutually Recursive Functions
Mutually Defined Tail-Recursion
Envless Functions and Closure-Functions
Higher-Order Functions
Example: Binary Search for Fun
Example: A Higher-Order Fun Puzzle
Currying and Uncurrying
4. Datatypes
Matching Clauses and Case-Expressions
Enumerative Datatypes
Recursively Defined Datatypes
Exhaustiveness of Pattern-Matching
Example: Binary Search Tree
Example: Evaluating Integer Expressions
5. Parametric Polymorphism
Function Templates
Polymorphic Functions
Polymorphic Datatypes
Example: Function Templates on Lists
Example: Mergesort on Lists
II. Support for Practical Programming
6. Effectful Programming Features
Example: Testing for Braun Trees
Example: A Counter Implementation
Example: Ordering Permutations
Example: Estimating the Constant Pi
Simple Input and Output
7. Modularity
Types as a Form of Specification
Static and Dynamic ATS Files
Generic Template Implementation
Specific Template Implementation
Abstract Types
Example: A Package for Rationals
Example: A Functorial Package for Rationals
8. Interaction with C
External Global Names
External Types and Values in ATS
Inclusion of External Code in ATS
Calling External Functions in ATS
Unsafe C-style Programming in ATS
Exporting Types in ATS for Use in C
Example: Constructing a Statically Allocated List
III. Programming with Dependent Types
9. Introduction to Dependent Types
Enhanced Expressiveness for Specification
Constraint-Solving during Typechecking
Example: String Processing
Example: Binary Search on Arrays
Termination-Checking for Recursive Functions
Example: Dependent Types for Debugging
10. Datatype Refinement
Dependent Datatypes
Example: Function Templates on Lists (Redux)
Example: Mergesort on Lists (Redux)
Sequentiality of Pattern Matching
Example: Functional Red-Black Trees
11. Theorem-Proving in ATS/LF
Encoding Relations as Dataprops
Constructing Proofs as Total Functions
Example: Distributivity of Multiplication
Example: Commutativity of Multiplication
Algebraic Datasorts
Example: Establishing Properties on Braun Trees
Programmer-Centric Theorem-Proving
12. Programming with Theorem-Proving
Circumventing Nonlinear Constraints
Example: Safe Matrix Subscripting
Specifying with Enhanced Precision
Example: Another Verified Factorial
Example: Verified Fast Exponentiation
IV. Programming with Views and Viewtypes
13. Introduction to Views and Viewtypes
Views for Memory Access through Pointers
Viewtypes as a Combination of Views and Types
Left-Values and Call-by-Reference
Stack-Allocated Variables
Heap-Allocated Linear Closure-Functions
14. Dataviews as Linear Dataprops
Optional Views
Disjunctive Views
Dataview for Linear Arrays
Dataview for Linear Strings
Dataview for Singly-Linked Lists
Proof Functions for View-Changes
15. Dataviewtypes as Linear Datatypes
Linear Optional Values
Linear Lists
Example: Merge-Sort on Linear Lists
Example: Insertion Sort on Linear Lists
Example: Quick-Sort on Linear Lists
Linear Binary Search Trees
Transition from Datatypes to Dataviewtypes
16. Abstract Views and Viewtypes
Simple Linear Objects
Memory Allocation and Deallocation
Example: Array-Based Circular Buffers
Locking and Unlocking
Linear Channels for Asynchronous IPC
V. Programming with Function Templates
17. From Genericity to Late-Binding
Genericity of Template Implementations
Example: Generic Operations on Numbers
Templates as a Special Form of Functors
Example: Templates for Loop Construction
Template-Based Support for Late-Binding