open Batteries
open Map

(* Function implementation
  - 'i: input
  - 'o: output
  - 'd: datatype

  - 'r: result

  Example: ('i, 'o, ('i, 'o) PMap.t) fi
*)

type ('i, 'o, 'd) fi =
  {
    make: unit -> 'd;
    set: 'i -> 'o -> 'd -> 'd;
    unset: 'i -> 'd -> 'd;
    get: 'i -> 'd -> 'o option;
    foldi: 'r. ('i -> 'o -> 'r -> 'r) -> 'd -> 'r -> 'r
  }

(* Function recursive implementation
  - 't: type (abstract type)
  - 'd: datatype (concrete type)
  - 'a: abstraction (abstraction of abstract type) (it's the same thing as the abstract type except that in C, 'c is replaced by unit
                                to allow differetiation function types treated as constants and function types being implemented)

  - 'c: constant type
  - 'it: input type
  - 'id: input datatype
  - 'ia: input abstraction
  - 'ot: output type
  - 'od: output datatype
  - 'oa: output abstraction
*)

type ('t, 'd, 'a) fri =
  | C: 'c -> ('c, 'c, unit) fri
  | F: ('it, 'id, 'ia) fri * ('ot, 'od, 'oa) fri * ('id, 'od, 'd) fi -> ('it -> 'ot, 'd, 'ia -> 'oa) fri

(* Function
  - 't type (abstract type)
  - 'd datatype (concrete type)
  - 'a abstract (abstraction of abstract type)
*)
type ('t, 'd, 'a) t =
  {
    data: 'd;
    implementation: ('t, 'd, 'a) fri
  }

(* That's where the 'a is supposed to help: I only need to match against F *)
let get1 i (f : ('t, 'd, 'ai -> 'ao) t) =
  match f.implementation with
  | F (ii, oi, fi) -> failwith "TODO" (* This words *)

(* But when I ty to actually implement the function, I get a weird error *)
let get2 i (f : ('t, 'd, 'ai -> 'ao) t) =
  match f.implementation with
  | F (ii, oi, fi) -> fi.get i f.data
  (*Error: This expression has type id#0 but an expression was expected of type
         id#0
       The type constructor id#0 would escape its scope
  *)

(* Google helped me find other people with the same problem and the answer was to add type arguments so I tried *)
let get3 (type t2) (type d) (type ai) (type ao) i (f : (t2, d, ai -> ao) t) =
  match f.implementation with
  | F (ii, oi, fi) -> fi.get i f.data
  (*Error: This expression has type id#0 but an expression was expected of type
         id#0
       The type constructor id#0 would escape its scope
  *)

(* I also tried removing the type restriction and matching both cases but it doesn't work either *)
let get4 i f  =
  match f.implementation with
  | C c -> Some c
  | F (ii, oi, fi) -> fi.get i f.data
  (* Error: This pattern matches values of type
         ('a -> 'b, 'a -> 'b, ex#0 -> ex#1) fri
       but a pattern was expected which matches values of type
         ('a -> 'b, 'a -> 'b, unit) fri
       Type ex#0 -> ex#1 is not compatible with type unit
  *)

(* And removing the type restriction and not matching C *)
let get5 i f =
  match f.implementation with
  | F (ii, oi, fi) -> fi.get i f.data
  (* Error: This expression has type id#0 but an expression was expected of type
         id#0
       The type constructor id#0 would escape its scope
  *)

(* And replacing by _ [http://caml.inria.fr/mantis/view.php?id=6264] *)
let get6 i (f : (_, _, _ -> _) t) =
  match f.implementation with
  | F (ii, oi, fi) -> fi.get i f.data
  (*Error: This expression has type id#0 but an expression was expected of type
         id#0
       The type constructor id#0 would escape its scope
  *)