Chapter 9. Introduction to Dependent Types

Table of Contents
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

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.

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

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 a variety of 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:

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 basics_pre.sats, which is automatically loaded by the ATS compiler:

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

Note that predicates can be sequenced together with the semicolon symbol (;) to form a conjunction:

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

It is also possible to define the subset sorts nat2 and nat3 as follows:

sortdef nat2 = {a: int | a == 0 || a == 1} // for 0, 1 sortdef nat3 = {a: int | 0 <= a && a <= 2} // for 0, 1, 2

where || and && stands for disjunction and conjunction, respectively.

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

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

These interfaces are all declared in the file integer.sats, which is automatically loaded by the ATS compiler. Note that the functions listed here can all be referred to by their standard names: ~ for g1int_neg, + for g1int_add, - for g1int_sub, * for g1int_mul, / for g1int_div, < for g1int_lt, <= for g1int_lte, > for g1int_gt, >= for g1int_gte, = for g1int_eq, != for g1int_neq, <> for g1int_neq (most of the time).

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:

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

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.