From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alain@frisch.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 1A91B81793
	for <caml-list@sympa.inria.fr>; Mon,  1 Jul 2013 09:50:12 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=pra; client-ip=193.252.23.213;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.213;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@msa.smtpout.orange.fr) identity=helo;
  client-ip=193.252.23.213;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alain@frisch.fr";
  x-sender="postmaster@msa.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApYCALsy0VHB/BfVcmdsb2JhbABawDGCYQQEAYEUDgEMCAwJFAMlgiMBAQUnEVELDgoJJQ8CRgYBDAgBAYgPuzKPKzqDZwOXSIYhjjc
X-IPAS-Result: ApYCALsy0VHB/BfVcmdsb2JhbABawDGCYQQEAYEUDgEMCAwJFAMlgiMBAQUnEVELDgoJJQ8CRgYBDAgBAYgPuzKPKzqDZwOXSIYhjjc
X-IronPort-AV: E=Sophos;i="4.87,972,1363129200"; 
   d="scan'208";a="24040810"
Received: from msa04.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.213])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 01 Jul 2013 09:50:11 +0200
Received: from [192.168.1.116] ([92.151.39.25])
	by mwinf5d30 with ME
	id uvqA1l00F0YZpAs03vqBzV; Mon, 01 Jul 2013 09:50:11 +0200
Message-ID: <51D134B2.70800@frisch.fr>
Date: Mon, 01 Jul 2013 09:50:10 +0200
From: Alain Frisch <alain@frisch.fr>
User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:22.0) Gecko/20100101 Thunderbird/22.0
MIME-Version: 1.0
To: David Allsopp <dra-news@metastack.com>, 
 OCaml List <caml-list@inria.fr>
References: <001001ce762e$1bedde30$53c99a90$@metastack.com>
In-Reply-To: <001001ce762e$1bedde30$53c99a90$@metastack.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Mixing two GADTs

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