Version française
Home     About     Download     Resources     Contact us    
Browse thread
bottom types and threaded exits
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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.