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 VAA24761 for caml-red; Sun, 24 Sep 2000 21:16:01 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA22292 for <caml-list@pauillac.inria.fr>; Sun, 24 Sep 2000 10:58:17 +0200 (MET DST)
Received: from dopamine.iq.org (dopamine.iq.org [203.4.184.129])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e8O8wET05015
	for <caml-list@inria.fr>; Sun, 24 Sep 2000 10:58:15 +0200 (MET DST)
Received: by dopamine.iq.org (Postfix, from userid 110)
	id 152DD10F41; Sun, 24 Sep 2000 01:25:50 +1100 (EST)
To: caml-list@inria.fr
Subject: bottom types and threaded exits
Cc: proff@iq.org
From: Julian Assange <proff@iq.org>
Date: 24 Sep 2000 01:25:48 +1100
Message-ID: <wx4s37qj6b.fsf@foo.iq.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Sender: weis@pauillac.inria.fr


Pervasives.exit is of type int -> 'a

Here we see ocaml using 'a to represent _|_. This hack is presumably
so type unification still works in the face of potentially
non-terminating computations, e.g:

let f a =
        try 
          f a
        with
          Failure _ -> exit(1)

How can one force 'a? For instance, Thread.exit and

        let f () = while true do () done 

has a type of unit -> unit.

One can write something such as

        let f () = while true do () done ; Pervasives.exit (1)

But this is clearly a hack.

If the type of Pervasices.exit is traced back, it originates in the
`external affairs powers' of the ocaml type system and is thus not
prone to type inferment. Functions never normally cause an *increase*
in generality. Trying to define a type of int -> 'a naturally leads
to a compiler error of 'a being unbound.

Cheers,
Julian.