Introduction to Programming in ATS: | ||
---|---|---|

<<< Previous | Next >>> |

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.

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)

~ (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*

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 |

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 |

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 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 |

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:

where<<< Previous | Home | Next >>> |

Dependent Types for Programming | Up | Constraint-Solving during Typechecking |