Type Theory Part IV: Monads

The new year marks a new style of blog posts. Super serious principle engineers can’t be bothered with words and therefore neither can I.

Functional Programming Basics After Dependent Type Theory?

This article is a bit of a step backwards, but covers important foundational FP content and sets the blog up to do an advanced trans-domain monads post later.

What is Functional Programming

Functional Programming is a programming paradigm- it is an abstract set of principles for writing code, and if you can make an argument that your code abides by those principles, it is functional code. Some programming languages mandate that these principles are followed. These languages are known as functional programming languages.

Languages that are considered functional are:

• Haskell
• Lean
• Idris

Languages that are not strictly functional but have language features that enable functional code to be written are:

• Python
• C#
• Scala

Principles of FP

• Immutable Data: Once a variable is assigned a value, that value cannot change and new data cannot be assigned to the existing variable.
• Functions Are First Class: Functions can be created and passed around as objects. Functions can take functions as arguments and return functions.
• Functions are Pure: Functions do not have side effects, in other words they do not mutate global state. Functions return results of computations instead. As a result, calling the same function twice will always return the same thing.
• Declarative: Code focuses on the result state (an intention) rather than how to achieve it (imperative statements).

The Problem

In functional programming, functions are pure and don’t have side effects.

Effects, like writing to a file or printing to a console are modelled using return types like IO.

Since we are constantly modelling effects with types, we are constantly wrapping results in containers.

We need a framework that enables entering data into the ecosystem and chaining actions on wrapped data.

The Solution: Monads

A monad is a kind of type. It is any type that implements the monadic interface. This interface requires the following:

• A type constructor T of kind * -> * representing an embedding of a type into a context.
• A way to enter an instance of a into the ecosystem and get back T[a]. This action is called return.
• A way to take 1) data in context (an instance of T[a]), 2) a function that sends maps data and embeds it in context (an instance of a -> T[b]) and get back data in context after the mapping. This action is called the monadic bind, or (>>=).

Since all effectful/contextful computations are modelled using types, every kind of computation has a corresponding monad.

A Single Monad in C#

This is the trivial monad.

Let T: * -> * be Box<T>

Let Return: a -> T[a] be Return

Let Bind: T[a] -> (a -> T[b]) -> T[b] be Bind

public class Box<T> {
    public T value { get; }

    public Box(T value) {
        this.value = value;
    }
}

public static class BoxMonad {
    public static Box<T> Return(T value) {
        return new Box<T>(value);
    }

    public static Box<U> Bind<T, U>(Box<T> a, Func<T, Box<U>> f) {
        return f(a.value);
    }
}

Box is a level 0 monad. It does the job. But it has a few shortcomings. Firstly, C# does not have the language features required to define the actual monad contract. So aside from the name we have no way to know that this type really is a monad.

If we were to implement the list monad, which represents nondeterministic computations, it would look like this:

public class ListWrapper<T> {
    public List<T> value { get; }

    public ListWrapper() {
        this.value = new List<T>();
    }

    public ListWrapper(T value) {
        this.value = new List<T>() { value };
    }
}

public static class ListWrapperMonad {
    public static ListWrapper<T> Return(T value) {
        return new ListWrapper<T>(value);
    }

    public static ListWrapper<U> Bind<T, U>(ListWrapper<T> a, Func<T, ListWrapper<U>> f) {
        var result = new ListWrapper<U>();
        foreach (var x in a.value)
        {
            result.value.AddRange(f(x).value);
        }
        return result;
    }
}

If we were to implement the maybe monad, which represents computations that may fail, it would look like this:

public class Maybe<T> {
    public T? value { get; }

    public Maybe() {
        this.value = null;
    }

    public Maybe(T value) {
        this.value = value;
    }
}

public static class MaybeMonad {
    public static Maybe<T> Return(T value) {
        if (value is null) {
            return new Maybe<T>();
        }
        return new Maybe<T>(value);
    }

    public static Maybe<U> Bind<T, U>(Maybe<T> a, Func<T, Maybe<U>> f) {
        if (a is null) {
            return new Maybe<U>();
        }
        return new Maybe<U>(f(a.value));
    }
}

There is a clearly a pattern that we can form a contract from:

1. TypeConstructor<T>
2. TypeConstructor<T> Return(T value)
3. TypeConstructor<U> Bind<T, U>(TypeConstructor<T> a, Func<T, TypeConstructor<U>> f)

But if we were to define a common interface for monads, it would have to look like

