Re: [Caml-list] Mixing two GADTs

[Alain Frisch <alain@frisch.fr>]

On 07/01/2013 09:39 AM, David Allsopp wrote:
> Obviously, I need type annotations for f and retr. I'd tried:
>
> let get2 : type s . s foo -> s = fun attr ->
>    let x : type t . (t -> s) * t bar =
>      match attr with
>        A -> (int_of_string, Z)
>      | B -> (string_of_float, Y)
>      | C -> ((=) 1, X)
>    in
>      let (f, retr) = x
>      in
>        f (g retr)

What you need is an existential quantification ("there exists some t 
such that x has type (t -> s) * t bar").  You can do this by wrapping 
the tuple in a third GADT:

type 's baz = T: ('t -> 's) * 't bar -> 's baz

let get2 : type s . s foo -> s = fun attr ->
   let x : s baz =
     match attr with
     | A -> T (int_of_string, Z)
     | B -> T (string_of_float, Y)
     | C -> T ((=) 1, X)
   in
   let (T (f, retr)) = x in
   f (g retr)


-- Alain