On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> I'm not sure I agree with this- especially the proposition that unit ==
> truth.  That would make a function of the type:
>     unit -> 'a
> equivelent to the proposition "If true then for all a, a", which is
> obviously bogus.  The assumption of the Ocaml type system is that you
> can not form "false" theorems within the type system (these correspond
> to invalid types).

Hence why (as you point out) any function which inhabits that type
must either throw an exception, abort the program, or loop, each of
which are a signal that there is a logical error in the program
(ignoring the use of exceptions as control structures).  But since
O'Caml's type system is not as powerful as, say, Coq's, it must let
such propositions through and instead catch them at runtime.

Take for example List.hd: 'a list -> 'a.  This is not a valid
proposition, since it claims we can construct any value from the empty
list.  But everything's OK, since Caml deals with this situation by
raising an exception at runtime.  The type system only lets List.hd
typecheck because it's perfectly aware that, thanks to its call to
"failure", it will never follow an execution path which triggers this
inconsistency.

- Chris