Effects

“A monad is just a monoid in the category of endofunctors, what’s the problem?” This infamous quip became the ur-meme of functional programming, spawning a thousand blog posts explaining monads via burritos, boxes, and space suits. The tragedy is that the concept is not hard. It just got wrapped in mystique before anyone explained it clearly.

Here is what matters: programs have effects. They might fail, consult state, perform IO, branch nondeterministically, or launch the missiles. In languages without effect tracking, any function call might do any of these things. You call getUsername() and hope it only reads from a database rather than initiating thermonuclear war. The type signature offers no guarantees. The question is how to represent effects in a way that lets us reason about composition and know, from the types alone, what a function might do. Monads are one answer. They capture a pattern for sequencing operations where each step produces both a result and some context. Bind chains these operations, threading the context automatically. Do notation makes the sequencing readable. The interface is minimal; the applications are broad.

But monads are not the only answer, and treating them as sacred obscures the deeper point. Algebraic effect systems, linear types, graded monads, and effect handlers all attack the same problem from different angles. What they share is the conviction that effects should be visible in types and that composition should be governed by laws. The specific mechanism matters less than the principle: make the structure explicit so that humans and machines can reason about it.

Lean uses monads because they work well and the ecosystem inherited them from functional programming research of the 1990s. They are a good tool. But the goal is not to be monadic; the goal is to capture effects algebraically, whatever form that takes. When you understand monads, you understand one particularly elegant solution to sequencing effectful computations. You also understand a template for how programming abstractions should work: a minimal interface, a set of laws, and the discipline to respect both.

The Option Monad

The simplest monad handles computations that might fail. You already understand this pattern: look something up, and if it exists, do something with it; if not, propagate the absence. Every programmer has written this code a hundred times. The monad just gives it a name and a uniform interface.

def safeDivide (x y : Nat) : Option Nat :=
  if y == 0 then none else some (x / y)

