Monad laws by Mark Seemann

An article for object-oriented programmers.

This article is an instalment in an article series about monads.

Just as functors must obey the functor laws, monads must follow the monad laws. When looked at from the right angle, these are intuitive and reasonable rules: identity and associativity.

That sounds almost like a monoid, but the rules are more relaxed. For monoids, we require a binary operation. That's not the case for functors and monads. Instead of binary operations, for monads we're going to use Kleisli composition.

This article draws heavily on the Haskell wiki on monad laws.

In short, the monad laws comprise three rules:

• Left identity
• Right identity
• Associativity

The article describes each in turn, starting with left identity.

Left identity #

A left identity is an element that, when applied to the left of an operator, doesn't change the other element. When used with the fish operator it looks like this:

id >=> h ≡ h

For monads, id turns out to be return, so more specifically:

return >=> h ≡ h

In C# we can illustrate the law as a parametrised test:

[Theory]
[InlineData(-1)]
[InlineData(42)]
[InlineData(87)]
public void LeftIdentityKleisli(int a)
{
    Func<int, Monad<int>> @return = Monad.Return;
    Func<int, Monad<string>> h = i => Monad.Return(i.ToString());
 
    Func<int, Monad<string>> composed = @return.Compose(h);
 
    Assert.Equal(composed(a), h(a));
}

Recall that we can implement the fish operators as Compose overloads. The above test demonstrates the notion that @return composed with h should be indistinguishable from h. Such a test should pass.

Keep in mind, however, that Kleisli composition is derived from the definition of a monad. The direct definition of monads is that they come with a return and bind functions (or, alternatively return and join). If we inline the implementation of Compose, the test instead looks like this:

[Theory]
[InlineData(-1)]
[InlineData(42)]
[InlineData(87)]
public void LeftIdentityInlined(int a)
{
    Func<int, Monad<int>> @return = Monad.Return;
    Func<int, Monad<string>> h = i => Monad.Return(i.ToString());
 
    Func<int, Monad<string>> composed = x => @return(x).SelectMany(h);
 
    Assert.Equal(composed(a), h(a));
}

or, more succinctly:

Assert.Equal(@return(a).SelectMany(h), h(a));

This is also the way the left identity law is usually presented in Haskell:

return a >>= h = h a

In Haskell, monadic bind is represented by the >>= operator, while in C# it's the SelectMany method. Thus, the Haskell and the C# representations are equivalent.

Right identity #

Right identity starts out similar to left identity. Using the fish operator, the Haskell wiki describes it as:

f >=> return ≡ f

Translated to a C# test, an example of that law might look like this:

[Theory]
[InlineData("foo")]
[InlineData("ploeh")]
[InlineData("lawful")]
public void RightIdentityKleisli(string a)
{
    Func<string, Monad<int>> f = s => Monad.Return(s.Length);
    Func<int, Monad<int>> @return = Monad.Return;
 
    Func<string, Monad<int>> composed = f.Compose(@return);
 
    Assert.Equal(composed(a), f(a));
}

Again, if we inline Compose, the test instead looks like this:

[Theory]
[InlineData("foo")]
[InlineData("ploeh")]
[InlineData("lawful")]
public void RightIdentityInlined(string a)
{
    Func<string, Monad<int>> f = s => Monad.Return(s.Length);
    Func<int, Monad<int>> @return = Monad.Return;
 
    Func<string, Monad<int>> composed = x => f(x).SelectMany(@return);
 
    Assert.Equal(composed(a), f(a));
}

Now explicitly call the f function and assign it to a variable m:

[Theory]
[InlineData("foo")]
[InlineData("ploeh")]
[InlineData("lawful")]
public void RightIdentityInlinedIntoAssertion(string a)
{
    Func<string, Monad<int>> f = s => Monad.Return(s.Length);
    Func<int, Monad<int>> @return = Monad.Return;
 
    Monad<int> m = f(a);
 
    Assert.Equal(m.SelectMany(@return), m);
}

