Haskell’s Type System Standing Alone

When you treat it as its own separate programming language, Haskell’s type system has some strange syntax, weird fundamental choices, and occasionally bad ergonomics. In other words, it’s like any other programming language.

What if we examined (a subset of¹) it like we might with any other programming language? We could go over the kinds of things that are possible in the language, without explaining why they are that way or how they get implemented under the hood. That’s what I’ll attempt to do here.

Language Basics

Like Java’s public static void main(String[] args), Haskell’s type system (HTS for short) has a fairly large preamble at the beginning of a program. At least the way I write it. It’s not all necessary for every HTS program, but understanding this preamble takes a bit more depth of knowledge than I can go into here. So, just like I would when teaching someone Java’s “Hello World”, I’ll just say “let’s deal with it another time”.

{-# LANGUAGE
    TypeFamilies
  , TypeOperators
  , DataKinds
  , UndecidableInstances
  , NoStarIsType
  , PolyKinds
#-}

import Data.Kind
import Data.Symbol.Ascii
import GHC.TypeLits

In HTS, we define a function with the type family keywords:

type family MyFunc

HTS is what we call a “type-level” language. Accordingly, we call values “types” and we call the type of a value its “kind”. We call functions “type families”, but it’s a habit of mine to just call them “functions” sometimes, for simplicity.

Arguments are supplied after the function name, with an argument name, then ::, then a kind. The return kind of the function comes last, after another ::. Implementations are defined as pattern matches, with the name of the function, then an argument pattern, then =, then the body. Type constructors (types like True or False) can optionally be specified with a ' tick in front, for some reason. The tick is occasionally required (e.g. on '[]), but mostly you can leave it off, and the compiler will complain when you need it.

For example, the function Not that inverts a boolean looks like this:

type family Not (b :: Bool) :: Bool where
  Not True = False
  Not False = True

b is the argument, of kind Bool. The function returns a Bool. Not True is defined as False, and vice versa.

We can evaluate this function by opening GHCi, loading in the module, and typing in :k! Not True. Also, λ is just the GHCi prompt, so you don’t need to worry about that bit.

λ :k! Not True

<interactive>:1:5: error:
    Not in scope: type constructor or class ‘True’
    A data constructor of that name is in scope; did you mean DataKinds?

Hmm, our first error. We can fix it by typing :set -XDataKinds into GHCi. Weird that we’re required to set up the HTS REPL every time we want to use it. However, we can now evaluate our function!

λ :set -XDataKinds
λ :k! Not True
Not True :: Bool
= 'False

Here’s our first coding style choice for HTS: I like to write the arguments to a function on separate lines, for clarity. And here’s another example: boolean And. It takes a Bool a and a Bool b and returns a type of kind Bool.

type family And
  (a :: Bool)
  (b :: Bool)
    :: Bool where
  And True True = True
  And True False = False
  And False True = False
  And False False = False

HTS does something pretty cool with partially defined functions. Instead of erroring out, it simply evaluates as far as it can, and returns whatever it got from doing that. Here’s an Or which is only defined in one case out of four.

type family Or
  (a :: Bool)
  (b :: Bool)
    :: Bool where
  Or True True = True

Trying to run it with unexpected arguments just gives back an unevaluated expression. It evaluates as far as it can though. Nifty!

λ :k! Or False True
Or False True :: Bool
= Or 'False 'True

λ :k! Or False (Or (Or True True) (Or True True))
Or False (Or (Or True True) (Or True True)) :: Bool
= Or 'False 'True

HTS has pretty good support for operations on the natural numbers.

type family PlusOne
  (n :: Nat)
    :: Nat where
  PlusOne n = n + 1

type family IsOdd
  (n :: Nat)
    :: Bool where
  IsOdd 0 = False
  IsOdd 1 = True
  IsOdd n = IsOdd (n - 2)

Multiplication might give strange errors at first, but ensuring you have {-# LANGUAGE NoStarIsType #-} at the top of the file will fix it.

We can introduce our own kinds in a way that’s eerily similar to Haskell’s data syntax, except of course we’re using types and kinds rather than terms and types.

data Direction
  = Forward Nat
  | Down Nat
  | Up Nat

You can also add a new name for an existing kind (newkind?) straightforwardly, if you think better names will help you out. Confusingly, the keyword to do this is type, and it also renames a type. Very strange.

type Bit = Nat

You’ll need :set -XKindSignatures to be able to write out the signature below, but otherwise it looks like our new kind was created successfully.

λ :k! [1,0,1] :: [Bit]
[1,0,1] :: [Bit] :: [Nat]
= '[1, 0, 1]

Branching comparisons

HTS relies heavily on pattern matching as its branching mechanism, and generous use of helper functions is recommended. For example, let’s say we want to compare two Nats, and return the greater of the two.

We can start with the overall interface: taking two Nats and returning a Nat:

type family Max
  (a :: Nat)
  (b :: Nat)
    :: Nat where
  Max a b = _

A convenient way to compare two naturals is with CmpNat which takes two Nats and gives us an Ordering—one of LT, EQ, or GT. With this extra ordering information, we can write a MaxHelper which gives us the answers we want.

type family MaxHelper
  (o :: Ordering)
  (a :: Nat)
  (b :: Nat)
    :: Nat where
  MaxHelper LT a b = b
  MaxHelper EQ a b = a
  MaxHelper GT a b = a

Then, we simply go back and fill in the definition of Max:

  Max a b = MaxHelper (CmpNat a b) a b

All is well.

λ :k! Max 7 999
Max 7 999 :: Nat
= 999

More Type Family Fun: Errors and Polymorphism

As mentioned, it’s possible to leave out certain pattern matches. The default behavior is that expressions will simply be left incompletely evaluated. However, sometimes it’s convenient to provide an error instead. We can do that with the TypeError type family.

type family Head
  (input :: [a])
    :: a where
  Head '[] = TypeError (Text "empty type-level list")
  Head (x : xs) = x

Note that Head uses the kind variable a, and so it works for various kinds, like Symbols (HTS’ name for strings), Nats, Types, etc.

λ :k! Head ["a","b","c"]
Head ["a","b","c"] :: Symbol
= "a"
λ :k! Head [1,2,3]
Head [1,2,3] :: Nat
= 1
λ :k! Head [Bool,Int,Char]
Head [Bool,Int,Char] :: Type
= Bool

This polymorphism suggests that we could write a function like this:

type family Map
  (f :: a -> b)
  (list :: [a])
    :: [b] where
  Map _ '[] = '[]
  Map f (x : xs) = f x : Map f xs

Indeed we can use this to map in certain cases, given that the kind signatures all line up properly. For example, because Monad has kind (Type -> Type) -> Constraint, we can map Monad over these familiar types of kind Type -> Type:

λ :k! Map Monad [Maybe, Either String]
Map Monad [Maybe, Either String] :: [Constraint]
= '[Monad Maybe, Monad (Either String)]

However, if we try to map a type family like our PlusOne :: Nat -> Bool from above, we run into a problem.

λ :k! Map PlusOne [1,2,3,4,5]

<interactive>:1:1: error:
    The type family ‘PlusOne’ should have 1 argument, but has been given none

Our problem here is that type families don’t allow for partial application—they must be fully saturated, meaning that they have all their arguments applied. Currying is good for something—who knew!

As of this writing, it’s possible to solve this problem by using the UnsaturatedTypeFamilies language extension and running a special version of GHC that supports it. Alternatively, note that we can get the same results just by doing more programming work per function we want to Map. In this case, this amounts to combining Map and PlusOne into MapPlusOne which does the work of both.

type family MapPlusOne
  (list :: [Nat])
    :: [Nat] where
  MapPlusOne '[] = '[]
  MapPlusOne (x : xs) = x + 1 : MapPlusOne xs

There we go:

λ :k! MapPlusOne [1,2,3,4,5]
MapPlusOne [1,2,3,4,5] :: [Nat]
= '[2, 3, 4, 5, 6]

It’s also possible to write Filter in this kind of way, but you’ll want an additional helper function that does the work of pattern matching out whether the filter should be applied or not.

type family FilterIsOdd
  (list :: [Nat])
    :: [Nat] where
  FilterIsOdd '[] = '[]
  FilterIsOdd (x : xs) = AppendIfOdd (IsOdd x) x xs

type family AppendIfOdd
  (isOdd :: Bool)
  (x :: Nat)
  (xs :: [Nat])
    :: [Nat] where
  AppendIfOdd True x xs = x : FilterIsOdd xs
  AppendIfOdd False _ xs = FilterIsOdd xs

Seems to work okay:

λ :k! FilterIsOdd [1,2,3,4,5]
FilterIsOdd [1,2,3,4,5] :: [Nat]
= '[1, 3, 5]

Parsing

We’ve seen that it’s possible to pattern match on type-level lists. However, symbols don’t come apart so easily. Instead, let’s use ToList from the symbols library to convert symbols to lists and then just do our usual list manipulation. ToList uses a fairly clever technique of looking up each character in a tree. I recommend reading the accompanying blog post if you’re interested in the details.

Let’s try a type family for parsing out natural numbers. We can adapt some code from symbols to make that easier. After a ToList, we can read in digit characters and do the math to parse a Nat from what was originally a Symbol.

type family ParseNat
  (s :: Symbol)
    :: Nat where
  ParseNat s = PNHelper (ToList s) 0

type family PNHelper
  (s :: [Symbol])
  (acc :: Nat)
    :: Nat where
  PNHelper ("0" : rest) acc = PNHelper rest (10 * acc + 0)
  PNHelper ("1" : rest) acc = PNHelper rest (10 * acc + 1)
  PNHelper ("2" : rest) acc = PNHelper rest (10 * acc + 2)
  PNHelper ("3" : rest) acc = PNHelper rest (10 * acc + 3)
  PNHelper ("4" : rest) acc = PNHelper rest (10 * acc + 4)
  PNHelper ("5" : rest) acc = PNHelper rest (10 * acc + 5)
  PNHelper ("6" : rest) acc = PNHelper rest (10 * acc + 6)
  PNHelper ("7" : rest) acc = PNHelper rest (10 * acc + 7)
  PNHelper ("8" : rest) acc = PNHelper rest (10 * acc + 8)
  PNHelper ("9" : rest) acc = PNHelper rest (10 * acc + 9)
  PNHelper _ acc = acc

This parses up to the first non-digit character (or the end of input), which is pretty convenient.

λ :k! ParseNat "1234 hello 789"
ParseNat "1234 hello 789" :: Nat
= 1234

We can write similar Parse functions to read in arbitrary formats. It’s much slower than a typical language’s parsing, but hey, it works.

type family Parse
  (chars :: [Symbol])
    :: [Direction] where
  Parse '[] = '[]
  Parse ("\n" : rest) = Parse rest
  Parse ("f" : "o" : "r" : "w" : "a" : "r" : "d" : " " : rest) =
    Forward (ParseNat rest) : Parse rest
  Parse ("u" : "p" : " " : rest) =
    Up (ParseNat rest) : Parse rest
  Parse ("d" : "o" : "w" : "n" : " " : rest) =
    Down (ParseNat rest) : Parse rest
  Parse (x : rest) = Parse rest

We’ve parsed Nats and Directions from a Symbol.

λ :k! Parse (ToList "forward 5\ndown 5\nforward 8\nup 3\ndown 8\nforward 2")
Parse (ToList "forward 5\ndown 5\nforward 8\nup 3\ndown 8\nforward 2") :: [Direction]
= '[ 'Forward 5, 'Down 5, 'Forward 8, 'Up 3, 'Down 8, 'Forward 2]

In Conclusion

HTS is a fun language. It’s got some goodies like pattern matching, algebraic data kinds, and an interesting partial-evaluation model. Lack of partial application can be annoying for someone used to fully-fledged functional programming, but UnsaturatedTypeFamilies fixes it (if you’re okay with your compiler being on a special branch just for this purpose).