(* A generic programming library for OCaml, based on first class modules.

   This follows in a line of work on type-encoded values in ML, which includes

     Encoding Types in ML-Like Languages.
     Zhe Yang
     ICFP 1998

     Generics for the working ML'er
     Vesa Karvonen
     ML Workshop 2007

     A generic programming toolkit for PADS/ML
     Mary Fernández, Kathleen Fisher, J. Nathan Foster, Michael Greenberg and Yitzhak Mandelbaum
     PADL 2008

[TODO: something about the differences between those papers and the present work]

*)

(* OCaml provides binary products and unit as standard, but not binary sums or
   the empty type.  Here are definitions of the latter two. *)
type ('a, 'b) either = Left of 'a | Right of 'b
type zero = { absurd : 'a . 'a}

(* A fixpoint operator *)
type 'a fix = Fix of ('a fix -> 'a)

(* The Interpretation signature gives the type of interpetations of type
   representations.  More simply, it gives the type of generic function
   implementations.

   An implementation of this signature is a generic function over all
   "representable" types.  (A type is representable if it can be constructed
   using the value fields in this signature.  "Representable" means,
   approximately, "first order and regular": most user-defined algebraic types
   are representable, but class types and functions are not.)

   See Show and Eq for example implementations of the Interpretation
   interface.  Each of these modules instantiates the type constructor 't'
   with a definition that is suitable for the type of the generic function.

   * Show has 'a t equal to 'a -> string, the type of functions that print
     values of type 'a.

   * Eq has 'a t equal to 'a -> 'a -> bool, the type of equality predicates
     for values of type 'a.

   Since we can't provide n-ary constructors for every possible n, several of
   the constructors (tuple, record, variant) accept an isomorphism as
   argument.  In the tuple case, for example, the isomorphism can be used to
   convert between nested pairs and an n-tuple.
*)
module type Interpretation =
sig
  type 'a tc

  (* Primitive types *)
  val int    : int tc
  val unit   : unit tc
  val string : string tc

  (* Tuples *)
  val ( * ) : 'a tc -> 'b tc -> ('a * 'b) tc
  val tuple : ('t -> 'pairs) -> ('pairs -> 't) -> 'pairs tc -> 't tc

  (* Records *)
  val unitr : unit tc
  val ( *:) : [ `Mutable of string | `Immutable of string] -> 'a tc -> 'a tc
  val (&) : 'a tc -> 'row tc -> ('a * 'row) tc
  val record : string -> ('r -> 'row) -> ('row -> 'r) -> 'row tc -> 'r tc

  (* Variants *)
  val (+:) : string -> 'a tc -> 'a tc
  val nil  : zero tc
  val (||) : 'a tc -> 'row tc -> ('a, 'row) either tc
  val variant : string -> ('s -> 'row) -> ('row -> 's) -> 'row tc -> 's tc
    
  (* Fixpoints *)
  val fix : 'a tc fix -> 'a tc
end

(* A type representation is a function from interpretations to generic
   functions at a particular type.  For example, a type representation for int
   is a function that takes the Show interpretation to a printer for ints, and
   the Eq representation to an equality predicate for ints, and so on.
*)
module type Repr =
sig
  type a
  module Interpret (I : Interpretation) :
  sig
    val result : a I.tc
  end
end

(* The repr type alias is just a convenient shorthand. *)
type 'a repr = (module Repr with type a = 'a)

(* "Smart constructors" for type representations.  Without these we'd have to
   write complicated module expressions every time we wanted to construct a
   type representation.  Instead, we write the complicated module expressions
   once for all.  They follow a straightforward pattern.
*)
let int : int repr =
  (module
     struct
        type a = int
        module Interpret (I : Interpretation) =
        struct
          let result = I.int
        end
      end : Repr with type a = int)

let unit : unit repr = 
  (module
     struct
        type a = unit
        module Interpret (I : Interpretation) =
        struct
          let result = I.unit
        end
      end : Repr with type a = unit)

let string : string repr =
  (module
     struct
        type a = string
        module Interpret (I : Interpretation) =
        struct
          let result = I.string
        end
      end : Repr with type a = string)

