Understanding Haskell's type system

February 19, 2024

What precisely is the type of 1 in Haskell?

ghci> :t 1
1 :: Num a => a

Why do I ask?

I'm currently teaching a second year university course on functional programming in Haskell. This will be my second time through. I inherited the slides from a colleague who created the course and taught it once. This time I'm busily converting the slides into Beamer format and taking the opportunity to improve them.

Inevitably, while improving things, I realise I understand some parts, but not others. This struck me particularly when working on the second lecture on Haskell's type system.

The basics

The first mention of type checking in the second lecture uses this example:

ghci> :t 3+4
3+4 :: Num a => a

I explain this as follows:

Num a => a is the type signature of the expression 3+4
Types starting with a lowercase letter, such as a, are type variables
The constraint operator => constrains types in the type signature
So the second line says that the type of 3+4 is any type that implements the Num type class
Haskell doesn't assign a concrete type to 3+4. It can be used as an Int, a Float, etc.

Types vs type signatures

According to Haskell 2010, a type signature has the form:

v₁, ..., vₙ :: cx => t

This declares that the variables v₁, ..., vₙ are of type t with respect to the context cx.

So in my example above, 3+4 :: Num a => a is actually a type signature and specifies that the type of 3+4 is a, for any type a that implements Num. That's also the type of 1, to answer my opening question.

Let's take a short detour to discuss the fact that a constant expression can have more than one type.

Parametric polymorphism and constant expressions

Parametric polymorphism is often understood to apply to functions. For example, the function head that returns the first element of a non-empty list has this type signature¹:

head :: [a] -> a

The function is polymorphic: it can be applied to any list, regardless of the type of the list elements.

But parametric polymorphism covers constants too. According to [1]:

Polymorphism means that one and the same expression can have (perhaps infinitely) many types.

Type inference

The type Num a => a above is inferred by the compiler. The Haskell wiki talks about the compiler inferring concrete types whenever possible, but type inference isn't all about concrete types as our example shows.

Take a slightly more complicated example map incr where:

incr x = x + 1

The compiler infers the type of incr to be Num a => a -> a and the type of map incr to be Num a => [a] -> [a]. What's going on here?

Principal types

Any expression in a valid Haskell 2010 program has a most general type, known as the principal type, that can be assigned to it. Another way of stating this is that Haskell 2010 has the principal type property. In most cases the compiler can infer the principal type of an expression.

Unfortunately, certain GHC extensions, notably Generalised Algebraic Data Types (GADTs) and rank-n types, destroy the principal type property. With such extensions, some expressions do not have a principal type since they would be satisfied by more than one incomparable type. They either require the compiler to choose one of the possible types and/or the programmer to narrow down the choice using type signatures.

Even Haskell 2010 requires type annotations in some cases (most notably for code with otherwise ambiguous types, and for code using polymorphic recursion). Each expression in Haskell 2010 has a principal type, but the compiler cannot discover it in these cases.

Going deeper

The following resources are long and deep.

[1] I started to read up on Haskell's type system and was soon exposed to the Hindley–Milner type system, which also underpins Standard ML.

[2] Typing Haskell in Haskell by Mark P Jones is a formal, in-depth account of building a Haskell type checker in Haskell.

[3] Type inference for Haskell is a 23-part series of articles by Jeremy Mikkola, which he wrote as a beginner-friendly companion to Jones's paper.

I think there's a gap in market for a description of type inference in Haskell between the level of this post and Mikkola's series, suitable for newcomers to Haskell (like my students). If anyone knows of such a description, I'd be grateful if they would email me via the “contact” link below.

#Haskell #FunctionalProgramming

Footnote:

This ignores the GHC-specific constraint GHC.Stack.Types.HasCallStack =>.

Thanks:

I revised the initial article based on feedback from Andres Löh.