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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 649097F8F2 for ; Fri, 23 May 2014 10:28:40 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of thomas.braibant@gmail.com) identity=pra; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="thomas.braibant@gmail.com"; x-sender="thomas.braibant@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of thomas.braibant@gmail.com designates 74.125.82.175 as permitted sender) identity=mailfrom; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="thomas.braibant@gmail.com"; x-sender="thomas.braibant@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f175.google.com) identity=helo; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="thomas.braibant@gmail.com"; x-sender="postmaster@mail-we0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuEBALEFf1NKfVKvlGdsb2JhbABZg1lYgmqpPoEHgwOTfwGBAAgWDgEBAQEHCwsJEiqCJQEBBSMEGQEbEgsBAwwGBQsNAgIJHQICIQEBEQEFAQoSBhMSCYgRAQMRDaVyjBGBcoMNmToKGScDCmSFQxEBBQyBHosSJoFwB4J1gUsEhF4FkxmBdoE9i3iEARgphGk8MA X-IPAS-Result: AuEBALEFf1NKfVKvlGdsb2JhbABZg1lYgmqpPoEHgwOTfwGBAAgWDgEBAQEHCwsJEiqCJQEBBSMEGQEbEgsBAwwGBQsNAgIJHQICIQEBEQEFAQoSBhMSCYgRAQMRDaVyjBGBcoMNmToKGScDCmSFQxEBBQyBHosSJoFwB4J1gUsEhF4FkxmBdoE9i3iEARgphGk8MA X-IronPort-AV: E=Sophos;i="4.98,892,1392159600"; d="scan'208";a="63384114" Received: from mail-we0-f175.google.com ([74.125.82.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 May 2014 10:28:39 +0200 Received: by mail-we0-f175.google.com with SMTP id t61so4560231wes.34 for ; Fri, 23 May 2014 01:28:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=xiJO2ARmZs1Uwv08+YhvF/nHR6ECQBqAkwxYchDAFKQ=; b=AleXHbvElg6UOGkrd3cbI1oAMw2/HQkDjyonHtnSmm9rtJl0ZAjxGqZFy29IkO0ZlF agyLmigF0PUUd3pdQbgEVsN+0Ub9Syxyc5bsZDD7IcHqYCW6QPKsm6SY/Ms7h1Q9D/UE EzxC3g4KdMz66SbVWrRXpam/3qyR/02USfz0dnrgSOPPUzSaLZd3b/63Apm5/unlILaD fVg4a+2rPnxN8ex29FwyBQKzjLUgJ4X4KOT1CAsZHjYJW0BpAnW9Hcqrp7Lz746pH3xY i7zsvmtjoleOuGpX7sQNRSESwQzicd6AWAj/liHtgonHuZ+ot2fHRuYfznQvc5XZD7A2 YqwA== X-Received: by 10.180.77.225 with SMTP id v1mr1818691wiw.5.1400833719566; Fri, 23 May 2014 01:28:39 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.138.15 with HTTP; Fri, 23 May 2014 01:28:19 -0700 (PDT) In-Reply-To: References: From: Thomas Braibant Date: Fri, 23 May 2014 09:28:19 +0100 Message-ID: To: Gabriel Scherer Cc: OCaML Mailing List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] GADT and local modules Oh my. I would never have thought that I could use commutative cuts in OCaml. I should have thought about this myself, given the time that I spent playing with these. For the interested reader, this solution is also called the convoy pattern in Coq, and is described here http://adam.chlipala.net/cpdt/html/MoreDep.html Thanks a lot Gabriel. On Fri, May 23, 2014 at 9:24 AM, Gabriel Scherer wrote: > You will be familiar with the solution from the Coq world. > > match t with > | Pack l -> > begin fun (type a') (type b') l -> > let module C = struct > type a = a' > type b = b' > let foo = l > end in > let module R = M(C) in > R.result > end l > > On Fri, May 23, 2014 at 10:15 AM, Thomas Braibant > wrote: >> Hi list, >> >> I would like to find a way to name (or capture) the variables that are >> existentially quantified in a GADT constructor, to put them inside a >> module and apply a functor on the said module. Attached below is a >> mockup of what I would like to have. (I can live without this coding >> pattern, but I would like to know whether or not it is possible to >> make it work, even if I suspect that the answer is no). >> >> Best, >> Thomas >> >> >> type t = Pack : 'a * 'b list -> t >> >> (* I want to unpack a t, and put its content in a module of signature S *) >> module type S = sig >> type a >> type b >> val foo : (a * b) list >> end >> >> (* I want to apply the functor M on my module to produce a result, >> whose type does not depend on the types in S. I am using a functor as >> a way to structure the computations that happen inside. I started with >> a version without modules, which requires to write quite a few type >> annotations... *) >> module M (C:S) : sig val result : int end= struct >> >> include C >> >> (* Here I want bar to have type (a * b) list. Of course, I could have >> bar s a function that takes two type variables as arguments, and a >> list, and returns a list of the right type. *) >> let bar = List.rev foo >> let result = List.length bar >> >> end >> >> (* Here, I do not know of a way to retrieve the type variables >> quantified in the GADT constructor Pack, to feed them in C *) >> let f (t : t) = >> match t with >> | Pack l -> let module C = .... in M(C) >> >> (* alternative with modules, which is not satisfying. *) >> >> module type S = sig >> val t : t >> end >> >> module M (C:S) : sig val result : int end = struct >> >> include C >> >> (* Now, I can unpack the t locally in each function, but I cannot >> open the existential in the whole module, which is painful. *) >> >> end >> >> -- >> 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