Chapter 3M: Gentle Type Theory Intro

Occasionally, we will have the chapters with M (for “Math”) attached. In them, we will be a bit more strict and try to give a bit more technical description of the concepts involved. You may skip or skim such chapters on the first reading, but they may prove useful for deeper understanding or as some basic reference material.

We will give some more strict Type Theory introduction in this chapter. We will not focus on proofs too much (or at all) but will be providing definitions and a hierarchy of concepts, which you can use as reference material as you delve deeper into the Haskell world. Strictly speaking, Haskell does not use the intuitionistic Type Theory per se but is rather based on so-called system-FC. However, we have found that having a more complete context of the type theory helps to reason about more advanced Haskell abstractions as well. Plus, in case you may want to venture to Idris, Coq, or invent your own language, the bigger picture will be even more helpful.

Also, one of the common misconceptions is that Haskell does not have dependent types. Strictly speaking and from the type-theoretical point of view, it does - for instance, typeclasses and type families are nothing less or more than a \(\sum\)-type. So, understanding some basic type theory will prove useful for any serious Haskell student.

Types and Functions

We have already defined a Type intuitively as “a bunch of stuff with similar characteristics thrown in a pot together”. In intuitionistic Type Theory types are usually referred to with capital letters - such as \(A\), \(B\), etc. In Haskell, concrete types (such as Int, Char, etc), as well as type functions (we will define them strictly below), that take a type and construct a different type out of it, such as Maybe a have to start from the capital letter as well.

In math, we construct all types from nothing, starting with Natural numbers \(\mathbb{N}\), which are usually called \(Nat\) in programming languages. The way to construct natural numbers is as follows:

We postulate the existence of zero as a value of type \(\mathbb{N}\) and define a function from \(\mathbb{N}\) to \(\mathbb{N}\). This way, we can say that \(1 \equiv succ \: 0\), \(2 \equiv succ \: 1\), etc. In a similar way, we can construct integers, reals, rings, fields, and basically all of math.

In Haskell (or any other real life language for that matter) we have a bunch of primitive types already provided to us as a basis from the Operating System or a specific compilation target, upon which we build our Type Universe using a subset of tools and rules detailed below.

Functions between types are written as \(f : A \rightarrow B\), a notation which denotes a function with domain equal to type \(A\) and codomain equal to type \(B\). In Haskell, the notation is very similar, with the only difference being that Haskell uses a double colon for the type signature. So, the function f above would be written as f :: A -> B, or recalling an example from the previous chapters, function whichNumberIsChar :: Char -> Int.

TK – picture of this function

This notation also means that if we have a value \(a\) of type \(A\), denoted as \(a:A\), we can apply a function \(f : A \rightarrow B\) to it, and will get a value \(f(a):B\) - f(a) of type B. As an example, having a value Z of type Char we can apply a function whichNumberIsChar to it and receive a number - a value of type Int. In both type theory and Haskell, function application does not require parenthesis and is written simply as f a.

Important to note that Functions are also first-class citizens of the type theory, which means we can pass them around as values, apply other functions to them, and classify them in types. So, \(A \rightarrow B\) is a type of all functions from A to B, just as \(Char \rightarrow Int\) is a type of all functions from Char to Int.

Types in type theory are also categorized in the hierarchy of Universes denoted with the letter \(U\). So, a type of a type is a universe - we can write \(A:U\) or \(Char:U\) to explicitly denote this fact. In math, universes are organized in an hierarchy \(U_0:U_1:...\), and we can build a similar hierarchy for Haskell. By definition all types that belong to a universe \(U_n\) also belong to a universe \(U_{n+1}\), so we will often write \(a:U\) without referencing number for the universe explicitly, when we want to talk about a type.

Maybe and Advanced Generalized Functions

So far, we have described concrete types where certain objects - values - live as well as functions between them - converting a Char to an Int, or an Int to an Int with something like f x = x * x etc. But what other “arrows” can we introduce in our universe?

One example that we have already seen is what we’ve called a “type function” - a function that takes a type and creates another type from it. We have defined two new types this way - String from Char and ListInt from Int. Since the type of any concrete type is a universe U, the type of all such “type functions” is U -> U. Haskell in fact uses asterisk * to denote something very close to U in type theory (even though there are some important differences, which we will discuss below), so this type in Haskell is written as * -> *, which simply means it’s a function that takes some concrete type and creates another concrete type out of it. Ubiqitous example is the two “type functions” we defined in the previous chapters - Maybe a and List a. Using GADT syntax, as it shows the relevant concepts better:

