Re: [Caml-list] How is this type inferred (GADTs)

[Oleg <oleg@okmij.org>]

Gabriel has given an excellent explanation, it is hard to add
anything. Yet I will still try.

> module F : sig
>   type ('f, 'r) t
>   val z : ('r, 'r) t
>   val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t
> end = struct
>   type ('f, 'r) t =
>     | Z : ('r, 'r) t
>     | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t
>   let z = Z
>   let (//) t f = S (t, f)
> end

Perhaps it will be easier to work out the types if we don't use
GADTs. They are not necessary in your example (and not needed for
the typed printf either).

Here is the adjusted code

module F : sig
  type ('f, 'r) t

  val z : ('r, 'r) t
  val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t

  val bind : 'f -> ('f, 'r) t -> 'r
 end = struct
  type ('f, 'r) t = 'f -> 'r

  let z = fun x -> x
  (* the type annotations are all optional. They are given to show
     which subexpressions have which types, and let the compiler confirm
     that.
     Alas, attaching type annotations requires too many parentheses
  *)  
  let (//) : type a r f. (f, a -> r) t -> (unit -> a) -> (f, r) t =
    fun t th ->
      fun (f:f) -> ((((t f):(a->r)) (th () : a)) : r)

  let bind f t = t f
end


let exp1 = F.(z // (fun () -> Int32.zero) // (fun () -> ""));;
(*
  val exp1 : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr>
*)

Just for reference, here is the implementation for the opposite order,
suggested by Gabriel.

module G : sig
  type ('f, 'r) t

  val z : ('r, 'r) t
  val (//) : ('f, 'r) t -> (unit -> 'a) -> ('a -> 'f, 'r) t

  val bind : 'f -> ('f, 'r) t -> 'r
 end = struct
  type ('f, 'r) t = {e: 'w. ('r -> 'w) -> ('f -> 'w)}

  let z = {e = fun x -> x}
  (* the type annotations are all optional. They are given to show
     which subexpressions have which types, and let the compiler confirm
     that
     Alas, attaching type annotations requires too many parentheses
  *)  
  let (//) : type a r f. (f, r) t -> (unit -> a) -> (a->f, r) t =
    fun t th ->
      {e = fun (type w) (k:(r->w)) -> fun (af:a->f) ->
        ((((t.e k):(f -> w)) ((af (th ())):f)):w)}

  let bind f t = t.e (fun x -> x) f
end

let test = G.(z // (fun () -> 3l) // (fun () -> "foo"));;
(* val test : (string -> int32 -> '_weak2, '_weak2) G.t = <abstr> *)

;;