Introduction to Programming in ATS:
<<< Previous		Next >>>

Introduction to Dependent Types

The types we have encountered so far in this book cannot offer adequate precision for capturing programming invariants. For instance, if we assign the type int to both of 0 and 1, then we simply cannot distinguish 0 from 1 at the level of types. This means that 0 and 1 are interchangeable as far as typechecking is concerned. In other words, we cannot expect a program error to be caught during typechecking if the error is caused by 0 being mistyped as 1. This form of imprecision in types is a crippling limitation if we ever want to build a type-based specification language that is reasonably expressive for practical use.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

Enhanced Expressiveness for Specification

The primary purpose of introducing dependent types into the type system of ATS is to greatly enhance the expressiveness of types so that they can be employed to capture program invariants with much more precision. Generally speaking, dependent types are types dependent on values of expressions. For instance, bool is a type constructor in ATS that forms a type bool(b) when applied to a given boolean value b. As this type can only be assigned to a boolean expression of the value b, it is often referred to as a singleton type, that is, a type for exactly one value. Clearly, the meaning of bool(b) depends on the boolean value b. Similarly, int is a type constructor in ATS that forms a type int(i) when applied to a given integer i. This type is also a singleton type as it can only be assigned to an integer expression of the value i. Note that both bool and int are overloaded as they also refer to (non-dependent) types. I will gradually introduce many other examples of dependent types. In particular, I will present a means for the programmer to declare dependent datatypes.

The statics of ATS is a simply-typed language, and the types in this language are called sorts so as to avoid some potential confusion (with the types for dynamic terms). The following four listed sorts are commonly used:

bool: for static terms of boolean values
int: for static terms of integer values
type: for static terms representing boxed types (for dynamic terms)
t@ype: for static terms representing unboxed types (for dynamic terms)

The sorts bool and int are classified as predicative sorts while the sorts type and t@ype are impredicative. A boxed type is a static term of the sort type while an unboxed type is a static term of the sort t@ype. As types, bool and int are static terms of the sort t@ype. As type constructors, bool and int are static terms of the sorts (bool) -> t@ype and (int) -> t@ype, respectively. Also note that the type constructor list0 is of the sort (t@ype) -> type, which indicates that list0 forms a boxed type when applied to an unboxed one. There are also various built-in static functions in ATS for constructing static terms of the sorts bool and int, and I list as follows some of these functions together with the sorts assigned to them:

~ (integer negation): (int) -> int
+ (addition): (int, int) -> int
- (subtraction): (int, int) -> int
* (multiplication): (int, int) -> int
/ (division): (int, int) -> int
> (greater-than): (int, int) -> bool
>= (greater-than-or-equal-to): (int, int) -> bool
< (less-than): (int, int) -> bool
<= (less-than-or-equal-to): (int, int) -> bool
== (equal-to): (int, int) -> bool
<> (not-equal-to): (int, int) -> bool
~ (boolean negation): (bool) -> bool
|| (disjunction): (bool, bool) -> bool
&& (conjunction) : (bool, bool) -> bool

By combining a sort with one or more predicates, we can define a subset sort. For instance, the following subset sorts are defined in the file prelude/sortdef.sats, which is automatically loaded by the ATS compiler:

sortdef nat = {a: int | a >= 0} // for natural numbers
sortdef pos = {a: int | a > 0}  // for positive numbers
sortdef neg = {a: int | a < 0}  // for negative numbers

sortdef two = {a: int | 0 <= a; a <= 1} // for 0 or 1
sortdef three = {a: int | 0 <= a; a <= 2} // for 0, 1 or 2

Note that predicates can be sequenced together with the semicolon symbol (;). It is also possible to define the subset sorts two and three as follows:

sortdef two = {a: int | a == 0 || a == 1} // for 0 or 1
sortdef three = {a: int | 0 <= a && a <= 2} // for 0, 1 or 2

Another possibility is to define a subset sort based on an existing one plus some predicates. For instance, the subset sorts two and three can also be given the following definitions:

sortdef two = {a: nat | a <= 1} // for 0 or 1
sortdef three = {a: nat | a <= 2} // for 0, 1 or 2

In order to unleash the expressiveness of dependent types, we need to employ both universal and existential quantification over static variables. For instance, the type Int in ATS is defined as follows:

