Type-Level Haskell from Zero to Advent

This material is from an in-person workshop I ran during my company’s Engineering Week, 2026.

Intro

In this workshop, we’ll treat Haskell’s type system as its own language, learning:

How to declare type-level data structures
How to define type-level functions
How to do type-level parsing

Finally, we’ll tackle some real Advent of Code problems using only types!

Getting Started

Make sure ghci is installed
- with a GHC version of 9.2 or above (ghci --version)
Follow along interactively, or grab the repo

Boxes like this one indicate a hands-on-keyboard exercise or instruction.

This was originally a workshop, so there are a lot of them!

Types and Kinds

By the end of this workshop, you’ll be able to solve Advent-of-Code-level problems using Haskell’s type system.

You should already know some Haskell, especially:

declaring datatypes
defining functions (pattern matching, recursion, basic syntax)
reading/writing type signatures
what a “kind” is (roughly, the type of a type)

Let’s distinguish values, types, and kinds.

Open ghci and run the :commands below.

We can ask ghci for the type of a value.

:t True

One level up, we can also ask for the kind of a type.

:k Bool

Some type signatures indicate value arguments.

:t id
:t (++)

Some kind signatures indicate type arguments.

:k Maybe
:k Either

What happens if we ask for the type of a type like Bool? First make a guess, then check that guess.

:t Bool

What happens if we ask for the kind of a value like True? First make a guess, then check that guess.

:k True

Promotion

Turn on the DataKinds language extension.

:set -XDataKinds

Now, we can ask for the kind of a “value”.

:k True

DataKinds did two “promotions” here:

promoted the constructor True to be a type
promoted the type Bool to be a kind

For added clarity, from now on I’ll start distinguishing two “languages”:

POH - plain old Haskell
HTS - Haskell Type System

POH refers to the values-and-types part of Haskell (i.e. “normal Haskell”). HTS refers to the types-and-kinds part (i.e. “type-level Haskell”).

Treating these concepts as two separate languages helps disambiguate when we’re talking about concepts which show up in both (e.g. “the type level”). We could call HTS “promoted” and POH “unpromoted”, but that’s more unwieldy.

We currently have all of these in scope:

the POH value True
the HTS type True
the POH type Bool
the HTS kind Bool

We’re allowed to have an HTS kind and HTS type with the same name, just like we’re allowed to have a POH type and POH value with the same name:

With DataKinds on, define Unit.

data Unit = Unit

Now we have all three varieties of Unit (value, type, kind) in scope. Check this with:

x = Unit
:t Unit
:k 'Unit

The ' in 'Unit lets GHC disambiguate HTS from POH. Compare against:

:k Unit

An easy way to create HTS datatypes is to write POH data declarations and turn on DataKinds to promote them.

Type Families

Promoting constructors from POH to HTS is nice! Unfortunately, we can’t simply promote POH functions to HTS functions.

Let’s rewrite the POH boolean-or operator (||) as an HTS function.

The POH type signature looks like:

(||) :: Bool -> Bool -> Bool

The HTS kind signature is similar, but begins with the type keyword. This syntax is enabled by the StandaloneKindSignatures language extension.

type Or :: Bool -> Bool -> Bool

A POH definition looks like:

(||) True  _ = True
(||) False x = x

In HTS, there’s an extra bit of preamble. Type-level functions in Haskell are called “type families”, and start with the type family keywords. This syntax is enabled by the TypeFamilies extension. In this workshop, I’ll call type families “HTS functions”. After type family, we state the function name, list its arguments, and end with where.

type family Or a b where

The rest of the HTS definition looks a lot like the POH definition.

  Or True  _ = True
  Or False x = x

For practice, define each of these HTS functions:

And, based on POH (&&)
Not, based on POH not
Nand, using your definitions of And and Not

Symbols and Nats

There are some other useful HTS kinds we should know about.

In POH, we’d use the Text type for messages…

