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