typedef Int = [a:int] int (a) // for unspecified integers

where the syntax [a:int] means existential quantification over a static variable a of the sort int. Essentially, this means that for each value of the type Int, there exists an integer I such that the value is of the type int(I). Therefore, any value that can be given the type int can also be given the type Int. A type like Int is often referred to as an existentially quantified type. As another example, the type Nat in ATS is defined as follows:

typedef Nat = [a:int | a >= 0] int (a) // for natural numbers

where the syntax [a:int | a >= 0] means existential quantification over a static variable a of the sort int that satisfies the constraint a >= 0. Therefore, each value of the type Nat can be assigned the type int(I) for some integer I satisfying I >= 0. Given that int(I) is a singleton type, the value equals I and thus is a natural number. This means that the type Nat is for natural numbers. The definition of Nat can also be given as follows:

typedef Nat = [a:nat] int (a) // for natural numbers

where the syntax [a:nat] is just a form of syntactic sugar that automatically expands into [a:int | a >= 0].

At this point, types have already become much more expressive. For instance, we could only assign the type (int) -> int to a function that maps integers to natural numbers (e.g., the function that computes the absolute value of a given integer), but we can now do better by assigning it the type (Int) -> Nat, which is clearly more precise. In order to relate at the level of types the return value of a function to its arguments, we need universal quantification. For instance, the following universally quantified type is for a function that returns the successor of its integer argument:

{i:int} int (i) -> int (i+1)

where the syntax {i:int} means universal quantification over a static variable i of the sort int and the scope of this quantification is the function type following it. One may think that this function type is also a singleton type as the only function of this type is the successor function on integers. Actually, there are infinitely may partial functions that can be given this type as well. For the successor function on natural numbers, we can use the following type:

{i:int | i >= 0} int (i) -> int (i+1)

where the syntax {i:int | i >= 0} means universal quantification over a static variable i of the sort int that satisfies the constraint i >= 0. This type can also be written as follows:

{i:nat} int (i) -> int (i+1)

where the syntax {i:nat} automatically expands into {i:int | i >= 0}. I list as follows the interfaces for some commonly used functions on integers:

fun ineg {i:int} (i: int i): int (~i) // negation
fun iadd {i,j:int} (i: int i, j: int j): int (i+j) // addition
fun isub {i,j:int} (i: int i, j: int j): int (i-j) // subtraction
fun imul {i,j:int} (i: int i, j: int j): int (i*j) // multiplication
fun idiv {i,j:int} (i: int i, j: int j): int (i/j) // division

fun ilt {i,j:int} (i: int i, j: int j): bool (i < j) // less-than
fun ilte {i,j:int} (i: int i, j: int j): bool (i <= j) // less-than-or-equal-to
fun gt {i,j:int} (i: int i, j: int j): bool (i > j) // greater-than
fun gte {i,j:int} (i: int i, j: int j): bool (i >= j) // greater-than-or-equal-to
fun eq {i,j:int} (i: int i, j: int j): bool (i == j) // equal-to
fun neq {i,j:int} (i: int i, j: int j): bool (i <> j) // not-equal-to

These interfaces are all declared in the file prelude/SATS/integer.sats, which is automatically loaded by the ATS compiler.

It is now a proper moment for me to raise an interesting question: What does a dependently typed interface for the factorial function look like? After seeing the above examples, it is natural for one to expect something along the following line:

fun ifact {i:nat} (i: int i): int (fact (i))

where fact is a static version of the factorial function. The problem with this solution is that a static function like fact cannot be defined in ATS. The statics of ATS is a simply-typed language that does not allow any recursive means to be employed in the construction of static terms. This design is adopted primarily to ensure that the equality on static terms can be decided based on a practical algorithm. As typechecking involving dependent types essentially turns into verifying whether a set of equalities (and some built-in predicates) on static terms hold, such a design is of vital importance to the goal of supporting practical programming with dependent types. In order to assign an interface to the factorial function that precisely matches the definition of the function, we need to employ a mechanism in ATS for combining programming with theorem-proving. This is a topic I will cover later.

<<< Previous	Home	Next >>>
Dependent Types for Programming	Up	Constraint-Solving during Typechecking