Eager, lazy, & small-step "correct" fixed points

fix-eval-eager.ml

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int

type value = Int of int
           | Fun of (value -> value)

type env = (var * value) list

exception RecursionError
exception TypeError

let rec eval (t: term) (env: env): value =
  match t with
  | Lit n -> Int n
  | Var x -> List.assoc x env
  | Lam (x, body) -> Fun (fun v -> eval body ((x,v) :: env))
  | App (fnc, arg) -> (match (eval fnc env, eval arg env) with
                       | (Fun f, v) -> f v
                       | _ -> raise TypeError)
  | Fix (x, body) ->
     (* we could be "lazy" and immediately return a Fun here,
      * but if you _don't_ want that things get interesting.
      *
      * for instance, what if the body calls "x" before yielding a function?
      * we could:
      *
      * - report an error
      * - recursively recompute body, which will probably infinite loop -
      *   unless `body` is nondeterministic! eg. imagine doing weird shit
      *   with a random number generator.
      *
      * here I'm just going to have it report an error in this case.
      *)
     let cell: (value -> value) ref = ref (fun x -> raise RecursionError) in
     let self: value = Fun (fun x -> !cell x) in
     match eval body ((x, self) :: env) with
     | Fun f as v -> (cell := f; v)
     | _ -> raise TypeError

let const: term = Fix ("f", Lam ("x", Lit 3))
(* produces f = \x. f x, ie infinite loop *)
let infloop: term = Fix ("f", Var "f")

(* try:

# eval (App (const, Lit 7)) [];;
- : value = Int 3
# eval (App (infloop, Lit 7)) [];; (* this infloops *)
  C-c C-cInterrupted.

*)

fix-eval-lazy.ml

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int

type value = Int of int
           | Fun of (value -> value)

type env = (var * value) list

exception RecursionError
exception TypeError

let apply: value -> value -> value = function
  | Fun f -> f
  | _ -> raise TypeError

let rec eval (t: term) (env: env): value =
  match t with
  | Lit n -> Int n
  | Var x -> List.assoc x env
  | Lam (x, body) -> Fun (fun v -> eval body ((x,v) :: env))
  | App (fnc, arg) -> apply (eval fnc env) (eval arg env)
  | Fix (x, body) ->
     let rec callme arg = apply (eval body ((x, Fun callme) :: env)) arg
     in Fun callme

let const: term = Fix ("f", Lam ("x", Lit 3))
let infloop: term = Fix ("f", Var "f")

(* try:

# eval (App (const, Lit 7)) [];;
- : value = Int 3
# eval (App (infloop, Lit 7)) [];; (* this infloops *)
  C-c C-cInterrupted.

*)

fix-small-step.ml

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int
          | Ifzero of term * term * term

type value = Int of int
           | Fun of (value -> value)

type promise = Now of value
             | Later of (unit -> value)

let force: promise -> value =
  function Now v -> v | Later f -> f ()

type env = (var * promise) list

exception RecursionError
exception TypeError

let apply: value -> value -> value = function
  | Fun f -> f
  | _ -> raise TypeError

let rec eval (t: term) (env: env): value =
  match t with
  | Lit n -> Int n
  | Ifzero (cnd,thn,els) ->
     eval (match eval cnd env with Int 0 -> thn | _ -> els) env
  | Var x -> force (List.assoc x env)
  | Lam (x, body) -> Fun (fun v -> eval body ((x, Now v) :: env))
  | App (fnc, arg) -> apply (eval fnc env) (eval arg env)
  | Fix (x, body) ->
     let rec self () = (print_endline "recursion!";
                        eval body ((x, Later self) :: env))
     in self ()

let const: term = Fix ("f", Lam ("x", Lit 3))
let infloop: term = Fix ("f", Var "f")

(* f x = if x = 0 then 3 else f 0 *)
let constrec: term =
  Fix ("f", Lam ("x", Ifzero (Var "x", Lit 3, App (Var "f", Lit 0))))

(* try:

# eval (App (const, Lit 7)) [];;
- : value = Int 3
# eval (App (constrec, Lit 7)) [];;
recursion!
recursion!
- : value = Int 3
# eval infloop [];; (* this infloops *)
recursion!
recursion!
recursion!
recursion!
[...]
  C-c C-cInterrupted.

*)