Accueil     À propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Void type?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-07-30 (13:35) From: Geoffrey Alan Washburn Subject: Re: Void type?
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.