[ NOTE: This is my fifth attempt to post this defense. The previous four were eaten by the forum software, which I maintain is running on an impure IO monad. Ironic. ]
Alright. ALRIGHT. I am tired of seeing "monads are not burritos" posts proliferate across this board like unchecked side effects in an imperative program. I am here today, once and for all, to provide a RIGOROUS, FORMAL, AND DEFINITIVELY CORRECT defense of the Burrito Analogy. Buckle your tortillas. nya~
PART I — What Even IS a Burrito? (A Formal Definition)
Let us begin with first principles. I propose the following type signature:
data Burrito filling = Burrito
{ tortilla :: Wrapper
, filling :: filling -- type parameter! she's right here!
, salsa :: Maybe Salsa -- optional effects!
, guac :: IO Guac -- impure. always impure.
}
class Monad m => BurritoMonad m where
wrap :: a -> m a -- return: put filling in tortilla
bind :: m a -> (a -> m b) -> m b -- >>=: open burrito, apply fn, re-wrap
flatten :: m (m a) -> m a -- join: burrito within a burrito → one burrito
You see? It's right there. The tortilla is the monadic wrapper. The filling is the type parameter. return wraps a value in a fresh tortilla. >>= opens the burrito, applies a function to the filling, and produces a new burrito. This is not a metaphor. This is a homomorphism.
PART II — The Diagrams (please do not skip the diagrams)
BURRITO MONAD STRUCTURE — Figure 1
════════════════════════════════════════════════════════════
return :: a → Burrito a
┌─────────────────────────┐
│ 🌯 TORTILLA WRAP │
│ ┌─────────────────┐ │
│ │ filling :: a │ │ ← your value lives here, nya~
│ └─────────────────┘ │
└─────────────────────────┘
Burrito a
(>>=) :: Burrito a → (a → Burrito b) → Burrito b
┌─────────────┐ ┌─────────────────────┐
│ 🌯 Burrito a│ ──────> │ f :: a → Burrito b │
│ ┌───────┐ │ unwrap │ │
│ │ a │ │ filling │ ┌───────────────┐ │
│ └───────┘ │ apply f │ │ 🌯 Burrito b │ │
└─────────────┘ │ └───────────────┘ │
└─────────────────────┘
join :: Burrito (Burrito a) → Burrito a
┌────────────────────────────┐
│ 🌯 OUTER TORTILLA │
│ ┌──────────────────┐ │
│ │ 🌯 INNER TORTILLA │ │ ← burrito-ception
│ │ ┌───────────┐ │ │
│ │ │ a │ │ │
│ │ └───────────┘ │ │
│ └──────────────────┘ │
└────────────────────────────┘
↓ join ↓
┌────────────────┐
│ 🌯 ONE BURRITO│
│ ┌───────────┐ │
│ │ a │ │
│ └───────────┘ │
└────────────────┘
(the outer tortilla is discarded. this is mathematically sound.)
(please do not @ me about the IO monad. i know about the IO monad.)
PART III — Responding to "But IO String doesn't CONTAIN a String"
I have heard this argument. I have heard it seventeen times in this thread alone across its various unlocked incarnations. My response:
-- The IO monad is a SEALED burrito.
-- You cannot open it yourself. The runtime opens it for you.
-- This is not a flaw in the analogy.
-- This is a FOOD SAFETY CONCERN.
--
-- newtype IO a = IO (RealWorld -> (RealWorld, a))
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-- The kitchen. The burrito is being MADE.
-- You cannot eat it until it exits the kitchen.
--
-- Complaining that IO doesn't "contain" a value is like complaining
-- that a burrito at a restaurant doesn't contain food
-- because it hasn't arrived at your table yet.
--
-- The burrito EXISTS. It merely exists in the kitchen (IO).
-- nya~
I rest my case for Part III. Counterarguments welcome. Wrong counterarguments will be refuted with additional diagrams.
PART IV — The Monad Laws as Burrito Laws
MONAD LAWS → BURRITO LAWS
══════════════════════════════════════════════════════
Left Identity: return a >>= f ≡ f a
"If you wrap a filling in a tortilla, then immediately
unwrap it and apply a function... just apply the function.
Do not create unnecessary burritos. This is wasteful."
Right Identity: m >>= return ≡ m
"If you unwrap a burrito and re-wrap the filling with no
changes... you have the same burrito. Obviously."
Associativity: (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
"The order in which you compose burrito operations
does not matter, as long as the sequence is the same.
This is a BURRITO RESTAURANT INVARIANT.
Your burrito tastes the same regardless of who
assembled which layer when."
QED. (Quite Edibly Demonstrated.) 🌯
I will be posting the full Burrito Manifesto in the Resources section. Please read it before replying. Thank you. nya~ 🌯🐱
-- FluffyBinder
=^.^= "A monad is just a monoid in the category of endofunctors.
A burrito is just a monad in the category of foods.
Therefore: QED. nya~"
[CGPA since 2021 | Burrito Theory Evangelist | she/her]