From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <thomas.braibant@gmail.com>
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 C26127F8F3
	for <caml-list@sympa.inria.fr>; Fri, 23 May 2014 10:15:59 +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=209.85.212.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 209.85.212.175 as
  permitted sender) identity=mailfrom;
  client-ip=209.85.212.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-wi0-f175.google.com) identity=helo;
  client-ip=209.85.212.175;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="thomas.braibant@gmail.com";
  x-sender="postmaster@mail-wi0-f175.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: At0BAFkDf1PRVdSvlGdsb2JhbABZhDGCaqpFmAMIFg4BAQEBBwsLCRIqgk8EGQEbHgMSEA8CJgIkAREBBQEiiD8BAxGiaoMRjBGBcoMNmTkKGScNZIVDEQEFDIEekCSBSwSZcpE2GCmEajs
X-IPAS-Result: At0BAFkDf1PRVdSvlGdsb2JhbABZhDGCaqpFmAMIFg4BAQEBBwsLCRIqgk8EGQEbHgMSEA8CJgIkAREBBQEiiD8BAxGiaoMRjBGBcoMNmTkKGScNZIVDEQEFDIEekCSBSwSZcpE2GCmEajs
X-IronPort-AV: E=Sophos;i="4.98,892,1392159600"; 
   d="scan'208";a="63380512"
Received: from mail-wi0-f175.google.com ([209.85.212.175])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 May 2014 10:15:32 +0200
Received: by mail-wi0-f175.google.com with SMTP id f8so423716wiw.14
        for <caml-list@inria.fr>; Fri, 23 May 2014 01:15:32 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:from:date:message-id:subject:to:content-type;
        bh=Gv5GXcBJDaE/eu5pmVL0L33tL1+miVfku/5wDKqAFW4=;
        b=GH+4DEhlZHwA7vfKAJNq1wJxzwhJw0ImRqBeF3+hevqBVGf205iVjABGOIuCTygIMe
         jLpFpftxW1v2HIDmBtpClLMsQkjm6st2P2XM50X5yf+zJfpm1e8eXrvHLDY0Oxvs4LlB
         +Pgdtmdb2ICozNBCzffC3x1penj5jwcJioXTTm6ZsFpL1EXIKNUVVW06lBx0IPYMvyEO
         fTLZOf7UiJq3gTNTg1MRpEFxXb6j0PrZqjYAtHKsoei81RuOryE5dxdYhR7j7NdshKY8
         a0//ze1sZJ3nonsc+yFZEBls8uMZd0truKVYWqNGkCvYHUVHCm2vZUxCrwVPsMkd0pPQ
         brvQ==
X-Received: by 10.194.94.202 with SMTP id de10mr318717wjb.84.1400832932314;
 Fri, 23 May 2014 01:15:32 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.194.138.15 with HTTP; Fri, 23 May 2014 01:15:11 -0700 (PDT)
From: Thomas Braibant <thomas.braibant@gmail.com>
Date: Fri, 23 May 2014 10:15:11 +0200
Message-ID: <CAHR=VkxembFPVePtEG+atG1ShiKYeo78QHYxbbLN+TXCBSQqJQ@mail.gmail.com>
To: OCaML Mailing List <caml-list@inria.fr>
Content-Type: text/plain; charset=UTF-8
Subject: [Caml-list] GADT and local modules

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