This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2000-09-26 (19:16) From: John Prevost Subject: Re: bottom types and threaded exits
```>>>>> "rv" == Remi VANICAT <remi.vanicat@labri.u-bordeaux.fr> writes:

rv> Julian Assange <proff@iq.org> writes:
>> 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.

>From what I can tell, what you're trying to do here is just make the
result type of a non-terminating computation go to 'a.  This is
actually quite easy--you just need to loop in a way that doesn't
constrain the type.  while ... do ... done always returns unit (which
is good, since usually you use it in a way that terminates.

The appropriate way to do it that will get type 'a is (in your case):

let rec f () = f ()

Note that if you choose the more direct translation

let rec f () = if true then f ()

you get constrained to type unit -> unit again, since a one-branched
if returns unit for the else branch.

So, an example of a vaguely useful function would be:

let rec call_forever f x = f x; call_forever f x

which has type:

val call_forever : ('a -> 'b) -> 'a -> 'c

So, it is not so much that 'a as bottom is a hack, as that the system
only produces such types when the result type is totally
unconstrained--and that doesn't happen with things like while loops,
only with recursion--where a function always returns the result of
calling itself (or another such function.)

John.

```