Inductive Datatypes I

To begin our discussion of immutable data and reasoning about data structures in our programs, we turn to that most ubiquitous of structures — the list — in its classical form — the linked list.

Example: linked lists

Remember from 6.101 the linked-list data structure, which was introduced something like this:

class LinkedList:
    def __init__(self, element, next_node):
        self.element = element
        self.next_node = next_node
    def __getitem__(self, index):
        if index == 0:
            return self.element
        if self.next_node is None:
            raise IndexError
        return self.next_node[index - 1]

a = LinkedList(8, LinkedList(16, None))
b = LinkedList(4, a)
b[1] # => 8

You implemented linked lists again in your Scheme interpreter, so that they worked something like this:

(begin
    (define a (cons 8 (cons 16 ())))
    (define b (cons 4 a))
    (list-ref b 1)) ; => 8

Every linked list in Scheme is either the empty list, represented by (), or a nonempty list represented as a “cons cell” that combines two pieces: the element at the front of the list and a linked list that contains the rest of the items.

In Dafny, we can define a linked-list data structure by explaining these two cases. Because the language demands that we be precise not only about the shape of the linked list but also about the types of elements inside it, we start with a linked list of natural numbers for now:

datatype NatList = NatNil | NatCons(head: nat, tail: NatList)

The datatype statement defines an inductive datatype by listing one or more constructors that can be used to create a value of the type:

• Each constructor can have parameters that specify the data stored by that variant of the type. In NatList, we have the two variants we expect: NatNil to represent the empty list of natural numbers, which has no data to store; and NatCons for nonempty lists of natural numbers.

• And because those parameters can recursively include instances of the type itself, we call these inductive types. In NatList, the NatCons constructor recursively requires a tail of type NatList. We can imagine enumerating the (infinite) collection of all possible NatList values by starting with NatNil and recursively applying NatCons with every natural number at every step.

To build the same example linked list as above:

var a := NatCons(8, NatCons(16, NatNil));
var b := NatCons(4, a);

Functions

Recursive functions are a natural fit for working with these recursive data structures.

We can build up a structure, such as the list of the first n counting numbers:

function FirstN(n: nat): NatList {
  if n == 0 then NatNil else NatCons(n, FirstN(n-1))
}

And break down a structure, for example to reduce a list of numbers to its sum:

function Sum(lst: NatList): nat {
  if lst.NatNil? then 0 else lst.head + Sum(lst.tail)
}

For each constructor Ctor in a datatype, Dafny defines a property Ctor? that lets us ask whether an instance of the type is that variant. And once we know the variant, we can access its associated data using the names from the datatype definition.

And how will we prove properties of these data structures and their functions? No surprises here — go ahead and complete the following proof, which Dafny would prove automatically if automatic induction were not disabled, so it only needs the smallest bit of help:

datatype NatList = NatNil | NatCons(head: nat, tail: NatList)

function FirstN(n: nat): NatList {
  if n == 0 then NatNil else NatCons(n, FirstN(n-1))
}

function Sum(lst: NatList): nat {
  if lst.NatNil? then 0 else lst.head + Sum(lst.tail)
}