public interface Monad<TypeConstructor<T>> {}

which C# does not allow. So despite all the monads kind of being similar, from a programmatic perspective there is no way to verify this similarity/common contract at compile time.

What we are asking for in the above snippet is a generic, but constrained so that the generic type is itself a type constructor. Unlike basic parametric polymorphism which seeks to abstract over types T, we want to abstract over entire type constructors T: * -> *, such as Maybe, Box and ListWrapper. This would give our monad interface itself the kind (* -> *) -> * as it takes a type constructor and produces a type.

Such a language feature does exist, but not in C#. Types that abstract over type constructors are known as ‘higher kinded types’ and they exist in Scala and Haskell.

Monad Typeclass in Haskell

Here is what the monad contract (typeclass) looks like in Haskell:

class Monad m where
    (>>=)  :: m a -> (a -> m b) -> m b  -- bind
    return :: a -> m a

m must be a type constructor, what we previously referred to as T. return is our Return and >>= is our Bind. We don’t name the concrete type underneath the type constructor as it isn’t used.

Note that this definition is not entirely consistent with modern Haskell. Historically, m has needed to be a Functor and following the AMP, m has needed to be an Applicative as well. But the implications of fulfilling the Functor/Applicative contracts are unused in the monad pattern and therefore not worth mentioning.

In Haskell we may define a type (in this case the list datatype) the following way:

data [a] = [] | a : [a]

and then a monad for the type as follows:

instance Monad [] where
    return x = [x]
    xs >>= f  = concat (map f xs)

Chaining computations on lists goes from messy nested concatMaps…

pairsSum :: [Int]
pairsSum =
  concatMap (\x ->
    concatMap (\y ->
      [x + y]
    ) [10,20]
  ) [1,2]

To clean automatic mapping and flattening.

pairsSum :: [Int]
pairsSum =
  [1,2] >>= \x ->
  [10,20] >>= \y ->
  return (x + y)

In fact, haskell provides the ‘do’ keyword and <- variable binding operator to simplify the lambdas.

pairsSum :: [Int]
pairsSum = do
  x <- [1,2]
  y <- [10,20]
  return (x + y)

In Haskell, x <- m inside a do block is just syntax for m >>= (\x -> ...), meaning the m (the type constructor wrapped around the data) is passed to the bind (>>=), which applies the function \x -> ... to the value inside m (in this case the non deterministic value 1/2 or 10/20); the do block is simply a chain of these binds.

In the case of Maybe, here is the before, with nested case statements…

compute :: Double -> Double -> Maybe Double
compute x y =
  case safeDivide x y of
    Nothing -> Nothing
    Just result1 ->
      case half result1 of
        Nothing -> Nothing
        Just result2 -> Just result2

and here is the after.

compute :: Double -> Double -> Maybe Double
compute x y = do
  result1 <- safeDivide x y
  result2 <- half result1
  return result2

In a language where wrapping is ubiquitous, the opportunity for this kind of prettification is everywhere and the benefit is great. So hopefully it is now clear why monads are necessary.

This is one step better than the C# monads, because the contract Monad enables code reuse and provides us a strict syntactic method of determining what is and is not a monad. However, ordinary FP programmers still have to manually remind themselves, when writing monads, that their monads adhere to the monad laws.

1. Left identity: return a >>= f = f a
2. Right identity: xs >>= return = xs
3. Associativity: (xs >>= f) >>= g = xs >>= (\x -> f x >>= g)

These laws mandate that entering data into the monadic ecosystem doesn’t change it and that it doesn’t matter how the binds are grouped. It is important for monads to adhere to these laws so that developers get the benefits of monads when using any monad.

Monad Record in Idris

Programmers proficient in dependent typing make no such assumptions that the rules are obeyed. All claims, especially those about equality, must be backed up by proofs. That is why the true monad looks like this:

record Monad (T : Type -> Type) : Type where
    field
        return : \forall {A} -> A -> T A
        _>>=_ : \forall {A B} -> T A -> (A -> T B) -> T B
        lunit : \forall {A B} {a : A} {f : A -> T B} -> (return a >>= f) == f a
        runit : \forall {A} {c : T A} -> (c >>= return) == c
        assoc : \forall {A B C} {c : T A} {f : A -> T B} {g : B -> T C} -> ((c >>= f) >>= g) == c >>= (\lambda x -> f x >>= g)

The implementation of such a monad is left as an exercise for the reader.