Structures

In this chapter we continue our development of basic concepts of functional programming. The critical new ideas are polymorphism (abstracting functions over the types of the data they manipulate) and higher-order functions (treating functions as data). We begin with polymorphism. Along the way, we'll talk about sets, an absolutely fundamental notion in mathematics (discrete and otherwise). We'll also introduce what will be a long running case study in the course: bioinformatics and computationally manipulating DNA.

Lists

Interesting programs need to be able to manipulate data structures. Let's start with lists. We'll need to work with lists with elements from a variety of types -- lists of nats, lists of booleans, lists of lists, etc. We could just define a new inductive datatype for each of these, for example...

... but this would quickly become tedious, partly because we have to make up different constructor names for each datatype, but mostly because we wouldn't get any reuse: if you're computing the length of a list, it doesn't matter what type the list holds... so why write the function more than once? To avoid all this repetition, Coq supports polymorphic (Greek: "poly-" many, "morphos" form, shape) inductive type definitions. For example, here is a polymorphic list datatype.

This is exactly like the definition of natlist above, except that the nat argument to the cons constructor has been replaced by an arbitrary type X, a binding for X has been added to the function header on the first line, and the occurrences of natlist in the types of the constructors have been replaced by list X. What sort of thing is list itself? A good way to think about it is that the definition of list is a function from Types to Inductive definitions; or, to put it more concisely, list is a function from Types to Types. For any particular type X, the type list X is the Inductively defined set of lists whose elements are of type X. Another name for a function that produces Types is "type constructor": list is a type constructor; if you give it a type X, then list X will "construct" the type of lists holding Xs.

The parameter X in the definition of list automatically becomes a parameter to the constructors nil and cons -- that is, nil and cons are now polymorphic constructors; when we use them, we must now provide a first argument that is the type of the list they are building. For example, nil nat constructs the empty list of type nat.

Similarly, cons nat adds an element of type nat to a list of type list nat. Here is an example of forming a list containing just the natural number 3.

What might the type of nil itself be? We can tell from Check (nil nat) above that nil takes a Type as input and produces a list as input. So you might say that nil : Type → list _. But what's _? Well, it's whatever Type was provided as nil's first argument! For nil to refer back to its type argument, we need a new feature: ∀ types. If e : ∀ (X:T₁), T₂, then e takes an X of type T₁ and produces a value of type T₂.

That is, nil takes a Type -- call it X -- and produces a value of type list X. The type of the return value depends on the type given as input. Similarly, the type of cons from the definition looks like X → list X → list X, but using this convention to explain the meaning of X results in the type ∀ X, X → list X → list X.