lemma {:induction false} Sum_FirstN(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{
  
}

What are the details of this proof? Here is an expanded version:

lemma Sum_FirstN(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{
  if (n == 0) {
    calc {
      Sum(FirstN(n));
      == // definition of FirstN
      Sum(NatNil);
      == // definition of Sum
      0;
      == // algebra
      n * (n + 1) / 2;
    }
  } else {
    calc {
      Sum(FirstN(n));
      == // definition of FirstN
      Sum(NatCons(n, FirstN(n-1)));
      == // definition of Sum
      NatCons(n, FirstN(n-1)).head + Sum(NatCons(n, FirstN(n-1)).tail);
      == // definition of NatCons
      n + Sum(FirstN(n-1));
      == { Sum_FirstN(n-1); } // induction hypothesis
      n + (n - 1) * n / 2;
      == // algebra
      n * (n + 1) / 2;
    }
  }
}

On the n == 0 side, we see how Dafny has automatically reasoned about FirstN(0) and Sum(NatNil) to reach a successful conclusion.

And on the n != 0 side, it has expanded the non-0 case of FirstN and then the non-NatNil case of Sum and then used the definition of NatCons to simplify the resulting NatCons(n, FirstN(n-1)).head and .tail expressions. The result contains an expression whose value it already knows by induction! And algebraic rearrangement gets Dafny the rest of the way.

As you work on more proofs with inductive datatypes, you will find some situations where Dafny collapses the work just as effectively, but there will be other situations where you must explicate: a definition to expand, a rearrangement to apply, a particular instance of the induction hypothesis to invoke, etc.

Pattern matching

In FirstN and Sum above we have only two cases to consider in each function: the empty-list case and the nonempty case. Writing the body of the function as an if then else expression is a reasonable choice.

In general, our datatype may have any number of constructors, and our functions for building up and breaking down values may have any number of cases to consider. Many languages designed with these datatypes in mind, including Dafny, provide a pattern-matching syntax that serves double duty. Given a value to be matched:

• Each pattern is a predicate on the value, and the value of the entire pattern-matching expression is determined by the first pattern to match (the job of the if in our implementations above).

• Each pattern can bind variables to components of the matched value, and those variables can be used in the corresponding expression.

For example:

function Sum(lst: NatList): nat {
  match lst
  case NatNil => 0
  case NatCons(h, t) => h + Sum(t) // h := lst.head, t := lst.tail
}

Type parameters

Finally for this introductory reading, it feels quite unsatisfactory to imagine duplicating our linked-list definition for every possible type of elements:

datatype IntList = IntNil | IntCons(head: int, tail: IntList)
datatype BoolList = BoolNil | BoolCons(head: bool, tail: BoolList)
datatype StringList = StringNil | StringCons(head: string, tail: StringList)

And to imagine duplicating all the functions we write for manipulating these lists? And when a user of these lists defines a new datatype, they will need to duplicate the definition and all the functions again?

We can instead define a generic datatype whose definition makes use of type parameters that act as placeholders for a type to be chosen by the user of the data structure:

datatype List<ET> = Nil | Cons(head: ET, tail: List<ET>)

Read this definition as: “for any type ET*, a List of elements of type ET is either: the empty list (Nil) or the nonempty list (the Cons) of a value head of type ET and a value tail of type List-of-elements-of-type-ET.”

We can now use List<nat>, where type nat fills in the placeholder ET, for the type formerly known as NatList. As shown below, functions like FirstN (whose result is a List<nat>) and Sum (whose input elements must at least be values we can add, let’s just settle for natural numbers for now) continue to work as before.

But for the (many) functions on linked lists that don’t depend on the type of elements, we can write generic functions that operate on generic lists. Complete the implementation of Length:

datatype List<ET> = Nil | Cons(head: ET, tail: List<ET>)

function FirstN(n: nat): List<nat> {
  if n == 0 then Nil else Cons(n, FirstN(n-1))
}

function Sum(lst: List<nat>): nat {
  if lst.Nil? then 0 else lst.head + Sum(lst.tail)
}

function Length<ET>(lst: List<ET>): nat {
  match lst
  
  
}

lemma Sum_FirstN(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{}

lemma Length_FirstN(n: nat)
  ensures Length(FirstN(n)) == n
{}

Summary

In this reading we have developed a definition for immutable linked lists:

datatype List<ET> = Nil | Cons(head: ET, tail: List<ET>)

This datatype declaration defines an infinite family of types, where we fill in the generic type parameter with each possible type ET, but we can reason about all those instantiations of List uniformly, and we can define functions that work for any or all of them.

Because our datatype definitions can recursively include instances of the type they define, either directly or by recursion through another datatype, we call them inductive datatypes, and we will generally manipulate them and reason about them recursively.