From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <lpw25@hermes.cam.ac.uk>
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 56B057EC41
	for <caml-list@sympa.inria.fr>; Tue, 23 Oct 2012 14:31:43 +0200 (CEST)
Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  lpw25@hermes.cam.ac.uk) identity=pra;
  client-ip=131.111.8.150;
  receiver=mail1-smtp-roc.national.inria.fr;
  envelope-from="lpw25@hermes.cam.ac.uk";
  x-sender="lpw25@hermes.cam.ac.uk";
  x-conformance=sidf_compatible
Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  lpw25@hermes.cam.ac.uk) identity=mailfrom;
  client-ip=131.111.8.150;
  receiver=mail1-smtp-roc.national.inria.fr;
  envelope-from="lpw25@hermes.cam.ac.uk";
  x-sender="lpw25@hermes.cam.ac.uk";
  x-conformance=sidf_compatible
Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@ppsw-50.csi.cam.ac.uk) identity=helo;
  client-ip=131.111.8.150;
  receiver=mail1-smtp-roc.national.inria.fr;
  envelope-from="lpw25@hermes.cam.ac.uk";
  x-sender="postmaster@ppsw-50.csi.cam.ac.uk";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ap8AAESNhlCDbwiWmWdsb2JhbABEwWUjAQEBAQEICwsHFCeCHwEFJxFBEAEKRlcGiBezXokIi18ahkQDm1WJCoQ7gWI
X-IronPort-AV: E=Sophos;i="4.80,634,1344204000"; 
   d="scan'208";a="178531078"
Received: from ppsw-50.csi.cam.ac.uk ([131.111.8.150])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 23 Oct 2012 14:31:42 +0200
X-Cam-AntiVirus: no malware found
X-Cam-SpamDetails: not scanned
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
Received: from hermes-1.csi.cam.ac.uk ([131.111.8.51]:59719)
	by ppsw-50.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.157]:25)
	with esmtpa (EXTERNAL:lpw25) id 1TQde2-0001ec-r9 (Exim 4.72)
	(return-path <lpw25@hermes.cam.ac.uk>); Tue, 23 Oct 2012 13:31:42 +0100
Received: from prayer by hermes-1.csi.cam.ac.uk (hermes.cam.ac.uk)
	with local (PRAYER:lpw25) id 1TQde2-0006fq-F2 (Exim 4.72)
	(return-path <lpw25@hermes.cam.ac.uk>); Tue, 23 Oct 2012 13:31:42 +0100
Received: from [128.232.9.0] by webmail.hermes.cam.ac.uk
	with HTTP (Prayer-1.3.5); 23 Oct 2012 13:31:42 +0100
Date: 23 Oct 2012 13:31:42 +0100
From: Leo P White <lpw25@cam.ac.uk>
To: Romain Bardou <romain.bardou@inria.fr>
Cc: caml-list@inria.fr
Message-ID: <Prayer.1.3.5.1210231331420.27886@hermes-1.csi.cam.ac.uk>
In-Reply-To: <508677C4.5040802@inria.fr>
References: <508677C4.5040802@inria.fr>
X-Mailer: Prayer v1.3.5
Mime-Version: 1.0
Content-Type: text/plain; format=flowed; charset=ISO-8859-1
Sender: "L.P. White" <lpw25@hermes.cam.ac.uk>
Subject: Re: [Caml-list] Constrained existential types

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,
>
>