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:

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

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`

:

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

:

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

All is well.

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

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:

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

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 `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.↩︎