(*
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.
*)
(* * // *)
(* First is a meta-circular interpretation *)
module MetaCirc = struct
type 'a exp = 'a (* representation of terms *)
type ('a,'b) arrow = 'a -> 'b (* The arrow type *)
let int x = x
let (+:) = (+)
let (-:) = (-)
let lam f = f
let (%:) f x = f x
let let_ x y = (lam y) %: 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
(* * // *)
(* 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;;
(* 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;;
(* 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;;
(* * // *)
(* 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;;
(* * // *)
(* 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 ();;
(* 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;;
(* Ditto *)
let t1SL = let module M = EX1(CBLazy) in run_cbl M.t;;
(* 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;;
(* Relationship with RPC: consider subtraction is `expensive' and
performed remotely
*)