Data Types

Data Types in ask

The things that ask programs compute and that ask proofs are about are data. Which data exist? Those whose existence we declare! We have inductive data types, introduced using a notation pinched from Haskell, and a little reminiscent of grammars. For example, we might invent the natural numbers by declaring

data Nat = Z | S Nat

or, if we feel lush with vertical space,

data Nat
  = Z
  | S Nat

Where grammars have productions, data types have constructors: Z and S are the constructors of Nat. Here, we are saying that Nat is a type of data, then after the = we say what type of data it is, by giving templates for the different ways you can make its values, separated by | which you can read as "or", even though it is just syntax here, not a logical connective. While grammar productions can freely mix terminal and nonterminal symbols, data types are more reassuringly predictable. Each template begins with a constructor, i.e. an identifier beginning with a capital letter, and is followed by zero or more placeholders for the payload data which that constructor brings. The simplest way to give such a placeholder is just to write the type of value expected in that place.

So what we are saying here is that Nat is a Type, and that every value in Nat is built in one of two ways. Either it is Z, or it is S n, where n is also a value in Nat. That is, natural numbers start from nothing and are made by counting. Indeed, we not merely permit but encourage you to name things in data declarations. You can and should write

data Nat
  = Z
  | S (n :: Nat)

where the :: means "has type".

Data Types with Parameters

There are some data type designs which are pleasingly reusable for different purposes, if only we can explain their adaptability. For example, it is not unusual to store data in binary trees. A binary tree is either a leaf or a node with some data between two subtrees. We do not need a new data type of binary trees for each type of data that we wish to store in the nodes. We can parametrize the notion of tree over the type of data stored in the nodes.

data Tree x
  = Leaf
  | Node (Tree x) x (Tree x)

Here, x stands for the type of data stored in the Nodes of the tree, and you can see that the Node constructor has three placeholders, for the left subtree, the value in x and the right subtree, respectively. We say that Tree is a type constructor and that Leaf and Node are value constructors. Their declaration styles differ in that we name the parameters of type constructors (and those names are in scope for the value constructor declarations) and we type the parameters of value constructors. So the x used as a type in the Node constructor template refers back to the x in Tree x. Indeed, that is how ask infers that x must be a Type. If in doubt, be fully explicit: in both sorts of declaration, it is encouraged to give both a name for the thing in a place and a type of the thing in the place.

data Tree (x :: Type)
  = Leaf
  | Node (tl :: Tree x) (k :: x) (tr :: Tree x)