def safeHead {α : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | x :: _ => some x

#eval safeDivide 10 2   -- some 5
#eval safeDivide 10 0   -- none
#eval safeHead [1, 2]   -- some 1
#eval safeHead ([] : List Nat)  -- none

Chaining Without Monads

Without the abstraction, chaining fallible operations produces the pyramid of doom: nested conditionals, each handling failure explicitly, the actual logic buried under boilerplate. This is not hypothetical. This is what error handling looks like in languages without monadic structure. It is also what early JavaScript looked like before Promises, which are, of course, monads by another name.

def computation (xs : List Nat) : Option Nat :=
  match safeHead xs with
  | none => none
  | some x =>
    match safeDivide 100 x with
    | none => none
    | some y => some (y + 1)

#eval computation [5, 2, 3]   -- some 21
#eval computation [0, 2, 3]   -- none (division by zero)
#eval computation []          -- none (empty list)

The bind Operation

The bind operation (written >>=) is the heart of the monad. It takes a value in context and a function that produces a new value in context, and chains them together. For Option, this means: if the first computation succeeded, apply the function; if it failed, propagate the failure. The pattern generalizes far beyond failure, but failure is the clearest example.

def computation' (xs : List Nat) : Option Nat :=
  safeHead xs |>.bind fun x =>
  safeDivide 100 x |>.bind fun y =>
  some (y + 1)

#eval computation' [5, 2, 3]  -- some 21
#eval computation' [0, 2, 3]  -- none
#eval computation' []         -- none

Do Notation

Do notation is syntactic sugar that makes monadic code look imperative. The left arrow ← desugars to bind; the semicolon sequences operations. This is not a concession to programmers who cannot handle functional style. It is recognition that sequential composition is how humans think about processes, and fighting that serves no purpose. The abstraction remains; only the syntax yields to ergonomics.

def computationDo (xs : List Nat) : Option Nat := do
  let x ← safeHead xs
  let y ← safeDivide 100 x
  return y + 1

#eval computationDo [5, 2, 3]  -- some 21
#eval computationDo [0, 2, 3]  -- none
#eval computationDo []         -- none

def validateInput (name : String) (age : Nat) : Option (String × Nat) := do
  if name.isEmpty then none
  if age == 0 then none
  return (name, age)

#eval validateInput "Alice" 30  -- some ("Alice", 30)
#eval validateInput "" 30       -- none
#eval validateInput "Bob" 0     -- none

Do Notation Desugaring

Do notation is syntactic sugar for bind chains. The compiler transforms your imperative-looking code into applications of >>= and pure. Understanding the desugaring helps when types do not match or when you want to optimize.

A monadic bind extracts the value and passes it to the continuation:

do                              e1 >>= fun x =>
  let x ← e1        ⟹           do es
  es

A pure let binding has no monadic involvement:

do                              let x := e
  let x := e        ⟹           do es
  es

An action without binding discards the result:

do                              e1 >>= fun () =>
  e1                ⟹           do es
  es

Pattern matching with a fallback handles failure:

do                              e1 >>= fun
  let some x ← e1   ⟹             | some x => do es
    | fallback                    | _ => fallback
  es

The return keyword is just pure:

return e            ⟹           pure e

The ← operator can appear as a prefix within expressions. Each occurrence is hoisted to a fresh binding, processed left-to-right, inside-to-outside:

do                              do
  f (← e1) (← e2)   ⟹             let x ← e1
  es                              let y ← e2
                                  f x y
                                  es

Effects like early return, mutable state, and loops with break/continue transform the entire do block rather than desugaring locally, similar to monad transformers.

Note

Semicolons can replace newlines in do blocks: do let x ← e1; let y ← e2; pure (x + y). This is rarely used since multiline format is “more readable.” Fifty years of programming language research and we still cannot agree on what makes syntax objectively good. Perhaps because syntax is more fashion and culture than science.

def withBind (xs : List Nat) : Option Nat :=
  safeHead xs >>= fun x =>
  safeDivide 100 x >>= fun y =>
  pure (y + 1)

def withDoNotation (xs : List Nat) : Option Nat := do
  let x ← safeHead xs
  let y ← safeDivide 100 x
  return y + 1

#eval withBind [5]        -- some 21
#eval withDoNotation [5]  -- some 21

def mixedBindings : Option Nat := do
  let x ← some 10      -- monadic bind
  let y := x + 5       -- pure let
  let z ← some (y * 2) -- monadic bind
  return z

#eval mixedBindings  -- some 30

Mutable Variables in Do

The let mut syntax introduces mutable bindings that desugar to StateT. Assignment with := modifies the state. The compiler threads the state automatically, transforming imperative-looking code into pure functional operations.

def imperativeSum (xs : List Nat) : Nat := Id.run do
  let mut total := 0
  for x in xs do
    total := total + x
  return total

def functionalSum (xs : List Nat) : Nat :=
  xs.foldl (· + ·) 0

#eval imperativeSum [1, 2, 3, 4, 5]  -- 15
#eval functionalSum [1, 2, 3, 4, 5]  -- 15

def countValid (xs : List Nat) : IO Nat := do
  let mut count := 0
  for x in xs do
    if x > 0 then
      count := count + 1
      IO.println s!"Valid: {x}"
  return count

The Id.run do pattern runs a do block that uses only local mutable state. The Id monad adds no effects; it just provides the scaffolding for the state transformation. For IO operations, you work directly in the IO monad and the mutations interleave with side effects.

The Except Monad

Option tells you that something failed but not why. Except carries the reason. This is the difference between a function returning null and a function throwing an exception with a message. The monadic structure is identical; only the context changes. This uniformity is the point. Learn the pattern once, apply it to failure, to errors, to state, to nondeterminism, to parsing, to probability distributions. The shape is always the same.

inductive ValidationError where
  | emptyName
  | invalidAge (age : Nat)
  | missingField (field : String)
  deriving Repr

def validateName (name : String) : Except ValidationError String :=
  if name.isEmpty then .error .emptyName
  else .ok name

def validateAge (age : Nat) : Except ValidationError Nat :=
  if age == 0 || age > 150 then .error (.invalidAge age)
  else .ok age

def validatePerson (name : String) (age : Nat) : Except ValidationError (String × Nat) := do
  let validName ← validateName name
  let validAge ← validateAge age
  return (validName, validAge)

#eval validatePerson "Alice" 30   -- Except.ok ("Alice", 30)
#eval validatePerson "" 30        -- Except.error ValidationError.emptyName
#eval validatePerson "Bob" 200    -- Except.error (ValidationError.invalidAge 200)

Transporter Malfunction

The transporter is Star Trek’s matter-energy teleportation device. It is also perhaps the most horrifying device in science fiction. It disassembles you at the atomic level, transmits your pattern as information, and reassembles a copy at the destination. The original is destroyed. What arrives is a perfect duplicate with all your memories, convinced it is you. Philosophers call this the teleportation problem. Starfleet calls it Tuesday.

From an engineering perspective, the transporter is a pipeline of fallible operations that must also maintain a log. Initialize the pattern buffer. Scan the subject. Dematerialize. Transmit. Rematerialize. Each step can fail (buffer overflows, Heisenberg compensator malfunctions), and each step should be logged for the accident investigation. This requires combining two effects: error handling and state.

inductive TransporterError where
  | bufferOverflow
  | patternDegradation (percent : Nat)
  | heisenbergCompensatorFailure
  | annularConfinementFailure
  deriving Repr

def TransporterError.describe : TransporterError → String
  | .bufferOverflow => "Pattern buffer overflow"
  | .patternDegradation p => s!"Pattern degradation at {p}%"
  | .heisenbergCompensatorFailure => "Heisenberg compensator offline"
  | .annularConfinementFailure => "Annular confinement beam failure"

structure CrewMember where
  name : String
  rank : String
  deriving Repr, BEq

structure TransportLog where
  entries : List String := []
  deriving Repr

def TransportLog.add (log : TransportLog) (entry : String) : TransportLog :=
  { entries := log.entries ++ [entry] }

Transformer Ordering Matters

When you combine StateT and Except, the order matters. These two type aliases have different semantics:

-- Two different monad transformer orderings with DIFFERENT semantics:

-- Stack A: State OUTSIDE Except
-- On error, state changes are PRESERVED (audit log semantics)
abbrev TransporterA := StateT TransportLog (Except TransporterError)

-- Stack B: State INSIDE Except
-- On error, state changes are ROLLED BACK (transaction semantics)
abbrev TransporterB := ExceptT TransporterError (StateM TransportLog)

The difference emerges when an operation fails partway through. With StateT on the outside, the error discards the accumulated state. With ExceptT on the outside, the state persists even after failure. In database terms: transaction rollback versus audit logging.

def logStepB (msg : String) : TransporterB Unit :=
  modify (·.add msg)

def transportB (crew : CrewMember) : TransporterB CrewMember := do
  logStepB s!"Initializing buffer for {crew.name}"
  logStepB s!"Scanning pattern..."
  if crew.name.length > 15 then
    logStepB s!"ERROR: Buffer overflow during scan"
    throw .bufferOverflow
  logStepB s!"Dematerializing {crew.name}..."
  logStepB s!"Pattern in buffer, subject no longer exists at origin"
  if crew.name == "Thomas Riker" then
    logStepB s!"ERROR: Heisenberg compensator failure during transmission"
    throw .heisenbergCompensatorFailure
  logStepB s!"Transmitting..."
  logStepB s!"Rematerializing at destination"
  logStepB s!"Transport complete: {crew.name} arrived safely"
  pure crew

The Philosophical Horror

Consider what happens when transport fails after dematerialization but before rematerialization. The log reads: “Pattern in buffer, subject no longer exists at origin” followed by “ERROR: Heisenberg compensator failure.”

With audit log semantics (ExceptT outside), the log persists. The crew member does not.

def runTransporterA (crew : CrewMember) : Except TransporterError TransportLog :=
  match StateT.run (transportA crew) {} with
  | .ok (_, log) => .ok log
  | .error e => .error e  -- log is lost!

def runTransporterA' (crew : CrewMember) : TransportLog × Option TransporterError :=
  -- Actually extract the log even on failure
  match StateT.run (transportA crew) {} with
  | .ok (_, log) => (log, none)
  | .error _ =>
    -- With StateT outside, we need a different approach to get the log
    -- This demonstrates the limitation: the log IS preserved in the state
    -- but Except's error case doesn't give us access to it directly
    ({}, some .bufferOverflow)

-- Better: run and always get the log
def runTransporterAWithLog (crew : CrewMember)
    : (Except TransporterError CrewMember) × TransportLog :=
  -- StateT s (Except e) α → s → Except e (α × s)
  -- We need to restructure to always return the log
  match StateT.run (transportA crew) {} with
  | .ok (crew, log) => (.ok crew, log)
  | .error e => (.error e, {})  -- log lost in this formulation!

def runTransporterB (crew : CrewMember) : TransportLog × Except TransporterError CrewMember :=
  -- ExceptT e (StateM s) α → s → (Except e α) × s
  -- State is ALWAYS returned, even on error
  let ((result, log)) := StateT.run (ExceptT.run (transportB crew)) {}
  (log, result)

For databases, you choose the transformer ordering based on requirements. Financial audits need persistent logs; atomic transactions need rollback. For humans, “transaction aborted after dematerialization” raises questions not covered in the Starfleet manual. The log shows you were disassembled. The error shows you were never reassembled. What exactly should rollback mean here?

Tip

Run from the repository: lake exe transporter

If formal verification ever finds a practical purpose beyond software, reassembling humans at the molecular level might be a suitable application. You would want mathematical certainty that the rematerialized crew member has all their organs in the correct configuration, that no quantum state got flipped during transmission, that the thing stepping off the pad is topologically equivalent to what stepped on. (A human turned inside-out is homeomorphic to the original, but the crew tends to file complaints.) Supposing we can get the Heisenberg compensator to work, of course. Until then, we practice on programs.

The State Monad

The state monad threads mutable state through a pure computation. You get the ergonomics of mutation, the ability to read and write a value as you go, without actually mutating anything. Each computation takes a state and returns a new state alongside its result. The threading is automatic, hidden behind the monadic interface. This is not a trick. It is a different way of thinking about state: not as a mutable box but as a value that flows through your computation, transformed at each step.

abbrev State' (σ α : Type) := σ → (α × σ)

def get'' {σ : Type} : State' σ σ := fun s => (s, s)

def set'' {σ : Type} (newState : σ) : State' σ Unit := fun _ => ((), newState)

def modify'' {σ : Type} (f : σ → σ) : State' σ Unit := fun s => ((), f s)

def runState' {σ α : Type} (init : σ) (m : State' σ α) : α × σ :=
  m init

