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 KAA15594 for caml-red; Mon, 2 Oct 2000 10:18:30 +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 QAA11857 for <caml-list@pauillac.inria.fr>; Sat, 30 Sep 2000 16:29:05 +0200 (MET DST)
Received: from tequila.cs.yale.edu (tequila.cs.yale.edu [128.36.229.152])
	by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e8UET4X04735
	for <caml-list@inria.fr>; Sat, 30 Sep 2000 16:29:04 +0200 (MET DST)
Received: from tequila.cs.yale.edu (localhost [127.0.0.1])
	by tequila.cs.yale.edu (8.9.3/8.9.3) with SMTP id KAA28343
	for <caml-list@inria.fr>; Sat, 30 Sep 2000 10:28:48 -0400
To: caml-list@inria.fr
From: "Stefan Monnier" <monnier+lists/caml/news/@RUM.cs.yale.edu>
Newsgroups: lists.caml
Subject: Re: bottom types and threaded exits
References: <wx4s37qj6b.fsf@foo.iq.org> <20000926111639.29744@pauillac.inria.fr> <wxzokqtf8r.fsf@suburbia.net>
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.0.90
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Path: rum.cs.yale.edu
NNTP-Posting-Host: rum.cs.yale.edu
Message-ID: <39d5f89a$1@tequila.cs.yale.edu>
Date: 30 Sep 2000 10:28:42 -0400
X-Trace: 30 Sep 2000 10:28:42 -0400, rum.cs.yale.edu
Sender: weis@pauillac.inria.fr

>>>>> "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