People reach for burritos and boxes to explain monads. I want to reach for something that actually lives on this coastline: rendezvous and docking.

Two spacecraft can each be in a perfectly good orbit and still be unable to simply touch. You can’t naively concatenate their trajectories. There’s an interface — a docking port with a specific geometry — and a procedure for bringing two things into contact so that afterward they behave as one. That awkward in-between step is the whole subject.

Composition wants to be trivial, and usually isn’t

Plain functions compose for free:

g ∘ f  :  A → B → C

Give me f : A → B and g : B → C and I hand you A → C, no ceremony. This is the base category, and it’s boring precisely because docking is trivial: the output type is the input type.

Effects break that. Consider functions that might fail:

parse   :: String -> Maybe Int
sqrtPos :: Int    -> Maybe Double

You cannot write sqrtPos ∘ parse. The port geometry is wrong: parse emits a Maybe Int, but sqrtPos expects a bare Int. The values are in orbit; they just can’t dock.

The docking procedure

A monad is exactly the equipment that makes the docking work. Two operations:

• return (or pure) — put a plain value into orbit: a -> m a.
• >>= (“bind”) — the docking maneuver: m a -> (a -> m b) -> m b.

bind is the interesting one. It reaches inside the first craft, pulls the value out if the geometry allows, and feeds it to the next stage:

parse "16" >>= sqrtPos    -- Just 4.0
parse "xy" >>= sqrtPos    -- Nothing, short-circuits

When parse returns Nothing, docking is aborted and the second stage never fires — exactly like a rendezvous that’s waved off. The Maybe monad encodes “abort cleanly on failure” as structure, not as scattered if checks.

Why the laws are the safety review

A monad isn’t just those two functions; it’s those two functions obeying laws:

1. Left identity — return a >>= f is just f a. Docking with a craft you only just launched changes nothing.
2. Right identity — m >>= return is just m. Docking with an empty craft changes nothing.
3. Associativity — it doesn’t matter how you parenthesize a chain of docks.

Those laws are the reason you can reason about a long pipeline the way you reason about a rocket that’s rated: the sequence of maneuvers has no surprising order-of-operations gotchas. Break a law and you’ve built something that looks like a monad and betrays you under composition — the software equivalent of a docking port that mostly seals.

The payoff of category theory isn’t the vocabulary. It’s that once you see “composition with an interface” as one idea, Maybe, async I/O, parsers, and state all turn out to be the same shape wearing different hulls.

That’s the whole trick. Find the docking port, verify the laws, and stop writing the glue by hand.

← All entries Reply by email →