Richard Jones a écrit :
> On Sun, Jul 29, 2007 at 02:58:23PM +0200, Arnaud Spiwack wrote:
>   
>> Here is what you can do with void1 and not with void2 :
>> type void1 = { v: 'a. 'a };;
>> # let void1_elim x = x.v;;
>> val void1_elim : void1 -> 'a = <fun>
>>     
>
> Maybe I should rephrase the question then.  What use is this function?
> The only Google searches for void type and the "elimination principle"
> all seem to point back to this very thread.
>
> Rich.
>   
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 don't know if it can come handy (it does in certain cases for 
dependant type programming in my experience). But it's part of the 
semantics of the type somehow. It is the function which says "void has 
no element". It occures to me that it might be needed if you need a void 
type.

One reason why it might be useful, is that it gives an equivalence 
between the types  t -> void   and  t -> 'a  (for any type t). Earlier 
in this thread it was mentioned that these sort of functions could be a 
reason to use a void type.

Since I have no concrete example in mind, I won't be able to be more 
specific. Still, there is something morally satisfying in being able to 
define this function without cheating, even if you don't need it. Uh 
well... then... what is morally satisfying is really a matter of tastes, 
I guess.


Arnaud Spiwack