(*
The modern reconstruction of
Extensible Denotational Language Specifications
Robert Cartwright, Matthias Felleisen
Theor. Aspects of Computer Software, 1994
and re-formulating their approach in terms of Extensible Effects.
The code for the HOPE presentation
*)
(*
* ------------------------------------------------------------------------
* Basic Framework: Fig 3 of EDLS
* As in EDLS (and common in denotational semantics), it is untyped.
* The typed version is possible -- it is essentially extensible effects.
*)
(* the domain of values, empty for now *)
(* It is the domain of values, so it has no bottom *)
(* We rely on extensible data types of OCaml. This is not a radical
new feature. Rather, it is a mere generalization of one extensible
data type that has been in ML for a long time: exceptions.
We could have used exceptions, albeit sacrificing clarity.
*)
type v = ..
(* The domain of effects. For now, there is one effect: error.
We parameterize the error by the error message. The parameterization
is not essential (so that Error may be considered a single effect)
but very convenient.
*)
type e = ..
type e += Error of string
(* Domain of denotations of expressions: computations. It should include bottom.
But we cannot represent it in OCaml and just wave hands about.
Anyway, OCaml values are all appropriately lifted and OCaml functions
are continuous.
The meaning of a computation is either a value or an effect request
(or, implicitly, bottom)
*)
type c = V of v | FX of e * (v -> c)
(* It is called inAC in EDLS *)
let send: e -> c = fun e -> FX(e,(fun x -> V x))
let error : string -> c = fun msg -> send (Error msg)
(* the function lift defined below also belongs to the basic framework *)
(*
* ------------------------------------------------------------------------
* First language: integers
*)
(* Language spec *)
module type Int = sig
type d (* representation domain *)
val int: int -> d
val (+): d -> d -> d
end
(* Examples: the first term in our simple language *)
module TInc(S:Int) = struct
open S
let res = (int 2 + int 3) + int 4
end
(* Implementation in terms of c *)
module RInt = struct
type v += VInt of int (* add integers to our value domain *)
type d = c
let int x = V (VInt x)
let rec (+) x y = match (x,y) with
| (V (VInt x), V (VInt y)) -> V (VInt (Pervasives.(x+y)))
| (V _, V _) -> error "addition type error"
| (FX (e,k),t) -> FX (e,fun x -> k x + t)
| (t,FX (e,k)) -> FX (e,fun x -> t + k x)
end
(* We now can evaluate our example *)
let V(RInt.VInt 9) = let module M = TInc(RInt) in M.res
(*
* ------------------------------------------------------------------------
* First extension: if-then-else
*)
(* Add equality and the if-expression *)
module type If = sig
include Int
val eq: d -> d -> d
val if_: d -> d -> d -> d
end
(* Example, reusing the earlier TInc *)
module TIf(S:If) = struct
open S
let tinc = let module M = TInc(S) in M.res (* earlier term*)
let res =
if_ (eq (int 3) tinc) (int 10) (tinc + int 1)
end
(* Implementation, reusing the earlier RInt *)
module RIf = struct
include RInt
type v += VBool of bool (* add booleans to our value domain *)
let rec eq x y = match (x,y) with
| (V (VInt x), V (VInt y)) -> V (VBool (Pervasives.(x=y)))
| (V _, V _) -> error "eq type error"
| (FX (e,k),t) -> FX (e,fun x -> eq (k x) t)
| (t,FX (e,k)) -> FX (e,fun x -> eq t (k x))
end
(* It becomes repetitive: the last two lines of eq are essentially the same
as those of (+), dealing with effect propagation. We can factor them out,
defining the following. It is called `handler' on Fig 3 of EDLS.
It has the same signature is monadic bind. We do not care for the right
unit law, however.
*)
let rec lift: c -> (v -> c) -> c = fun c k -> match c with
| V x -> k x
| FX (e,k1) -> FX (e, fun x -> lift (k1 x) k)
;;
(* Extending lift to two arguments, by nesting *)
let lift2: c -> c -> ((v*v) -> c) -> c = fun c1 c2 k ->
lift c1 @@ fun x ->
lift c2 @@ fun y ->
k (x,y)
(* Factoring out the effect propagation *)
module RIf = struct
include RInt
type v += VBool of bool (* add booleans to our value domain *)
let eq x y = lift2 x y @@ function
| (VInt x, VInt y) -> V (VBool (Pervasives.(x=y)))
| (_, _) -> error "eq type error"
let if_ t t1 t2 = lift t @@ function
| VBool true -> t1
| VBool false -> t2
| _ -> error "if_ type error"
end
(* The earlier example works just as it is with the extended RIf
semantics.
*)
let V (RInt.VInt 9) = let module M = TInc(RIf) in M.res
let V (RInt.VInt 10) =
let module M = TIf(RIf) in M.res
(* More examples. We don't have to introduce functors *)
(* Demonstrating that our if_ works correctly, even in the presence of
errors *)
let V (RInt.VInt 11) =
let open RIf in
int 1 + if_ (eq (int 1 + int 2) (int 3)) (int 10) (error "Bang!")
let FX (Error "Bang!", _) =
let open RIf in
int 1 + if_ (eq (int 1 + int 2) (int 4)) (int 10) (error "Bang!")
;;
(*
* ------------------------------------------------------------------------
* Adding state
*)
module type State = sig
type d
val get: d
val put: d -> d
end
(* Adding State to the previous features since it is not that useful
on its own
*)
module type StatePlus = sig
include If
include (State with type d := d)
end
module TSt(S:StatePlus) = struct
open S
let tinc = let module M = TInc(S) in M.res (* earlier term*)
let res = if_ (eq (int 3) (put tinc))
(put (int 20))
(put (int 1 + get))
end
(* Introduce new effect labels. It sounds easy at first *)
module RState = struct
include RIf
type e += Get | Put of v
let get = send Get
let put t = lift t @@ fun v -> send (Put v)
end
(* That is the correct denotation, but not the one we have expected *)
let FX (RState.Put (RInt.VInt 9), _) =
let module M = TSt(RState) in M.res
(* We need the observation function, giving the meaning of the whole program
So far, we had the meaning function M (Fig 3 of EDLS), the meaning of
expressions. Now we need a function to give a meaning to whole programs.
*)
(* We need to handle the State requests. *)
module RState = struct
include RIf
type e += Get | Put of v
let get = send Get
let put t = lift t @@ fun v -> send (Put v)
let rec observe: v -> c -> c = fun state -> function
| V x -> V x
| FX (Get,k) -> observe state (k state)
| FX (Put state,k) -> observe state (k state)
| FX (e,k) -> FX (e, fun x -> observe state (k x))
end
let V (RInt.VInt 10) =
let module M = TSt(RState) in
RState.(observe (VInt 0) M.res)
(* One may observe that 'observe' appears in RState but not in
the State signature. So, it is `meta-theoretic' so to speak and
exists outside of the object language -- literally following EDLS
(where it is called admin, in Fig 3)
One may wonder though why not to make observe a part of the language
proper. Then we get handlers!
And we will be doing something like this next.
*)
(*
* ------------------------------------------------------------------------
* Adding first-class functions
*)
module type Lambda = sig
type d
type varname = string
val var: varname -> d
val lam: varname -> d -> d
val ($$): d -> d -> d (* application, left associative *)
end
(* Adding Lambda to the language of Int and conditional *)
module type LamInt = sig
include If
include (Lambda with type d := d)
end
module TLam(S:LamInt) = struct
open S
let tinc = let module M = TInc(S) in M.res (* earlier term*)
let res0 = lam "x" (var "x" + int 1)
let res01 = res0 $$ tinc
let res1 = lam "x" @@ lam "y" @@
if_ (eq (var "x") (var "y")) (var "x") (var "y" + int 1)
let res11 = res1 $$ int 1 $$ int 2
(* Higher-order functions *)
let res2 = (lam "z" (lam "x" (var "z" $$ var "x"))) $$
(res1 $$ int 1) $$ (* partial application of res1 *)
(int 2)
end
(* Implementation: lexical scope, call-by-value, left-to-right *)
let rec lookup_def: 'w -> 'a -> ('a * 'b) list -> ('b -> 'w) -> 'w =
fun def x l k -> match l with
| [] -> def
| (h,v)::_ when x = h -> k v
| _::t -> lookup_def def x t k
module CBV = struct
include RIf
type v += VFun of (v -> c) (* denotations of functions *)
(* Alternative choice: a closure
data structure: defunctionalization*)
type varname = string
type env = (varname * v) list
type e += EVar of varname (* dereferencing a variable: *)
(* generalization of Get *)
| EClosure of varname * d (* Creating a closure *)
(* Variable dereference and closure creation. Lambda is an effect! *)
let var x = send (EVar x)
let lam v body = send (EClosure (v,body))
let ($$) f x = lift2 f x @@ function
| (VFun f,x) -> f x
| _ -> error "app type error"
let rec observe : env -> c -> c = fun env -> function
| V x -> V x
| FX (EVar var,k) -> lookup_def (error @@ "unbound var " ^ var) var env @@
fun v -> observe env (k v)
| FX (EClosure (var,body), k) ->
let v = VFun (fun x -> observe ((var,x)::env) body) in
observe env (k v)
| FX (e,k) -> FX (e, fun x -> observe env (k x))
end
(* Test cases *)
let [V (CBV.VFun _); V (RInt.VInt 10); V (CBV.VFun _); V (RInt.VInt 3);
V (RInt.VInt 3)]
=
let module M = TLam(CBV) in
CBV.(List.map (observe []) [M.res0; M.res01; M.res1; M.res11; M.res2])
(* Other calling conventions (call-by-name, etc) and dynamic scope are
left as an exercise to the reader
*)
;;
(*
* ------------------------------------------------------------------------
* Higher-order plus State: combining the existing features
*)
(* The order of 'include' statements is immaterial *)
module type LamState = sig
include If
include (State with type d := d)
include (Lambda with type d := d)
end
module TLamSt(S:LamState) = struct
open S
let incf = let module M = TLam(S) in M.res0 (* increment function *)
let incs = put (incf $$ get)
(* incf but counting the invocation in the state *)
let incf = lam "x" ((lam "_" @@ var "x" + int 10) $$ incs)
let c2 = lam "f" @@ lam "z" @@ var "f" $$ (var "f" $$ var "z")
let res = c2 $$ incf $$ (int 100) + get
end
(* But we do not need any functors! *)
let V (RInt.VInt 122) =
let open RState in
let open CBV in
let incf = let module M = TLam(CBV) in M.res0 (* increment function *) in
let incs = put (incf $$ get) in
(* incf but counting the invocation in the state *)
let incf = lam "x" ((lam "_" @@ var "x" + int 10) $$ incs) in
let c2 = lam "f" @@ lam "z" (var "f" $$ (var "f" $$ var "z")) in
let res = (c2 $$ incf $$ (int 100)) + get
in
RState.observe (RInt.VInt 0) @@ CBV.observe [] res
(*
#use "edlsng.ml";;
*)
let _ = print_endline "All Done"
;;