Length-indexed Lists

Even and Odd-lengthed Lists

Our first example is bit artifical, but helps illustrate a usage of mutually inductive types.

Here, we’re defining two types constructors called even and odd, (i.e, just \(T_1\) and \(T_2\) from our formal definition), both with a single parameter (a:Type), for the type of the lists’ elements, and no indexes.

All lists of type even a have an even number of elements—zero elements, using its first constructor ENil, or using ECons, one more than the number of elements in an odd a, a list with an odd number of elements. Elements of the type odd a are constructed using the constructor OCons, which adds a single element to an even a list. The types are mutually inductive since their definitions reference each other.

type even (a:Type) =
 | ENil : even a
 | ECons : a -> odd a -> even a
and odd (a:Type) =
 | OCons : a -> even a -> odd a

Although closely related, the types even a and odd a are from distinct inductive types. So, to compute, say, the length of one of these lists one generally write a pair of mutually recursive functions, like so:

let rec elength #a (e:even a)
  : n:nat { n % 2 == 0}
  = match e with
    | ENil -> 0
    | ECons _ tl -> 1 + olength tl
and olength #a (o:odd a)
  : n:nat { n % 2 == 1 }
  = let OCons _ tl = o in
    1 + elength tl

Note, we can prove that the length of an even a and odd a are really even and odd.

Now, say, you wanted to map a function over an even a, you’d have to write a pair of mutually recursive functions to map simultaneoulsy over them both. This can get tedious quickly. Instead of rolling out several mutually inductive but distinct types, one can instead use an indexed type to group related types in the same inductive family of types.

The definition of even_or_odd_list below shows an inductive type with one parameter a, for the type of lists elements, and a single boolean index, which indicates whether the list is even or odd. Note how the index varies in the types of the constructors, whereas the parameter stays the same in all instances.

type even_or_odd_list (a:Type) : bool -> Type =
 | EONil : even_or_odd_list a true
 | EOCons : a -> #b:bool -> even_or_odd_list a b -> even_or_odd_list a (not b)

Now, we have a single family of types for both even and odd lists, and we can write a single function that abstracts over both even and odd lists, just by abstracting over the boolean index. For example, eo_length computes the length of an even_or_odd_list, with its type showing that it returns an even number with b is true and an odd number otherwise.

let rec eo_length #a #b (l:even_or_odd_list a b)
  : Tot (n:nat { if b then n % 2 == 0 else n % 2 == 1})
        (decreases l)
  = match l with
    | EONil -> 0
    | EOCons _ tl -> 1 + eo_length tl

This is our first type with with both parameters and indices. But why stop at just indexing to distinguish even and odd-lengthed lists? We can index a list by its length itself.

Vectors

Let’s look again at the definition of the vec type, first shown in the introduction.

type vec (a:Type) : nat -> Type =
  | Nil : vec a 0
  | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)

Here, we’re defining just a single type constructor called vec (i.e, just \(T_1\)), which a single parameter (a:Type) and one index nat.

vec has two data constructors: Nil builds an instance of vec a 0, the empty vector; and Cons hd tl builds an instance of vec a (n + 1) from a head element hd:a and a tail tl : vec a n. That is, the two constructors build different instances of vec—those instances have the same parameter (a), but different indexes (0 and n + 1).

type option a =
  | None
  | Some of a

type option a =
  | None : option a
  | Some : a -> option a

Getting an element from a vector

With our length-indexed vec type, one can write functions with types that make use of the length information to ensure that they are well-defined. For example, to get the i th element of a vector, one can write:

let rec get #a #n (i:nat{i < n}) (v:vec a n)
  : a
  = match v with
    | Nil -> false_elim()
    | Cons hd tl ->
      if i = 0 then hd
      else get (i - 1) tl

The type of get i v says that i must be less than n, where n is the length of v, i.e., that i is within bounds of the vector, which is enough to prove that get i v can always return an element of type a. Let’s look a bit more closely at how this function is typechecked by F*.

The first key bit is pattern matching v:

match v with
| Nil -> false_elim()
| Cons hd tl ->

In case v is Nil, we use the library function Prims.false_elim : squash False -> a to express that this case is impossible. Intuitively, since the index i is a natural number strictly less than the length of the list, we should be able to convince F* that n <> 0.

