prelude :: Reader -> Page
prelude, for the patient reader
“a program is a proof in disguise” — pencilled in a margin, ca. 1989
Welcome. This page is not a product launch. It is a notebook, kept by a person who has spent an unreasonable amount of time arranging values into types and types into proofs. If you are looking for a download link, a pricing tier, or a friendly chatbot to onboard you, you have arrived at the wrong manuscript — though you are very welcome to stay and read.
The intended reader is anyone willing to slow down. You may be a working
Haskell programmer, a curious onlooker, or simply someone who likes the
way >>= looks on the page. The folios
that follow are short essays — six in total — each ending with
a one-line equation that I hope earns its
-- QED.
The intuition first. Functional programming is, for me, less a technology than a habit of thought: the habit of asking what a thing is before asking what it should do. The folios that follow are arranged like a small proof tree — premises above, conclusion below — in the hope that, if you read them in order, the last folio will feel like the obvious next line.
There are six folios. The first explains who this is for; the second sketches what it is to think in types; the third treats equational reasoning as an everyday tool; the fourth meditates on three quiet virtues — laziness, purity, and totality; the fifth is about composition as a way of life; and the sixth is the only place where anything actually happens.
prelude = readWith patience . turnPage
-- QED