Re: [Caml-list] Re: Void type?

["Christopher L Conway" <cconway@cs.nyu.edu>]

I'm no expert on this subject, but I'd like to pause this thread to
point out that we  have, on the one hand, people trying to explain the
Curry-Howard isomorphism and, on the other, people trying to explain
the pragmatics of the OCaml type system, and that it does not appear
that this thread is converging towards either party comprehending the
other...

So... from the Curry-Howard perspective the "void" (uninhabited) type
represents false, because it is a proposition (=type) that has no
proofs (=values). I think (and here I'm treading on thin ice) that a
type (X -> void) would represent a reductio ad absurdum proof of (not
X) whereas a type (void -> X) would simply have no meaning. If you're
interested in the connection between ML and Curry-Howard, and you have
some spare time, you might read:
research.microsoft.com/~simonpj/papers/not-not-ml/index.htm

Chris

On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> Geoffrey Alan Washburn wrote:
>
> > 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.
>
>
> 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).  So either this assumption is false, or unit is the
> void type in the Ocaml type system.
>
> 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.  Specially, the
> utility of void type is strictly limited.  Given a function of type void
> -> whatever, you can't call it- because to call it, you need to create a
> value of type void, and by definition the type void has no element.  You
> can create empty data structures of type void, but (since you can't
> change the type held by the data structure) you can never add elements
> to the data structure.
>
> 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.
>
> Brian
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>