Browse thread
bottom types and threaded exits
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Julian Assange <proff@i...> |
| Subject: | bottom types and threaded exits |
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.