def counter' : State' Nat Nat := fun n => (n, n + 1)

#eval runState' 0 counter'       -- (0, 1)
#eval runState' 10 counter'      -- (10, 11)

StateM in Practice

Lean provides StateM, a production-ready state monad. The operations get, set, and modify do exactly what their names suggest. Combined with do notation, stateful code looks almost identical to imperative code, except that the state is explicit in the type and the purity is preserved. You can run the same computation with different initial states and get reproducible results. You can reason about what the code does without worrying about hidden mutation elsewhere.

def tick : StateM Nat Unit := modify (· + 1)

def getTicks : StateM Nat Nat := get

def countOperations : StateM Nat Nat := do
  tick
  tick
  tick
  let count ← getTicks
  return count

#eval countOperations.run 0    -- (3, 3)
#eval countOperations.run 10   -- (13, 13)

The List Monad

Lists as a monad represent nondeterministic computation: a value that could be many things at once. Bind explores all combinations, like nested loops but without the nesting. This is how you generate permutations, enumerate possibilities, or implement backtracking search. The abstraction is the same; only the interpretation differs. A monad does not care whether its context is failure, state, or multiplicity. It only knows how to sequence.

def pairs (xs : List Nat) (ys : List Nat) : List (Nat × Nat) :=
  xs.flatMap fun x => ys.map fun y => (x, y)

