Categorical Abstract Machine

Using the connection between Cartesian closed categories and lambda calculus, we can construct an abstract machine.

The state of CAM may be described as a triple:

• a register (for the environment and computed value),
• a stack (for saving and restoring environments), and
• a code area.

Section 3 of Cousineau, Curien, Mauny sketches correctness of the CAM:

Establishing the correctness of our machine amounts to formally justify that it is both like a reduction machine, and like a ‘De Bruijn’ machine, i.e. a device performing \(\beta\) reductions in the De Bruijn’s notation. More precisely we want to prove

1. that the CAM stops with empty code and stack if and only if the evaluated term reduces in innermost strategy to the term of the final configuration, using the rules of Section 1;
2. that the innermost combinatory evaluation of a term stops if and only if its call-by-value evaluation by De Bruijn's \(\beta\) reduction stops, and that the final De Bruijn’s term realizes the final combinatory term in a sense which we define below.

We typically study CAM as a target for compiling an ML-like language. Note the ML-like language is desugared and we may assume it has already been typechecked. Hinze gives us:

type Var = String -- variables
type Con = Int    -- desugared type constructors
data Sys x where  -- primitive functions
  SVal :: a -> Sys a -- values, like bools, ints, characters, etc.
  SUnary :: Sys a -> Sys b -- primitive unary operators
  SBin :: Sys a -> Sys b -> Sys c -- primitive bindary operators

data Expr = EVar Var
          | ApplyPrim Sys [Expr]
          | EmptyTuple
          | Pair (Expr, Expr)
          | Construct Con Expr
          | App Expr Expr
          | Lam Pat Expr
          | IfThenElse Expr Expr Expr
          | ECase Expr [(Pat, Expr)]
          | ELet (Pat, Expr) Expr
          | ELetRec (Pat, Expr) Expr;

data Pat = PVar Var
         | PEmpty
         | PPair (Pat, Pat)
         | PLayer Var Pat;

Compile :: Expr -> [Instruction]

• Lambek & Scott, Introduction to Higher Categorical Logic. CUP, 1986.
• Gerard Huet, "Cartesian Closed Categories and Lambda-Calculus". PDF, 13 pages.
• Cousineau G., Curien P.-L., Mauny M. "The categorical abstract machine". LNCS, 201, Functional programming languages computer architecture, 1985, pp.50–64.
• Ralf Hinze, "The Categorical Abstract Machine: Basics and Enhancements". PDF dated April 28, 1993.
• Gerard Huet,
  "Cartesian Closed Categories and Lambda-Calculus".
  PDF, 13 pages.
• Implementation in OCaml