Re: bottom types and threaded exits

[Pierre Weis <Pierre.Weis@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/