WIP

higher.ml

module M : sig
  type 'a logic
  (* We describe there that there is conversion from 'b to 'a *)
  type ('a, 'b) fancy  

  val lift : 'a  -> ('a,'a) fancy
  val inj  : ('a,'b) fancy -> ('a, 'b logic) fancy
end = struct
  type 'a logic = 'a
  type ('a,'b) fancy = 'a
  let lift x = x
  let inj  x = x
end

(* from higher kinded types library *)
module Higher = struct
  open M
  type ('p, 'f) app

  module type Newtype1 = sig
    type 'a s
    type t
    val inj : 'a s -> ('a, t) app 
    val prj : ('a, t) app -> 'a s 

    val funky : (('a, t) app, ('b, t) app) fancy -> ('a s, 'b s) fancy 
    val fmap1 : (('a, 'b) fancy, 't) app -> (('a, 't)app, ('b, 't)app) fancy 
  end

  module Common = struct
    type t
    external inj : 'a -> 'b = "%identity"
    external prj : 'a -> 'b = "%identity"
  end

  module Newtype1 (T : sig type 'a t end) : Newtype1 with type 'a s = 'a T.t = 
  struct
    type 'a s = 'a T.t
    include Common

    external funky : (('a, t) app, ('b, t) app) fancy -> ('a s, 'b s) fancy 
      = "%identity"
    external fmap1 : (('a, 'b) fancy, 't) app -> (('a, 't)app, ('b, 't)app) fancy 
      = "%identity"
  end

  module type Newtype2 = sig
    type ('a, 'b) s
    type t
    val inj : ('a, 'b) s -> ('a, ('b, t) app) app 
    val prj : ('a, ('b, t) app) app -> ('a, 'b) s 
    val wrap : 
      ('a, ('b,t) app) app -> 
      (('a,'a logic) fancy, (('b,'b logic) fancy,t) app) app
    val wrap2 : 
      ('a, ('b,t) app) app -> ('a -> 'c) -> ('b -> 'd) ->
      ('c, ('d,t) app) app
    val funky: (('a, 'a logic) fancy, (('b, 'b logic) fancy, t) app) app
      -> (('a, 'a logic) fancy, ('b, 'b logic) fancy) s
    val  wtf: ( ('a,'b)fancy, ('c,'d)fancy) s ->
      (('a,'c) s, ('b,'d) s) fancy
  end

  module Newtype2 (T : sig type ('a, 'b) t end) 
    : Newtype2 with type ('a,'b) s = ('a,'b) T.t = 
  struct
    type ('a, 'b) s = ('a, 'b) T.t
    include Common

    (* need to add something here *)
    external wrap : 
      ('a, ('b,t) app) app -> 
      (('a,'a logic) fancy, (('b,'b logic) fancy,t) app) app = "%identity"

    let wrap2 : 
      ('a, ('b,t) app) app -> ('a -> 'c) -> ('b -> 'd) ->
      ('c, ('d,t) app) app = fun x _ _ -> Obj.magic ()

    external funky: (('a, 'a logic) fancy, (('b, 'b logic) fancy, t) app) app
      -> (('a, 'a logic) fancy, ('b, 'b logic) fancy) s = "%identity"

    external wtf: ( ('a,'b)fancy, ('c,'d)fancy) s ->
      (('a,'c) s, ('b,'d) s) fancy = "%identity"
  end
end

open M;;
open Higher;;

(* for 1 parametric types everything seems to be OK *)
type 'a maybe = Just of 'a | Nothing ;;
module Maybe = Newtype1(struct type 'a t = 'a maybe end);;
let (_:(int maybe, int logic maybe logic) fancy) =
  inj @@ Maybe.funky @@ Maybe.fmap1 @@ Maybe.inj (Just (inj@@lift 5))
;;


(* for two-parametric ..... *)
type ('a,'b) result = OK of 'a | Error of 'b;;
module Result = Newtype2(struct type ('a,'b) t = ('a,'b) result end);;
let ok : 'a. 'a -> ( ('a,'a logic) fancy, string) result = 
  fun x -> OK (inj@@lift x);;
(* I want
   let (_: ((int,string) result, (int logic,string logic) result logic) fancy) =  *)

let (_:  ((int,string)result, (int logic,string logic) result logic) fancy)
  =  (* Need to put fancy somehow to the second argument *)
  inj @@
  Result.wtf@@
  Result.funky @@ Result.wrap2 
                    (Result.inj (OK 5)) 
                    (fun n -> inj@@lift n)
                    (fun (_:string) -> inj@@lift "") 
;;