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 LAA13406; Tue, 7 May 2002 11:12:04 +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 LAA13338 for ; Tue, 7 May 2002 11:12:03 +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 g479C2v05290; Tue, 7 May 2002 11:12:02 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:EDO4bMlhNUcWQ9GVyceEBGxoyPKzISpN@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id LAA4674009; Tue, 7 May 2002 11:12:01 +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 LAA109255455; Tue, 7 May 2002 11:12:00 +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 g479Bxd14950; Tue, 7 May 2002 11:11:59 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:E+dPgniqk5j/jlI/2E8xebqiMFpmaW5t@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002050600) with ESMTP id g479BwG26258; Tue, 7 May 2002 11:11:59 +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 g479Bv618597; Tue, 7 May 2002 11:11:57 +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 g479Bwh20117; Tue, 7 May 2002 11:11:58 +0200 Message-ID: <3CD79ADF.57E5B040@ps.uni-sb.de> Date: Tue, 07 May 2002 11:14:07 +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] Re: Encoding "abstract" signatures References: <3CCD55BD.6DB352F5@ps.uni-sb.de> <20020429172853.A6314@pauillac.inria.fr> <3CCD794B.142F65D@ps.uni-sb.de> <20020430090732.A16788@pauillac.inria.fr> <000701c1f032$a69072c0$e8abfea9@melbourne> <20020430171846.A28745@pauillac.inria.fr> <000801c1f112$d4c266e0$e8abfea9@melbourne> <20020502094713.D27687@pauillac.inria.fr> <3CD107B5.E300E47E@ps.uni-sb.de> <20020506092740.B11517@pauillac.inria.fr> Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk François, > It would be interesting to devise a type system that has this property. Didier > Rémy noticed the need for such a feature back in 1994 when writing `Dynamic > typing in polymorphic languages' (see section 4.2 of the SRC tech report). Ah, indeed, he is discussing something quite similar. Interesting. But I strongly suspect that even a system like that wouldn't be enough to encode OCaml's modules. Consider that higher-order type again: functor(Y : sig module type T end) -> functor(X : Y.T) -> ... The idea was representing this as Forall k. forall T:(k->*). forall ts:k. T(ts) -> ... (*) But that is still not good enough, because we might apply T = sig module type U module type V end The result had to be something like Forall k1. Forall k2. forall U:(k1->*). forall V:(k2->*). ... so (*) is not an appropriate encoding -- application may also result in an indefinite number of kind quantifiers. We might try to tackle that by introducing another universe of "hyperkinds" and repeat the same trick. But unfortunately, that just pushes the problem to yet another level -- no finite number of additional universes will help, because what OCaml provides with nested abstract signatures is essentially Type:Type. So I conjecture that it is impossible to faithfully encode OCaml's modules into a non-dependent system (which comes to no surprise taking into account that it is known to be undecidable). -- 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