ind_ocaml.ml

module type T = sig
  module type S
end

module T = struct
  module type S = T
end

module type K_Bool = functor (X : T) (Y : T) -> T

module K_true = functor (X : T) (Y : T) -> X
module K_false = functor (X : T) (Y : T) -> Y

module T_Bool = struct
  module type S = sig
    module K : K_Bool

    module I : functor
      (P : functor (_ : K_Bool) -> T)
      (X : P(K_true).S)
      (Y : P(K_false).S)
      -> P(K).S
  end
end

module T_true = struct
  module K = K_true

  module I =
  functor
    (P : functor (_ : K_Bool) -> T)
    (X : P(K_true).S)
    (Y : P(K_false).S)
    ->
    X
end

module T_false = struct
  module K = K_false

  module I =
  functor
    (P : functor (_ : K_Bool) -> T)
    (X : P(K_true).S)
    (Y : P(K_false).S)
    ->
    Y
end

module Ind_bool =
functor
  (B : T_Bool.S)
  (P : functor (_ : K_Bool) -> T)
  (X : P(K_true).S)
  (Y : P(K_false).S)
  ->
  B.I (P) (X) (Y)

module Either (A : T) (B : T) = struct
  module type S = functor
    (K : T)
    (_ : functor (Tag : T_Bool.S) (_ : Tag.K(A)(B).S) -> K.S)
    -> K.S
end

module Left (A : T) (B : T) (X : A.S) =
functor
  (K : T)
  (F : functor (Tag : T_Bool.S) (_ : Tag.K(A)(B).S) -> K.S)
  ->
  F (T_true) (X)

module Right (A : T) (B : T) (X : B.S) =
functor
  (K : T)
  (F : functor (Tag : T_Bool.S) (_ : Tag.K(A)(B).S) -> K.S)
  ->
  F (T_false) (X)

module Match
    (A : T)
    (B : T)
    (K : T) (L : functor (_ : A.S) -> K.S) (R : functor (_ : B.S) -> K.S)
    (E : Either(A)(B).S) =
  E
    (K)
    (functor
       (Tag : T_Bool.S)
       (Content : Tag.K(A)(B).S)
       ->
       Ind_bool
         (Tag)
         (functor
            (Tag_K : K_Bool)
            ->
            struct
              module type S = functor (Content : Tag_K(A)(B).S) -> K.S
            end)
         (L)
         (R)
         (Content))

(* TODO: example *)
module Int = struct
  module type S = sig
    val x : int
  end
end

module String = struct
  module type S = sig
    val x : string
  end
end

module E =
  Left (Int) (String)
    (struct
      let x = 1
    end)

module To_string (E : Either(Int)(String).S) =
  Match (Int) (String) (String)
    (functor
       (Content : Int.S)
       ->
       struct
         let x = string_of_int Content.x
       end)
    (functor (Content : String.S) -> Content)
    (E)

let () =
  print_endline
    (let module M =
       To_string
         (Left (Int) (String)
            (struct
              let x = 1
            end)) in
    M.x)

let () =
  print_endline
    (let module M =
       To_string
         (Right (Int) (String)
            (struct
              let x = "hi"
            end)) in
    M.x)