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.TypeLitsIn 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 = FalseHTS 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 'TrueHTS 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 Nats, and return the greater of the two.
We can start with the overall interface: taking two Nats and returning a Nat:
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 = aThen, 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) = xNote 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
= BoolThis 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 xsIndeed 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 noneOur 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 xsThere 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 xsSeems 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 = accThis 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 restWe’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]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 Nats and doing arithmetic), but I think the type-families-based approach used in this post makes for a fairly cohesive set of language features.↩︎