Polymorphism

Previously, our sqrt n function was defined (more or less arbitrarily) to return 0 when n is not the square of any natural number. It's usually more desirable to have a distinct value to represent a "no result" outcome. We can easily define a new type for this purpose:

That is, a natoption is either SomeNat n where n is some number, or else it is NoNat.

However, this is such a useful construct that we will often want to use it with elements of other types in addition to nat. This is achieved by parameterizing the definition by the type of the "some" element.

This type is also known as option in ML, and Maybe in Haskell.

At this point it's instructive to look at the type of not only the constructors, but of option itself.

We see that option is actually a function, although it is a function between types: it takes a type A of elements as a parameter, and returns the type option A, whose values are of the form None A and Some A a, where a : A.

The types of Some and None are also interesting: they take a type A as their first argument, and the types of (the second argument and) the result depend on the particular choice of A, in the sense that A occurs in those types. The forall syntax is used to express a function type with this kind of a dependence. In fact, an ordinary function types written as A -> B is only syntactic sugar for forall _ : A, B.

Implicit arguments

Consider the term Some nat 42. The argument nat is needed in order to specify what the type of the second argument and the result should be. However, 42 by itself is already of type nat, so specifying the first argument is redundant. In fact, Coq can infer it:

In a term (and not a pattern), the underscore _ is a way of telling Coq: "infer this argument". However, when we want Coq to always infer an argument (and we often do), we can make it "implicit" as follows:

Now we can just elide the first argument completely and Coq will infer it. When we do need to give the first argument explicitly, we can do so by prepending the name of the function with @:

From the above discussion, it should be clear that types are not very much different from other kinds of terms in Coq. A function can take a type as a parameter, and a function can be applied to a type, and a type even has its own type, Type. Nearly everything that we can do with ordinary terms, we can also do with types, and this is part of what gives Coq its great expressive power.

Pairs

Continuing our quick survey on how common functional concepts are realized in Coq, we now turn to pairs. A pair of A and B is straightforward enough to define: the type has one constructor, and that takes two arguments, of types A and B, respectively.

An inductive type with a single constructor represents a kind of a record or structure: it doesn't encode any information about choices between alternatives, it is just a collection of elements. Coq provides a special syntax for defining inductive types like these:

The Structure syntax lets us name the single constructor, pair, and it also directly defines simple accessors to the fields of the structure. When we print out their definitions both with pretty-printing enabled and without it, we can see how a structure is just an inductive type. We also see the let-syntax that allows easier pattern matching on single-constructor types.

Again, we don't want to give the type arguments explicitly all the time since they can usually be inferred.

The type of pairs is often called a Cartesian product, hence the name prod. We provide a nice infix syntax for both the product type and the pairs themselves. Although the syntax A * B is already used for multiplication, there's no ambiguity, because this new A * B is only used with types.

Just for fun, here is a simple function that reverses the elements of a pair. It demonstrates the let-syntax, and one further language feature: the parameters in braces {A B} are immediately made implicit.

Let's try it out:

Sums

As a counterpart to the product types, there are sum types. An A + B is either an A or a B. In Haskell, the equivalent type is known as Either A B.