1 data Maybe a::* where
2         Just :: a -> Maybe a
3         Nothing :: Maybe a

In effect, Maybe : U -> U is a function that takes any concrete type a:U and creates a new concrete type Maybe a out of it. We can even write in Haskell type MaybeInt = Maybe Int where we give a new name - MaybeInt - to the type that we get by applying a type function Maybe to a concrete type Int. In practice, no-one really does it with Maybe, as it’s easier to just write Maybe Int, but you may want to introduce such named new types with more complicated type functions such as monad transformer stacks, which we will look at much later.

A very important question is what is Just and Nothing in our case? Let’s stare at the type signatures attentively. We can re-write Just as Just(x:a) : Maybe a, which means that Just takes a concrete value of type a and returns a concrete value of type Maybe a as a result. It is also called a constructor function. Same with Nothing - it takes no arguments and returns a value of type Maybe a, or we can even say that Nothing is a value of type Maybe a.

You have to internalize this distinction: Maybe is a “type function” - it takes a concrete type as an argument and returns a new concrete type as a result. Under the hood, it combines 2 data constructors - Just and Nothing, which can be treated as “normal” functions.

So what happens if we do write type MaybeInt = Maybe Int? You simply need to substitute type variable a for the concrete type Int in our Maybe a definition:

1 data Maybe Int where
2         Just :: Int -> Maybe Int
3         Nothing :: Maybe Int

So, our type function Maybe got a specific type (Int) and produced a new concrete type with 2 data constructors as a result. This is exactly what happens under the hood when you write something like x = Just 4 - Haskell deduces that 4 is of some concrete numeric type (can be Int, Short etc), creates a concrete type Maybe Int from Maybe a based on this information and then applies a data constructor Just :: Int -> Maybe Int to our 4:Int value.

Here we can also note an important difference between U in type theory and * in Haskell. The latter only means a concrete type, but cannot mean a type function such as Maybe itself or List - i.e., you cannot write Maybe List in Haskell, but you can - Maybe (List Int). In type theory however, both Maybe and List have a type U since they live in our universe of types. To be strict and respect this distinction, we can say that * is equal to U0 in type theory, and then we can say that all type functions with signature * -> * or, equivivalently, U0 -> U0 will live in the next level universe U1.

TK – picture illustrating this concept

How about functions of type U -> A, i.e. functions that take a concrete type as an argument and produce a value of a concrete type as a result? E.g., what if we want to have a function EN : U -> Nat that enumerates all the types that live in our universe and returns a specific type’s number? We could say that EN Char = 0, EN Int = 1 etc. This is a perfectly valid construct in Type Theory, but not in Haskell.

What if we go the other direction and want a function of type A -> U? This is what is normally called “dependent types” in CS, or type families in Type Theory, and is implemented in lanugages such as Idris, but not strictly speaking in Haskell, even though there is pretty active research in this direction. Everyone’s favorite example is the type of Vectors of a given length n. Ensuring safety of a bunch of operations that require vectors of the same size would work much better if we could do it at type level rather than by introducing runtime checks. This topic brings us to

Dependent Function Types (PI-types)

A dependent function type is a type of functions, whose codomain (type of their result) depends on the argument. It is written as

and means that a function of this type takes an argument x of type A and returns a result of type B(x) - so a type may vary depending on what x is. In case the type B(x) does not depend on x and is constant, it becomes our “regular” function type A -> B.

As an example, let’s say we have a type Vec n:Nat a:U of vectors of a given length n that store elements of type a. E.g., we can use Vec 3 Double to store coordinates of physical bodies. Then, we should be able to define a concatenation function that takes two vectors of type Vec n:Nat a:U and Vec m:Nat a:U and produce a vector of new type Vec (n+m):Nat a:U that depends on the exact type of its arguments. The full type signature of such a function would be written as:

This is a mouthful. In this specific case since the result type depends on type of the arguments, not on the arguments themselves, we can actually use our “regular” function signature type and write Vec n:Nat a:U -> Vec m:Nat a:U -> Vec (n+m):Nat a:U - which is in fact quite similar to how it is done in Idris.

UNFINISHED CHAPTER. TBD: Formal ADT, \(\sum\)-types, connection to haskell concepts (typeclasses, type and data families), better examples.