The assertion is now the C# version of the normal Haskell definition of the right identity law:

m >>= return = m

In other words, return is the identity element for monadic composition. It doesn't really 'do' anything in itself.

Associativity #

The third monad law is the associativity law. Keep in mind that an operator like + is associative if it's true that

(x + y) + z = x + (y + z)

Instead of +, the operator in question is the fish operator, and since values are functions, we typically call them f, g, and h rather than x, y, and z:

(f >=> g) >=> h ≡ f >=> (g >=> h)

Translated to a C# test as an example, the law looks like this:

[Theory]
[InlineData(0)]
[InlineData(1)]
[InlineData(2)]
public void AssociativityKleisli(double a)
{
    Func<double, Monad<bool>> f = i => Monad.Return(i % 2 == 0);
    Func<bool, Monad<string>> g = b => Monad.Return(b.ToString());
    Func<string, Monad<int>> h = s => Monad.Return(s.Length);
 
    Func<double, Monad<int>> left = (f.Compose(g)).Compose(h);
    Func<double, Monad<int>> right = f.Compose(g.Compose(h));
 
    Assert.Equal(left(a), right(a));
}

The outer brackets around (f.Compose(g)) are actually redundant; we should remove them. Also, inline Compose:

[Theory]
[InlineData(0)]
[InlineData(1)]
[InlineData(2)]
public void AssociativityInlined(double a)
{
    Func<double, Monad<bool>> f = i => Monad.Return(i % 2 == 0);
    Func<bool, Monad<string>> g = b => Monad.Return(b.ToString());
    Func<string, Monad<int>> h = s => Monad.Return(s.Length);
 
    Func<double, Monad<string>> fg = x => f(x).SelectMany(g);
    Func<double, Monad<int>> left = x => fg(x).SelectMany(h);
 
    Func<bool, Monad<int>> gh = x => g(x).SelectMany(h);
    Func<double, Monad<int>> right = x => f(x).SelectMany(gh);
 
    Assert.Equal(left(a), right(a));
}

If there's a way in C# to inline the local compositions fg and gh directly into left and right, respectively, I don't know how. In any case, the above is just an intermediate step.

For both left and right, notice that the first step involves invoking f with x. If, instead, we call that value m, we can rewrite the test like this:

[Theory]
[InlineData(0)]
[InlineData(1)]
[InlineData(2)]
public void AssociativityInlinedIntoAssertion(double a)
{
    Func<double, Monad<bool>> f = i => Monad.Return(i % 2 == 0);
    Func<bool, Monad<string>> g = b => Monad.Return(b.ToString());
    Func<string, Monad<int>> h = s => Monad.Return(s.Length);
 
    Monad<bool> m = f(a);
 
    Assert.Equal(m.SelectMany(g).SelectMany(h), m.SelectMany(x => g(x).SelectMany(h)));
}

The above assertion corresponds to the way the associativity law is usually represented in Haskell:

(m >>= g) >>= h = m >>= (\x -> g x >>= h)

Once more, keep in mind that >>= in Haskell corresponds to SelectMany in C#.

Conclusion #

A proper monad must satisfy the three monad laws: left identity, right identity, and associativity. Together, left identity and right identity are know as simply identity. What's so special about identity and associativity?

As Bartosz Milewski explains, a category must satisfy associativity and identity. When it comes to monads, the category in question is the Kleisli category. Or, as the Haskell wiki puts it:

Monad axioms:
Kleisli composition forms
a category.

Subsequent articles in this article series will now proceed to give examples of concrete monads, and what the laws look like for each of these.

Next: The List monad.

Comments

public static Func<T, Monad<T2>> Compose<T, T1, T2>(
    Func<T, Monad<T1>> action1,
    Func<T1, Monad<T2>> action2)

public static Func<object, Monad<object>> Compose(
    Func<object, Monad<object>> action1,
    Func<object, Monad<object>> action2)

• ← Previous
• Archive
• Next →