Intro to monad transformers in Haskell

NOTE: this tutorial assumes you are already familiar with monads. If not, I would recommend learning about monads first.

Why monad transformers?

Let’s say we have functions with the following signatures:

type UserId = String

fetchUsersName :: UserId -> IO (Maybe String)

fetchUsersSurname :: UserId -> IO (Maybe String)

fetchUsersAge :: UserId -> IO (Maybe Int)

Imagine we are building an app and this is an API we are given to access specific user’s data. These functions take user’s id and go into the world to perform an IO action - e.g. a network request, or read from the disk. Also, an IO action can fail if e.g. there was no network connection available - that is why Maybe is in the return type.

With that, we want to implement the following function:

fetchUsersData :: UserId -> IO (Maybe (String, String, Int))

This function tries to fetch all the data for the specific user (name, surname and age) and if any piece of this data couldn’t be obtained it will declare itself as failed by returning Nothing within IO monad.

This is how we would go about implementing fetchUsersData:

fetchUsersData :: UserId -> IO (Maybe (String, String, Int))
fetchUsersData userId = do
    maybeName <- fetchUsersName userId
    case maybeName of
        Nothing -> return Nothing
        Just name -> do
            maybeSurname <- fetchUsersSurname userId
            case maybeSurname of
                Nothing -> return Nothing
                Just surname -> do
                    maybeAge <- fetchUsersAge userId
                    case maybeAge of
                        Nothing -> return Nothing
                        Just age -> return (Just (name, surname, age))

And this would work! The only not so nice thing is that we have this “staircasing” typical when nesting multiple Maybes. We would normally solve this by running things within a Maybe monad, but this time we are in IO monad so we can’t do that!

To generalize the problem, it occurs when we have one monad within another (Maybe within IO here) and would like to access “powers” of the inner monad to make our code nicer.

This is a common case when using monads in Haskell and exactly what monad transformers are set to solve - making it possible to user “powers” of one monad within another monad. In this case, we would like to extend IO’s capabilities with Maybe’s power to exit the computation early.

What is a monad transformer?

Here is what the documentation says:

A monad transformer makes a new monad out of an existing monad, such that computations of the old monad may be embedded in the new one.

And then there is a typeclass MonadTrans which every monad transfomer has to implement, which means monad transformer is actually a type. Monad transformer is a monad as well.

Here is how it looks like in our case, where we want to extend IO with Maybe capabilities:

newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }

MaybeT m a is a monad transformer version of Maybe a. There is only that extra m which stands for an “inner” monad that will be expanded with Maybe capabilities.

Regarding the named field of MaybeT (runMaybeT), here’s another bit from the documentation:

Each monad transformer also comes with an operation runXXXT to unwrap the transformer, exposing a computation of the inner monad.

If we wrapped IO within MaybeT and then couldn’t get it back again that would be a problem, since the function we are implementing needs to return IO (Maybe (String, String, Int)).

From this we can generalize and conclude that a monad transformer has:

• one additional type parameter (compared to its monad counterpart) - an inner monad that is being expanded with capabilities of the outer monad
• runXXXT function/field which returns the original, “inner” monad

What does it mean “monads don’t compose”?

If you have been learning about monad transformers, odds are you came across this statement. I did too, and often it was the first thing discussed when talking about monad transformers. But I couldn’t understand what does it mean to “compose” monads nor why it is a problem if that cannot be done.

As you also probably know and as we saw in the example with Maybe, each monad has its monad transformer counterpart (Maybe and MaybeT, Either and EitherT, …). Each of these monad transformer counterparts had to be manually and separately implemented by somebody.

That is exactly what the statement in question (monad composition) challenges - why do we have to do so much work, do we really need to implement xxxT version of each monad? It would be awesome if we could somehow automate this.

And that is where composing monads would come in handy. Monad composition is creating a new type which is parametrized by (any) two monads and is then also itself a monad. It would look like this:

newtype MonadComposition m1 m2 a = MonadComposition { getMC :: m1 (m2 a)) }

This is the general case of the example above, where m1 and m2 were IO and Maybe, respectively (one monad wrapped in another).

Now the main question here is can we implement the following:

instance (Monad m1, Monad m2) => Monad (MonadComposition m1 m2) where
    return = ...
    join = ...

If we could, that would mean MonadComposition m1 m2 is also a monad. Meaning that we solved the general case of composing any two monads! If that was true, we wouldn’t need to bother with implementing MaybeT, EitherT, ReaderT separately - MonadComposition would cover all of that for us automatically!

