Here is another kind of example I've boiled down as much as I could (it is somewhat related to the Leibniz equality).
Oleg Kiselyov and Jeremy Yallop ( http://okmij.org/ftp/ML/first-class-modules/ ) have noticed that first-class modules could be leveraged to produce an variant of the Finally Tagless approach (which consist in replacing the use of a gadt by a typeclass signature, in Haskell, to denote expressions). I like to call it Initially Tagless.
The idea is to start with a signature representing your language, a field for each language construct. Here, the language admits two types (int and bool) and one operation on each:
module type S = sig
type 'a t
val int : int -> int t
val bool : bool -> bool t
val (+) : int t -> int t -> int t
val if_ : bool t -> 'a t -> 'a t -> 'a t
end
An interpreter for the language is a module of type S. The type of expressions [a Expr.t] is, then, defined as that of things which, for any interpretor X, can be interpreted into an [a X.t]. Here goes the code in OCaml 3.12, you might notice it is very repetitive:
module Expr : sig
include S
module Interp (X:S) : sig
val x : 'a t -> 'a X.t
end
end = struct
module type T = sig
type a
module Interp (X:S) : sig
val x : a X.t
end
end
type 'a t = (module T with type a = 'a)
module Interp (X:S) = struct
let x (type w) (e:w t) : w X.t=
let module E = (val e : T with type a = w) in
let module IE = E.Interp(X) in
IE.x
end
let int x =
let module M = struct
type a = int
module Interp (X:S) = struct
let x = X.int x
end
end in
(module M : T with type a = int)
let bool x =
let module M = struct
type a = bool
module Interp (X:S) = struct
let x = X.bool x
end
end in
(module M : T with type a = bool)
let (+) n p =
let module M = struct
type a = int
module Interp (X:S) = struct
let x =
let module MN = (val n : T with type a=int) in
let module IN = MN.Interp(X) in
let n' = IN.x in
let module MP = (val p : T with type a=int) in
let module IP = MN.Interp(X) in
let p' = IP.x in
X.(n'+p')
end
end in
(module M : T with type a = int)
let if_ (type w) b (t:w t) (e:w t) =
let module M = struct
type a = w
module Interp (X:S) = struct
let x =
let module MB = (val b : T with type a=bool) in
let module IB = MB.Interp(X) in
let b' = IB.x in
let module MT = (val t : T with type a=w) in
let module IT = MT.Interp(X) in
let t' = IT.x in
let module ME = (val e : T with type a=w) in
let module IE = ME.Interp(X) in
let e' = IE.x in
X.if_ b' t' e'
end
end in
(module M : T with type a = w)
end
My proposition of syntax aims at dealing gracefully with some of the repetitive parts. It would look something like :
module Expr : sig
include S
val interp : (X:S) => 'a t -> 'a X.t
end = struct
module type T = sig
type a
val interp : (X:S) => a X.t
end
type 'a t = (module T with type a = 'a)
let interp {{X:S}} (type w) (e:w t) : w X.t =
let module E = (val e : T with type a = w) in
E.interp {{X}}
let int x =
let module M = struct
type a = int
let interp {{X:S}} = X.int x
end in
(module M : T with type a = int)
let bool x =
let module M = struct
type a = bool
let interp {{X:S}} = X.bool x
end in
(module M : T with type a = bool)
let (+) n p =
let module M = struct
type a = int
let interp {{X:S}} =
let module MN = (val n : T with type a=int) in
let module MP = (val p : T with type a=int) in
X.((MN.interp {{X:S}})+(MP.interp {{X:S}})
end
end in
(module M : T with type a = int)
let if_ (type w) b (t:w t) (e:w t) =
let module M = struct
type a = w
let interp {{X:S}} =
let module MB = (val b : T with type a=bool) in
let module MT = (val t : T with type a=w) in
let module ME = (val e : T with type a=w) in
X.if_ (MB.interp{{X:S}}) (MT.interp{{X:S}}) (ME.interp{{X:S}})
end in
(module M : T with type a = w)
end
The code could be shrinked even more dramatically if we were allowed to define [Expr.t] directly as
type 'a t = (X:S) => 'a t
But I doubt it would be easy to make that possible. In my proposition, this is the same as
type 'a t = (X:S) => 'b t
Which is unfortunate, but at least is quite compatible with how first-class modules are dealt with in the current versions of OCaml.
--
Arnaud