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 356A47EDE3 for ; Tue, 23 Oct 2012 14:34:41 +0200 (CEST) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of romain.bardou@inria.fr) identity=pra; client-ip=138.231.176.54; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="romain.bardou@inria.fr"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of romain.bardou@inria.fr) identity=mailfrom; client-ip=138.231.176.54; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="romain.bardou@inria.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of postmaster@ariane2.ens-cachan.fr designates 138.231.176.54 as permitted sender) identity=helo; client-ip=138.231.176.54; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="romain.bardou@inria.fr"; x-sender="postmaster@ariane2.ens-cachan.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArABAC6OhlCK57A2kWdsb2JhbABEDr4Qg0cjAQEBARQSFCeCHgEBBScLAQVAARALGAkWDwkDAgECAUUGDQEHAogArCOQQItfGoZEA5VxhWSNBz+BYQ X-IronPort-AV: E=Sophos;i="4.80,634,1344204000"; d="scan'208";a="178531967" Received: from ariane2.ens-cachan.fr ([138.231.176.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 23 Oct 2012 14:34:39 +0200 Received: from localhost (localhost [127.0.0.1]) by ariane2.ens-cachan.fr (Postfix) with ESMTP id 26FE323C299; Tue, 23 Oct 2012 14:34:38 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at ens-cachan.fr Received: from ariane2.ens-cachan.fr ([127.0.0.1]) by localhost (ariane2.ens-cachan.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id PnYbiqtW2jG8; Tue, 23 Oct 2012 14:34:38 +0200 (CEST) Received: from olive.lsv.ens-cachan.fr (olive.lsv.ens-cachan.fr [138.231.81.248]) by ariane2.ens-cachan.fr (Postfix) with ESMTP id 0A7DB23C176; Tue, 23 Oct 2012 14:34:37 +0200 (CEST) Received: from [172.31.81.30] (gwvisitors.lsv.ens-cachan.fr [138.231.81.8]) by olive.lsv.ens-cachan.fr (Postfix) with ESMTP id 9CA5E4C019A; Tue, 23 Oct 2012 14:24:56 +0200 (CEST) Message-ID: <50868F25.9010306@inria.fr> Date: Tue, 23 Oct 2012 14:35:49 +0200 From: Romain Bardou User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.7) Gecko/20120922 Icedove/10.0.7 MIME-Version: 1.0 To: Leo P White CC: caml-list@inria.fr References: <508677C4.5040802@inria.fr> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Validation-by: romain.bardou@inria.fr Subject: Re: [Caml-list] Constrained existential types Interesting. I can't use OCaml 4.00 or more for this project (yet) but I'll keep that in mind. Cheers, -- Romain Bardou Le 23/10/2012 14:31, Leo P White a écrit : > 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 > > > 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, >> >> > >