From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA07986; Mon, 29 Apr 2002 18:46:36 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA07981 for ; Mon, 29 Apr 2002 18:46:35 +0200 (MET DST) Received: from indyio.rz.uni-sb.de (indyio.rz.uni-sb.de [134.96.7.3]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g3TGkYD29374; Mon, 29 Apr 2002 18:46:34 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:sdBDbfbwd2yCpJ7qwnYdjhLUM1sCWyoN@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id SAA4413988; Mon, 29 Apr 2002 18:46:34 +0200 (CEST) Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by mars.rz.uni-sb.de (8.8.8/8.8.4/8.8.2) with ESMTP id SAA103020856; Mon, 29 Apr 2002 18:46:34 +0200 (CEST) Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.252.31]) by uni-sb.de (8.12.2/2002030600) with ESMTP id g3TGkXd20456; Mon, 29 Apr 2002 18:46:33 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:WNlxYJ/B2IVV2syXEZsMJqsphFPGQtpU@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g3TGkWW18261; Mon, 29 Apr 2002 18:46:33 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.12.3/2002040900) with ESMTP id g3TGkV623382; Mon, 29 Apr 2002 18:46:31 +0200 (CEST) X-Authentication-Warning: email: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from ps.uni-sb.de (zoidberg.ps.uni-sb.de [134.96.186.121]) by ps.uni-sb.de (8.11.6/8.11.0) with ESMTP id g3TGkWh12754; Mon, 29 Apr 2002 18:46:32 +0200 Message-ID: <3CCD794B.142F65D@ps.uni-sb.de> Date: Mon, 29 Apr 2002 18:48:11 +0200 From: Andreas Rossberg Organization: =?iso-8859-1?Q?Universit=E4t?= des Saarlandes X-Mailer: Mozilla 4.78 [en] (X11; U; Linux 2.4.9-21 i686) X-Accept-Language: de, en MIME-Version: 1.0 To: Francois.Pottier@inria.fr CC: caml-list@inria.fr Subject: Re: [Caml-list] Polymorphic Variants and Number Parameterized Types References: <3CCD55BD.6DB352F5@ps.uni-sb.de> <20020429172853.A6314@pauillac.inria.fr> Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hi François, > > Note that Russo showed [1] that you can actually get rid of dependent > > typing and interpret ML modules (without nested signatures) as a lambda > > calculus with higher-order polymorphism (i.e., definitely not > > simply-typed). The basic idea is to view functors as functions > > polymorphic over their type arguments. > > This interesting idea was also developed by Mark Jones: IIRC, he does not consider generative functors, though. > > In this setting, adding abstract signatures would at least require adding > > polymorphic kinds, I believe. > > What do you mean? In this encoding, modules are only records, so module types > are ordinary types, and there is no distinction between ordinary abstract > types (introduced by explicit polymorphic abstraction) and ``abstract > signatures''. There is, as far as I can tell, no need for kind polymorphism. Well, if you have a functor like F : functor(X : sig module type S module Y:S end) -> ... then it would be polymorphic in an unknown number of types. To capture this, you had to make the functor polymorphic in the kind carrying the record of abstract types bound in S (i.e. you would also need record kinds). Something along the lines of: F : forall k. forall S:*. forall ts:k. {Y:S} -> ... The application F (struct module type S = sig type t type u val x : t end module Y = struct type t = int type u = bool val x = 7 end end) corresponds to something like F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}} I'm being sketchy here, of course, since I haven't thought about it in real depth. It probably gets even messier when you go higher-order: consider signatures projected from an applicative functor, for example. In that case you might even need quantifiers on the kind level to encode it. Also, the kind k should be restricted to record kinds, so you want some subkinding discipline (or row polymorphism on the kind level? ;-). Well, and somewhere in that mess we must have taken the step into the realms of undecidable subtyping (because if it encodes OCaml modules it must be undecidable). Cheers, - Andreas -- Andreas Rossberg, rossberg@ps.uni-sb.de "Computer games don't affect kids; I mean if Pac Man affected us as kids, we would all be running around in darkened rooms, munching magic pills, and listening to repetitive electronic music." - Kristian Wilson, Nintendo Inc. ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners