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 72FAA7F8F2 for ; Fri, 23 May 2014 10:25:30 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.128.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.128.173 as permitted sender) identity=mailfrom; client-ip=209.85.128.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-ve0-f173.google.com) identity=helo; client-ip=209.85.128.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ve0-f173.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBALUEf1PRVYCtlGdsb2JhbABZg1lYgmqpPpgJAYEACBYOAQEBAQcLCwkSKoIlAQEEASMEGQEbEgsBAwELBgULDQICCR0CAiEBAREBBQEKEgYTEgmIEQEDCQgNpXOMEYFygw2ZOwoZJwMKZIVDEQEFDIEeixKCFgeCdYFLBIReBZMZgXaBPYt4hAEYKYRqOw X-IPAS-Result: AtEBALUEf1PRVYCtlGdsb2JhbABZg1lYgmqpPpgJAYEACBYOAQEBAQcLCwkSKoIlAQEEASMEGQEbEgsBAwELBgULDQICCR0CAiEBAREBBQEKEgYTEgmIEQEDCQgNpXOMEYFygw2ZOwoZJwMKZIVDEQEFDIEeixKCFgeCdYFLBIReBZMZgXaBPYt4hAEYKYRqOw X-IronPort-AV: E=Sophos;i="4.98,892,1392159600"; d="scan'208";a="63383414" Received: from mail-ve0-f173.google.com ([209.85.128.173]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 May 2014 10:25:29 +0200 Received: by mail-ve0-f173.google.com with SMTP id pa12so5898103veb.32 for ; Fri, 23 May 2014 01:25:28 -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=E79i/mqEaA2vGx6QtTpZpC7riSEfoRXh7oFkp7hNNeQ=; b=D78dpFPCLttxgm0VZh91v0AWDASSaHUd5sWoHnwaPpo8N+f8NfN2AyA8+FZ6yBkWk6 I7n7Pjt9N3oHXvnBw0NYHUE1P0LRTNJUSLXBXyemWsouJio5VxBSSQmHvR6OOiX4Kmlc O4QrbJiYJXVv+YPDd3EsPgBSb0/Wp+C6A1O6A5pSNWywBRj9qGc0z9DMJK726k+CSCeT 8k4bV8nwzoA04rzEeJwEHJfwBgMS7wDuiupNpTb8mvwD2RLUgo0Z3eIWUIUH9VdQUJ0E Jx/PnKCDLEv882qVYxofzqlLJuzlnpBiiFHMV319sXsuhgKQ6lIuvntQ82eoajLMzmHa kHHg== X-Received: by 10.220.12.66 with SMTP id w2mr2865212vcw.15.1400833528755; Fri, 23 May 2014 01:25:28 -0700 (PDT) MIME-Version: 1.0 Received: by 10.58.90.227 with HTTP; Fri, 23 May 2014 01:24:48 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 23 May 2014 10:24:48 +0200 Message-ID: To: Thomas Braibant Cc: OCaML Mailing List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] GADT and local modules 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