But as you reckon, that is not the case. It is not possible to make MonadComposition m1 m2 an instance of Monad typeclass. It can be proved and it is not trivial. From the intuitive perspective, we can understand that we need more information, the general case is not covering it. If the “outer” monad is Maybe, we need to implement what MaybeT will do in terms of Nothing and Just x, which means we need the specifics.

So that is it! Now you know what “monads don’t compose” means and why it is important.

MaybeT

We used it as an example in the introduction, but let’s now officially take look at it.

From the docs:

The MaybeT monad transformer extends a monad with the ability to exit the computation without returning a value.

A sequence of actions produces a value only if all the actions in the sequence do. If one exits, the rest of the sequence is skipped and the composite action exits.

Here is the type definition:

newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }

m being an arbitrary monad composed with Maybe monad. Let’s now see it in action with our example from the beginning:

fetchUsersData :: UserId -> IO (Maybe (String, String, Int))
fetchUsersData userId = runMaybeT $ do
    name <- MaybeT $ fetchUsersName userId
    surname <- MaybeT $ fetchUsersSurname userId
    age <- MaybeT $ fetchUsersAge userId

    return (name, surname, age)

We can see from the types this works. We don’t end on the left hand side of <- anymore with Maybe a which we then have to unpack (leading to the staircasing we saw before), but we get a directly.

But what actually happens behind the curtains? Let’s see how MaybeT implements Monad typeclass:

instance Monad (MaybeT m) where
    -- yields a computation that produces value
    return :: a -> MaybeT m a
    return = MaybeT . return . Just

    -- if a computation within monad failed, short-circuits to failed.
    (>>=) :: MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
    x >>= f = MaybeT $ do -- entering inner monad m
        v <- runMaybeT x  -- unpacking x from `MaybeT m a` to `Maybe a`
        case v of
            Nothing -> return Nothing
            Just y -> runMaybeT (f y)

We can see that actually here MaybeT does the heavy lifting for us, what we previously did manually (staircasing example) - it operates within m (IO in the example) and gets to Maybe a and then does that “manual” check whether it is Nothing or not.

Lifting

We said monad transformers are all about combining the powers of two or more monads. With our MaybeT IO a example we’ve shown how we can get Maybe’s power and make sure that the whole computation is short-circuited to Nothing if some sub-computation failed. But what if we wanted to do some IO stuff, e.g. print Fetching data...?

This is why we have lift, which is the only function of MonadTrans typeclass:

class MonadTrans t where
    -- | Lift a computation from the argument monad to the constructed monad.
    lift :: (Monad m) => m a -> t m a

Argument monad is the “inner” monad (IO in our example) and constructed monad is the actual monad transformer (MaybeT in our case).

So this is the function that allows us to “lift” the inner monad’s computation into the monad transformer’s realm, hence the name. It allows us to do this:

fetchUsersData :: UserId -> IO (Maybe (String, String, Int))
fetchUsersData userId = runMaybeT $ do
    lift $ putStrLn "Fetching data..." -- <- NEW

    name <- MaybeT $ fetchUsersName userId
    surname <- MaybeT $ fetchUsersSurname userId
    age <- MaybeT $ fetchUsersAge userId

    return (name, surname, age)

lift here does exactly what it says in its signature, takes IO () and lifts it into MaybeT IO () so we can call this printing action within MaybeT monad.

It is also maybe interesting to see how MaybeT implements lift:

instance MonadTrans MaybeT where
    lift = MaybeT . liftM Just

In the case of printing from above, IO () would come in, liftM Just would produce IO (Just ()) and then MaybeT data constructor would create an instance of MaybeT IO () type.

Phew, we just went through our first monad transformer! Let’s now take a look at another one - ExceptT.

ExceptT

ExceptT is a monad transformer version of Either and is very similar to MaybeT, just as Either is similar to Maybe. The only difference is that in the case of the failure the exception that is thrown actually contains a value (additional error data) rather than just Nothing.

Here is the type definition:

newtype ExceptT e m a = ExceptT (m (Either e a)) -- e is the exception type

runExceptT :: ExceptT e m a -> m (Either e a)
runExceptT (ExceptT m) = m -- just unwraps and returns the inner monad

So let’s just quickly go through the analogous example - let’s assume we are given following API functions:

type UserId = String
type ErrorMsg = String

fetchUsersName :: UserId -> IO (Either ErrorMsg String)

fetchUsersAge :: UserId -> IO (Either ErrorMsg Int)

And we want to implement:

fetchUsersData :: UserId -> IO (Either ErrorMsg (String, Int))

If we try do to it without ExceptT monad transformer, we’ll again bump into the staircasing issue:

