Skip to content

Commit ffc7470

Browse files
author
Thomas Mahler
committed
add documentation
1 parent b583b2e commit ffc7470

1 file changed

Lines changed: 319 additions & 0 deletions

File tree

‎src/CCC/compiler-readme.md‎

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
# Compiling Lambda Expressions to Categorical Expressions
2+
3+
This document explains how `CCC.Compiler` translates untyped lambda calculus
4+
expressions (`Expr`) into typed categorical morphisms (`CatExpr a b`), and how
5+
those morphisms are then interpreted back into Haskell functions.
6+
7+
## Overview
8+
9+
The pipeline is:
10+
11+
```
12+
Source text >── Parser ──▶ Environment + Expr >── Compiler ──▶ CatExpr () Integer >── Interpreter ──▶ () -> Integer
13+
```
14+
15+
The compiler targets a **Closed Cartesian Category** (CCC) represented as a GADT.
16+
Every compiled program is a morphism `CatExpr () Integer`: it takes no input and
17+
produces an integer.
18+
19+
## Source language
20+
21+
`Expr` is a minimal untyped lambda calculus with integer literals:
22+
23+
```haskell
24+
data Expr = App Expr Expr | Var String | Int Integer | Lam String Expr
25+
```
26+
27+
Programs are written as a list of `name = expr` bindings (an `Environment`).
28+
The compiler resolves `main` by looking it up in the environment and recursively
29+
inlining variable references.
30+
31+
## Target language: CatExpr
32+
33+
`CatExpr a b` is a GADT representing morphisms in a CCC. The key constructors:
34+
35+
| Constructor | Type | Role |
36+
|---|---|---|
37+
| `Id` | `CatExpr a a` | Identity morphism |
38+
| `Comp f g` | `CatExpr a c` | Composition $f \circ g$ |
39+
| `Fst` | `CatExpr (a,b) a` | First projection |
40+
| `Snd` | `CatExpr (a,b) b` | Second projection |
41+
| `Dup` | `CatExpr a (a,a)` | Diagonal / fan-out |
42+
| `Par f g` | `CatExpr (a,c) (b,d)` | Parallel product $f \times g$ |
43+
| `IntConst n` | `CatExpr a Integer` | Constant morphism |
44+
| `Add`, `Sub`, `Mul` | `CatExpr (a,a) a` | Arithmetic on pairs |
45+
| `Eql`, `Leq`, ... | `CatExpr (a,a) (CatExpr (b,b) b)` | Comparisons (Scott-encoded) |
46+
| `Apply` | `CatExpr (CatExpr a b, a) b` | Closed-category application |
47+
| `Curry f` | `CatExpr a (CatExpr b c)` | Currying |
48+
| `Lift f` | `CatExpr a b` | Embed a Haskell function |
49+
| `Fix step` | `CatExpr a b` | Fixpoint combinator |
50+
51+
The helper `fanC f g = Par f g . Dup` (often written $\langle f, g \rangle$) duplicates the
52+
input and applies two morphisms in parallel, producing a pair.
53+
54+
## Compilation strategy
55+
56+
### Intermediate representation: RVal
57+
58+
The compiler does not translate `Expr` directly to `CatExpr`. Instead it uses a
59+
staging representation `RVal c`, parameterised by the CatExpr context type `c`:
60+
61+
```haskell
62+
data RVal c
63+
= RInt (CatExpr c Integer) -- a known-integer morphism
64+
| RSel (CatExpr c (CatExpr (Integer, Integer) Integer)) -- a Scott-encoded boolean
65+
| RFun (RVal c -> Either String (RVal c)) -- a meta-level function
66+
```
67+
68+
`RVal` is a **Normalisation by Evaluation (NBE)** trick: lambda abstractions stay
69+
as Haskell functions (`RFun`) during compilation and are only reified into
70+
`CatExpr` when their results are consumed. This avoids the need to explicitly
71+
manage De Bruijn indices or perform substitution in the target AST.
72+
73+
### Core compilation: `compile`
74+
75+
```haskell
76+
compile :: Environment -> [(String, RVal c)] -> Expr -> Either String (RVal c)
77+
```
78+
79+
`compile` takes the global environment, a local scope of `RVal` bindings, and an
80+
expression. It pattern-matches on the expression:
81+
82+
#### Integer literals
83+
84+
```
85+
Int i ⟶ RInt (IntConst i)
86+
```
87+
88+
The integer $i$ becomes a constant morphism that ignores its input and returns $i$.
89+
90+
#### Variables
91+
92+
Looked up first in the local scope (returning an `RVal` directly), then in the
93+
global environment (recursively compiling the referenced expression), and finally
94+
in the builtin table.
95+
96+
#### Lambda abstractions
97+
98+
```
99+
Lam p body ⟶ RFun (\arg -> compile env ((p, arg) : local) body)
100+
```
101+
102+
A lambda becomes an `RFun` — a Haskell closure that extends the local scope with
103+
the parameter bound to whatever `RVal` is passed as the argument. The body is
104+
compiled lazily when the function is applied.
105+
106+
This is the key NBE insight: function values are never directly encoded as
107+
`CatExpr` terms. They exist only at the meta-level during compilation.
108+
109+
#### Application
110+
111+
For a normal (non-fixpoint) application `App f x`:
112+
113+
1. Compile `f` to get an `RVal`.
114+
2. Compile `x` to get an `RVal`.
115+
3. If `f` compiled to `RFun fn`, call `fn x` at the Haskell level.
116+
117+
This means beta-reduction happens at compile time. The result is a fully
118+
normalised `CatExpr` with no residual lambdas — only compositions of primitive
119+
morphisms.
120+
121+
### Worked example: addition
122+
123+
Consider compiling $(\lambda x\, y.\; + \; x \; y) \; 3 \; 5$.
124+
125+
1. `Lam "x" (Lam "y" (App (App (Var "+") (Var "x")) (Var "y")))` compiles to
126+
`RFun` (a Haskell closure).
127+
128+
2. Applying `RInt (IntConst 3)` binds `x = RInt (IntConst 3)` in the local scope
129+
and returns another `RFun`.
130+
131+
3. Applying `RInt (IntConst 5)` binds `y = RInt (IntConst 5)`.
132+
133+
4. The body `App (App (Var "+") (Var "x")) (Var "y")` is compiled:
134+
- `"+"` resolves to the builtin `rBin RInt Add`.
135+
- Applying the builtin to `RInt (IntConst 3)` then `RInt (IntConst 5)` yields:
136+
137+
```
138+
RInt (Comp Add (Comp (Par (IntConst 3) (IntConst 5)) Dup))
139+
```
140+
141+
which is $\texttt{Add} \circ \langle \texttt{IntConst 3}, \texttt{IntConst 5} \rangle$.
142+
143+
5. `expectInt` extracts the `CatExpr () Integer` from the `RInt`.
144+
145+
The interpreter evaluates this as $(+)(3, 5) = 8$.
146+
147+
## Builtins
148+
149+
Builtins are pre-built `RVal` values looked up by name:
150+
151+
| Name | RVal kind | Compiles to |
152+
|---|---|---|
153+
| `+`, `-`, `*`, `sub` | `RFun` → `RFun` → `RInt` | $\texttt{op} \circ \langle x, y \rangle$ |
154+
| `sub1` | `RFun` → `RInt` | $\texttt{Sub} \circ \langle x, \texttt{IntConst 1} \rangle$ |
155+
| `is0` | `RFun` → `RSel` | $\texttt{Eql} \circ \langle x, \texttt{IntConst 0} \rangle$ |
156+
| `eql`, `leq`, `geq` | `RFun` → `RFun` → `RSel` | $\texttt{op} \circ \langle x, y \rangle$ |
157+
| `true`, `false` | `RSel` | `Lift (const Snd)`, `Lift (const Fst)` |
158+
| `if` | `RFun` → `RFun` → `RFun` → `RInt` | $\texttt{Apply} \circ \langle sel, \langle else, then \rangle \rangle$ |
159+
160+
### Scott-encoded booleans
161+
162+
Booleans are **not** a separate type. A boolean is a *selector morphism*
163+
`CatExpr (b, b) b` that picks one element from a pair:
164+
165+
- **TRUE** = `Snd` — selects the second element (like the A combinator: $\lambda t\, e.\; e$)
166+
- **FALSE** = `Fst` — selects the first element (like the K combinator: $\lambda t\, e.\; t$)
167+
168+
Comparison operators (`Eql`, `Leq`, ...) return these selectors. At the `RVal`
169+
level they are tracked as `RSel` to distinguish them from plain integers.
170+
171+
Conditionals are compiled as:
172+
173+
$$\texttt{if}\;\mathit{cond}\;\mathit{then}\;\mathit{else} \;\longrightarrow\; \texttt{Apply} \circ \langle \mathit{selector}, \langle \mathit{elseVal}, \mathit{thenVal} \rangle \rangle$$
174+
175+
The selector is applied to a pair of alternatives. Note the argument order:
176+
`then` is the second element (selected by `Snd`/TRUE) and `else` is the first
177+
(selected by `Fst`/FALSE).
178+
179+
## Fixpoint compilation
180+
181+
Recursive functions defined with `y` or `fix` are compiled structurally using the
182+
`Fix` combinator rather than unfolding the Y combinator at the lambda level.
183+
184+
### Detection
185+
186+
`isFixOp` checks whether the function position of an application is the fixpoint
187+
combinator. It follows variable aliases through the environment (with cycle
188+
detection) until it finds `"y"` or `"fix"`, or determines it is something else.
189+
190+
### The Fix combinator
191+
192+
`Fix` has type:
193+
194+
```haskell
195+
Fix :: CatExpr (CatExpr a b, a) b -> CatExpr a b
196+
```
197+
198+
It takes a *step function* that receives a pair of (self-reference, input) and
199+
produces an output. The interpreter implements it as:
200+
201+
```haskell
202+
interp (Fix step) = \a -> let rec = Fix step in interp step (rec, a)
203+
```
204+
205+
### Compilation of $\texttt{y}\;(\lambda f.\;\lambda a_1 \ldots \lambda a_n.\;\mathit{body})\;x_1 \ldots x_n$
206+
207+
1. **Peel lambdas**: Extract the self-reference name $f$ and parameter names
208+
$[a_1, \ldots, a_n]$ from the step function.
209+
210+
2. **Build IntArgs**: The type-level structure of the parameter tuple is captured
211+
by a GADT:
212+
213+
```haskell
214+
data IntArgs input where
215+
OneArg :: IntArgs Integer -- single arg
216+
MoreArgs :: IntArgs rest -> IntArgs (Integer, rest) -- nested pair
217+
```
218+
219+
For arity 3, this builds `MoreArgs (MoreArgs OneArg)` representing the type
220+
`(Integer, (Integer, Integer))`.
221+
222+
The existential is opened via CPS with `withIntArgs`:
223+
```haskell
224+
withIntArgs :: Int -> (forall input. IntArgs input -> r) -> Maybe r
225+
```
226+
227+
3. **Build the curried RVal**: `curryIntArgs` constructs an `RFun` that collects
228+
$n$ integer arguments one at a time, then passes them all to a continuation:
229+
230+
```haskell
231+
curryIntArgs :: IntArgs input -> ([CatExpr c Integer] -> Either String (RVal c)) -> RVal c
232+
```
233+
234+
4. **Compile the step body**: Inside the continuation, the compiler:
235+
236+
- Packs the collected arguments into a nested tuple using `tupleFromExprs`.
237+
- Builds a `recCall` binding for the self-reference $f$ — another curried
238+
`RVal` that collects arguments and produces $\texttt{Apply} \circ \langle \texttt{Fst}, \mathit{args} \rangle$.
239+
Here `Fst` projects the self-reference from the `(CatExpr a b, a)` context
240+
of the `Fix` body.
241+
- Builds parameter bindings by projecting from `Snd` of the fix context:
242+
$a_1 = \texttt{Comp Fst Snd}$, $a_2 = \texttt{Comp Fst (Comp Snd Snd)}$, etc.
243+
- Compiles the body expression with these bindings in scope.
244+
- Wraps everything as `Comp (Fix stepBody) paramTuple`.
245+
246+
### Worked example: factorial
247+
248+
Source:
249+
```
250+
fact = y(λf n. if (is0 n) 1 (* n (f (sub1 n))))
251+
main = fact 5
252+
```
253+
254+
Compilation of $\texttt{y}\;(\lambda f\, n.\;\mathit{body})\;5$:
255+
256+
1. $f$ = self-reference, $n$ = parameter, arity = 1, so `IntArgs` = `OneArg`.
257+
258+
2. The outer `curryIntArgs OneArg` collects one argument: `IntConst 5`.
259+
260+
3. Inside the Fix body (context type = `(CatExpr Integer Integer, Integer)`):
261+
- $f$ is bound to `recCall`: an `RFun` that produces
262+
$\texttt{Apply} \circ \langle \texttt{Fst}, \mathit{arg} \rangle$.
263+
- $n$ is bound to `RInt Snd` (project the integer input from the context).
264+
265+
4. The body `if (is0 n) 1 (* n (f (sub1 n)))` compiles to a `CatExpr` that
266+
uses `Eql`, `Sub`, `Mul`, `Apply`, `Fst`, `Snd` — all composed together.
267+
268+
5. The final result is `Comp (Fix stepBody) (IntConst 5)`.
269+
270+
The interpreter evaluates this by repeatedly calling `interp step (rec, n)`
271+
until the base case is reached.
272+
273+
### Multi-argument recursion
274+
275+
For arity > 1 (e.g. `ack = y(λf n m. ...)`), arguments are packed into nested
276+
tuples. With arity 2 the input type is `(Integer, Integer)` and the Fix context
277+
is `(CatExpr (Integer, Integer) Integer, (Integer, Integer))`.
278+
279+
- $n$ projects as `Comp Fst Snd`
280+
- $m$ projects as `Comp Snd Snd`
281+
- A recursive call $f\;a\;b$ packs $(a, b)$ via `fanC` and applies via
282+
$\texttt{Apply} \circ \langle \texttt{Fst}, \langle a, b \rangle \rangle$.
283+
284+
## Interpretation
285+
286+
`CCC.Interpreter.interp` converts a `CatExpr a b` morphism into a Haskell
287+
function `a -> b` by structural recursion:
288+
289+
```haskell
290+
interp :: CatExpr a b -> (a -> b)
291+
interp (Comp f g) = interp f . interp g
292+
interp Fst = fst
293+
interp Snd = snd
294+
interp (IntConst i) = const i
295+
interp Add = uncurry (+)
296+
interp Apply = uncurry interp
297+
interp (Fix step) = \a -> let rec = Fix step in interp step (rec, a)
298+
...
299+
```
300+
301+
The `Fix` case ties the knot: `rec` is the `Fix step` morphism itself, passed
302+
back into the step function as its first argument. Haskell's laziness ensures
303+
this only unfolds as far as needed.
304+
305+
## Summary of key design decisions
306+
307+
1. **NBE via RVal**: Lambdas stay as Haskell closures during compilation. This
308+
eliminates substitution, alpha-renaming, and De Bruijn bookkeeping.
309+
310+
2. **Scott-encoded booleans**: No boolean type in the target language.
311+
Comparisons produce selector morphisms; conditionals are just `Apply`.
312+
313+
3. **Structural Fix**: The Y combinator is intercepted and compiled to the `Fix`
314+
primitive, preserving recursion structure in the output rather than encoding it
315+
as self-application.
316+
317+
4. **Type-safe arity via IntArgs GADT**: The nested-tuple type of multi-argument
318+
fixpoints is tracked at the Haskell type level, ensuring `tupleFromExprs` and
319+
`projections` are type-correct despite the arity being determined at runtime.

0 commit comments

Comments
 (0)