Little Elpier

What eats a fly? Ask the pond.

A small pond: algae, snails and flies, frogs and fish, a duck, a heron and an otter. Eleven short lines say who eats whom. Type a question, eats X fly, and a program answers: the frog, then the fish. It does not search the web or guess. It answers only from what the lines say, and it tells you when they say nothing.

That is a logic program: a list of things that are true, and a way to ask what follows. This little book teaches the idea from zero, in the question-and-answer style of The Little Schemer. Each page is two columns, a short question on the left and a short answer on the right. Cover the answers with a card, try, then look. Now and then a box states a Maxim, a short rule the questions above it have earned, from "A fact says what is true. A question asks whether it follows." to "A typing rule is a clause. A type checker is a logic program, and it runs both ways."

The language is λProlog, a younger and stranger relative of Prolog. It adds three things: types, so the computer turns away nonsense before it runs; predicates you pass around like numbers; and two small words, pi and =>, that let a program say "for any new thing" and "suppose this were true". Those three additions are what higher-order logic programming means. With them, a type checker for a little programming language fits in seven short clauses, and the same seven clauses infer types they were never told. That is where the book ends.

What you will learn

1. Facts and Questions. Constants, predicates, capital letters as holes, and what "no" really means.
2. Rules and Recursion. :- as "if", recursion that knows when to stop, and the search tree behind every answer.
3. Terms and Unification. Numbers built as trees, and how the engine makes two terms the same, or fails.
4. Lists. One append, run three ways: join, check and split. A relation has no inputs and outputs until you ask it something.
5. Types. Kinds, types and modes, and a checker that reads the program before it runs.
6. Predicates as Values. One rule for "above", "upstream of" and "older than"; map, filter and fold.
7. Lambdas. Predicates without names, terms with holes, and binders that cannot be captured.
8. Pi and Implication. What-if questions about a pond that is not quite this one.
9. The Little Type Checker. Seven clauses that check the types of a little language and, asked with a hole, infer them.

Who it is for

Students and programmers who have never taken a logic course. You need some programming in any language, a pencil, and patience. No mathematics, no Prolog and no Lean are assumed. You do not need to know what ∀ means; by Chapter 8 you will have written it. A chapter is an evening's work.

What you get

• 9 short chapters, 541 questions with their answers, and 11 Maxims collected on one page
• 35 exercises graded ★ to ★★★, each with a solution that runs
• 14 diagrams: the food web, search trees, term trees, and binders
• A two-page cheat sheet and a guided "Where to Go Next"
• The Apache-2.0 companion code at github.com/Volland/little-elpier: every program in the book, with every printed output kept as a golden file that a test checks

Every example runs

The engine is lean-elpi, an implementation of the ELPI dialect of λProlog written in Lean 4. pip install leanelpi gives you the whole engine with nothing to compile, on macOS, Linux and Windows with WSL; a Docker image and a build from source work too. The book's site, volland.github.io/little-elpier, has a sample of the frames.