From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id EBCFE7EDE3 for ; Tue, 23 Oct 2012 15:54:09 +0200 (CEST) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jacques.garrigue@gmail.com) identity=pra; client-ip=209.85.214.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of jacques.garrigue@gmail.com designates 209.85.214.182 as permitted sender) identity=mailfrom; client-ip=209.85.214.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f182.google.com) identity=helo; client-ip=209.85.214.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="postmaster@mail-ob0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgoBAJGghlDRVda2kGdsb2JhbABEDq9HB4kfAYhhCCMBAQEBCQkNBxQEI4IeAQEBAwESAhMZAS0LAQMBCwEFBQsNDSEiEgEFAQoSBhMSEIdQAwkGC51ICQOOFIEKhSonAwpMiQIBBQyLUxqGRAOIWI0ZgReNQRYpgViBfEyBVA X-IronPort-AV: E=Sophos;i="4.80,635,1344204000"; d="scan'208";a="178548723" Received: from mail-ob0-f182.google.com ([209.85.214.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 Oct 2012 15:54:08 +0200 Received: by mail-ob0-f182.google.com with SMTP id wc20so6314443obb.27 for ; Tue, 23 Oct 2012 06:54:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; bh=ecKd648f8wWn9mVi9ivQaBbHTlEhcG0zuh71Z+LkaWo=; b=NMWSGMCTcxh3aC/j0Bv8gv3d8EmeY+lAIujLt6n9yxYrCwuvRF7IovfUpzAQnlRhNd lMBCjg27QqW6XXTBpxq4nVhvSjcIXfNACUeZGUCORceM7iCRunhQc1bVfZIfX3dptlLz ZMBnVDBlzefFLfWhSZgaYuIG46Nwqj08jev80S+dCFxipvAuxvwm1qIcEuOd9FdUZuI7 PHT0UWAHDAzLJdW+RwRA4H7m0vU1vO+kne7OMYnTLrOtwcQpKimuyFVrlmW3Rj+1TmWD e0uX/xuVlfLqtjkXfx3YyEBHTwMw9aZioc2O6fHyLE77JYXbocEuMEfQHpR8ufUQWBer tXCg== MIME-Version: 1.0 Received: by 10.60.3.69 with SMTP id a5mr11322595oea.117.1351000447770; Tue, 23 Oct 2012 06:54:07 -0700 (PDT) Sender: jacques.garrigue@gmail.com Received: by 10.182.71.130 with HTTP; Tue, 23 Oct 2012 06:54:07 -0700 (PDT) Received: by 10.182.71.130 with HTTP; Tue, 23 Oct 2012 06:54:07 -0700 (PDT) In-Reply-To: References: <508677C4.5040802@inria.fr> Date: Tue, 23 Oct 2012 22:54:07 +0900 X-Google-Sender-Auth: ua_YtkqMu9oKp4ySpLLtipqEZTI Message-ID: From: Jacques Garrigue To: Leo P White Cc: OCaML List Mailing , Romain Bardou Content-Type: multipart/alternative; boundary=e89a8f83a5a5c7dfe004ccba4d44 Subject: Re: [Caml-list] Constrained existential types --e89a8f83a5a5c7dfe004ccba4d44 Content-Type: text/plain; charset=ISO-8859-1 2012/10/23 21:32 "Leo P White" : > > It is a bit convoluted, but you can achieve this by using a GADT: > > > type 'a t constraint 'a = [< `A | `B ];; > > module type SIG = > sig > type a = private [< `A | `B ] > val x: a t > end;; > > type 'a aux = Aux: 'a t -> ([< `A | `B] as 'a) aux;; > > let create y = > let helper: type u. u aux -> unit = > fun (Aux y) -> let module M: SIG = > > struct > type a = u > let x = y > end > in > () > in > helper (Aux y) > ;; > > Regards, > > Leo This is very interesting. I was actually convinced that this was impossible. The problem is that the (type u) syntax does not support abstract rows. But you could avoid it by using a gadt which restores this abstract row after abstracting the whole type. Actually the type u. u aux->unit is hard to understand here. The point is that it expand to 'u. 'u aux->unit, which really requires a polymorphic row variable. Unfortunately the following implicit (type u) does not capture it buy your gadt does the trick. Jacques Garrigue > On Oct 23 2012, Romain Bardou wrote: > >> (This is the 4th time I send this e-mail because it does not seem to work. I'm trying with another SMTP server.) >> >> Hello list, >> >> I'm trying to use first-class modules to have existential types. But my existential type must be constrained. I have the following code: >> >> type 'a t constraint 'a = [< `A | `B ] >> >> module type SIG = >> sig >> type a = private [< `A | `B ] >> val x: a t >> end >> >> let create (type u) (y: u t) = >> let module M: SIG = >> struct >> type a = u >> let x = y >> end >> in >> () >> >> It does not compile, because of the following error: >> >> Error: This type u should be an instance of type [< `A | `B ] >> >> In the manual I did not see any way to constrain type u. If I write something like this instead: >> >> let create (y: 'a t) = >> let module M: SIG = >> struct >> type a = 'a >> let x = y >> end >> in >> () >> >> Then the definition "type a = 'a" is not correct, because 'a is not bound. >> >> Is there any way to have constrained existential types? >> >> Thanks, >> >> > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs --e89a8f83a5a5c7dfe004ccba4d44 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

2012/10/23 21:32 "Leo P White" <lpw25@cam.ac.uk>:
>
> It is a bit convoluted, but you can achieve this by using a GADT:
>
>
> type 'a t constraint 'a =3D [< `A | `B ];;
>
> module type SIG =3D
> sig
> =A0 type a =3D private [< `A | `B ]
> =A0 val x: a t
> end;;
>
> type 'a aux =3D Aux: 'a t -> ([< `A | `B] as 'a) aux= ;;
>
> let create y =3D
> =A0let helper: type u. u aux -> unit =3D
> =A0 =A0fun (Aux y) -> =A0 =A0 =A0 =A0let module M: SIG =3D
>
> =A0 =A0 =A0 =A0struct
> =A0 =A0 =A0 =A0 =A0type a =3D u
> =A0 =A0 =A0 =A0 =A0let x =3D y
> =A0 =A0 =A0 =A0end
> =A0 =A0 =A0 =A0in
> =A0 =A0 =A0 =A0()
> =A0in
> =A0 =A0helper (Aux y)
> ;;
>
> Regards,
>
> Leo

This is very interesting.
I was actually convinced that this was impossible.
The problem is that the (type u) syntax does not support abstract rows.
But you could avoid it by using a gadt which restores this abstract row aft= er abstracting the whole type.

Actually the type u. u aux->unit is hard to understand here.
The point is that it expand to 'u. 'u aux->unit, which really re= quires a polymorphic row variable.
Unfortunately the following implicit (type u) does not capture it buy your = gadt does the trick.

Jacques Garrigue

> On Oct 23 2012, Romain Bardou wrote:
>
>> (This is the 4th time I send this e-mail because it does not seem = to work. I'm trying with another SMTP server.)
>>
>> Hello list,
>>
>> I'm trying to use first-class modules to have existential type= s. But my existential type must be constrained. I have the following code:<= br> >>
>> type 'a t constraint 'a =3D [< `A | `B ]
>>
>> module type SIG =3D
>> sig
>> =A0 type a =3D private [< `A | `B ]
>> =A0 val x: a t
>> end
>>
>> let create (type u) (y: u t) =3D
>> =A0 let module M: SIG =3D
>> =A0 =A0 struct
>> =A0 =A0 =A0 type a =3D u
>> =A0 =A0 =A0 let x =3D y
>> =A0 =A0 end
>> =A0 in
>> =A0 ()
>>
>> It does not compile, because of the following error:
>>
>> Error: This type u should be an instance of type [< `A | `B ] >>
>> In the manual I did not see any way to constrain type u. If I writ= e something like this instead:
>>
>> let create (y: 'a t) =3D
>> =A0 let module M: SIG =3D
>> =A0 =A0 struct
>> =A0 =A0 =A0 type a =3D 'a
>> =A0 =A0 =A0 let x =3D y
>> =A0 =A0 end
>> =A0 in
>> =A0 ()
>>
>> Then the definition "type a =3D 'a" is not correct, = because 'a is not bound.
>>
>> Is there any way to have constrained existential types?
>>
>> Thanks,
>>
>>
>
>
> --
> Caml-list mailing list. =A0Subscription management and archives:
> https://sympa.i= nria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://cam= l.inria.fr/bin/caml-bugs

--e89a8f83a5a5c7dfe004ccba4d44--