Types of Functional Languages: Coq and Haskell (Part 1/3)

As most computer programmers interested in Functional Programming (FP) know, it’s worth studying different languages to better understand the underlying mathematical concepts behind FP. In this article we look at Coq and Haskell. For the uninitiated, Coq and Haskell are two purely functional languages, among many. Impure counterparts might include the relatively more popular Agda and Clojure.

In part 1 of this series, we will look at and compare the two language types systems, from a high level. Examples will be light and brief. We will only be talking about Haskell sans language pragmas. As a note, it should be known that language extensions in Haskell are highly used in the community, e.g. overloaded strings and rank n types, so what you are about to read is not so much how people actually use the language in practice, but serves more as an initial reference to the basics of the language. Reader be aware. In part 2 we will investigate the underlying similarities and differences from a more conceptual point of view, point to more formal concepts as a refefference. In part 3 we will examine the feasibility and practicality of using language extensions in Haskell to more or less attempt to implement mathematical proofs.

This article is not rigorous. It is an informal discussion. There may be mistakes. Please let me know if you find any. An intermediate understanding of Coq and Haskell is recommended.

At a Glance

Coq’s is designed to be as restrictive and expressive as possible, whereas Haskell is designed with flexibility and practicality in mind. This namely has to do with the fact that Coq is after all a bit more than just a programming language: it’s also an interactive mathematical theorem prover. However, Coq is not Turing Complete and deals with general recursion in a specific way (avoiding the halting problem), while Haskell is turning complete, allowing it to tersely solve a broader range or programming challenges. But while Haskell, a burgeoning industry language, is not designed to be provably correct, it has many language extensions or pragmas which mostly allow practitioners to reap benefits similar to what they might get if they were using Coq.

The role of Haskell’s type inference is important in how it is designed. We can see this with the exclusion of multi-parameter type classes from the core language. Multi-parameter type classes, along with a few other language pragmas including functional dependencies, nullary type classes, and type families are what permits Haskell to truly shine as a more lofty tool for handling software correctness via dependent types, but at the same time reflects Haskell’s practicality and natural evolution over time. Because these pragmas sometimes convolute type meanings they make for more difficult development.

Inductive Type and Algebraic Data Types (ADTs)

Here we have two inductive Coq types, nat and bool. These types actually sit in a predefined standard module meaning we don’t need to define them, but for the sake of this exercise let us introduce them here. The go-to example for demonstrating inductive types is encoding natural numbers using Peano’s encoding.

Inductive nat : Type :=
  | Zero : nat
  | Succ : nat -> nat.

Check nat.
(* ===> nat : Set *)

Inductive bool : Type :=
  | true : bool
  | false : bool.

Check bool.
(* ===> bool : Set *)

This reads, “the inductive type nat has type Type and is enumerated as following, a Zero of type nat, and a Succ (successor) of type nat arrow nat. Period, end of inductive type. The inductive type for bool reads similarly.

Inductive types are a type theory discovery. They are a basic building block that allow us to create new types with constants and functions for terms of that type. Coq inductive types have primitive recursion, which in number theory supports addition and division, the factorial and exponential function. Primitive recursion is for natural numbers only, and means 0 is defined, as well as n + 1 in terms of its definition for n, or in this case Succ. The correctness of this can be proved, and serves as a mechanism for enumerating types. More or less, inductive types are like basic C data structures. It is also worth noting that this primitive recursion is essential for ensuring or Coq programs terminate. It would be incredibly easy to write unsound proofs for the user if this were not the case.

The Haskell version appears to be more concise.

data Bool = True | False

data Natural = Zero | Succ Natural

And here we see ADTs that support general and structural recursion. A better example showcasing Haskell’s recursion is as follows:

data Tree a = Nil
            | Node { left  :: Tree a
                   , value :: a
                   , right :: Tree a
                   }

Universes and Kinds

So what is the type of nat? We can check.

Check nat.
(* ===> nat : Set *)

It’s a Set. What about the type of Set?

Check Set.
(* ===> Set : Type *)

And Type?

Check Type.
(* ===> Type  : Type *)

Coq has, predictably, hierarchical types. To understand how this makes sense, you must know Coq types exist in a universe. A universe is a type containing elements of type type, the thinking of which comes from constructive type theory discovered by Per Martin-Löf. And Coq supports an infinite nesting of universes.

Set Printing Universes.

Check nat.
(* ===> nat : Set *)

Check Set.
(* ===> Set : Type@{Set+1} *)

Check Type.
(* ===> Type@{Top.8} : Type@{Top.8+1} *)
(* Top.8 |=  *)

The above code shows type hierarchy information, annotated with + meaning, e.g., Set is 1 up from the bottom range of types.

Haskell has the incredibly loose equivalent to universe: kinds. And I mean the only similarity is that both are a higher-order, or “one level up” from the corresponding inductive types and ADTs. The differences between universes and kinds is important. Kinds are in fact types as of Haskell 8. In type theory, a kind is the type of a type constructor. Specifically, the type of a higher-order type operator. Ordinary Haskell types have kind *. Type constructors have kind A -> Z, where A and Z are kinds. For instance:

Int :: *
Maybe :: * -> *
Maybe Bool :: *
a -> a :: *
[] :: * -> *
(->) :: * -> * -> *

The distinction between universes and kinds in Haskell arises from the reality that Coq has a common term language while Haskell has three: one for handling base terms or runtime values, one for handling type-level terms, e.g. types and type constructors; and, a language for handling kind-level terms.

Dependent and Non-Dependent Types (Π-Types)

While we can and will go much deeper into the differences between Coq and Haskell term languages, now is a good time to take take a break from kinds and universes and look and something else! has Π-types (Pi-types i.e. is dependently typed) while Haskell is non-dependently typed. Again - this is at least without using any Haskell language extensions. In so many words, dependently typed means that Coq functions can return different types as opposed to just one. It’s worth mentioning Coq only accepts terminating function definitions. Here’s an example of a Coq non-dependently typed lambda function:

Definition example (n : nat) (b : bool) :=
  if b then n else Succ (Succ (Succ Zero)).

Check example.
(* ===> example : nat -> bool -> nat *)

It takes a natural number and a boolean (x of type nat and y of type bool) and returns a nat. This is straight forward. Here’s an example of a Haskell non-dependently types function:

example :: Natural -> Bool -> Natural
example n b = if b then x else 100

-- λ > :t example
-- example :: Natural -> Bool -> Natural

Also obvious. An example of a dependently typed function can be seen in an identity function:

Definition id : forall (A : Type), A -> A := fun A => fun x => x.
Check id.
(* ===> id : forall A : Type, A -> A *)

Here, we see a Coq function definition stating that for all types A, A implies A which is equal to a lambda A implying another lambda function x which returns x.

Dependent types are based on Martin-Lof’s type theory, the benefits of which include logical propositions within data and function types and the ability to include proof terms within data and functions. This is great primer for understanding the basic differences between the two type systems.

Conclusion

We have barely even scratched the surface here. I’ve tried to be as accurate and concise as possible, so if you notice any mistakes please let me know.