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 QAA05183; Mon, 29 Apr 2002 16:14:54 +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 QAA05179 for ; Mon, 29 Apr 2002 16:14:53 +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 g3TEErD25857 for ; Mon, 29 Apr 2002 16:14:53 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:nHKTsCRuD7nH/OgbLnGpm9M1O+FON3CO@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id QAA3818997 for ; Mon, 29 Apr 2002 16:14:52 +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 QAA103029307 for ; Mon, 29 Apr 2002 16:14:52 +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 g3TEEpd16898 for ; Mon, 29 Apr 2002 16:14:52 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:bjPeDe5Ps1OGYWvLHGekW+cTh+9yQgFj@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g3TEEpW12078 for ; Mon, 29 Apr 2002 16:14:51 +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 g3TEEn615612 for ; Mon, 29 Apr 2002 16:14:49 +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 g3TEEoh02537; Mon, 29 Apr 2002 16:14:50 +0200 Message-ID: <3CCD55BD.6DB352F5@ps.uni-sb.de> Date: Mon, 29 Apr 2002 16:16:29 +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: caml-list@inria.fr Subject: Re: [Caml-list] Polymorphic Variants and Number Parameterized Types References: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk "Krishnaswami, Neel" wrote: > > Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote: > > Neel Krishnaswami wrote: > > > > > There's no recursion in the module system because that would break > > > the termination guarantee. If you think of modules as records, and > > > functors as lambda abstractions, you can see that the module system > > > defines a simply-typed lambda calculus. As you've noticed with C++, > > > adding recursion to it would mean you can write nonterminating module > > > expressions. (All this is wonderfully clearly explained in > > > the paper, "A modular module system".) > > > > I'm not sure about "simply-typed". Did the situation change since > > that of http://caml.inria.fr/archives/199907/msg00027.html ? > > Wow! I didn't even know that was possible. I thought that typechecking > record subtyping was decidable...? Well, module types are (a limited form of) dependent types. What concretely triggers undecidability of subtyping in OCaml is the presence of abstract module types, at least in combination with the contravariance of higher-order functors. 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. In this setting, adding abstract signatures would at least require adding polymorphic kinds, I believe. [1] @inproceedings{Russo:NonDependentTypes, author = "Claudio Russo", title = "Non-Dependent Types for {Standard} {ML} Modules", booktitle = "International Conference on Principles and Practice of Declarative Programming", address = "Paris, France", year = 1999, month = sep, } -- 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