Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data structure invariants. To find interesting uses of dependent data structures, however, we need not look to the favorite examples of data structures and algorithms textbooks. More basic examples like length-indexed and heterogeneous lists come up again and again as the building blocks of dependent programs. There is a surprisingly large design space for this class of data structure, and we will spend this chapter exploring it.

More Length-Indexed Lists

We begin with a deeper look at the length-indexed lists that began the last chapter.

We might like to have a certified function for selecting an element of an ilist by position. We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly. It is helpful to define a type family fin, where fin n is isomorphic to {m : nat | m < n}. The type family name stands for "finite."

An instance of fin is essentially a more richly typed copy of a prefix of the natural numbers. Every element is a First iterated through applying Next a number of times that indicates which number is being selected. For instance, the three values of type fin 3 are First 2, Next (First 1), and Next (Next (First 0)). Now it is easy to pick a Prop-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
      | Nil => fun idx => ?
      | Cons _ x ls' => fun idx =>
        match idx with
          | First _ => x
          | Next _ idx' => get ls' idx'
        end
    end.
    

We apply the usual wisdom of delaying arguments in Fixpoints so that they may be included in return clauses. This still leaves us with a quandary in each of the match cases. First, we need to figure out how to take advantage of the contradiction in the Nil case. Every fin has a type of the form S n, which cannot unify with the O value that we learn for n in the Nil case. The solution we adopt is another case of match-within-return, with the return clause chosen carefully so that it returns the proper type A in case the fin index is O, which we know is true here; and so that it returns an easy-to-inhabit type unit in the remaining, impossible cases, which nonetheless appear explicitly in the body of the match.
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
      | Nil => fun idx =>
        match idx in fin n' return (match n' with
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
        match idx with
          | First _ => x
          | Next _ idx' => get ls' idx'
        end
    end.
    

Now the first match case type-checks, and we see that the problem with the Cons case is that the pattern-bound variable idx' does not have an apparent type compatible with ls'. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the Nil case body has type match X with | O => A | S _ => unit end for a unification variable X, while it is expected to have type A. We can see that setting X to O resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a return annotation, used with an in annotation, leads us to a more informative error message, saying that idx' has type fin n1 while it is expected to have type fin n0, where n0 is bound by the Cons pattern and n1 by the Next pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be. We need to use match annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both ls and idx; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function pred to express the relationship between the types of these variables.
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
      | Nil => fun idx =>
        match idx in fin n' return (match n' with
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
        match idx in fin n' return ilist (pred n') -> A with
          | First _ => fun _ => x
          | Next _ idx' => fun ls' => get ls' idx'
        end ls'
    end.
    

There is just one problem left with this implementation. Though we know that the local ls' in the Next case is equal to the original ls', the type-checker is not satisfied that the recursive call to get does not introduce non-termination. We solve the problem by convoy-binding the partial application of get to ls', rather than ls' by itself.

A few examples show how to make use of these definitions.

  Cons 0 (Cons 1 (Cons 2 Nil))
     : ilist nat 3

     = 0
     : nat

     = 1
     : nat

     = 2
     : nat

Our get function is also quite easy to reason about. We show how with a short example about an analogue to the list map function.

It is easy to prove that get "distributes over" imap calls.

The only tricky bit is remembering to use our dep_destruct tactic in place of plain destruct when faced with a baffling tactic error message.

Heterogeneous Lists

Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a "type-level" list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq.

We parameterize our heterogeneous lists by a type A and an A-indexed type B.

We can implement a variant of the last section's get function for hlists. To get the dependent typing to work out, we will need to index our element selectors (in type family member) by the types of data that they point to.

Because the element elm that we are "searching for" in a list does not change across the constructors of member, we simplify our definitions by making elm a local variable. In the definition of member, we say that elm is found in any list that begins with elm, and, if removing the first element of a list leaves elm present, then elm is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define member in Type so that we may decompose its values to guide computations. We can use member to adapt our definition of get to hlists. The same basic match tricks apply. In the HCons case, we form a two-element convoy, passing both the data element x and the recursor for the sublist mls' to the result of the inner match. We did not need to do that in get's definition because the types of list elements were not dependent there.

By putting the parameters A and B in Type, we enable fancier kinds of polymorphism than in mainstream functional languages. For instance, one use of hlist is for the simple heterogeneous lists that we referred to earlier.

     = 5
     : (fun T : Set => T) nat

     = true
     : (fun T : Set => T) bool

We can also build indexed lists of pairs in this way.

There are many other useful applications of heterogeneous lists, based on different choices of the first argument to hlist.

A Lambda Calculus Interpreter

Heterogeneous lists are very useful in implementing interpreters for functional programming languages. Using the types and operations we have already defined, it is trivial to write an interpreter for simply typed lambda calculus. Our interpreter can alternatively be thought of as a denotational semantics (but worry not if you are not familiar with such terminology from semantics). We start with an algebraic datatype for types.

Now we can define a type family for expressions. An exp ts t will stand for an expression that has type t and whose free variables have types in the list ts. We effectively use the de Bruijn index variable representation. Variables are represented as member values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment.

We write a simple recursive function to translate types into Sets.

Now it is straightforward to write an expression interpreter. The type of the function, expDenote, tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list ts is simply an hlist typeDenote ts. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use hget to implement the Var case, and we use HCons to extend the environment in the Abs case.

Like for previous examples, our interpreter is easy to run with simpl.

    = tt
     : typeDenote Unit

     = fun x : unit => x
     : typeDenote (Arrow Unit Unit)

     = fun x _ : unit => x
     : typeDenote (Arrow Unit (Arrow Unit Unit))

     = fun _ x0 : unit => x0
     : typeDenote (Arrow Unit (Arrow Unit Unit))

     = tt
     : typeDenote Unit

We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. Other, more common approaches to language formalization often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties.

Recursive Type Definitions

There is another style of datatype definition that leads to much simpler definitions of the get and hget definitions above. Because Coq supports "type-level computation," we can redo our inductive definitions as recursive definitions. Here we will preface type names with the letter f to indicate that they are based on explicit recursive function definitions.

We say that a list of length 0 has no contents, and a list of length S n' is a pair of a data value and a list of length n'.

We express that there are no index values when n = O, by defining such indices as type Empty_set; and we express that, at n = S n', there is a choice between picking the first element of the list (represented as None) or choosing a later element (represented by Some idx, where idx is an index into the list tail). For instance, the three values of type ffin 3 are None, Some None, and Some (Some None).

Our new get implementation needs only one dependent match, and its annotation is inferred for us. Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out.

Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use.

The definition of fhlist follows the definition of filist, with the added wrinkle of dependently typed data elements.

The definition of fmember follows the definition of ffin. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for ffin we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that idea with a sum type whose left branch is the appropriate equality proposition. Since we define fmember to live in Type, we can insert Prop types as needed, because Prop is a subtype of Type. We know all of the tricks needed to write a first attempt at a get function for fhlists.
  Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
    match ls with
      | nil => fun _ idx => match idx with end
      | _ :: ls' => fun mls idx =>
        match idx with
          | inl _ => fst mls
          | inr idx' => fhget ls' (snd mls) idx'
        end
    end.
    

Only one problem remains. The expression fst mls is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the inl case of the inner match.

By pattern-matching on the equality proof pf, we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality.

Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x

In a proposition x = y, we see that x is a parameter and y is a regular argument. The type of the constructor eq_refl shows that y can only ever be instantiated to x. Thus, within a pattern-match with eq_refl, occurrences of y can be replaced with occurrences of x for typing purposes.

How does one choose between the two data structure encoding strategies we have presented so far? Before answering that question in this chapter's final section, we introduce one further approach.

Data Structures as Index Functions

Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor.

Every Node of a tree has a natural number argument, which gives the number of child trees in the second argument, typed with ilist. We can define two operations on trees of naturals: summing their elements and incrementing their elements. It is useful to define a generic fold function on ilists first.