The way this works is that F* typechecks the branch in a context that includes an equation, namely that the v : vec a n equals the pattern Nil : vec a 0. With the assumption that v == Nil in the context, F* tries to check that false_elim is well-typed, which in turn requires () : squash False. This produces an proof obligation sent to the SMT solver, which is able to prove False in this case, since from v = Nil we must have that n = 0 which contradicts i < n. Put another way, the branch where v = Nil is unreachable given the precondition i < n.

let rec get #a #n (i:nat{i < n}) (v:vec a n)
  : a
  = let Cons hd tl = v in
    if i = 0 then hd
    else get (i - 1) tl

Now, turning to the second case, we have a pattern like this:

match v with
| Cons hd tl ->

But, recall that Cons has an implicit first argument describing the length of tl. So, more explicitly, our pattern is of the form below, where tl : vec a m.

match v with
| Cons #m hd tl ->

F* typechecks the branch in a context that includes the equation that v == Cons #m hd tl, which lets the solve conclude that n == m + 1, from the type of Cons.

If i=0, we’ve found the element we want and return it.

Otherwise, we make a recursive call get (i - 1) tl and now F* has to:

• Instantiate the implicit argument of get to m, the length of tl. That is, in explicit form, this recursive call is really get #m (i - 1) tl. F* does this by relying on a unification algorithm implemented as part of its type inference procedure.

• Prove that (i - 1) < m, which follows from i < n and n == m + 1.

• Prove that the recursive call terminates, by proving that m << n, or, equivalently, since m and n are natural numbers, m < n. This is easy, since we have n == m + 1.

Let’s try a few exercises. The main work is to find a type for the functions in question. Once you do, the rest of the code will “write itself”.

Exercises

val append (#a:Type) (#n #m:nat) (v1:vec a n) (v2:vec a m)
  : vec a (n + m)

let rec append #a #n #m (v1:vec a n) (v2:vec a m)
  : vec a (n + m)
  = match v1 with
    | Nil -> v2
    | Cons hd tl -> Cons hd (append tl v2)

let rec split_at #a #n (i:nat{i <= n}) (v:vec a n)
  : vec a i & vec a (n - i)
  = if i = 0
    then Nil, v
    else let Cons hd tl = v in
         let l, r = split_at (i - 1) tl in
         Cons hd l, r

let rec reverse #a #n (v:vec a n)
  : vec a n
  = match v with
    | Nil -> Nil
    | Cons hd tl -> append (reverse tl) (Cons hd Nil)

let split_at_tail #a #n (i:nat{i <= n}) (v:vec a n)
  : vec a i & vec a (n - i)
  = let rec aux (j:nat{j <= i})
                (v:vec a (n - (i - j)))
                (out:vec a (i - j))
      : vec a i & vec a (n - i)
      = if j = 0
        then reverse out, v
        else let Cons hd tl = v in
             aux (j - 1) tl (Cons hd out)
    in
    aux i v Nil

Vectors: Probably not worth it

Many texts about dependent types showcase length-indexed vectors, much as we’ve done here. Although useful as a simple illustrative example, the vec type we’ve seen is probably not what you want to use in practice. Especially in F*, where regular lists can easily be used with refinement types, length-indexed vectors are redundant because we simply refine our types using a length function. The code below shows how:

module LList

let rec length #a (l:list a)
  : nat
  = match l with
    | [] -> 0
    | _::tl -> 1 + length tl

let rec get #a (i:nat) (v:list a { i < length v })
  = let hd :: tl = v in
    if i = 0 then hd
    else get (i - 1) tl

let rec split_at #a (i:nat) (v:list a { i <= length v })
  : r:(list a & list a){
        length (fst r) == i /\
        length (snd r) == (length v - i)
     }
  = if i = 0
    then [], v
    else let hd :: tl = v in
         let l, r = split_at (i - 1) tl in
         hd::l, r

let rec append #a (v1 v2:list a)
  : v:list a { length v == length v1 + length v2 }
  = match v1 with
    | [] -> v2
    | hd::tl -> hd :: append tl v2

In the next few sections, we’ll see more useful examples of indexed inductive types than just mere length-indexed vectors.