This site is updated infrequently. For up-to-date information, please visit the new OCaml website at 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:11) From: Brian Hurt Subject: Re: [Caml-list] Re: Void type?
```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

```