I asked an AI what a monadic law looked like, here's what it answered.

How to Monad

Where we learn that Monads, like Functors, should abide the Laws.

Michel Belleville
Published in
5 min readApr 4, 2024

--

me> So, Functors have laws, and those are not even scary. How about the dreaded Monads?

wat> They have laws too. One more than Functors, and a bit more complicated, but nothing too scary either as you’ll see.

me> Well, what are these laws about?

wat> Just like with Functors, they’re about how you can compose with a Monad. But first, a bit of vocabulary:

-- A good little Monad is like a context around a value (or values)
-- that we can `andThen` on, so we can take what's inside the
-- context and use it to produce a new context.

-- So, first, we need that `andThen` function:
M.andThen : (a -> M b) -> M a -> M b

-- The magic of `andThen` for a Monad is that it knows how to handle
-- "re-packaging" in the context of its Monad.

-- Now we'll also need an operation that takes a value and put it in
-- the "most minimal and useful" context of the monad.
-- Let's call it `wrap`:
M.wrap : a -> M a

-- While you will find `andThen` functions for most Elm types that
-- behave as Monads (sometimes named differently, like `concatMap`
-- for the `List` type), you won't find a `wrap` function in most of
-- those packages because it's not that very useful to have in Elm,
-- except as a tool to enforce laws, but here's how it'd look
-- like for a few Monads you may know:
Maybe.wrap a = Just a
Result.warp a = Ok a
List.wrap a = [a]
Json.Decode.wrap a = Json.Decode.succeed a

-- As you can see, `wrap` is all about "wapping" a value in the
-- "simplest" ([a] vs [a, a]), most "useful" ((Just a) vs Nothing)
-- context we have with that monad.

-- You will find in `Haskell`-adjacent literature `andThen` is known
-- as `>>=` (pronounced "bind" for some reason) and `wrap` is named
-- `return`, but your favorite ducky finds those names rather
-- confusing. Sorry Hasky, we love you but you're not that...
-- approachable.

me> So far, so not difficult. We have a function that can take a Monad’s content to produce new content and context, and we have a function that wraps any value in the “simplest most useful” context this Monad provides. Now what do we do about them?

wat> We check the laws! Of which there are three this time:

-- Left identity
wrap a |> andThen f == f a

-- Right identity
m |> andThen wrap == m

-- Associativity
m |> andThen (f andThen g) == m |> andThen f |> andThen g

me> Ok… so, let’s start with the identities?

wat> Yes… and let’s use a simple example with the Maybe type:

-- Left identity

-- let's start by defining a function, any monadic function that'll work
-- with our monads will do, but we'll make it extra spicy by having one
-- that may return Nothing and not always return a Just value
divide7By x =
if x /= 0 then
Just (7 / x)
else
Nothing

-- now le'ts check if our left identify law holds with this function

Maybe.wrap 1 -- == Just 1
|> Maybe.andThen divide7By -- == Just 7/1 => Just 7
== divide7By 1. -- == Just 7

-- so far, so good, we can divide 7 by 1 consistantly

Maybe.wrap 7 -- == Just 7
|> Maybe.andThen divide7By -- == Just 7/7 => Just 1
== divide7By 7 -- == Just 1

-- yup, still holding when dividing by 7

Nothing -- == Nothing
|> Maybe.andThen divide7By -- == Nothing
== Nothing -- == Nothing

-- still holding starting with Nothing

Maybe.wrap 0 -- == Just 0
|> Maybe.andThen divide7By -- == Nothing
== divide7By 0 -- == Nothing

-- and now it's even holding when dividing by 0!

me> So, your Left identity seems to hold… what about right identity?

-- let's try and wrap what's in a Nothing, just for funsies

Nothing |> Maybe.andThen Maybe.wrap -- == Nothing
== Nothing

-- it wraps ; now let's get on with wrapping something in a Just

Just 10 |> Maybe.andThen Maybe.wrap -- == Just 10
== Just 10

-- it also wraps

wat> It’s a wrap! And now, the piece de resistance, associativity:

-- ladies and gentlemen, tonight for your entertainment our two amazing
-- monadic functions f, and g

-- f is a function that will decrement a number if and only if it is more
-- than 0
f x =
if x > 0 then
Just x - 1
else
Nothing

-- g is a function that will multiply a number if and only if it is more
-- than 0
g x =
if x > 0 then
Just x * 3
else
Nothing

-- now please observe that there is no trickery but a simple monadic
-- side-effect, as our functions, for our type-safety, will wrap their
-- results in a Maybe instance

-- now observe how they elegantly associate for your pleasure
-- first with a number that chains with both
Just 10
|> andThen (f >> andThen g) -- Just 27
==
Just 10
|> andThen f -- Just 9
|> andThen g -- Just 27

-- then with a number our first function f disagrees with
Just 0
|> andThen (f >> andThen g) -- Nothing (f 0 == Nothing)
==
Just 0
|> andThen f -- Nothing
|> andThen g -- Nothing

-- then with a number our function g disagrees with
Just 1
|> andThen (f >> andThen g) -- Nothing (g 0 == nothing)
==
Just 1
|> andThen f -- Just 0
|> andThen g -- Nothing

-- even a nothing cannot break the law
Nothing
|> andThen (f >> andThen g) -- Nothing
==
Nothing
|> andThen f -- Nothing
|> andThen g -- Nothing

-- you can even reverse the order of those functions and check that the
-- law still holds
Just 10
|> andThen (g >> andThen f) -- Just 29
==
Just 10
|> andThen g -- Just 30
|> andThen f -- Just 29

-- ladies and gentlemen, that was f and g in their amazing demonstration of
-- the associativity laws!

me> Well… looks like we’ve got a nice little monad there!

wat> Sure does. Though to pass mustard, the Monadic law would have to hold for any monadic function and any value passed that work with those fuctions…

me> Yes, that’s what a math surgeon would say I guess.

wat> They sure like to demonstrate things work for all cases (or disprove that they do). But for us living in the “real world” of computers, we have a potent way to try and make sure things work and keep on working: automated tests.

me> Hmm… let me guess, that’s what the next episode is going to be about…

wat> Could be, could be… stay tuned 😉

--

--