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

[Arnaud Spiwack <arnaud.spiwack@gmail.com>]

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>

Of course there are various ways to get the same for void2 :
# let void2_elim1 (x:void2) = assert false;;
val void2_elim1 : void2 -> 'a = <fun>

# let rec void2_elim2 (x:void2) = void2_elim2 x;;
val void2_elim2 : void2 -> 'a = <fun>

# let void2_elim3 (x:void2) = Obj.magic x;;
val void2_elim3 : void2 -> 'a = <fun>


But none of these are really functional/well typed except maybe 
void2_elim2 but it looks like cheating. Of course these are all safe 
because void has no closed instance. But I'd consider void1 to be 
morally much more satisfying. It really contains the essence of what a 
void type should be.



Arnaud Spiwack

Richard Jones a écrit :
> On Sun, Jul 29, 2007 at 01:36:24PM +0200, Arnaud Spiwack wrote:
>   
>> Jon Harrop a écrit :
>>     
>>> On Sunday 29 July 2007 12:05:47 Arnaud Spiwack wrote:
>>>  
>>>       
>>>> It is the good solution if you work with the original syntax (and it's
>>>> absolutely equivalent to the dual definition in term of empty variant
>>>> which you can write in the revised syntax).
>>>>    
>>>>         
>>> I don't quite understand this "empty variant from the revised syntax 
>>> thing". How is:
>>>
>>>  type void
>>>
>>> not an empty variant?
>>>
>>>  
>>>       
>> Well, not technically I believe. It's a type with no definition. I 
>> wouldn't be adamant about that but I reckon it's not considered as a sum 
>> type by OCaml type system.
>> Plus you cannot write the empty matching :
>>       match x with []
>> in the original syntax, preventing you from writing a function of type 
>> void -> 'a  without using exceptions or Obj.magic or an obviously 
>> looping function or such.
>>
>> Thus it does not really have the logical behavior of an empty variant.
>>     
>
> Can you explain what you mean a bit more?
>
> type void1 = { v: 'a. 'a };;
> let f (_ : void1) = 1;;
> --> val f : void1 -> int = <fun>
> let f () : void1 = failwith "error";;
> --> val f : unit -> void1 = <fun>
>
> type void2;;
> let f (_ : void2) = 1;;
> --> val f : void2 -> int = <fun>
> let f () : void2 = failwith "error";;
> --> val f : unit -> void2 = <fun>
>
> They seem to be fairly similar to me.
>
> Rich.
>
>