(* Higher-kinded polymorphism
arising in DSL embedding in tagless-final style
*)
(* Warm-up: a simple example whose generalization leads to the higher-kinded
polymorphism
*)
(* Simple, perhaps the simplest DSL of addition. To be generalized later *)
module type add_i = sig
type repr
val int : int -> repr
val add : repr -> repr -> repr
end
(* Sample term -- as a functor *)
module AddEx1(I:add_i) = struct
open I
let res = add (add (int 1) (int 2)) (int 3)
end
(* Define a function that uses the add interface: parameterized by the
implementation of the interface: add a term to itself n times.
*)
module NTimes(I:add_i) = struct
include I
let rec ntimes : int -> repr -> repr = fun n x ->
if n<=0 then int 0 else if n=1 then x else
add x (ntimes (n-1) x)
end
(* Usage example, using the earlier AddEx1 *)
module AddEx2(I:add_i) = struct
open NTimes(I)
module M = AddEx1(I)
let res = ntimes 3 M.res
end
(* But AddEx1, NTimes, AddEx2 are all functors. We would like terms *)
(* Thus, we would like to turn the interface abstraction from functor to
an ordinary function.
Using first-class module facility, we turn add_i (a signature) to
an ordinary type.
We use the ordinary polymorphism, to abstract over the representation type
*)
type 'r add_t = (module add_i with type repr = 'r)
(* Re-write earlier examples as terms: polymorphic terms.
Moreover, bounded-polymorphic terms: the type variable is instantiated
only to those types which have an implementation of add_i (and we pass
that implementation as the witness)
*)
(* We must write the signature though *)
let add_ex1 : type r. r add_t -> r = fun (module I) ->
I.(add (add (int 1) (int 2)) (int 3))
let rec ntimes : type r. r add_t -> int -> r -> r = fun (module I) n x ->
let open I in
if n<=0 then int 0 else if n=1 then x else
add x (ntimes (module I) (n-1) x)
let add_ex2 : type r. r add_t -> r = fun repr ->
ntimes repr 3 (add_ex1 repr)
(* we could have also used OCaml objects *)
(* Final convenience: hide the implementation passing
Here we need first-class polymorphism
*)
type add_term = {e: 'r. 'r add_t -> 'r}
(* In Coq notation,
forall repr:Type, add repr -> repr
*)
(* a bit verbose, but we fix it soon. Type annotation r add_t is required *)
let add_ex1 : add_term = {e = fun (type r) ((module I):r add_t) ->
I.(add (add (int 1) (int 2)) (int 3))}
(* But add_term is an initial add_i algebra! *)
module AddSelf : (add_i with type repr = add_term) = struct
type repr = add_term
let int n = {e = fun (type r) (module I:add_i with type repr=r) ->
I.int n}
let add {e=e1} {e=e2} =
{e = fun (type r) ((module I:add_i with type repr=r) as i) ->
I.add (e1 i) (e2 i)}
end
(* Therefore, we can write example so much simpler, and without annotations
The terms and functions have the simplest, the most straightforward
expression. They are no longer overtly polymorphic~--and so we lost
a bit of automatic extensibility: but only a bit. We can use the old terms
with an extended interface: we only need to apply the `coercion'
explicitly. We show an example later. No need to re-write the terms
themselves.
*)
let add_ex1 = AddSelf.(add (add (int 1) (int 2)) (int 3))
let rec ntimes = fun n x ->
let open AddSelf in
if n<=0 then int 0 else if n=1 then x else
add x (ntimes (n-1) x)
let add_ex2 = ntimes 3 add_ex1
(* Generalization: extend the language with booleans and the if statement.
We now get something close to the language in Chap 3 of TAPL
*)
(* Since the DSL now has types: integers and booleans, the representation
type is parameterized by the DSL type
*)
module type sym = sig
type 'a repr
val int : int -> int repr
val add : int repr -> int repr -> int repr
val iszero : int repr -> bool repr
val if_ : bool repr -> 'a repr -> 'a repr -> 'a repr
end
(* Sample term -- as a functor *)
module SymEx1(I:sym) = struct
open I
let t1 = add (add (int 1) (int 2)) (int 3) (* intermediate binding *)
let res = if_ (iszero t1) (int 0) (add t1 (int 1))
end
(* Two interpreters of sym, so we could do something with the terms we write *)
(* The first interpreter: the evaluator *)
module R : (sym with type 'a repr = 'a) = struct
type 'a repr = 'a
let int = Fun.id
let add = (+)
let iszero = (=) 0
let if_ b th el = if b then th else el
end
(* The second interpreter: a printer *)
module S : (sym with type 'a repr = string) = struct
type 'a repr = string
let paren x = "(" ^ x ^ ")"
let int x = let t = string_of_int x in if x >= 0 then t else paren t
let add e1 e2 = paren @@ e1 ^ " + " ^ e2
let iszero x = paren @@ "iszero " ^ x
let if_ b th el = "if " ^ b ^ " then " ^ th ^ " else " ^ el
end
(* We can now run the examples *)
let _ = let module M = SymEx1(R) in M.res
(* - : int = 7 *)
let _ = let module M = SymEx1(S) in M.res
(*
- : string = "if (iszero ((1 + 2) + 3)) then 0 else (((1 + 2) + 3) + 1)"
*)
(* But to write something like add_term, we need higher-kinded polymorphism! *)
(*
We need something like, in Coq-like notation,
forall A:Type, forall repr:Type -> Type, sym repr -> repr A)
Or, generalizing our previous add_term,
type 'a sym_term = {e: 'R. (module sym with type repr = 'R) -> 'a 'R}
But this requires the type variable 'R of the higher-kind, i.e.,
type constructor polymorphism. OCaml does not support it directly.
*)
(* For int type. Alas, in OCaml, a package (existential)
type may include only the
module path, not general module types. So we have to name the functor.
*)
module type symF = functor (I:sym) -> sig val res : int I.repr end
type sym_term_int = (module symF)
(* We now want to abstract over int. There are two ways of doing it. *)
(* One way: add another argument to the functor. Since functors arguments may
only be signatures, we have to introduce a trivial signature
module type typ = sig type typ end
module type symF =
functor (T:typ) (I:sym) -> sig val res : T.typ I.repr end
Although this works, we can't use it to define an ordinary polymorphic type,
because the following does not work:
type 'a sym_term = (module SymF(struct type typ='a end))
*)
(* The other way is to wrap a functor into a module
*)
module type symF = sig
type a
module Term(I:sym) : sig val res : a I.repr end
end
type 'a sym_term = (module (symF with type a = 'a))
(* SymEx1 as a term *)
(* Here, the type annotation is needed. However, we let the type of the term
to be _, as schematic variable. OCaml infers it as int
*)
let sym_ex1 : _ sym_term =
(module struct type a = int module Term = SymEx1 end)
(* evaluation: a bit cumbersome *)
let _ = let module N = (val sym_ex1) in
let module M = N.Term(R) in M.res
(* sym_term can be made initial algebra *)
module SymSelf : (sym with type 'a repr = 'a sym_term) = struct
type 'a repr = 'a sym_term
let int : int -> int repr = fun n ->
let module M(I:sym) = struct let res = I.int n end in
(module struct type a = int module Term = M end)
let add : int repr -> int repr -> int repr = fun (module E1) (module E2) ->
let module M(I:sym) =
struct module E1T = E1.Term(I) module E2T = E2.Term(I)
let res = I.add (E1T.res) (E2T.res)
end in
(module struct type a = int module Term = M end)
let iszero : int repr -> bool repr = fun (module E) ->
let module M(I:sym) =
struct module ET = E.Term(I)
let res = I.iszero (ET.res)
end in
(module struct type a = bool module Term = M end)
let if_ : type ar. bool repr -> ar repr -> ar repr -> ar repr =
fun (module E) (module E1) (module E2) ->
let module M(I:sym) =
struct module ET = E.Term(I)
module E1T = E1.Term(I) module E2T = E2.Term(I)
let res = I.if_ (ET.res) (E1T.res) (E2T.res)
end in
(module struct type a = ar module Term = M end)
end
(* That was a mouthful. But now writing sym terms becomes much easier
And no type annotation is required
*)
let sym_ex1 =
let open SymSelf in
let t1 = add (add (int 1) (int 2)) (int 3) in (* intermediate binding *)
if_ (iszero t1) (int 0) (add t1 (int 1))
let _ = let module N = (val sym_ex1) in
let module M = N.Term(R) in M.res
let _ = let module N = (val sym_ex1) in
let module M = N.Term(S) in M.res
(* A different way to make SymEx1 term-level
We want to write something like
let sym_ex1 (module I:sym) : int I.repr = ...
but it doesn't work because `The type constructor I.repr would escape its scope'
Indeed, I is scoped only over the body of sym_ex1, but the result type
of sym_ex1 has the global scope.
With higher-kind type variables, we could have written
let sym_ex1 (module I:(sym with type 'a repr = 'a 'I)) : int 'I = ...
which solves the scoping problem because 'I is in global scope.
*)
(* A different way of accomplishing the same. First, the simplest way.
All its operations are the identity
*)
module HK : sig
type ('a,'d) hk (* abstract *)
module MakeHK : functor (S: sig type 'a t end) -> sig
type anyt (* also abstract *)
val inj : 'a S.t -> ('a,anyt) hk
val prj : ('a,anyt) hk -> 'a S.t
end
end = struct
type ('a,'d) hk = 'd
module MakeHK(S:sig type 'a t end) = struct
type anyt = Obj.t
let inj : 'a S.t -> ('a,anyt) hk = Obj.repr
let prj : ('a,anyt) hk -> 'a S.t = Obj.obj
end
end
module type sym_hk = sig
include sym
include module type of HK.MakeHK(struct type 'a t = 'a repr end)
end
(* Now we can write sym_ex1 as we wanted *)
let sym_ext1hk (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
let open I in
add (add (int 1) (int 2)) (int 3) |> inj (* intermediate term *)
let sym_ex1hk (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
let open I in
let t1 = sym_ext1hk (module I) |> prj in (* reuse the earlier term *)
if_ (iszero t1) (int 0) (add t1 (int 1)) |> inj
(* Usage example *)
module RHK = struct
include R
include HK.MakeHK(struct type 'a t = 'a repr end)
end
let _ = sym_ex1hk (module RHK) |> RHK.prj
(* - : int = 7 *)
module SHK = struct
include S
include HK.MakeHK(struct type 'a t = 'a repr end)
end
(* expected error
let _ = sym_ex1hk (module SHK) |> RHK.prj
*)
let _ = sym_ex1hk (module SHK) |> SHK.prj
(*
- : string = "if (iszero ((1 + 2) + 3)) then 0 else (((1 + 2) + 3) + 1)"
*)
(* A different way to implement HK, without magic *)
type 'a trep = ..
type ('a,'b) eq = Refl : ('a,'a) eq
type 'a prj = {prj: 'b. 'b trep -> ('a,'b) eq option}
module TypeCmp(S:sig type t end) = struct
type 'a trep += Tag: S.t trep
let eqp : type b.b trep -> (S.t,b) eq option = function
| Tag -> Some Refl
| _ -> None
end
module HK = struct
type ('a,'d) hk = 'a trep * 'd
module MakeHK(S:sig type 'a t end) : sig
type anyt
val inj : 'a S.t -> ('a,anyt) hk
val prj : ('a,anyt) hk -> 'a S.t
end = struct
type anyt = Ex : 'a prj * 'a S.t -> anyt
let inj : type a. a S.t -> (a,anyt) hk = fun x ->
let module M = TypeCmp(struct type t=a end) in
(M.Tag, Ex ({prj=M.eqp},x))
let prj : type a. (a,anyt) hk -> a S.t = fun (tr,Ex (trp,x)) ->
match trp.prj tr with Some Refl -> x | _ -> assert false
end
end
module type sym_hk = sig
include sym
include module type of HK.MakeHK(struct type 'a t = 'a repr end)
end
(* Now we can write sym_ex1 as we wanted *)
let sym_ext1hk (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
let open I in
add (add (int 1) (int 2)) (int 3) |> inj (* intermediate term *)
let sym_ex1hk (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
let open I in
let t1 = sym_ext1hk (module I) |> prj in (* reuse the earlier term *)
if_ (iszero t1) (int 0) (add t1 (int 1)) |> inj
(* Usage example *)
module RHK = struct
include R
include HK.MakeHK(struct type 'a t = 'a repr end)
end
let _ = sym_ex1hk (module RHK) |> RHK.prj
(* - : int = 7 *)
module SHK = struct
include S
include HK.MakeHK(struct type 'a t = 'a repr end)
end
(* expected error
let _ = sym_ex1hk (module SHK) |> RHK.prj;;
*)
let _ = sym_ex1hk (module SHK) |> SHK.prj
(*
- : string = "if (iszero ((1 + 2) + 3)) then 0 else (((1 + 2) + 3) + 1)"
*)
;;