Version française
Home     About     Download     Resources     Contact us    
Browse thread
bottom types and threaded exits
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Stefan Monnier <monnier+lists/caml/news/@R...>
Subject: Re: bottom types and threaded exits
>>>>> "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