(Side note on notation: In .v files, the "forall" quantifier is spelled out in letters. In the generated HTML files and in the way various IDEs show .v files, depending on the settings of their display controls, ∀ is usually typeset as the usual mathematical "upside down A," though you'll still see the spelled-out "forall" in a few places. This is just a quirk of typesetting: there is no difference in meaning.) Having to supply a type argument for every single use of a list constructor would be rather burdensome; we will soon see ways of reducing this annotation burden.

We can now go back and make polymorphic versions of all the list-processing functions that we wrote before. Here is repeat, for example:

Type Annotation Inference

Let's write the definition of repeat again, but this time we won't specify the types of any of the arguments. Will Coq still accept it?

Indeed it will. Let's see what type Coq has assigned to repeat':

It has exactly the same type as repeat. Coq was able to use type inference to deduce what the types of X, x, and count must be, based on how they are used. For example, since X is used as an argument to cons, it must be a Type, since cons expects a Type as its first argument; matching count with 0 and S means it must be a nat; and so on. This powerful facility means we don't always have to write explicit type annotations everywhere, although explicit type annotations can still be quite useful as documentation and sanity checks, so we will continue to use them much of the time.

Type Argument Synthesis

To use a polymorphic function, we need to pass it one or more types in addition to its other arguments. For example, the recursive call in the body of the repeat function above must pass along the type X. But since the second argument to repeat is an element of X, it seems entirely obvious that the first argument can only be X -- why should we have to write it explicitly? Fortunately, Coq permits us to avoid this kind of redundancy. In place of any type argument we can write a "hole" _, which can be read as "Please try to figure out for yourself what belongs here." More precisely, when Coq encounters a _, it will attempt to unify all locally available information -- the type of the function being applied, the types of the other arguments, and the type expected by the context in which the application appears -- to determine what concrete type should replace the _. This may sound similar to type annotation inference -- and, indeed, the two procedures rely on the same underlying mechanisms. Instead of simply omitting the types of some arguments to a function, like
      repeat' X x count : list X := we can also replace the types with holes
      repeat' (X : _) (x : _) (count : _) : list X := to tell Coq to attempt to infer the missing information. Using holes, the repeat function can be written like this:

In this instance, we don't save much by writing _ instead of X. But in many cases the difference in both keystrokes and readability is nontrivial. For example, suppose we want to write down a list containing the numbers 1, 2, and 3. Instead of this...

...we can use holes to write this:

Implicit Arguments

In fact, we can go further and even avoid writing _'s in most cases by telling Coq always to infer the type argument(s) of a given function. The Arguments directive specifies the name of the function (or constructor) and then lists its argument names, with curly braces around any arguments to be treated as implicit.

Now, we don't have to supply type arguments at all:

Alternatively, we can declare an argument to be implicit when defining the function itself, by surrounding it in curly braces instead of parens. For example:

Let's finish by implementing a few other standard list functions on our new polymorphic lists.

Exercise: 2 stars, standard (allb)

Complete the definition of allb : list bool → bool. It should return true if every bool in the list is true. What should you return if the list is empty? It's a question of convention, but here's a hint: your match shouldn't do anything special for single-element lists.

Exercise: 2 stars, standard (sum)

Complete the definition of sum : list nat → nat. It should sum up a list. What should you return if the list is empty? It's a question of convention, but the same hint applies: your match should only have two cases.

Exercise: 3 stars, standard (zero_to_n)

Write a function zero_to_n that builds a list from 0 to n, inclusive. Coq's termination requirements will get in your way here. There are two approaches: either write a helper function or post-process the list. Why not use app? Well, appending each element to the end as a new list means you need to visit the whole list n times (why?), whereas you can make this function work in just one trip through the list (or zero)! Coq tip: you can define helper functions externally using Fixpoint or Definition, but you can also define them inline using let. You can write: [ let fix foo (m : TYPE) := ... in ... ] to mean: [ let foo = fix foo (m : TYPE) := ... in ... ] but NB that you can't write the return type.

Supplying Type Arguments Explicitly

One small problem with declaring arguments Implicit is that, once in a while, Coq does not have enough local information to determine a type argument; in such cases, we need to tell Coq that we want to give the argument explicitly just this time. For example, suppose we write this:

(The Fail qualifier that appears before Definition can be used with any command, and is used to ensure that that command indeed fails when executed. If the command does fail, Coq prints the corresponding error message, but continues processing the rest of the file.) Here, Coq gives us an error because it doesn't know what type argument to supply to nil. We can help it by providing an explicit type declaration (so that Coq has more information available when it gets to the "application" of nil):

Alternatively, we can force the implicit arguments to be explicit by prefixing the function name with @.

Polymorphic Pairs

Lists are a very common data structure---whole programming languages use them as their only data structures (the "Lisp" family comes from "LISt Programming"). But a programmer needs plenty of data structures in their toolbelt, some more complex, some less. It's often useful to have a fixed, finite number of things. can be generalized to polymorphic pairs, often called products or tuples by mathy folks:

As with lists, we make the type arguments implicit and define the a nice concrete notation.

We can also use the Notation mechanism to define the standard notation for product types:

(The annotation : type_scope tells Coq that this abbreviation should only be used when parsing types, not when parsing expressions. This avoids a clash with the multiplication symbol.) It is easy at first to get (x,y) and X×Y confused. Remember that (x,y) is a value built from two other values, while X×Y is a type built from two other types. If x has type X and y has type Y, then (x,y) has type X×Y. Why does one match pattern suffice? Well, prod has only one constructor! We could just as well say:
   let (x, y) := p in x + y Which is a bit nicer. If we care about what's inside the pair we may want more arms after all:
   match p with
   | (0, y) ⇒ y
   | (x, 0) ⇒ x
   | (x, y) ⇒ x × y
   end The first and second projection functions extract the parts of pairs. We've put them in a module because you should avoid them where possible, usually matching on the pair is much better.

Exercise: 2 stars, standard (pair_exercises)

Let's get some practice with pairs. First, write a function to swap the two elements of a pair:

Next, let's write a quirky little version of andb. Note that this is not a polymorphic function!

Finally, let's write a silly function that builds a pair of alternatives from two numbers. The first will be the product of the numbers, and the second will be their sum.

Exercise: 2 stars, standard, optional (currying)

In Coq, a function f : A → B → C really has the type A → (B → C). That is, if you give f a value of type A, it will give you function f' : B → C. If you then give f' a value of type B, it will return a value of type C. This allows for partial application, as in plus3. Processing a list of arguments with functions that return functions is called currying, in honor of the logician Haskell Curry. Conversely, we can reinterpret the type A → B → C as (A × B) → C. This is called uncurrying. With an uncurried binary function, both arguments must be given at once as a pair; there is no partial application. Concretely, currying says that it doesn't matter if you take your arguments all at once---like a math function---or if you do it one at a time. Suppose we have the math-y function, f : nat × nat → nat where f(x,y) = 2*x+y. Notice how the math notation has you take both x and y at once. You could write it differently, though mathematicians may squint at you:
f' : nat → (nat → nat)
f'(x) = g_x(y)

g_x : nat → nat
g_x(y) = 2*x + y The subscript on g, written here as g_x, conveys the idea that g is "closed over" x. Here's an example:
   f(20, 7) = 2*20 + 7 = 40 + 7 = 47

   f'(20) = g_20

   g_20(7) = 2*20 + 7 = 40 + 7 = 47 Functional programming languages like Gallina typically use curried functions; most other languages use uncurried functions. We can define currying as follows:

As an exercise, define its inverse, prod_uncurry.

Polymorphic Options

Our next polymorphic type is polymorphic options. You might think of an option as a list with exactly zero or exactly one element. Maybe you've programmed in languages that have a 'null' or 'None' value. Gallina has no notion of 'null', but options let us express the idea that a value is "nullable" or "optional". This bears repeating: Coq has no notion of null or None. If you have a variable of type nat or list bool or whatever, you are guaranteed that there is actually a natural number or a list there and not a sneaky missing-value value. But then, how do we specify and implement functions that might fail to return a value, or functions that take optional arguments? Languages like Coq, Haskell, Rust, and others replace a special null value (which is a member of every type) with a new type, often called option, with two constructors: None, which is an option containing no value (analogous to null); and Some v, which is an option containing a value. option X is a different type from X, so we can't do the things we might want to do with an X without first checking that the option is indeed Some. These will both give type errors:
Compute (Some 4) + 5.
Compute app (cons 3 (cons 2 nil)) (cons 1 nil). If you want to actually use a value inside of an option X, you need to get the X (if any) out of the option. In other words, you're forced to double check that the option isn't, in fact, None. The equivalent in Python would be to surround every do_stuff(thing) with if thing is not None: do_stuff(thing), which would be tedious and inefficient.
Definition opt_example (num_opt : option nat) : nat :=
  match num_opt with
  | None ⇒ 5
  | Some n ⇒ n + 5
  end.

Definition list_opt_example (list_opt : option (list nat)) : list nat :=
  match list_opt with
  | None ⇒ (cons 1 nil)
  | Some lst ⇒ app lst (cons 1 nil)
  end. If Coq didn't give it to us already, option would be defined something like this:

We can now write the nth_error function, which tries to get the nth element of a list. What should it return if there aren't enough elements in the list? We have no way of creating a "default" X, so we actually can't define this polymorphic function without option X. If you don't believe me, just try!

Exercise: 1 star, standard (hd_error)

Complete the definition of a polymorphic version of the hd_error function. It should return the first element of the list, if possible. Don't just call nth_error!

Once again, to force the implicit arguments to be explicit, we can use @ before the name of the function.

Exercise: 1 star, standard (list_min)

We defined min and min3 earlier, but we would never want to define min4, min5, etc. Instead, let's define a function list_min that takes a list of natural numbers and returns the least element of the list. What should you do if the list is empty?

In the Rust standard library (as an example), Option defines a variety of useful functions for processing optional values without throwing matches everywhere. The simplest may be unwrap_or, which lets us provide a default value in case the option is None, otherwise it uses what's inside the option.

Exercise: 1 star, standard (unwrap_or)

Often we want to process a possibly-missing value, preserving the missing status if the value is a None. option_map takes us from an option X to an option Y if we have a function f from X → Y, calling f with the X if present to produce the Y. For this one, think about the types you have and the types you want, and how f gives you a way to make a Y from an X.

Exercise: 1 star, standard (option_map)

Sometimes we don't have a guaranteed way to produce a Y from an X---in other words if the conversion from X to Y may fail (or, if they are the same, the processing of X into a different X may fail). In such cases we have and_then, which is like option_map but takes an f : X → option Y. Again, think of the types as a plumbing problem! You have to get the types to fit together properly, and that will basically give you the solution.

Exercise: 1 star, standard (and_then)

For practice, let's implement option_map using and_then. No matches allowed! Note how and_then and option_map only differ in one place, and that's the place that and_then allows for abstracting over!

Exercise: 1 star, standard (option_map')

We can even come up with option versions of boolean operators. First, consider xor_option, which returns None if either zero or both of the input option values are Some x, otherwise returns the value of whichever was not None:

Exercise: 1 star, standard (xor_option)

Next, let's take a look at and_option, which takes an option X and an option Y and produces an option (X × Y) if they are both Some. You can do this in just four lines of code, not including the type declaration!

Exercise: 1 star, standard (and_option)

More Polymorphic Functions

Now that we have polymorphic functions, we can make a much more general and interesting version of argmin and argmin3 from day 2. Notice that except for the type signature, the code is exactly the same!

Here's another (somewhat contrived) example:

Remember our favorite_day example from Day 2? Well, we could have implemented it using select, although it's arguable whether this is any improvement. Note that types X and Y here are both day!

Finally, let's look at one more polymorphic type: result.

Let's imagine we're reading in data from files. This can go wrong in a variety of ways. In reality there are hundreds of errors we might see!

FileError_FirstTry has that unpleasant ok value. We'd prefer not to have to always check if a given "error" is actually ok or not. Even worse---let's say our read_file function returns a string × FileError_FirstTry pair: the file contents (if any, or else the empty string) and the error (if any, or else ok). This is essentially the choice that the go programming language makes in its standard library. But this is gnarly! You have to remember to check for ok all the time, sometimes the string you get back has a meaning and sometimes it doesn't---it's just a recipe for disaster. We can use a better pair of types to help us out of this mess:

Now result can either be a success value or a failure value, and we parameterize it both on the type of success value and the type of error:

In real life we'd read the file in from path, checking for errors, and return something appropriate. Here we'll just return an error:

This result type indicates not only success or failure (like an option), but also a reason for the failure. It can be useful in all kinds of places: Parsing strings into numbers, compiling programs, acting on user input, and more. If we don't mind losing the reason for the failure, we can convert a result to an option:

Remember our option combinators like option_map? We can do the same kinds of things with result. result_map is like option_map in that it passes along a failure unchanged, but a success gets transformed by the given function.

Exercise: 1 star, standard (result_map)

Next, let's mess around with nested results and options. result_transpose goes from a result (option X) Err to an option (result X Err). Ok None should map to just None. This kind of type plumbing can be useful for long chains of combinators!

Exercise: 1 star, standard (result_transpose)

We could define result_and_then, but instead let's try result_or_else, which calls the given operation if the result is Error but passes the Ok x through unchanged if the original result was a success.

Exercise: 1 star, standard, optional (result_or_else)