List Monad

example definition program theorem

The list monad encodes nondeterminism (many-worlds: return all results at once):

instance Monad [] where
  as >>= k = concat (fmap k as)      -- join = concat
  return a = [a]                     -- determinism is trivial nondeterminism

Nested loops of imperative languages become binds: as aggregates the inner loop, k is the outer loop body. Thanks to laziness a Haskell list behaves like an iterator/generator.

Sources: DaoFP §14.1 (“Nondeterminism”), §14.4, §14.5 (pairs), §15.3 (“Free monoid and the list monad”), §14.8 (“the list monad is not free because its join irreversibly smashes the lists together”), §14.9 (the two Applicative instances: cartesian and zip); Kittenlab Lecture 7 (Free-Forgetful Adjunction); 7 Sketches §5.2.4; CTfS Example 5.3.2.2, Example 4.3.1.8, Exercise 4.3.1.9

From the free monoid adjunction (Monads from Adjunctions, Free Monoid): $F⊣U$ between $\mathbf{Set}$ and $\mathbf{Mon}$; ${\eta }_X:X\to UFX$ sends $x$ to the singleton [x] (return); the counit ${\epsilon }_M:FUM\to M$ is the monoid morphism foldMap id = foldr mappend mempty, one direction of $\mathbf{Set}(a,Um)\cong \mathbf{Mon}(Fa,m)$; whiskering, $\mu =U\epsilon F$ instantiates $\epsilon$ at the free monoid ([], (++)), giving join = foldr (++) [] = concat.

• The monad laws on an example (CTfS Example 5.3.2.2): $\mu$ flattens $[[q,p,r],[],[q,r,p,r],[r]]\mapsto [q,p,r,q,r,p,r,r]$; the unit laws say that flattening $[[p],[q],[q]]$ or $[[p,q,q]]$ gives back $[p,q,q]$, and associativity that flattening $[[[p,q],[r]],[],[[r,q,q]]]$ inside-first or outside-first both give $[p,q,r,r,q,q]$. Flattening and singletons are natural transformations $\mathrm{List}\circ \mathrm{List}\Rightarrow \mathrm{List}$ and $\mathrm{id}\Rightarrow \mathrm{List}$ (CTfS Example 4.3.1.8).
• pairs as bs = do { a <- as; b <- bs; return (a, b) } enumerates all pairs (Do Notation, DaoFP Exercise 14.5.2).
• Two Applicative Functor structures: the monadic one applies every function to every argument; the zip one (pure = repeat, fs <*> as = zipWith ($) fs as) is applicative but not a monad (DaoFP Exercise 14.9.3). The Monoidal instance is the cartesian product of lists (DaoFP Exercise 14.9.1).

JuliaLeanHaskell

Docs: Kittenlab Lecture 7

ret(a) = [a]
bind(as, k) = reduce(vcat, (k(a) for a in as); init=Any[])   # concat ∘ map
pairs(as, bs) = bind(as, a -> bind(bs, b -> ret((a, b))))
pairs(1:2, 'a':'b')                    # [(1,'a'), (1,'b'), (2,'a'), (2,'b')]
# Catlab/Kittenlab: the free monoid on a set is the list monoid, μ = concat

import Mathlib
#check @List.bind            -- l.bind f = (l.map f).join
#check @List.join
#check @List.singleton       -- return; Lean's List is an instance of Monad
example : List (ℕ × Char) := do let a ← [1, 2]; let b ← ['a', 'b']; pure (a, b)

pairs :: [a] -> [b] -> [(a, b)]
pairs as bs = do
  a <- as
  b <- bs
  return (a, b)
 
epsilon :: Monoid m => [m] -> m          -- the counit of F ⊣ U
epsilon = foldr mappend mempty
joinL :: [[a]] -> [a]
joinL = foldr (++) []                    -- = concat