From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p7JFd59h002334 for ; Fri, 19 Aug 2011 17:39:05 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjMCADWDTk5KfVK2kGdsb2JhbABChEuUJY8VCBQBAQEBCQkNBxQEIYFZAg8dARInAw0FCQc3AiQSAQUBPRqgVoJYCot5gxWEe4koAgMGhTKBEASTE4xZPIE/giM X-IronPort-AV: E=Sophos;i="4.68,251,1312149600"; d="scan'208";a="116322373" Received: from mail-wy0-f182.google.com ([74.125.82.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Aug 2011 17:39:00 +0200 Received: by wyh15 with SMTP id 15so3999860wyh.27 for ; Fri, 19 Aug 2011 08:39:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; bh=bHwiu16Y2NaNmarjiuHMdmn+BOYoz7PosuIJ4wUQzbs=; b=JUjAeiRtTEP4ibcNGo/FvFEBL6K1c6dLzWP6TZe82cQYd8WjShwk7WY+5ctreUiZiz MojO7kbxELqu+ZS2O+LQrQsm0ApSLb/G+Z6mXLFx/shkzWP8hGicPfxxYP8w++d88lUb LDfr9dSinQbe3hGYuKMZVyJ0YHgajVGXibJyM= Received: by 10.227.202.65 with SMTP id fd1mr1884359wbb.104.1313768340119; Fri, 19 Aug 2011 08:39:00 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.227.143.142 with HTTP; Fri, 19 Aug 2011 08:38:20 -0700 (PDT) From: Arnaud Spiwack Date: Fri, 19 Aug 2011 17:38:20 +0200 X-Google-Sender-Auth: LzF2WF2Ab7ool098TBE_seFwBAg Message-ID: To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=0015175925dc3ae2a204aadd87a0 Subject: [Caml-list] First-class module and higher-order types --0015175925dc3ae2a204aadd87a0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear all, One way to use first-class module is to "extend" a functor without resorting to a new functor. Like, for instance: type ('a,'t) set =3D (module Set.S with type elt =3D 'a and type t =3D 't) let add2 (type a) (type t) (m:(a,t) set) x y s =3D let module S =3D (val m:Set.S with type elt =3D a and type t =3D t) in S.add x (S.add y s);; But if that works pretty with Set, it won't work with Map for two reasons. One is that syntax won't allow us to write something like with 'a t =3D =E2=80=A6 in the type constraints. Another, probably more serious, is that there is no equivalent to (type t), for type families ( (type 'a t) ?). Now that would be a pretty useful thing to do, in some case. Hence I have a twofold question: 1. On the practical side, does anyone knows a workaround ? Could I find a way to extend Map without a functor if I'm tricky? 2. On the theoretical side, how hard is it to design a variant of Hindley-Milner's typing algorithm with type-family quantification? (I understand that Ocaml's typing machinery is pretty hard to change, and t= hat it will most likely not be happening any time soon in practice) -- Arnaud Spiwack --0015175925dc3ae2a204aadd87a0 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear all,

One way to use first-class module is to "extend"= a functor without resorting to a new functor. Like, for instance:

<= div style=3D"margin-left:40px">type ('a,'t) set =3D (module Set.S with type elt =3D 'a a= nd type t =3D 't)

let add2 (type a) (type t) (m:(a,t) set) x y s =3D
=C2=A0=C2=A0 let module S =3D (val m:Set.S with= type elt =3D a and type t =3D t) in
=C2=A0=C2=A0 S.add x (S.a= dd y s);;

B= ut if that works pretty with Set, it won't work with Map for two reason= s. One is that syntax won't allow us to write something like

with 'a t =3D =E2=80=A6

in the type cons= traints. Another, probably more serious, is that there is no equivalent to = (type t), for type= families ( (type 'a = t) ?).


Now that would be a pretty useful thing to do, in some case. Hence = I have a twofold question:

  1. On the practical side, does anyon= e knows a workaround ? Could I find a way to extend Map without a functor i= f I'm tricky?
  2. On the theoretical side, how hard is it to design a variant of Hindley-= Milner's typing algorithm with type-family quantification? (I understan= d that Ocaml's typing machinery is pretty hard to change, and that it w= ill most likely not be happening any time soon in practice)

--
Arnaud Spiwack
--0015175925dc3ae2a204aadd87a0--