The types we have encountered so far in this book are often not adequately precise in capturing programming invariants. For instance, if we assign the type int to both of integers 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 can become 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.

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 greater 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. Please 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 flexible 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)

~ (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*<> (not-equal-to):

*(int, int) -> bool*~ (boolean negation):

*(bool) -> bool*|| (disjunction):

*(bool, bool) -> bool*&& (conjunction) :

*(bool, bool) -> bool*

sortdef nat = {a: int | a >= 0} // for natural numbers sortdef pos = {a: int | a >= 1} // for positive numbers sortdef neg = {a: int | a <= ~1} // for negative numbers sortdef nat1 = {a: nat | a < 1} // for 0 sortdef nat2 = {a: nat | a < 2} // for 0, 1 sortdef nat3 = {a: nat | a < 3} // for 0, 1, 2 sortdef nat4 = {a: nat | a < 4} // for 0, 1, 2, 3

sortdef nat2 = {a: int | 0 <= a; a < 2} // for 0, 1 sortdef nat3 = {a: int | 0 <= a; a < 3} // for 0, 1, 2 sortdef sgn = { i:int | ~1 <= i; i <= 1 } // for ~1, 0, 1

sortdef nat2 = {a: int | a == 0 || a == 1} // for 0, 1 sortdef nat3 = {a: int | 0 <= a && a <= 2} // for 0, 1, 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:

where the syntax [a:int] means existential quantification over a static variable a of the sortAt 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:

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: where the syntax {i:int | i >= 0} means universal quantification over a static variable i of the sortfun g1int_neg {i:int} (int i): int(~i) // negation fun g1int_add {i,j:int} (int i, int j): int(i+j) // addition fun g1int_sub {i,j:int} (int i, int j): int(i-j) // subtraction fun g1int_mul {i,j:int} (int i, int j): int(i*j) // multiplication fun g1int_div {i,j:int} (int i, int j): int(i/j) // division fun g1int_lt {i,j:int} (int i, int j): bool(i < j) // less-than fun g1int_lte {i,j:int} (int i, int j): bool(i <= j) // less-than-or-equal-to fun g1int_gt {i,j:int} (int i, int j): bool(i > j) // greater-than fun g1int_gte {i,j:int} (int i, int j): bool(i >= j) // greater-than-or-equal-to fun g1int_eq {i,j:int} (int i, int j): bool(i == j) // equal-to fun g1int_neq {i,j:int} (int i, int j): bool(i != j) // not-equal-to

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 only natural for one to expect something along the following line of thought:

where