#eval pairs [1, 2] [10, 20]  -- [(1, 10), (1, 20), (2, 10), (2, 20)]

def pythagTriples (n : Nat) : List (Nat × Nat × Nat) :=
  (List.range n).flatMap fun a =>
  (List.range n).flatMap fun b =>
  (List.range n).filterMap fun c =>
    if a * a + b * b == c * c && a > 0 && b > 0 then
      some (a, b, c)
    else
      none

#eval pythagTriples 15  -- [(3, 4, 5), (4, 3, 5), (5, 12, 13), ...]

Iteration Type Classes

The ForIn type class powers for loops. Any type with a ForIn instance can be iterated with for x in collection do. The mechanism is more flexible than it first appears: you can implement custom iteration patterns, control early exit, and work in any monad.

structure CountDown where
  start : Nat

instance : ForIn Id CountDown Nat where
  forIn cd init f := do
    let mut acc := init
    let mut i := cd.start
    while i > 0 do
      match ← f i acc with
      | .done a  => return a  -- break
      | .yield a => acc := a  -- continue
      i := i - 1
    return acc

def sumCountDown (n : Nat) : Nat := Id.run do
  let mut total := 0
  for i in CountDown.mk n do
    total := total + i
  return total

#eval sumCountDown 5  -- 15 (5+4+3+2+1)

