[Caml-list] Mixing two GADTs

[Caml-list] Mixing two GADTs

[David Allsopp]

Suppose I have the following two GADTs:

type _ foo = A : int foo
           | B : string foo
           | C : bool foo

type _ bar = X : int bar
           | Y : float bar
           | Z : string bar

In my actual use case, these two GADTs cannot be altered. Suppose I then
define the following two functions:

let g : type s . s bar -> s = function
  X -> 42
| Y -> 42.0
| Z -> "42"

let get1 : type s . s foo -> s = function
  A -> int_of_string (g Z)
| B -> string_of_float (g Y)
| C -> (=) 1 (g X)

So far, so good. Now what I'd like to try to do is alter get1 to be of the
form:

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

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)

But I get an error with int_of_string being of type string -> int instead of
type t -> s.

(Incidentally, the notation I expected to be able to use of [(let ((f, retr)
: type t . (t -> s) * t bar)] resulted in a syntax error although looking at
7.13 in the manual, I think that's probably correct?)

Is there a type annotation which will allow this to work? Any help (or a
statement that this happens to be impossible!) much appreciated...


David

Re: [Caml-list] Mixing two GADTs

[Alain Frisch]

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