fetchUsersDataNoT :: UserId -> IO (Either ErrorMsg (String, Int))
fetchUsersDataNoT userId = do
  nameE <- fetchUsersName userId
  case nameE of
    Left nameError -> return $ Left nameError
    Right name -> do
      ageE <- fetchUsersAge userId
      case ageE of
        Left ageError -> return $ Left ageError
        Right age -> return $ Right (name, age)

Now let’s try with ExceptT:

fetchUsersData :: UserId -> IO (Either ErrorMsg (String, Int))
fetchUsersData userId = runExceptT $ do
  lift $ putStrLn "Fetching user's data..."

  name <- ExceptT $ fetchUsersName userId
  age <- ExceptT $ fetchUsersAge userId

  return (name, age)

Nice! Let’s also take a look at how ExceptT implements Monad:

instance (Monad m) => Monad (ExceptT e m) where
    return a = ExceptT $ return (Right a) -- wraps it in the inner monad

    m >>= k = ExceptT $ do -- enter inner monad
        a <- runExceptT m -- run inner monad computation
        case a of
            Left e -> return (Left e) -- end early
            Right x -> runExceptT (k x) -- continue with the execution

And that’s it! This is almost exactly the same as MaybeT, the only difference being the error message that Either brings with itself.

ReaderT

As we know, Reader monad is useful

Intro to type-level programming in Haskell - Part 2

This is the second part of the series of posts on this topic. You can find the first part here.

In the previous part of this tutorial we created a List a empty for which we could tell from its type whether it is empty or not (by empty being other Empty or NonEmpty). This is how our final code looked like:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data ListStatus = Empty | NonEmpty

data List (a :: * ) (empty :: ListStatus) where
    End :: List a 'Empty 
    Cons :: a -> List a empty -> List a 'NonEmpty

safeHead :: List a NonEmpty -> a
safeHead (Cons elem _ ) = elem

The question where we left off was: can we create safeTail function that would accept only non-empty lists?

Let’s try to construct its type signature:

safeTail :: List a NonEmpty -> List a ?
safeTail (Cons elem rest) = rest

Everything makes sense except one thing - we don’t know in compile time what is empty going to be for a returned list. It depends on the input list - if it has only one element, the result will be Empty. Otherwise, it will be NonEmpty But the problem is that with our current type system we cannot differentiate between them and they are both marked as NonEmpty.

[Going deeper] But what if we just put List a smth as a return type?

In the previous part of the tutorial we had cases where the created list had empty type param which just stayed general and that worked. So what would happen if we tried that here?

Ok, so here is what we are trying to compile:

safeTail :: List a NonEmpty -> List a smth
safeTail (Cons elem rest) = rest

This looks like we are trying to leave to the compiler to determine what will smth actually be, we just say “this will be something/anything”. Plus we have a type param value smth that doesn’t appear anywhere in the function arguments, on the “left” side, but just in the result. I am not sure if that could make sense in any case?

But interesting thing is, the following compiles:

safeTail :: List a NonEmpty -> List a smth
safeTail (Cons elem rest) = undefined

It doesn’t say “you have type param value smth which doesn’t appear anywhere on the left side.” which surprised me a bit. I still wonder why could that be valid?

NOTE: On the other hand, we can have Nothing :: Maybe a and in that case it is ok to have a on the right side only, so I guess that is ok actually.

But if we try to compile the original function, it fails. The error message is a bit longer as usual with Haskell, but from what I understood it basically says the following: “I can see from the List constructors that any list you create will have a specific type, and you are here trying to say it will be just anything. Tell me exactly what it is.”

TODO: I am not sure if I got this completely right. Figure out what is exactly the reason this does not compile.

The conclusion from all this is: we need a more expressive type so we can specifically say what is the type of the returned list going to be!

Example: Length indexed lists (vectors)

NOTE: in other tutorials often is used the term “Vector” instead of “List”, which we used so far.

What is the next piece of information about the list we could know, besides whether it is empty or not? It is its length - and if we could knew that, we could implement safeTail without problems. We wouldn’t worry what “type” of non-emptiness input list has - we would just reduce the length by one.

Let’s see how we can encode length into the type of our list.

Encoding list’s length in its type

Our list type is going to look like this:

data List length a

Again we have two type parameters, a is for type of elements in the list while length is for type from which we can tell the list’s length.

Before we had just two values (or “list states”) that we needed to encode with types, Empty and NonEmpty, so we created two types (or one type with two data constructors when we used DataKinds - then from that DataKinds created the types for us). But this time we have infinite amount of values, since length of a list can be any natural number. So how do we represent that with types? We can do it in the same way we defined the list itself, recursively:

