Re: bottom types and threaded exits

["Stefan Monnier" <monnier+lists/caml/news/@RUM.cs.yale.edu>]

>>>>> "Julian" == Julian Assange <proff@iq.org> writes:
> It depends on what level of semantics you are looking at. As far as
> type proofing is concerned, 'a is correct. However at a higher level
> you can say `the function never returns so saying that it returns any
> type is incorrect'. The problem is that some functions that do return,

A function of type "t1 -> t2" does not necessarily return an object of type t2.
But if it does return, then the value is of type t2.
Similarly, a function of type "t1 -> 'a" (if it returns) returns an value
of type 'a.  Parametricity allows us to infer from that that if t1 does
not contain 'a as a free type variable, then the function will necessarily
never return (since it has no way to construct an value of
type 'a).

It would maybe be a good idea to analyze the types based on a few
such parametricity-derived theorems and print a more meaningful type
(i.e. use 'noreturn rather than 'a for the above case or 'ignored
for an argument type 'a which appears only once).


        Stefan