Xavier Leroy <Xavier.Leroy@inria.fr> writes:

> That's one way of putting it, but as Pierre Weis mentioned, fully
> polymorphic types such as 'a appear naturally during type inference
> for non-terminating expressions.

Yes, I found that quite cool.

> Semantically, it is correct to assign type 'a to any expression that
> never returns normally: there are no values of type 'a, but such
> expressions never result in a value.

It depends on what level of semantics you are looking at. As far as
type proofing is concerned, 'a is correct. However at a higher level
you can say `the function never returns so saying that it returns any
type is incorrect'. The problem is that some functions that do return,
return 'a. Ocaml's overloading of 'a, is much the same as lisps
overloading of nil and C's overloading of 0 or void*. You might
counter saying that 'a is defined in terms of type-unification, thus
reading additional meaning into the type is bogus. But such a view
denies the semantics of what is being typed. A computer language --
one of the important semantics of which is that is capable of capable
of generating functions that fail to return.

> Thread.exit should also have type unit -> 'a; the reason it currently
> has type unit -> unit is due to the way it is implemented
> (as Thread.kill(Thread.self())), but this is more of an historical
> accident.

I've used:

   let exit = Thread.exit (); assert false

to get the required type. While clearly a hack, it's better to use a
simple construct like this instead of having a casting to 'a
mechanism. Although I find full-bown determinacy types, mercury style
(but god forbid mercury heavy handed type syntax) quite appealing.

> Finally, concerning "while true do e done", there is only one typing
> rule in the type-checker for "while p do e done", which assumes that
> "p" may become false and the loop may thus terminate with the result
> "()", hence the "unit" type.

This is fair. I think an assert false at the end of the loop, or

let bottom f = f (); assert false
bottom (fun () -> while true do () done)

is effective. Although, once again, it'd be nice to see a 'bottom rather
than 'a type come out of this, even if the two are semantically equivalent
in the eye of the type checker.

Cheers,
Julian.