The ForInStep type controls loop flow. Returning .done value breaks out of the loop with the accumulated result. Returning .yield value continues to the next iteration. This desugars to monadic operations, so early return in a for loop is not a special case but an application of the general mechanism.

def printAll (xs : List String) : IO Unit := do
  for x in xs do
    IO.println x

def sumWithIndex (arr : Array Nat) : Nat := Id.run do
  let mut total := 0
  for h : i in [0:arr.size] do
    total := total + arr[i]
  return total

#eval sumWithIndex #[10, 20, 30]  -- 60

def manualForIn (xs : List Nat) : Option Nat :=
  ForIn.forIn xs 0 fun x acc =>
    if x == 0 then some (.done acc)   -- early exit
    else some (.yield (acc + x))      -- continue

#eval manualForIn [1, 2, 3, 4]  -- some 10
#eval manualForIn [1, 2, 0, 4]  -- some 3 (stopped at 0)

The forIn function can be called directly when you need explicit control over the accumulator and continuation. The callback returns some (.done acc) to break or some (.yield acc) to continue. Returning none propagates failure in the Option monad. This is how Lean unifies iteration with monadic effects.

Collection Operations

Lists and arrays share a common vocabulary of operations. These functions compose naturally into data processing pipelines.

def vessels : List String := ["Enterprise", "Defiant", "Voyager", "Reliant"]
def registries : List String := ["NCC-1701", "NX-74205", "NCC-74656", "NCC-1864"]

-- zip: pair elements from two collections
#eval vessels.zip registries
-- [("Enterprise", "NCC-1701"), ...]

-- map: transform each element
#eval vessels.map String.toUpper
-- ["ENTERPRISE", "DEFIANT", "VOYAGER", "RELIANT"]

-- filter: keep elements matching predicate
#eval vessels.filter (·.startsWith "V")
-- ["Voyager"]

-- take/drop: slice prefix or suffix
#eval vessels.take 2
-- ["Enterprise", "Defiant"]
#eval vessels.drop 2
-- ["Voyager", "Reliant"]

-- filterMap: filter and transform in one pass
#eval ["42", "bad", "17"].filterMap String.toNat?
-- [42, 17]

-- find?: first element matching predicate
#eval vessels.find? (·.length > 7)
-- some "Enterprise"

-- any/all: check predicates
#eval vessels.any (·.startsWith "E")  -- true
#eval vessels.all (·.length > 3)      -- true

-- zipIdx: pair with indices
#eval ["a", "b", "c"].zipIdx
-- [("a", 0), ("b", 1), ("c", 2)]

The operations compose cleanly: filter selects, map transforms, filterMap fuses both. find? returns Option because absence is a valid result, not an exception.

Folds

Folds are the fundamental iteration pattern. Every loop, every accumulation, every reduction can be expressed as a fold. Understanding folds means understanding how computation flows through a data structure.

A left fold processes elements left-to-right, accumulating from the left:

\[ \text{foldl}(f, z, [a, b, c]) = f(f(f(z, a), b), c) = ((z \oplus a) \oplus b) \oplus c \]

A right fold processes elements right-to-left, accumulating from the right:

\[ \text{foldr}(f, z, [a, b, c]) = f(a, f(b, f(c, z))) = a \oplus (b \oplus (c \oplus z)) \]

Here \(\oplus\) is just \(f\) written infix: \(a \oplus b = f(a, b)\).

For associative operations like addition, both folds give the same result. For non-associative operations, the parenthesization matters:

-- foldl: left fold, accumulator on the left
#eval [1, 2, 3, 4].foldl (· + ·) 0        -- 10
#eval ["a","b","c"].foldl (· ++ ·) ""     -- "abc"

-- foldr: right fold, accumulator on the right
#eval [1, 2, 3, 4].foldr (· + ·) 0        -- 10
#eval ["a","b","c"].foldr (· ++ ·) ""     -- "abc"

-- the difference: subtraction is not commutative
-- foldl f z [a,b,c] = f(f(f(z,a),b),c) = ((z⊕a)⊕b)⊕c
-- foldr f z [a,b,c] = f(a,f(b,f(c,z))) = a⊕(b⊕(c⊕z))
#eval ([1, 2, 3, 4] : List Int).foldl (· - ·) 0   -- -10: ((((0-1)-2)-3)-4)
#eval ([1, 2, 3, 4] : List Int).foldr (· - ·) 0   -- -2:  (1-(2-(3-(4-0))))

-- foldl builds left-to-right (tail recursive)
#eval [1, 2, 3].foldl (fun acc x => x :: acc) []  -- [3, 2, 1]

-- foldr builds right-to-left (preserves structure)
#eval [1, 2, 3].foldr (fun x acc => x :: acc) []  -- [1, 2, 3]

-- practical uses
#eval [10, 25, 8, 42, 3].foldl max 0              -- 42
#eval [2, 3, 4].foldl (· * ·) 1                   -- 24
#eval [1, 2, 3].foldl (fun acc x => acc + x * x) 0  -- 14

The cons example reveals the structural difference. Building a list with foldl reverses order because each new element is prepended to the growing accumulator. Building with foldr preserves order because the accumulator grows from the right. This is why map is typically defined using foldr: map f xs = foldr (fun x acc => f x :: acc) [] xs.

Left folds are tail-recursive and run in constant stack space. Right folds are not tail-recursive but can work with lazy data structures since they do not need to traverse to the end before producing output. In strict languages like Lean, prefer foldl for efficiency unless you need the structural properties of foldr.

The Monad Type Class

Under the hood, all monads implement the same interface. pure lifts a plain value into the monadic context. bind sequences two computations, passing the result of the first to the second. That is the entire interface. Everything else, the do notation, the specialized operations, the ergonomic helpers, builds on these two primitives. The simplicity is deliberate. A minimal interface means maximal generality.

class Monad' (M : Type → Type) extends Functor M where
  pure' : {α : Type} → α → M α
  bind' : {α β : Type} → M α → (α → M β) → M β

instance : Monad' Option where
  map f
    | none => none
    | some x => some (f x)
  pure' := some
  bind' m f := match m with
    | none => none
    | some x => f x

instance : Monad' List where
  map := List.map
  pure' x := [x]
  bind' m f := m.flatMap f

Monad Laws

Here is where the algebra becomes essential. Monads must satisfy three laws: left identity, right identity, and associativity. These are not suggestions. They are the contract that makes generic programming possible.

In the traditional bind/return formulation:

The same laws look cleaner in the Kleisli category, where we compose monadic functions directly. If $f : A \to M B$ and $g : B \to M C$, their Kleisli composition is $g \circ f : A \to M C$:

The Kleisli formulation reveals that monads give you a category where objects are types and morphisms are functions $A \to M B$. The laws say pure is the identity morphism and >=> is associative composition. A monad is a way of embedding effectful computation into the compositional structure of functions.

-- Left identity: pure a >>= f  =  f a
example (f : Nat → Option Nat) (a : Nat) :
    (pure a >>= f) = f a := rfl

-- Right identity: m >>= pure  =  m
example (m : Option Nat) : (m >>= pure) = m := by
  cases m <;> rfl

-- Associativity: (m >>= f) >>= g  =  m >>= (fun x => f x >>= g)
example (m : Option Nat) (f : Nat → Option Nat) (g : Nat → Option Nat) :
    ((m >>= f) >>= g) = (m >>= fun x => f x >>= g) := by
  cases m <;> rfl

Tip

In Haskell (and most other languages), you can claim your monad follows the laws but the compiler takes your word for it. In Lean, you can prove it. The laws become theorems, and proving them means constructing values of the corresponding types. This is the Curry-Howard correspondence at work. The Proofs article shows how.

