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 SAA19666 for caml-red; Mon, 2 Oct 2000 18:20:09 +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 PAA17209 for ; Mon, 2 Oct 2000 15:11:18 +0200 (MET DST) Received: from fledge.watson.org (fledge.watson.org [204.156.12.50]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e92DBGn15346 for ; Mon, 2 Oct 2000 15:11:17 +0200 (MET DST) Received: from localhost (patrick@localhost) by fledge.watson.org (8.9.3/8.9.3) with SMTP id JAA69056; Mon, 2 Oct 2000 09:11:01 -0400 (EDT) (envelope-from patrick@watson.org) Date: Mon, 2 Oct 2000 09:11:01 -0400 (EDT) From: Patrick M Doane To: Stefan Monnier cc: caml-list@inria.fr Subject: Re: bottom types and threaded exits In-Reply-To: <39d5f89a$1@tequila.cs.yale.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: weis@pauillac.inria.fr On 30 Sep 2000, Stefan Monnier wrote: > 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). 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. Patrick Doane