Puddle is an editor for an extension of λ-calculus, Alanzo Church's functional programming language circa 1931. Pomagma is an inference engine for combinatory logic, Shönfinkel and Curry's functional programming language circa 1920s. Felice Cardone and Roger Hindley have written a wonderful survey of the history of both languages. See Pomagma's Philosophy for further information.
Much of Puddle's code deals with compiling from λ-calculus to combinatory algebra and decompiling back. When the puddle editor (the browser client) loads the corpus, it decompiles it into lambda form. The lambda form what the user sees and edits.
Puddle's corpus is body of code in combinatory form consisting of a set of statements or lines. Each line is either an assertion or a definition. Definitions have names, and assertions are anonymous. The meaning of each line depends on the definitions of variables referenced in that line.
Each line's meaning is either valid or invalid,
and there are two types of invalid lines: overdefined and underdefined
(corresponding to validity.is_top and validity.is_bot, respectively).
The Pomagma engine that tries to determine
whether each line is valid or invalid.
Sometimes the engine cannot decide;
sometimes it can decide that a term is not overdefined but may be underdefined;
sometimes it can decide that a term may be overdefined but is not underdefined.
Puddle conveys this partial validity state via validity icons:
colored triangles and squares to the left of each line.
| Symbol | Color | Overdefined? | Underdefined? | Valid? |
|---|---|---|---|---|
| (none) | no | no | yes | |
| /\ | gray | no | yet undecided | yet undecided |
| / | gray | yet undecided | no | yet undecided |
| [] | gray | yet undecided | yet undecided | yet undecided |
| /\ | yellow | no | cannot decide | cannot decide |
| / | yellow | cannot decide | cannot decide | cannot decide |
| [] | yellow | cannot decide | cannot decide | cannot decide |
| /\ | red | no | yes | no |
| / | red | yes | no | no |