(*
Embedding a higher-order domain-specific language (simply-typed
lambda-calculus with constants) with a selectable evaluation order:
Call-by-value, call-by-name, call-by-need.
This is an OCaml version of CBAny.hs
*)
(* The (higher-order abstract) syntax of our DSL *)
module type EDSL = sig
type 'a exp (* representation of terms *)
type ('a,'b) arrow (* The arrow type *)
val int : int -> int exp
val (+) : int exp -> int exp -> int exp
val (-) : int exp -> int exp -> int exp
val lam : ('a exp -> 'b exp) -> ('a,'b) arrow exp
val (/) : ('a,'b) arrow exp -> ('a exp -> 'b exp) (* application *)
end;;
(* Add syntactic sugar: let-expressions (could've been called `bind')
Also add the convenient binary lam (the analogue of zip)
*)
module Let(S:EDSL) = struct
open S
let (let-) : 'a exp -> ('a exp -> 'b exp) -> 'b exp = fun e body ->
lam body / e
let lam2 : ('a exp -> 'b exp -> 'c exp) -> ('a,('b,'c)arrow)arrow exp =
fun f -> lam @@ fun x -> lam @@ fun y -> f x y
end
(* A sample EDSL term *)
module EX0(S:EDSL) = struct
open S
include Let(S)
let t =
(lam (fun x -> let- y = x + x in y + y)) / int 10
end;;
(* We now embed our EDSL into OCaml: we write several interpreters
of EDSL, or several implementations of the signature EDSL
Our principle is to write a term once and evaluate many times,
in different evaluation orders.
*)
(* * // *)
(* First is a meta-circular interpretation: essentially identity *)
module MetaCirc = struct
type 'a exp = 'a (* representation of terms *)
type ('a,'b) arrow = 'a -> 'b (* The arrow type *)
let int x = x
let (+) = Stdlib.(+)
let (-) = Stdlib.(-)
let lam f = f
let (/) f x = f x
end
(* QUIZ: Is it CBV, CBN, or Lazy interpretation *)
(* QUIZ: How can we test? *) (* Hint: see below *)
let toMS = let module M = EX0(MetaCirc) in M.t
(* val toMS : int = 40 *)
(* * // *)
(* An EDSL expression of the type 'a is interpreted as a OCaml value
unit -> 'a. Thunking is a well-known trick to delay evaluation
*)
(* * // *)
(* Call-by-name interpretation *)
module CBName = struct
type 'a exp = unit -> 'a (* representation of terms *)
type ('a,'b) arrow = (unit -> 'a) -> (unit ->'b) (* The arrow type *)
let int x = fun () -> x
let (+) x y = fun () ->
let xv = x () in let yv = y () in
Printf.printf "Adding %d and %d\n" xv yv;
xv + yv
let (-) x y = fun () ->
let xv = x () in let yv = y () in
Printf.printf "Subtracting %d and %d\n" xv yv;
xv - yv
let lam f = fun () -> f
let (/) x y = fun () -> x () y ()
end
let run_cbn m = m ()
(* The addition (x + x) is performed twice because y is bound
to a computation, and y is evaluated twice
*)
let t0SN = let module M = EX0(CBName) in run_cbn M.t
(*
Adding 10 and 10
Adding 10 and 10
Adding 20 and 20
val t0SN : int = 40
*)
(* A more elaborate example *)
module EX1(S:EDSL) = struct
open S
open Let(S)
let t =
let- x = int 10 - int 5 in
let- y = x + x in
let- z = int 20 - int 10 in
z + (z + (y + y))
end
(* Duplication of computations is more pronounced *)
let t1SN = let module M = EX1(CBName) in run_cbn M.t
(*
Subtracting 20 and 10
Subtracting 20 and 10
Subtracting 10 and 5
Subtracting 10 and 5
Adding 5 and 5
Subtracting 10 and 5
Subtracting 10 and 5
Adding 5 and 5
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SN : int = 40
*)
(* An even better example *)
module EX2(S:EDSL) = struct
open S
open Let(S)
let t =
let- z = int 100 - int 10 in
let- x = int 5 + int 5 in
let- y = x + x in
y + y
end
(* The result of subtraction was not needed, and so it was not performed
OTH, (int 5 `add` int 5) was computed four times.
*)
let t2SN = let module M = EX2(CBName) in run_cbn M.t
(*
Adding 5 and 5
Adding 5 and 5
Adding 10 and 10
Adding 5 and 5
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SN : int = 40
*)
(* * // *)
(* Call-by-value interpretation *)
(*
The only difference is the interpretation of lam:
before evaluating the body, _always_ evaluate the argument
*)
module CBValue = struct
include CBName
(* The only difference from CBName: a new interpretation of lam *)
(* Now lam first evaluates its argument, no matter what. *)
(* This is the definition of CBV after all *)
let lam f = fun () ->
fun y -> let yv = y () in f (fun () -> yv)
end
let run_cbv m = m ()
(* We now re-evaluate the previously written tests EX0, Ex1, EX2
under the new interpretation
*)
let t0SV = let module M = EX0(CBValue) in run_cbv M.t
(*
Adding 10 and 10
Adding 20 and 20
val t0SV : int = 40
*)
let t1SV = let module M = EX1(CBValue) in run_cbv M.t
(*
Subtracting 10 and 5
Adding 5 and 5
Subtracting 20 and 10
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SV : int = 40
*)
(* Although the result of subtraction was not needed, it was still performed.
OTH, (int 5 `add` int 5) was computed only once
*)
let t2SV = let module M = EX2(CBValue) in run_cbv M.t
(*
Subtracting 100 and 10
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SV : int = 40
*)
(* * // *)
(* Call-by-need interpretation *)
(* The only difference is the interpretation of lam:
before evaluating the body, share the argument
The argument is evaluated _at most_ once
*)
module CBLazy = struct
include CBName
(* The only difference from CBName: a new interpretation of lam *)
(* Now lam shares its argument, no matter what. *)
(* This is the definition of CBNeed after all *)
let lam f = fun () ->
fun y ->
let rec yr =
ref (fun () ->
let v = y () in yr := (fun () -> v); v) in
f (fun () -> !yr ())
end
let run_cbl m = m ()
(* QUIZ: Why is this correct? Why didn't we add sharing to
add and sub and app? After all, it is they which force computations.
Shouldn't (add (int 1) (int 2)) be likewise enclosed in a thunk
that memoizes its value when forced? Currently (add (int 1) (int 2))
is a thunk but does no memoization. Is this correct?!
*)
(* We now re-evaluate the previously written tests EX0, Ex1, EX2
under the new interpretation
*)
(* Here, Lazy is just as efficient as CBV *)
let t0SL = let module M = EX0(CBLazy) in run_cbl M.t
(*
Adding 10 and 10
Adding 20 and 20
val t0SL : int = 40
*)
(* Ditto *)
let t1SL = let module M = EX1(CBLazy) in run_cbl M.t
(*
Subtracting 20 and 10
Subtracting 10 and 5
Adding 5 and 5
Adding 10 and 10
Adding 10 and 20
Adding 10 and 30
val t1SL : int = 40
*)
(* Now, Lazy is better than both CBN and CBV: subtraction was not needed,
and it was not performed.
All other expressions were needed, and evaluated once.
*)
let t2SL = let module M = EX2(CBLazy) in run_cbl M.t
(*
Adding 5 and 5
Adding 10 and 10
Adding 20 and 20
val t2SL : int = 40
*)