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 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: 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 is thus a natural number. This means that the type Nat is for natural numbers. The definition of Nat can also be given as follows: 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:
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 many 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 sort int that satisfies the constraint i >= 0. This type can also be written as follows: 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 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 fact is a static version of the factorial function. The very 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.