- The following is a tiny example of DML code. This example demonstrates
that we can define a zip function which can only be applied to
a pair of lists of the same length.
datatype 'a list with nat =
nil(0)
| {n:nat} cons(n+1) 'a * 'a list(n)
The withtype clause is a type annotation supplied by the
programmer. Note that <n> is a metric used to
verify that this function is terminating.
fun zip ([], []) = []
| zip (x :: xs, y :: ys) = (x, y) :: zip (xs, ys)
withtype {n:nat} <n> => 'a list(n) * 'b list(n) -> ('a * 'b) list(n)
This leads to a safer and faster implementation of zip
than a correspnding one in Standard ML.
- The following example defines a size function for Braun trees. A
binary tree is a Braun tree if for every branch node, the the size of
its left son is the same as or one more than that of the right son.
It can be readily proven that Braun trees are balanced trees. Notice
that the following declared datatype for Braun trees precisely
captures the invariant of Braun trees.
datatype 'a brauntree with nat =
L(0)
| {m:nat, n:nat | n <= m <= n+1}
B(m+n+1) of 'a * 'a brauntree(m) * 'a brauntree(n)
fun('a)
diff (k, L) = 0
| diff (k, B(_, l, r)) =
if k = 0 then 1
else if k % 2 = 1 then diff (k/2, l) else diff (k/2 - 1, r)
withtype {k:nat, n:nat | k <= n <= k+1} <n> => int(k) * 'a brauntree(n) -> int(n-k)
fun('a)
size (L) = 0
| size (B(_, l, r)) =
let val n = size r in 1 + n + n + diff (n, l) end
withtype {n:nat} <n> => 'a brauntree(n) -> int(n)
- The following is an example in de Caml, a dialect of DML based on Caml-light.
type order = LESS | EQUAL | GREATER
and 'a answer = NotFound | Found of int * 'a ;;
This program implements a binary search function on vectors.
The novelty in the program is that all array accesses have been
verified to be safe through type-checking in de Caml.
let{size:nat} binary_search cmp key vec =
let rec look(lo, hi) =
if ge_int hi lo then
let m = (hi + lo) / 2 in
let x = vec..(m) in
match cmp key x with
LESS -> look(lo, m-1)
| GREATER -> look(m+1, hi)
| EQUAL -> Found(m, x)
else NotFound
withtype {l:int}{h:int | 0 <= l <= size /\ 0 <= h+1 <= size }
int(l) * int(h) -> 'a answer in
look (0, vect_length vec - 1)
withtype ('a -> 'a -> order) -> 'a -> 'a vect(size) -> 'a answer
;;
Notice that the index m in the program is not monotonic.
Therefore, it seems highly
challenging for an approach based on flow analysis to
eliminate array bound checks in this example.