(*
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 *)
(* A convenient abbreviation
(could've been called `bind') *)
val let_ : 'a exp -> ('a exp -> 'b exp) -> 'b exp
end;;
(* A sample EDSL term *)
module EX0(S:EDSL) = struct
open S
let t =
(lam (fun x -> let_ (x +: x) (fun y -> 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.
*)
(* * // *)
(* An EDSL expression of the type 'a is interpreted as a OCaml value
unit -> 'a
(imagine it to be a reader monad with () as the environment).
*)
(* * // *)
(* 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 ()
let let_ x y = (lam y) %: x
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
let t = (lam (fun x ->
let_ (x +: x) (fun y ->
lam (fun z -> z +: (z +: (y +: y))))))
%: (int 10 -: int 5)
%: (int 20 -: int 10)
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
let t = (lam (fun z -> lam (fun x ->
let_ (x +: x) (fun y -> y +: y))))
%: (int 100 -: int 10)
%: (int 5 +: int 5)
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)
let let_ x y = (lam y) %: x
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 ())
let let_ x y = (lam y) %: x
end;;
let run_cbl m = m ();;
(* 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
*)