Re: Void type?

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

Arnaud Spiwack wrote:

> Well, I don't really know why to use a void type in OCaml as well, thus 
> my answer may be quite abstract. But when I provide a new type, I give a 
> way to build it and a way to use it. In the case of the void type, there 
> is no way to build an element of that type, but there is a way to use 
> one such element : a void element can be used in place of any type.

I think this is a slightly, or perhaps merely subtly, misleading 
characterization.  A void type (0), not to be confused with "void" as 
used by C, Java, etc. is a type without any inhabitants.  It is the the 
programming language equivalent of falsehood in logic.  Dually, the unit 
type (1), called "unit" in OCaml, has a single inhabitant and is the 
programming language equivalent of truth in logic.

It is important to distinguish between a void element and the reasoning 
principle provided by its elimination form.  A term of type void cannot
be used in place of any type, but its elimination form which can be
realized as a function with the signature

   val elim_void : void -> 'a

can be used to seemingly produce a value of any type.

However, most realistic programming languages are not usable as 
consistent logics, and therefore have means to construct "proofs of 
falsehood", that is expressions with a void type.  If you are using a 
type-safe language, unless you are subverting the type system, for 
example by using Obj.magic, all of these "proofs" are usually a 
diverging expression or one that makes use of some kind of control 
transfer such as an abort, invoking continuation, or raising an 
exception.  So any implementation of elim_void will never actually 
return a value of any type.

Elements of a "bottom" type more closely model something that may be 
used at any type.  Bottom types show up more often in languages with 
subtyping, where they are subtypes of all types.  The null value in 
Java, while not having an explicit type of its own (to my knowledge) is 
a good example of a bottom element.

Hopefully this clarifies some confusion and conflation going on in this 
thread.