Now we might like to prove that inc does not decrease a tree's sum.

  n : nat
  i : ilist (tree nat) n
  ============================
   ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
   ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
 

We are left with a single subgoal which does not seem provable directly. This is the same problem that we met in Chapter 3 with other nested inductive types.

  tree_ind
     : forall (A : Set) (P : tree A -> Prop),
       (forall a : A, P (Leaf a)) ->
       (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
       forall t : tree A, P t

The automatically generated induction principle is too weak. For the Node case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of tree.

First, let us try using our recursive definition of ilists instead of the inductive version.

  Inductive tree : Set :=
  | Leaf : A -> tree
  | Node : forall n, filist tree n -> tree.

Error: Non strictly positive occurrence of "tree" in
 "forall n : nat, filist tree n -> tree"

The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types. We defined filist recursively, so it may not be used in nested inductive definitions. Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, reflexive types. Instead of merely using fin to get elements out of ilist, we can define ilist in terms of fin. For the reasons outlined above, it turns out to be easier to work with ffin in place of fin.

A Node is indexed by a natural number n, and the node's n children are represented as a function from ffin n to trees, which is isomorphic to the ilist-based representation that we used above.

We can redefine sum and inc for our new tree type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose domain is some ffin type, and it folds another function over the results of calling the first function at every possible ffin value.

Now we are ready to prove the theorem where we got stuck before. We will not need to define any new induction principle, but it will be helpful to prove some lemmas.

Even if Coq would generate complete induction principles automatically for nested inductive definitions like the one we started with, there would still be advantages to using this style of reflexive encoding. We see one of those advantages in the definition of inc, where we did not need to use any kind of auxiliary function. In general, reflexive encodings often admit direct implementations of operations that would require recursion if performed with more traditional inductive data structures.

Another Interpreter Example

We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's cond. Each of our conditional expressions takes a list of pairs of boolean tests and bodies. The value of the conditional comes from the body of the first test in the list to evaluate to true. To simplify the interpreter we will write, we force each conditional to include a final, default case.

A Cond is parameterized by a natural n, which tells us how many cases this conditional has. The test expressions are represented with a function of type ffin n -> exp' Bool, and the bodies are represented with a function of type ffin n -> exp' t, where t is the overall type. The final exp' t argument is the default case. For example, here is an expression that successively checks whether 2 + 2 = 5 (returning 0 if so) or if 1 + 1 = 2 (returning 1 if so), returning 2 otherwise.

We start implementing our interpreter with a standard type denotation function.

To implement the expression interpreter, it is useful to have the following function that implements the functionality of Cond without involving any syntax.

Now the expression interpreter is straightforward to write.

We will implement a constant-folding function that optimizes conditionals, removing cases with known-false tests and cases that come after known-true tests. A function cfoldCond implements the heart of this logic. The convoy pattern is used again near the end of the implementation.

Like for the interpreters, most of the action was in this helper function, and cfold itself is easy to write.

To prove our final correctness theorem, it is useful to know that cfoldCond preserves expression meanings. The following lemma formalizes that property. The proof is a standard mostly automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis.

It is also useful to know that the result of a call to cond is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function cond is extensional; that is, it is unaffected by substitution of functions with input-output equivalents.

Now the final theorem is easy to prove.

We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct.

Choosing Between Representations

It is not always clear which of these representation techniques to apply in a particular situation, but I will try to summarize the pros and cons of each. Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy match annotations. Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings. Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the simpl tactic (which is among the ingredients in crush) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call get l f, where variable l has type filist A (S n). The type of l would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where filist is expected but a pair type is found in the "simplified" version. The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may "simplify" when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value. Another disadvantage of recursive types is that they only apply to type families whose indices determine their "skeletons." This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far. The fact that a piece of syntax has type Nat tells us nothing about the tree structure of that syntax. Finally, Coq type inference can be more helpful in constructing values in inductive types. Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type. This downside can be mitigated to an extent by writing "constructor" functions for a recursive type, mirroring the definition of the corresponding inductive type. Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures.