Introduction to Programming in ATS

Hongwei Xi

<hwxi AT cs DOT bu DOT edu>

Copyright © 2010-201? Hongwei Xi

0.0.1

Dedication

To Jinning and Zoe.

Table of Contents

I. Basic Functional Programming

Preparation for Starting

A Running Program
A Template for Single-File Programs
A Makefile Template

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

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
Tail-Call and Tail-Recursion
Example: Solving the Eight Queens Puzzle
Mutually Recursive Functions
Mutual Tail-Recursion
Envless Functions and Closure Functions
Higher-Order Functions
Example: Binary Search
Currying and Uncurrying

Patterns
Pattern-Matching
Matching Clauses and Case-Expressions
Enumerative Datatypes
Recursive Datatypes
Exhaustiveness of Pattern-Matching
Example: Evaluating Integer Expressions

Parametric Polymorphism

Function Templates
Polymorphic Functions
Polymorphic Datatypes
Example: Function Templates on Lists
Example: Mergesort on Lists

II. Support for Practical Programming

Effectful Programming Features

Exceptions
Example: Testing for Braun Trees
References
Example: Implementing Counters
Arrays
Example: Ordering Permutations
Matrices
Example: Estimating the Constant Pi
Simple Input and Output

Convenience in Programming

Macro Definitions
Compile-Time Directives
Overloading

Types as a Form of Specification
Static and Dynamic ATS Files
Generic Template Implementation
Abstract Types
Example: A Package for Rationals
Example: A Functorial Package for Rationals
Specific Template Implementation
Example: A Temptorial Package for Rationals

Library Support

The prelude Library
The libc Library
The libats Library
Contributed Packages

Interaction with the C Programming Language

III. Dependent Types for Programming

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

Datatype Refinement

Dependent Datatypes
Example: Function Templates on Lists (Redux)
Example: Mergesort on Lists (Redux)
Sequentiality of Pattern Matching
Example: Functional Random-Access Lists
Example: Functional Red-Black Trees

Theorem-Proving in ATS/LF

Encoding Relations as Dataprops
Constructing Proofs as Total Functions
Example: Proving Distributivity of Multiplication
Datasorts
Example: Proving Properties on Braun Trees

Programming with Theorem-Proving

Circumventing Nonlinear Constraints
Example: Safe Matrix Subscripting
Specifying with Enhanced Precision
Example: Another Verified Factorial Implementation
Example: Verified Fast Exponentiation

IV. Linear Types for Programming

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

Dataviews as Linear Dataprops

Optional Views
Linear Arrays
Singly-Linked Lists
Proof Functions for View Changes
Example: Quicksort

Dataviewtypes as Linear Datatypes

Linear Optional Values
Linear Lists
Example: Mergesort on Linear Lists
Linear Binary Search Trees
Transition from Datatypes to Dataviewtypes

Abstract Views and Viewtypes

Memory Allocation and Deallocation
Simple Linear Objects
Example: Implementing an Array-Based Circular Buffer
From linearity to non-linearity

		Next >>>
		Preface