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 of1) 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.↩︎