-- Uninhabitated types
data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two -- or Succ (Succ (Succ Zero))

Succ stands for Successor. We can see that since Succ is a parametrized type constructor we can actually from it create infinite amount of types and that solves our problem. This works, but as in a previous example it would be better to use DataKinds so we have kind safety (otherwise somebody could write nonsense such as Succ Bool and it would be a valid term):

{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat

And this is it! From this, DataKinds will create type constructors 'Zero and 'Succ nat. Let’s see their kinds and compare them to types of the data constructors they originated from (Zero and Succ).

-- Types of data constructors
> :type Zero
Zero :: Nat

> :type Succ
Succ :: Nat -> Nat

-- Kinds of type constructors
> :kind 'Zero
'Zero :: Nat

> :kind 'Succ
'Succ :: Nat -> Nat

The types of data constructors look exactly the same as kinds of newly created type constructors! This is what DataKinds does - promotes data into types, and types into kinds. We ended up with a new kind Nat and we can create infite amount of types with that kind:

{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat

type One = 'Succ 'Zero
type Two = 'Succ One
Type Three = 'Succ ('Succ ('Succ 'Zero))

Now let’s use this and create a type for our length-indexed list:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = Zero | Succ Nat

data List (length :: Nat) (a :: * ) where
    End :: List 'Zero a
    Cons :: a -> List length a -> List ('Succ length) a

The main difference from the previous example is how we are managing types in Cons. Instead of just putting e.g. NonEmpty, here we are building on top of the input type, length of the input list. So if the input list had length 'Succ 'Zero, the new one will have 'Succ ('Succ 'Zero).

And that is it! We have now defined list which will have its length contained in its type. Let’s see it in action:

> :t End
End :: List 'Zero a

> oneElemList = Cons "elem" End
> :t oneElemList
oneElemList :: List ('Succ 'Zero) [Char]

> twoElemList = Cons "elem2" oneElemList
> :t twoElemList
twoElemList = List ('Succ ('Succ 'Zero)) [Char]

Wohoo, it works! Now we can finally implement safeTail:

safeTail :: List ('Succ n) a -> List n a
safeTail (Cons _ rest) = rest

Let’s test it out:

> emptyList = End
> safeTail emptyList
Error: Couldn't match type 'Zero with 'Succ n

> oneElemList = Cons "elem" End
> safeTail oneElemList
End

Everything works as expected. This time we didn’t have any trouble defining safeTail’s types - we restricted input list to have at least one element ('Succ n) and then output will simply be of length n.

The basic implementation of length-index list is now done. We can create a list and we can also operate with safeTail and safeHead on it. Is there anything else we might need?

List concatenation - making it work on type level

For example, what if we wanted to concatenate two lists? Logically, we know that the resulting list will have length which is the sum of lengths of the input lists. But how do we represent that on type level?

Let’s try to see what will the function signature look like. We will call this function append (so we don’t confuse it with Prelude’s concat) - it will take two lists and produce a new list which is a concatenation of those two input lists:

append :: List n a -> List m a -> List ? a

Let’s also see a few examples of how it would work:

> twoElems = append (Cons "a" End) (Cons "b" End)
> :t twoElems
twoElems :: List ('Succ ('Succ 'Zero)) [Char]

> twoEmptyLists = append End End
> :t twoEmptyLists
twoEmptyLists :: List 'Zero a

So we take two lists of lengths n and m respectively (we don’t care if they are empty or not in this case, since there isn’t any “unsafe” scenario) and we produce a new list of length n + m. But how do we represent its length, what do we put in place of ??
Obviously, we want to sum m and n - but how do we do that on a type level?

Wouldn’t it be handy if there was a way to define a function that operates on types? Then we could define things like this:

append :: List n a -> List m a -> List (Add n m) a

Where Add n m is a “type” function that would take two types n and m and produce a new type which would represent their sum.

Type families - functions that operate on types

Turns out there is a special mechanism for this in Haskell and it is provided in form of another language extension named TypeFamilies. This is how we would define our type family Add n m:

type family Add (x :: Nat) (y :: Nat) :: Nat where
Add 'Zero n = n
Add ('Succ n) m = Add n ('Succ m)

Since we are dealing with recursive types ('Succ), this type function has to work in the same way. In the base case when the left type is 'Zero, we simply return the second type. In the general case we keep “deconstructing” the left argument and “piling” it on the right type until we reach the base case.

This looks like a logical way to do it. But if, we try to compile it we will get the following error:

• The type family application
    is no smaller than the instance head ‘Add n ('Succ m)’
    (Use UndecidableInstances to permit this)
• In the equations for closed type family ‘Add’
    In the type family declaration for ‘Add’

The problem is that GHC is here scared that our general recursion case might never terminate. I checked out docs of UndecidableInstances and here is what it says: These restrictions ensure that instance resolution terminates: each reduction step makes the problem smaller by at least one constructor.

And this is exactly what is the problem: we made a reduction step, but we still have the same number of constructors ('Succ) - we just moved it from one argument to another and that made GHC suspicious we are designing a system that actually terminates.

If we e.g. did this (although it is conceptually wrong, does not produce the result we want):

Add ('Succ n) m = Add n  m

we wouldn’t get any errors - GHC sees that we got rid of one 'Succ and is happy and convinced that we will eventually come to the end.

TODO: Why GHC doesn’t complain if we do Add ('Succ n) m = 'Succ (Add n m), since we still have the same number of constructors? Is it because Add is not at the beginning anymore?

This was pretty impressive for me, I didn’t know GHC watches over this kind of stuff, “counting” how our recursion is doing.

Anyhow, we can solve the problem from above by introducing UndecidableInstances extension. With it, our code from above successfully compiles.

Now that we know how to sort out things on the type-level, let’s actually write the function which appends two lists:

append :: List n a -> List m a -> List (Add n m) a
append End xs = xs
append (Cons elem rest) xs = Cons elem (append rest xs)

We again do it recursively, always taking the first element “out” and calling append again for the reduced first list and the second list (general case). When first list reaches End, append will just return the second list (base case).

But, if we try compile this we get an error! This is what it says:

• Could not deduce: Add n1 ('Succ m) ~ 'Succ (Add n1 m)
      from the context: n ~ 'Succ n1
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Nat).
                            a -> List n a -> List ('Succ n) a,
                 in an equation for ‘append’
        at gadtNonEmptyList.hs:121:9-20
      Expected type: List (Add n m) a
        Actual type: List ('Succ (Add n1 m)) a
    • In the expression: Cons a (append rest xs)

What this error says is it basically complains that return type is not correct, it is different from what we declared in the function signature. In the signature we said that return type is List (Add n m) a. When append’s function body is evaluated, Cons elem (append rest xs), it will be of type List ('Succ (Add n m) a).

Why? Let’s deconstruct Cons elem (append rest xs) from the inside out. append rest xs is of type List (Add n m) a. And Cons’s type signature is Cons :: a -> List n a -> List ('Succ n) a - whatever n is, Cons will put 'Succ on it. So in our case, where n is Add n m (from append rest xs), applying Cons on it will produce type List ('Succ (Add n m)) a. And what we promised to GHC in append’s return type was List (Add n m) a.

Even if GHC tries to evaluate Add n m to see what is under the hood, it will again see from the general step that Add x y is produced. So when comparing returned and expected type (List ('Succ (Add n m)) a and List (Add n m) a), GHC sees that extra 'Succ and concludes “wait, this is not what I expected, I was looking for Add but I got 'Succ” and throws an error.

The root of the problem is in what we experienced when defining Add n m type family, that GHC doesn’t understand that Add n m will eventually produce a concrete type ('Succ in this case), because of the way we designed our recursion which always puts Add in the front. We managed previously to patch it up with enabling UndecidableInstances, but now it is coming back to haunt us again.

We can solve it by slightly changing Add’s definition, the general case of the recursion:

type family Add (x :: Nat) (y :: Nat) :: Nat where
Add 'Zero n = n
Add ('Succ n) m = 'Succ (Add n m)
-- Before: Add ('Succ n) m = Add n ('Succ m)

So what we did is rearrange things a bit so now 'Succ comes in front. With this change we don’t get any errors and we can also disable UndecidableInstances. When GHC sees this it decides our recursion will eventually terminate and doesn’t complatin. I am not sure exactly why, my guess is because here we applied Add to the “reduced” argument (n, while input was 'Succ n) so that tells GHC that our recursion is moving in the right direction, that we are reducing the problem. Previously we just moved 'Succ from one argument to another so I guess that was the problem, we haven’t “reduced” anything. This is my current assumption and I would still like to understand this better.

And this is it, with this last change everything works as expected! Now we can see append in action, but let’s first just do one more thing:

instance Show a => Show (List n a) where
    show End = "End"
    show (Cons e es) = show e ++ " - " ++ (show es)

I implemented List as an instance of Show typeclass so we can nicely visualize our lists.

Let’s now see append on a few examples:

> append (List "a" End) (List "b" End)
"a" - "b" - End

> :t append ((List "a" End) (List "b" End))
 append ((List "a" End) (List "b" End)) :: List ('Succ ('Succ Zero)) [Char]

> append (List "a" End) End
"a" - End

We can see how everything works and also that types accurrately reflect number of elements in the list.

For the end, here some of my thoughts on type-level programming after trying it out on these examples:

• Type-level programming let’s us put put more features/properties into types and achieve compile time safety for them, but not without a cost - we have to program things both on type and data level (e.g. as we did with append function).
• It is important to consider how we will implement and structure types to match well in all instances, since it is possible run into non-obvious errors such as we hadd with Add n m.

All together it was really cool for me to learn about this! I hope you found it useful - let me know if you have any questions or if I could have done anything better.

Intro to type-level programming in Haskell - Part 1

I heard a lot lately about using types in Haskell to describe function arguments in more details (e.g. function takes a list that is non-empty) and thus achieve higher compile-time safety. It sounded cool so I decided to research more about it and I created this blog post as a memo of what I learned.

Resources I used:

• Tutorial on GADTs and DataKinds by andre.tips
  • explains GADTs well, but DataKinds not so much. I would recommend to start with this one. [The page seems to be down, so I linked to the Wayback Machine url.]
• Basic Type Level Programming in Haskell by Matt Parsons
  • pretty extensive, but not so intuitive. Still the most complete intro (and pretty much the only one) to the topic. Most of my examples below are taken from it.

Why type-level programming?

As I wrote above, my current understanding is that with it we can add more info into the type signature of a function, making it “safer” in the compile time. E.g. instead of just saying “this function takes a list” we can say “this function takes a non-empty list”, or “this function takes Int which is > 10 and < 127” (although this last one might be solved just by creating an appropriate type, e.g. using TH?).

TODO: I would love to learn about more examples where this is used.

Example: A function that accepts only a non-empty list

We want to be able to tell from its type whether a list is empty or not. To do that we will create a new type which will have that information stored in it.

First, let’s see how we would create a “normal” list type on our own:

data List a = End | Cons a (List a)

This is a usual recursive definition of list (Cons stands for Constructor). Once there is an instance of this type we can tell which type of elements the list contains (e.g. List Int or List (Maybe String)), but nothing more than that. We cannot deduce from its type (which means in compile time) whether it is empty or not.

We could of course check it in runtime and throw an exception if the list is empty, but we want to be stricter than that. We want to ensure that program cannot even be compiled if an empty list is provided where it shouldn’t be.

What are we missing?

The problem with the “normal” list we defined above is that we are missing information in its type. We have only one piece of information and that is type of the elements within the list - we use type parameter a to declare that. We can also use it to define functions that work only for a specific a. E.g. here is a function that works only on a list of integers:

sumListElements :: List Int -> Int

This is guaranteed in compile-time. If we call this function with a list of e.g. Bools, the compiler will throw an error at us.

Using type params to encode extra information

So here’s an idea - why don’t we just use the same mechanism again (having a type parameter) to know whether a list is empty or not. If we added another type parameter to keep track of that, our type (disregarding data constructors for now) would look like this:

data List a empty

Just as type param a means any type (e.g. Int or MyType), the same applies for empty. E.g. we could have List Int Double or List String Bool or List Int SomeCustomType. Just as we restricted function sumListElements above to work only when a is Int, we can use empty in the same way.

Let’s say we want to implement a safe version of head function - that means it accepts only a non-empty list as an argument, otherwise it won’t compile. We will call it safeHead.

Ok, we introduced empty as another type parameter, but the question we are facing now is what do we do with it? Which concrete types will take its place and how?

Lets introduce two new types:

data Empty
data NonEmpty

The interesting thing here is that we have only type constructors for these types and no data constructors. That means we cannot create instances (values) of these types, but that is ok! We need these types only at the type level, in function signatures. Such types are also called uninhabited or empty.

Now let’s imagine we have a way to correctly assign Empty and NonEmpty to empty and non-empty lists’ types. Then we could define safeHead as follows:

safeHead :: List a NonEmpty -> a
safeHead (Cons elem _ ) = elem

We wouldn’t even have to define a case for End since the type guarantees it can’t ever happen.

Assigning correct type to empty

The main question that is left is how do we produce such lists with an extra type parameter, and how do we make sure which type empty takes when? This is what we will look at now.

This is how our type List looks once we have added empty as a second type parameter:

data List a empty = End | Cons a (List a empty)

Except adding that extra type parameter, nothing else changed. When I first saw this, I was confused by the fact there is a type parameter on the left side that doesn’t appear anywhere on the right side as a data. How is that possible, why would that make sense? (Ok, there is empty on the right side here, but only as a part of a type designation and not as a part of data constructor. Which means there will never be anything of type empty in some value of this type).

But turns out it does make sense, since we use it as a designation at the type level only, to show that an underlying value has a certain property (empty or non-empty in this case). Such types, which have a type parameter(s) on the left side that don’t appear on the right are also called phantom types.

Let’s see now what happens if we create an instance of our new List and test its type in GHCi:

> emptyList = End
> :t emptyList
List a empty

> nonEmptyList = Cons "haskell" End
> :t nonEmptyList
nonEmptyList :: List [Char] empty

As we can see, GHCi concluded that a is a string in nonEmptyList, but could not deduce anything for empty in either case, since it is not used anywhere. So how can we solve that and make sure that empty becomes Empty for emptyList and NonEmpty for nonEmptyList?

GADTs

Before we continue, let’s check types of our data constructors, End and Cons (since they are functions as well, we can do that):

> :t End
List a empty

> :t Cons
a -> List a empty -> List a empty

We can see they have no power to change or specify empty type param in any way. End will leave it unspecified, while Cons will preserve it from the input list. Also, we have no way to change these type signatures as they are automatically derived from List type definition.

This is exactly where GADTs come in. GADTs (Generalized Algebraic Data Types) is a Haskell extension that lets us explicitly define the type signatures of data constructors.

Before seeing GADTs in action, let’s first remind ourselves of the standard, non-GADT definition of List we used above:

data List a empty = End | Cons a (List a empty)

Now let’s rearrange it a bit and add types of data constructors in comments so we can more easily reason about them:

data List a empty =
    End |                   -- End :: List a empty
    Cons a (List a empty)   -- Cons :: a -> List a empty -> List a empty

As we mentioned, the types in the comments are automatically derived and we cannot control them. But that is exactly what we want to do, and GADTs let us achieve that using the following syntax:

{-# LANGUAGE GADTs #-}

data List a empty where
    End :: List a Empty
    Cons :: a -> List a empty -> List a NonEmpty

We can see it is very similar to our “rearranged” List definition above! What GADTs let us do is write by ourselves types of data constructors (which were in the previous definition in the comments), giving us control to specify them as we wish!

The difference in the syntax is that we have to add where after the type name and then for each data constructor we specify its type signature.

Now we finally have the power to control empty type parameter (in List a empty)! We specified that End will mark list as Empty, while Cons will mark it as NonEmpty. And this is exactly what we wanted to do, because if we used End we know the list is empty, while if we used Cons we know there is at least one element in it, which makes it non-empty.

Let’s see it in action! Using it stays the same as without GADTs, just that this time there will be empty type param which assumes an appropriate type:

> :t End
End :: List a Empty

> :t (Cons 5 End)
Cons 5 End :: Num a => List a NonEmpty

Wohoo, this works now! We see we can construct values of this type and we will always know whether it is empty or not. safeHead function we defined above will work on these without any problems.

Can we just use smart constructors instead of GADTs?

One possible “downside” of GADTs is that it is a language extension we have to enable, thus making our codebase a bit heavier (longer compilation time?) and less “standard”.

Sometimes we can avoid using GADTs with smart constructors. Let’s see what that is and how it would work in this case.

Smart constructor is simply a function that is used to create a certain value instead of using its data constructor directly. We typically do that (hide data constructors and expose smart constructor functions) when we want to have extra control over the value creation. E.g. we want to make some extra checks, or make sure an invalid value isn’t provided etc.

For example, we could provide a following smart constructor to create an empty list:

data Empty
data NonEmpty

data List a empty = End | Cons a (List a empty)

createEmptyList :: List a Empty
createEmptyList = End

And this works! By defining the type signature of createEmptyList we made sure that empty will always assume the type of Empty when this function is called. Since End has a type signature End :: List a empty, we just “casted” type param empty here into a specific type.

Let’s try to do the same for the other data constructor, adding an element to the list:

data Empty
data NonEmpty

data List a empty = End | Cons a (List a empty)

addElemToList :: a -> List a empty -> List a NonEmpty
addElemToList elem list = Cons elem list

What we are trying to achieve here is make sure that whenever an element is added to the list, empty becomes NonEmpty, and we again use type signature for that, to provide that extra information. But if we try to compile this, we get the following error: Couldn't match type ‘empty’ with ‘NonEmpty’.

To understand the problem, let’s remind ourselves of Cons’s type:

Cons :: a -> List a empty -> List a empty.

The problem is in that Cons requires empty to stay the same, so whatever type it is in the input list, it must stay the same in the newly constructed list. Although we specified we want to change it to NonEmpty in the addElemToList’s type signature, Cons is not flexible enough to do that and this is why we got an error during compilation.

Although smart constructors might be a solution in some simpler cases (e.g. when we have “flat” data and we are merely “casting” general type params into the specific ones, such as we did with End), in this case where we have a recursive data structure it wasn’t enough because the initial data constructor was too rigid.

What is List Int Double?

Well, List Int Double means nothing, it doesn’t make sense. We can only construct and know how to work with lists whose empty type parameter is either Empty or NonEmpty.

But the problem is although it doesn’t make sense, we can still write things like this and it will happily compile:

someListFn :: List a Bool -> Int
someListFn list = 23

There is no way to execute this function since there is no way to construct such a list where empty type param is Bool, but strange stuff can appear in our codebase and we cannot detect it in compile time.

Here is a more “real world” example when this could be a problem: let’s say you are using Empty and NonEmpty types for list as we explained above, but you are also using Yes and No types for something else in your codebase. And then your colleague starts implementing some new functionality for your lists, and by mistake he starts using Yes and No in the place of empty. And there is nothing to stop him until he actually tries to connect everything together and run the code!

The problem we see is there is no “safety” at the type level, we cannot say “empty can be only this kind of type”. But, there is a mechanism that can help us.

Not all types are used in the same way

Just a short observation before we continue. I wanted to put attention to the fact that we are now differentiating between two possible uses of a type:

• type is used to produce values (store data) - e.g. Int, Maybe Bool, …
• type is used only at the type level as a designation of something, never producing an actual value - e.g. Empty and NonEmpty

Despite these very different uses, we currently don’t have a way to differentiate between such types - we declare them both in the same way and Haskell can’t tell how are we going to use them later.

Data kinds

In standard Haskell each type has a kind, which can be thought of as a “type of a type”. E.g.:

> :k Int
Int :: *                // Has values (e.g. 1, 2, 3, ...).

> :k Maybe
Maybe :: * -> *         // When given a value-producing type, has values.

> :k Either
Either :: * -> * -> *   // When given 2 value-producing types, has values.

And that is it, all kinds are expressed with *s and automatically derived for us. * means a type that has values.

But as we saw earlier, this is not enough for us. We also want to cover that other use case so we can say “here goes only type(s) that tell us whether a list is empty or not.”

And this is exactly what DataKinds extension allows us to do, it lets us define other kinds besides *:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data ListStatus = Empty | NonEmpty

data List a empty where
    End :: List a 'Empty 
    Cons :: a -> List a empty -> List a 'NonEmpty

Now let’s see what happened here. We made a new type ListStatus and then we use its data constructors (prefixed with ') in the place of types in GADT for List. Wut?

The thing with DataKinds is the following: for every type we create it additionaly creates for us new types, named after data constructors we used and prefixed with '. It also creates a new kind, which is named after the type’s name. Specifically for this case:

• DataKinds created for us two extra types, 'Empty and 'NonEmpty
• Kinds of these new types are ListStatus
• These types cannot have values, they can be used only at the type level

I was really confused the first time I realized this. This extension just like that creates extra types for us, without even asking us about it, for every type we create!

Since we are using only types of ListStatus kind in List’s data constructors’ signatures, Haskell inferred from that that empty type param must be of kind ListStatus and won’t let us use anythng else. If we try to create a function which takes List a Bool, we will receive the following error:

Expected kind ‘ListStatus’, but ‘Bool’ has kind ‘*’

Which is exactly what we wanted! With this we achieved kind safety, besides the usual type safety in the compile time.

To make things even more explicit, we can turn on KindSignatures extension which lets us explicitly define kinds of type parameters in a type:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data ListStatus = Empty | NonEmpty

data List (a :: * ) (empty :: ListStatus) where
    End :: List a 'Empty 
    Cons :: a -> List a empty -> List a 'NonEmpty

Now everybody can see that a is a “standard” type that has values, while empty can be only 'Empty or 'NonEmpty. We didn’t have to write this explicit version as Haskell can infer it on its own, but it is a matter of style and documentation. We can also omit ' in front of types and Haskell in a lot of cases can infer by itself if it is a type or data constructor. I found it easier to have everything explicit for now, a lot is going on behind the scenes so this made it clearer for me.

And that is it for this first part! We learned about type-level programming, how to use GADTs and data kinds and saw everything together in action. Hope you found it useful, please let me know in the comments if you have any questions, I said something wrong or I can explain something better.

In Part 2 we will go even deeper and take a look at some more cool examples that build on top of this one! Here’s a teaser question: with our List a empty that we developed above, how would you implement safeTail function which works only on non-empty lists, analogous to what we have done with safeHead? Can you do it, what is its return type?