(* Tuples *)
let ( * ) : 'a 'b. 'a repr -> 'b repr -> ('a * 'b) repr
  = fun (type a') (type b') arepr brepr ->
  (module
     struct
        type a = a' * b'
        module A = (val arepr : Repr with type a = a')
        module B = (val brepr : Repr with type a = b')
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          module BI = B.Interpret(I)
          open I
          let result = AI.result * BI.result
        end
      end : Repr with type a = a' * b')

let tuple : 't 'pairs. ('t -> 'pairs) -> ('pairs -> 't) -> 'pairs repr -> 't repr
  = fun (type t) (type pairs) fromtup totup pair_rep ->
  (module
     struct
        type a = t
        module A = (val pair_rep : Repr with type a = pairs)
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          let result = I.tuple fromtup totup AI.result
        end
      end : Repr with type a = t)
    
(* Records *)
let unitr : unit repr = 
  (module
     struct
        type a = unit
        module Interpret (I : Interpretation) =
        struct
          let result = I.unitr
        end
      end : Repr with type a = unit)

let ( *:) : 'a. [ `Mutable of string | `Immutable of string] -> 'a repr -> 'a repr =
  fun (type t) label arepr ->
  (module
     struct
        type a = t
        module A = (val arepr : Repr with type a = t)
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          let result = I.( *:) label AI.result
        end
      end : Repr with type a = t)

let (&) : 'a 'row. 'a repr -> 'row repr -> ('a * 'row) repr =
  fun (type a') (type row') arepr brepr ->
  (module
     struct
        type a = a' * row'
        module A = (val arepr : Repr with type a = a')
        module R = (val brepr : Repr with type a = row')
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          module RI = R.Interpret(I)
          open I
          let result = AI.result & RI.result
        end
      end : Repr with type a = a' * row')

let record : 'r 'row. string -> ('r -> 'row) -> ('row -> 'r) -> 'row repr -> 'r repr =
  fun (type r) (type row) name fromrec torec rec_rep ->
  (module
     struct
        type a = r
        module A = (val rec_rep : Repr with type a = row)
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          let result = I.record name fromrec torec AI.result
        end
      end : Repr with type a = r)

(* Variants *)
let (+:) : 'a. string -> 'a repr -> 'a repr =
  fun (type t) label arepr ->
  (module
     struct
        type a = t
        module A = (val arepr : Repr with type a = t)
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          let result = I.( +:) label AI.result
        end
      end : Repr with type a = t)

let nil : zero repr =
  (module
     struct
        type a = zero
        module Interpret (I : Interpretation) =
        struct
          let result = I.nil
        end
      end : Repr with type a = zero)

let (||) : 'a 'row. 'a repr -> 'row repr -> ('a, 'row) either repr =
  fun (type a') (type row') arepr brepr ->
  (module
     struct
        type a = (a', row') either
        module A = (val arepr : Repr with type a = a')
        module R = (val brepr : Repr with type a = row')
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          module RI = R.Interpret(I)
          open I
          let result = AI.result || RI.result
        end
      end : Repr with type a = (a', row') either)

let variant : string -> ('s -> 'row) -> ('row -> 's) -> 'row repr -> 's repr =
  fun (type r) (type row) name fromvar tovar var_rep ->
  (module
     struct
        type a = r
        module A = (val var_rep : Repr with type a = row)
        module Interpret (I : Interpretation) =
        struct
          module AI = A.Interpret(I)
          let result = I.variant name fromvar tovar AI.result
        end
      end : Repr with type a = r)

let fix : 'a. 'a repr fix -> 'a repr =
  fun (type t) (Fix fix as fx) ->
    (module
     struct
       type a = t
       module F = (val fix fx : Repr with type a = t)
       module Interpret (I : Interpretation) =
       struct
         module FI = F.Interpret(I)
         let result : t I.tc = FI.result
       end
     end : Repr with type a = t)

(* An example representation for a user-defined type. *)
let option : 'a. 'a repr -> 'a option repr =
  fun (type t) arepr ->
     variant "option"
       (function
          | None -> Left ()
          | Some v -> Right (Left v))
       (function
          | Left v -> None
          | Right (Left v) -> Some v
          | Right (Right {absurd}) -> absurd)
       ("None" +: unit
     || "Some" +: arepr
     || nil)

(* NB: we should be able to write this using the top-level combinators
   defined above, but the attempt to do so below (list') results in
   an infinite loop.  We'll stick with this version for the moment. *)
let list : 'a. 'a repr -> 'a list repr =
  fun (type s) arepr ->
    (module
     struct
       type a = s list
       module A = (val arepr : Repr with type a = s)
       module Interpret (I : Interpretation) =
       struct
         open I
         module AI = A.Interpret(I)
         open I
         let result : s list I.tc =
           fix
             (Fix
                (fun tlist ->
                   variant "list"
                     (function 
                        | [] -> Left ()
                        | x :: xs -> Right (Left (x, xs)))
                     (function 
                        | Left () -> []
                        | Right (Left (x, xs)) -> x :: xs
                        | Right (Right {absurd}) -> absurd)
                     ("[]" +: unit || "::" +: (AI.result * fix tlist) || nil)))
       end
     end : Repr with type a = s list)

(* NB: this version results in an infinite loop.  We'll stick with the
   more verbose version above for the moment. *)
let list' : 'a. 'a repr -> 'a list repr =
  fun (type s) arepr ->
    fix
      (Fix (fun tlist -> 
              (variant "list"
                 (function 
                      [] -> Left ()
                    | x :: xs -> Right (Left (x, xs)))
                 (function 
                      Left () -> []
                    | Right (Left (x, xs)) -> x :: xs
                    | Right (Right {absurd}) -> absurd)
                 ("[]" +: unit || "::" +: arepr *  fix tlist || nil))))

(* 

   Our first example of a generic function.  Note that 'a Interpretation.t is
   equal here to 'a -> string, the type of printers for values of type 'a.
   The implementation of each field then follows straightforwardly from its
   type.

   It's possible to give a prettier printer, of course, but this gives the
   idea.
*)
module Show
  : Interpretation with type 'a tc = 'a -> string =
struct
  type 'a tc = 'a -> string

  (* Primitive types *)
  let int     = string_of_int
  let unit _  = "()"
  let string s = "\""^ String.escaped s ^"\""

  (* Tuples *)
  let ( * ) f g (a, b) = "(" ^ f a ^ "," ^ g b ^ ")"
  let tuple fromtup totup show_tuple v =
    "(" ^ show_tuple (fromtup v) ^ ")"

  (* Records *)
  let unitr () = ""
  let ( *:) label show_field field =
    match label with
        `Mutable label
      | `Immutable label -> label ^ " : " ^ show_field field
  let (&) show_field show_fields (f, fields) =
    show_field f ^ "; " ^ show_fields fields
  let record name fromrec torec show_fieldlist record = 
    "{" ^ show_fieldlist (fromrec record) ^ "}"

  (* Variants *)
  let nil v = v.absurd
  let (+:) ctor show_arg arg = 
    ctor ^ " " ^ show_arg arg
  let (||) showl showr = function
    | Left v -> showl v
    | Right v -> showr v
  let variant name fromvar tovar show_variant v = 
    show_variant (fromvar v)

  (* Fixpoints *)
  let fix (Fix fix as fx) fixed =
      fix fx fixed
end

(* A second generic function: equality predicates.  We use SML-style equality
   rather than OCaml-style: equality is structural for "value" types and
   physical for "reference" types. *)
module Eq
  : Interpretation with type 'a tc = 'a -> 'a -> bool =
struct
  type 'a tc = 'a -> 'a -> bool

  (* For records with mutable fields we use physical equality.  We start off
     by assuming structural equality, raising the Mutable exception if we
     encounter a mutable field.  The `record' function catches the Mutable
     exception and falls back to a physical equality test.
  *)
  exception Mutable

  (* Primitive types *)
  let int      = (=)
  let unit _ _ = true
  let string   = (=)

  (* Tuples *)
  let ( * ) eq1 eq2 (l1, l2) (r1, r2) =
    eq1 l1 r1 && eq2 l2 r2
  let tuple fromtup totup tupeq l r =
    tupeq (fromtup l) (fromtup r)

  (* Records *)
  let unitr _ _ = true

  let ( *:) label fieldeq = match label with
      `Mutable _ -> raise Mutable
    | `Immutable _ -> fieldeq

  let (&) fieldeq fieldlisteq (fieldl, fieldlistl) (fieldr, fieldlistr) =
    fieldeq fieldl fieldr && fieldlisteq fieldlistl fieldlistr

  let record _name fromrec torec fields_eq l r =
    try
      fields_eq (fromrec l) (fromrec r)
    with Mutable ->
      l == r

  (* Variants *)
  let nil l r = l.absurd
  let (+:) ctor eqc l r = eqc l r
  let (||) eqc eqrow l r =
    match l, r with
      | Left l, Left r -> eqc l r
      | Right l, Right r -> eqrow l r
      | _ -> false
  let variant _name fromvar tovar vareq l r =
    vareq (fromvar l) (fromvar r)

  (* Fixpoints *)
  let fix (Fix fix as fx) fixed =
    fix fx fixed
end

type 'dom memoizer = { memoizer: 'cod. ('dom -> 'cod) -> ('dom -> 'cod) }

module TDM
  : Interpretation with type 'a tc = 'a memoizer =
struct
  type 'a tc = 'a memoizer

  (* Primitive types *)
  let int : int tc
    = { memoizer = 
        fun f -> 
          let mref = Hashtbl.create 10 in
          fun x ->
            let check r =
              try
                Hashtbl.find r;
                assert false
              with Not_found -> 
                assert false 
            in
            assert false }
  let unit : unit tc
    = { memoizer = 
        fun f -> 
          let mref = ref None in
          fun () -> match !mref with
            | Some x -> x
            | None -> let v = f () in
                      mref := Some v;
                      v }
  let string : string tc
    = { memoizer = fun _ -> assert false }

  (* Tuples *)
  let ( * ) : 'a tc -> 'b tc -> ('a * 'b) tc
    = fun mda mdb -> { memoizer = fun f -> 
      assert false
                     }

  let tuple : ('t -> 'pairs) -> ('pairs -> 't) -> 'pairs tc -> 't tc
    = fun from into v -> { memoizer = fun _ -> assert false }

  (* Records *)
  let unitr : unit tc
    = { memoizer = fun _ -> assert false }
  let ( *:) : [ `Mutable of string | `Immutable of string] -> 'a tc -> 'a tc
    = fun label t -> { memoizer = fun _ -> assert false }
  let (&) : 'a tc -> 'row tc -> ('a * 'row) tc
    = fun field row -> { memoizer = fun _ -> assert false }
  let record : string -> ('r -> 'row) -> ('row -> 'r) -> 'row tc -> 'r tc
    = fun lab from into row -> { memoizer = fun _ -> assert false }

  (* Variants *)
  let (+:) : string -> 'a tc -> 'a tc
    = fun label t -> { memoizer = fun _ -> assert false }
  let nil : zero tc
    = { memoizer = fun _ -> assert false }
  let (||) : 'a tc -> 'row tc -> ('a, 'row) either tc
    = fun field row -> { memoizer = fun _ -> assert false }
  let variant : string -> ('s -> 'row) -> ('row -> 's) -> 'row tc -> 's tc
    = fun label from into row -> { memoizer = fun _ -> assert false }
    
  (* Fixpoints *)
  let fix : 'a tc fix -> 'a tc
    = fun f -> { memoizer = fun _ -> assert false }

end

(* For each generic function we can give a convenient alias that unpacks the
   type representation, applies the interpretation functor, and calls the
   result. *)
let show : 'a . 'a repr -> 'a -> string =
  fun (type a) repr v -> 
    let module R = (val repr : Repr with type a = a) in 
    let module N = R.Interpret (Show)
    in N.result v

let eq : 'a. 'a repr -> 'a -> 'a -> bool =
  fun (type a) repr -> 
    let module R = (val repr : Repr with type a = a) in 
    let module N = R.Interpret (Eq)
    in N.result

(* With first class modules, generic functions are just normal OCaml
   functions, so it's easy to write other functions that make use of them.

   Here's an example.  The show_uniq uses both show and eq generic functions.
   Note also that show_uniq takes a representation of 'a, but can easily use a
   representation of 'a list.  This is analogous to a Haskell function with a
   constraint for a type `a' in the signature making use of an instance for
   `[a]'.
*)

(* An auxiliary function: Haskell's List.nub.*)
let nub : 'a. ('a -> 'a -> bool) -> 'a list -> 'a list =
  fun eq -> 
    let rec nub = function
      | []
      | [_] as l -> l
      | x :: (y :: xs as tail) when eq x y -> nub tail
      | x :: tail -> x :: nub tail
    in nub
        
(* Replace all adjancent duplicates in a list with single values, then prints
   out the result. *)
let show_uniq : 'a. 'a repr -> 'a list -> unit =
  fun (type s) repr items ->
    print_endline (show (list repr)
                     (nub (eq repr) items))

(*
  A simple test.

  It exercises
    * the representations for string, pair and int
    * the "user-defined" representations for option and list
    * the generic functions eq and show
    * the generic-function-using-function show_uniq.
*)
let print_uniq_pairs () = 
  show_uniq (list string * option int)
    [(["one"], Some 2);
     (["two"; "three"], Some 4);
     (["two"; "three"], Some 4);
     (["two"; "three"], Some 4);
     ([], None);
     ([], None);
     (["four"; "five"], Some 5)]