module SECD: sig .. end
A toy implementation of SECD machine in OCaml.
type 'a id
The type of identifer. We use abstract type instead of string for the
sake of type safety. Use primitive i to generate new identifier
type 'a term
The type of a term to be executed
val i : unit -> 'a id
i () generate a new identifer.
val u : unit id
Predefined identifier for unit
val v : 'a id -> 'a term
v id refers to the value of a single identifer id as a term
val p : 'a -> 'a term
The entry point from OCaml world to SECD world. p x converts arbitray
OCaml value x to its SECD correspondence p x.
val ($) : ('a -> 'b) term -> 'a term -> 'b term
the application combinator of SECD terms. f $ x represents the result
of f term applied to x term as a term
val fn : 'a id -> 'b term -> ('a -> 'b) term
the abstraction (lambda) combinator of SECD terms. fn x t represents
fun x -> t as a term
val cond : bool term -> 'a term -> 'a term -> 'a term
the condition (if) combinator of SECD term. cond b t1 t2 represents if
b then t1 else t2 as a term.
val yc : (('a -> 'b) -> 'a -> 'b) term -> ('a -> 'b) term
the recursion (Y) combinator of SECD term. yc f represents a function
term f_rec where f_rec = f f_rec
val cbv : 'a term -> 'a
The entry point from SECD world to OCaml world. cbv t evaluate SECD
term t to the corresponding OCaml value based on call-by-value
strategy.
val cbn : 'a term -> 'a
Similar to cbv, but use a call-by-name strategy to evaluate