Skip to content

Commit 82dc99b

Browse files
author
Thomas Mahler
committed
add comparison of HHI reducer and CCC interp.
1 parent ed08a66 commit 82dc99b

1 file changed

Lines changed: 112 additions & 14 deletions

File tree

README.md

Lines changed: 112 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -616,28 +616,126 @@ Using this implementation of the Y-combinator instead of the source level define
616616
The [sourcecode for this section can be found here](https://github.com/thma/lambda-ski/blob/main/src/LambdaToSKI.hs).
617617

618618

619+
## Evaluating Combinator Expressions as Haskell Functions
620+
621+
The graph-reduction machine described above is not the only evaluation backend in this project.
622+
Two further evaluators follow a different philosophy: instead of allocating terms into a mutable graph and rewriting it in place, they compile source expressions into an intermediate representation and then execute that representation by mapping it directly to Haskell functions.
623+
Both are implemented in the `src/` tree and are exercised by the same benchmark programs (factorial, fibonacci, Ackermann, tak).
624+
625+
### The HhiReducer
626+
627+
[`src/HhiReducer.hs`](src/HhiReducer.hs) operates on combinator terms (`CL` / `CExpr`).
628+
The pipeline has three stages:
629+
630+
1. **Compile** — a λ-expression is bracket-abstracted to a `CL` combinator tree (by `Kiselyov.compileEta` / `compileBulk`).
631+
2. **Translate**`translate :: CL -> CExpr` turns the combinator tree into a `CExpr` value.
632+
`CExpr` is an untyped ADT with four constructors:
633+
```haskell
634+
data CExpr = CComb Combinator | CApp CExpr CExpr | CFun (CExpr -> CExpr) | CInt Integer
635+
```
636+
3. **Link & execute** `link primitives :: CExpr -> CExpr` replaces every `CComb` node with its
637+
Haskell-function definition from the `primitives` table, and reduces every `CApp` node with the
638+
`(!)` operator, which pattern-matches on `CFun f` and applies it:
639+
```haskell
640+
(!) :: CExpr -> CExpr -> CExpr
641+
(CFun f) ! x = f x
642+
```
643+
The final result is a `CInt` (or a `CFun` for partially applied programs).
644+
645+
Recursion comes from the `Y` entry in `primitives`:
646+
```haskell
647+
Y --> CFun (\(CFun f) -> fix f)
648+
```
649+
Booleans are Scott-encoded: `TRUE = A` (select second) and `FALSE = K` (select first).
650+
Comparison primitives like `EQL` and `GEQ` return `trueCExpr` / `falseCExpr` combinator values that continue as selectors in conditionals.
651+
652+
### The CCC Pipeline
653+
654+
[`src/CCC/Compiler.hs`](src/CCC/Compiler.hs) and [`src/CCC/Interpreter.hs`](src/CCC/Interpreter.hs)
655+
follow a categorical approach.
656+
657+
1. **Compile**`compileNumExpr :: Environment -> Expr -> CatExpr a Integer` translates a λ-expression
658+
directly to a `CatExpr`, a *typed GADT* of categorical morphisms:
659+
```haskell
660+
data CatExpr a b where
661+
Comp :: CatExpr b c -> CatExpr a b -> CatExpr a c
662+
Fst :: CatExpr (a, b) a
663+
Snd :: CatExpr (a, b) b
664+
Apply :: CatExpr (CatExpr a b, a) b
665+
Curry :: CatExpr (a, b) c -> CatExpr a (CatExpr b c)
666+
Fix :: CatExpr (CatExpr a b, a) b -> CatExpr a b
667+
Add :: CatExpr (a, a) a
668+
IfVal :: CatExpr (Bool, (a, a)) a
669+
-- … and more
670+
```
671+
The compiler uses a mixed strategy: for ordinary terms it applies Normalisation by Evaluation (NBE),
672+
keeping lambdas as Haskell closures at compile time and never building explicit `Curry`/`Uncurry`
673+
nodes for them; for recursive `y`-expressions it builds an explicit `Fix` node in the output.
674+
675+
2. **Interpret** `interp :: CatExpr a b -> (a -> b)` gives each constructor its meaning as a
676+
Haskell function in the `(->)` category:
677+
```haskell
678+
interp (Comp f g) = interp f . interp g
679+
interp Fst = fst
680+
interp Apply = uncurry interp
681+
interp (Fix step) = \a -> let rec = Fix step in interp step (rec, a)
682+
interp Add = addC -- (+) via the NumCat class
683+
interp IfVal = \(test,(t,e)) -> if test then t else e
684+
--
685+
```
686+
The result is an ordinary Haskell function; calling it on an input computes the final value.
687+
688+
Because `CatExpr` is a GADT, type errors such as `Comp Add Fst` (mismatched types) are rejected at
689+
compile time by GHC, not at run time.
690+
691+
### Similarities
692+
693+
Both approaches share the same fundamental idea:
694+
695+
- **Staged execution** — source λ-expressions are first compiled to an intermediate language; execution
696+
is a separate pass over that language, not a direct recursive walk of the source AST.
697+
- **Haskell functions as semantic objects** — in both cases the "values" that circulate at run time are
698+
Haskell functions (either `CFun (CExpr -> CExpr)` or a Haskell closure produced by `interp`).
699+
- **Haskell evaluation drives computation** — neither backend has its own explicit reduction loop for
700+
the full program at run time; once linking or interpretation has mapped combinators/morphisms to
701+
native functions, GHC's own evaluator takes over.
702+
- **Same recursion host** — both ultimately delegate fixed-point recursion to Haskell's `fix`
703+
(HhiReducer via the `Y` primitive, CCC via the `Fix` constructor in `interp`).
704+
- **Same benchmark programs** — factorial, fibonacci, gaussian, Ackermann, and tak all work through
705+
both backends, verified by `test/ReducerKiselyovSpec.hs` and `test/CCCCompilerSpec.hs`.
706+
707+
### Differences
708+
709+
| Dimension | HhiReducer | CCC Pipeline |
710+
|---|---|---|
711+
| **Intermediate language** | `CExpr` — untyped ADT (`CComb \| CApp \| CFun \| CInt`) | `CatExpr a b` — typed GADT of categorical morphisms |
712+
| **Typing** | Untyped; bad applications fail at runtime via pattern-match (`can't handle`) | Strongly typed; ill-typed compositions rejected by GHC |
713+
| **Source input** | `CL` combinator tree produced by bracket abstraction | `Expr` λ-term compiled directly without prior bracket abstraction |
714+
| **Compilation strategy** | Structural translation of combinator application tree | Mixed NBE (for ordinary terms) + direct `Fix`-node construction (for `y`-recursion) |
715+
| **Application model** | `(!) :: CExpr -> CExpr -> CExpr` — pattern-matches on `CFun f` and applies it | `interp Apply = uncurry interp` — functions are first-class `CatExpr` values |
716+
| **Booleans** | Scott-encoded: `TRUE = A (= λt e. e)`, `FALSE = K (= λt e. t)`; comparisons return combinator values | Primitive `T`, `F` constructors; conditionals via `IfVal :: CatExpr (Bool,(a,a)) a` |
717+
| **Branching** | Continuation-passing via Scott-encoding: `if c t e``c t e` reduces by combinator rule | `interp IfVal = \(test,(t,e)) -> if test then t else e` — native Haskell `if` |
718+
| **Arithmetic** | `arith op = CFun \(CInt a) -> CFun \(CInt b) -> CInt (op a b)` wraps native operators as `CFun` | `Add`, `Sub`, `Mul` GADT constructors; `interp Add = addC` via `NumCat` type class |
719+
| **Recursion** | `Y --> CFun (\(CFun f) -> fix f)` in `primitives` | `Fix` constructor in `CatExpr`; `interp (Fix step) = let rec = Fix step in interp step (rec, a)` |
720+
| **Structure of terms** | Binary application trees (left-nested `CApp` chains, like the combinator spine) | Cartesian products and projections (`Fst`, `Snd`, `Dup`, `Par`) carry the argument structure |
721+
| **Normal form** | The final `CInt` (or partial `CFun`) reached after all `(!)` applications are exhausted | The value of type `b` returned when the Haskell function `interp morph` is applied to its input |
722+
| **Failure mode** | `error` via explicit `can't handle` match or arithmetic pattern failure | `error` in `compileNumExpr` for unsupported terms; type-level safety otherwise |
723+
724+
In short: HhiReducer is an *operational* evaluator — it treats programs as trees of combinator applications and executes them by a chain of function lookups and applications.
725+
The CCC pipeline is a *denotational* evaluator — it gives each morphism a direct mathematical meaning as a function in the `(->)` category and computes by interpreting that meaning.
726+
Both reach the same results, but the CCC route preserves more structure explicitly in the intermediate representation and leverages the Haskell type system to rule out malformed programs.
727+
728+
---
729+
619730
## Next steps
620731

621732
Here are some ideas for possible future extensions and improvements.
622733

623734
- Extending this very basic setup to a fully working pogramming environment with a REPL
624735
- Implement direct and mutual recursion (i.e. `letrec`) for global function definitions
625736
- experimemnt with different bracket abstraction algorithms to improve object code size and execution time.
626-
- Implement bracket abstraction from λ-expressions to [closed cartesian categories](https://thma.github.io/posts/2021-04-04-Lambda-Calculus-Combinatory-Logic-and-Cartesian-Closed-Categories.html) and extend the graph-reduction to also cover the resulting combinators `apply` and `(△)`.
737+
627738
- extend the language to include lists, maybe even provide it with a LISPKIT frontend.
628739
- Add support for implicit and explicit parallelism of the graph-reduction engine.
629740
(implicit parallelism for strict operations, and an explicit `P`-combinator)
630741

631-
## Todo
632-
# FFI Library target (wrapper around mhseval)
633-
MHSEVAL_LIB = libmhseval.so
634-
MHSEVAL_HEADER = src/runtime/mhseval.h
635-
MHSEVAL_SOURCE = src/runtime/mhseval.c
636-
637-
$(MHSEVAL_LIB): $(MHSEVAL_SOURCE) $(MHSEVAL_HEADER)
638-
$(CC) $(RTSINC) -fPIC -O2 -Wall -DWANT_STDIO=1 -DWANT_FLOAT=1 -shared -o $@ $(MHSEVAL_SOURCE)
639-
640-
mhseval-lib: $(MHSEVAL_LIB)
641-
642-
mhseval-clean:
643-
rm -f $(MHSEVAL_LIB)

0 commit comments

Comments
 (0)