Re: Void type?

[Geoffrey Alan Washburn <geoffw@cis.upenn.edu>]

Brian Hurt wrote:

> I'm not sure I agree with this- especially the proposition that unit == 
> truth.  

There really isn't anything to disagree with.  That is how the 
Curry-Howard Isomorphism is defined.

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

Firstly, as I said, OCaml's type system cannot be treated as a 
consistent logic: A logic where false cannot be proven.  This is a 
consequence of its many impure language features (including general 
recursion).

However, there is a difference between being unsafe and not being usable 
as a logic.

> So either this assumption is false, or unit is the 
> void type in the Ocaml type system.

Because it is possible to prove false using the OCaml type system, it is 
of course possible to prove anything, including a seeming proof that 
unit is void.  Just as you can prove that an int is a function.

> More pragmatically, I don't see any situation in which void can be used 
> where unit couldn't be used just as well, if not better.  

On the whole, the nature and utility of void is technical point that is 
not likely to come up typical programs.  It will probably become more 
relevant as dependently typed languages become more mainstream.

> The type of bottom (the function that either throws an exception or 
> never returns) in Ocaml is unit -> 'a.   Note that the return type of 
> this function, since it's completely unconstrained, can unify with any 
> other type.

I will again point out that void and bottom should not be conflated. 
Bottom is only really relevant in languages with subtyping, and does not 
have a logic interpretation in traditional logics.