At this point someone usually asks what a monad “really is.” The answers have become a genre: a burrito, a spacesuit, a programmable semicolon, a monoid in the category of endofunctors. These metaphors are not wrong, but they are not enlightening either. A monad is the three laws above and nothing else. Everything follows from the laws. The metaphors are for people who want to feel like they understand before they do the work of understanding.

If you want the category theory (colloquially known as “abstract nonsense,” which is their term of endearment for their own field): a monad is a monoid object in the monoidal category of endofunctors under composition. Equivalently, it is a lax 2-functor from the terminal 2-category to Cat. A category is just a monoid in the endomorphism hom-category of the bicategory of spans. The Kleisli category is the free algebra of the monad. some is just the identity morphism in the Kleisli category of Option. In Haskell it is called Just, which humorously is Just an endomorphism in the Kleisli category of Option. If this clarified nothing, congratulations: you understood monads before and still do now.

Early Return

Do notation supports early return, loops, and mutable references, all the imperative conveniences. Combined with monads, this gives you the syntax of imperative programming with the semantics of pure functions. You can write code that reads like Python and reasons like Haskell. This is not cheating. It is the whole point: capturing effects in types so that the compiler knows what your code might do, while letting you write in whatever style is clearest.

def findFirst {α : Type} (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if p x then return x
  none

#eval findFirst (· > 5) [1, 2, 3, 7, 4]  -- some 7
#eval findFirst (· > 10) [1, 2, 3]       -- none

def processUntilError (xs : List Nat) : Except String (List Nat) := do
  let mut results := []
  for x in xs do
    if x == 0 then
      throw "encountered zero"
    results := results ++ [x * 2]
  return results

#eval processUntilError [1, 2, 3]     -- Except.ok [2, 4, 6]
#eval processUntilError [1, 0, 3]     -- Except.error "encountered zero"

Combining Monadic Operations

Functions like mapM and filterMap combine monadic operations over collections. Map a fallible function over a list and either get all the results or the first failure. Filter a list with a predicate that consults external state. These combinators emerge naturally once you have the abstraction. They are not special cases but instances of a general pattern, composable because they respect the monad laws.

def mayFail (x : Nat) : Option Nat :=
  if x == 0 then none else some (100 / x)

def processAll (xs : List Nat) : Option (List Nat) :=
  xs.mapM mayFail

#eval processAll [1, 2, 4, 5]   -- some [100, 50, 25, 20]
#eval processAll [1, 0, 4, 5]   -- none

def filterValid (xs : List Nat) : List Nat :=
  xs.filterMap mayFail

#eval filterValid [1, 0, 2, 0, 4]  -- [100, 50, 25]

The Larger Pattern

Monads are one algebraic structure among many. Functors capture mapping. Applicatives capture independent combination. Monads capture dependent sequencing. Comonads capture context extraction. Arrows generalize computation graphs. Algebraic effects decompose monads into composable pieces. Each abstraction comes with laws, and those laws are the actual content. The specific names matter less than the discipline: identify a pattern, find its laws, and build an interface that enforces them.

The trajectory of programming language research has been toward making this structure explicit. Effects that C programmers handle with conventions, functional programmers handle with types. Invariants that documentation describes, dependent types enforce. Properties that tests sample, proofs establish. Each step reduces the burden on human memory and attention, encoding knowledge in artifacts that machines can check.

This matters because the economics of software are changing. When code is cheap to generate, correctness becomes the bottleneck. A language model can produce plausible implementations faster than any human, but “plausible” is not “correct.” The leverage shifts to whoever can specify precisely what correct means. Types, laws, contracts, proofs: these are the tools for specifying. Monads are a small example, one worked case of a pattern made precise. The concept itself was always simple. Sequencing with context. The value was never in the mystery but in the laws that let us reason compositionally about programs we increasingly do not write ourselves and cannot fully understand. (For more on where this is heading, see Artificial Intelligence.)

From Abstract to Concrete

Monads describe effects abstractly. The next article makes them concrete: actual file I/O, process management, environment variables, and the runtime machinery that connects your pure descriptions to the impure world. This completes the programming half of our journey.