{-# LANGUAGE OverloadedStrings #-}

import Data.Text (Text)

message :: Text
message = "hello world"

…but in HTS we use the Symbol kind.

import GHC.TypeLits (Symbol)

type Message :: Symbol
type Message = "hello world"

What’s the type of "hello"? What’s the kind of "hello"? Check with ghci.

The ExplicitNamespaces extension lets us import type-level operators, as seen with type (+) here:

import GHC.TypeLits (type (+))

What’s the type of (+)? What’s the kind of (+)? Check with ghci.

What’s the kind of 1 + 2? Check with ghci:

:k 1 + 2

ghci actually has built-in support for evaluating HTS expressions!

Try this and compare against the previous command’s output:

:k! 1 + 2

Define an HTS function AddOne that uses HTS (+) to add 1 to an input number.

Let’s also import CmpNat :: Nat -> Nat -> Ordering.

import GHC.TypeLits (CmpNat)

What do you expect the result of CmpNat 6 7 to be? Check with ghci.

What do you expect the result of CmpNat 6 to be? Check with ghci.

Use CmpNat to test AddOne on a few different inputs.

Symbol to Chars

Unlike a POH String, an HTS Symbol can’t be directly manipulated as a list of characters.

However, since GHC 9.2, there’s a helpful HTS function called UnconsSymbol.

import GHC.TypeLits (UnconsSymbol)

Its kind is:

UnconsSymbol :: Symbol -> Maybe (Char, Symbol)

UnconsSymbol acts like a rather unwieldy POH (x:xs) pattern match. It takes a Symbol, splitting it into Just the first Char and the rest of the Symbol, or giving us Nothing when that’s not possible.

We can use the results of UnconsSymbol to recursively build up a [Char] in a helper function:

type SymbolCharsHelper :: Maybe (Char, Symbol) -> [Char]
type family SymbolCharsHelper maybeUnconsed where

Base case: if there are no characters, the list is empty.

  SymbolCharsHelper 'Nothing = '[]

Recursive case: add the first Char to the growing [Char].

  SymbolCharsHelper ('Just '(first, rest)) =
    first ': SymbolChars rest

Write the SymbolChars HTS function that converts a Symbol into a [Char]. It should use SymbolCharsHelper to do its dirty work.

We included ' ticks on all the promoted constructors in SymbolCharsHelper. Until now, we haven’t needed many promotion ticks (refer back to 'Unit in the Promotion section). Some of them aren’t actually necessary here, but others are!

Place your bets, then delete individual ' marks to discover which ones we actually need. Try to formulate a rule for which ones are necessary and which ones aren’t.

Parsing

With the ability to treat a Symbol as a [Char], we can now start parsing inputs.

Write an HTS function ParseDigit :: Char -> Nat. It takes any single digit character and converts it into a number. Advent of Code input is always well-formed, so ParseDigit can simply ignore any input that isn’t actually a digit.

Incidentally, what are our other options for error handling in HTS?

Write an HTS function ParseNat :: [Char] -> Nat. It should act like the equivalent of the POH read :: String -> Int (ignoring negatives). Test it on Number.

type Number = SymbolChars "8675309"

Write an HTS function ParseLines to split the lines of a [Char] input into a [[Char]]. Test it on this poem (“The Kitten” by Odgen Nash).

type Poem = SymbolChars
  "The trouble with a kitten is\nTHAT\nEventually it becomes a\nCAT."

Finally, put the previous parser pieces together and write ParseNatList :: Symbol -> [Nat]. Test it on some inputs like NumberList.

type NumberList = "123\n8675309\n0\n525600\n555"

Try implementing this with a generic HTS Map function. It should act like POH’s map :: (a -> b) -> [a] -> [b]. What issues did you run into? What did you learn?

Advent of Code 2021 Day 1

Solve Advent of Code 2021 Day 1.

This problem was carefully selected to use material we’ve already seen. You’ll likely want to include several HTS functions from the previous exercises. Excluding parsing, my solution is only three HTS functions long.

Advent of Code

Solve another Advent of Code problem in Haskell’s Type System.