Version française
Home     About     Download     Resources     Contact us    
Browse thread
Void type?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Brian Hurt <bhurt@j...>
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