From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id UAA05283 for caml-red; Thu, 5 Oct 2000 20:39:18 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA07738 for ; Thu, 5 Oct 2000 20:39:02 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e95Id1H15436; Thu, 5 Oct 2000 20:39:01 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id UAA10715; Thu, 5 Oct 2000 20:39:01 +0200 (MET DST) From: Pierre Weis Message-Id: <200010051839.UAA10715@pauillac.inria.fr> Subject: Re: bottom types and threaded exits In-Reply-To: <20001002182809.A13821@miss.wu-wien.ac.at> from Markus Mottl at "Oct 2, 100 06:28:09 pm" To: mottl@miss.wu-wien.ac.at (Markus Mottl) Date: Thu, 5 Oct 2000 20:39:01 +0200 (MET DST) Cc: caml-list@inria.fr X-Mailer: ELM [version 2.4ME+ PL28 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: weis@pauillac.inria.fr > On Mon, 02 Oct 2000, Patrick M Doane wrote: > > This may be too obvious to point out, but that statement isn't always > > true. From the Pervasives library: > > > > val input_value : in_channel -> 'a > > > > clearly returns. I don't quite understood why the return type isn't > > a monomorphic type variable though. > > The "input_value"-function is unfortunately not type safe: you can "cast" > whatever data you get from the channel to any kind of type - whether this > is correct or not. There is currently no better way to do it if you want to > reconstruct marshalled data (data that was sent with output_value). You > have to trust that the OCaml-data you get is of the type you expect. > > Pierre mentioned that there is work going on in this field (a PhD-thesis) > that should make I/O much safer. Is there any news about this? > > Best regards, > Markus Mottl > > -- > Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl Nothing to add to Markus explanation, except that the type of (the equivalent of) input_value in the new system is Forall $a. in_channel -> $a the $ in $a meaning that this is not a regular structural polymorphic type parameter, but a special ``dynamic'' type parameter (with special typing rule and compilation). Jun Furuse is working on the subject. His PhD-thesis is on the way (more than 150 pages written). The type system and compiler are up and running on top of a 2.99 Objective Caml system. The current plan is to distribute this version as soon as the final draft of the thesis is achieved, since the thesis definitively has the highest priority. Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/