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^{1}) 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.

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:

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:

`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!

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.

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.

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.

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.

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.

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 `Nat`

s, and return the greater of the two.

We can start with the overall interface: taking two `Nat`

s and returning a `Nat`

:

A convenient way to compare two naturals is with `CmpNat`

which takes two `Nat`

s 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`

:

All is well.

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 `Symbol`

s (HTS’ name for strings), `Nat`

s, `Type`

s, 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:

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:

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.

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 `Nat`

s and `Direction`

s 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]
```

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).

As an exercise, pick some data structure and write the equivalent of **Foldable and Traversable** for it in HTS, using as much polymorphism as possible. Use unsaturated type families to achieve this.

Then, make a joke about polyunsaturated FaT and chuckle to yourself.

There are many other possible ways to treat the type system as a language (down to just encoding your programs in

`Nat`

s and doing arithmetic), but I think the type-families-based approach used in this post makes for a fairly cohesive set of language features.↩︎