Void type?

Void type?

[Stefan Monnier]

Is there a void type in OCaml (i.e. a type which has no values), or a way to
simulate it?


        Stefan

Re: [Caml-list] Void type?

[Erik de Castro Lopo]

Stefan Monnier wrote:

> 
> Is there a void type in OCaml (i.e. a type which has no values), or a way to
> simulate it?

Yes, the unit type which is written "()".

    Objective Caml version 3.09.2
    # let x = () ;;
    val x : unit = ()

Unit can also be returned from a function, and a function
can have its input of type unit:

    # let f () = 3.141 ;;
    val f : unit -> float = <fun>

Erik
-- 
-----------------------------------------------------------------
Erik de Castro Lopo
-----------------------------------------------------------------
"Unix and C are the ultimate computer viruses." -- Richard P Gabriel

Re: [Caml-list] Void type?

[Chris King]

On 7/28/07, Stefan Monnier <monnier@iro.umontreal.ca> wrote:
> Is there a void type in OCaml (i.e. a type which has no values), or a way to
> simulate it?

If you're looking for a "true" void (as opposed to the unit type,
which has exactly one value), just declaring it as an abstract type:

type void

should do the trick.  You will be unable to instantiate any values of
that type using pure O'Caml (i.e. no Obj.magic or C code).

- Chris

Re: [Caml-list] Void type?

[Daniel de Rauglaudre]

Hi,

On Sat, Jul 28, 2007 at 12:14:40AM -0400, Stefan Monnier wrote:
> 
> Is there a void type in OCaml (i.e. a type which has no values), or a way to
> simulate it?

You can do that with the revised syntax in Camlp5 :
    type t = [];

No equivalent in normal syntax.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

Re: Void type?

[Chung-chieh Shan]

Stefan Monnier <monnier@iro.umontreal.ca> wrote in article <jwvvec5dv32.fsf-monnier+gmane.comp.lang.caml.inria@gnu.org> in gmane.comp.lang.caml.inria:
> Is there a void type in OCaml (i.e. a type which has no values), or a way to
> simulate it?

type void = Void of void

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
It is the first responsibility of every citizen to question authority.
Benjamin Franklin

Re: Void type?

[Sébastien Hinderer]

Stefan Monnier :
> 
> Is there a void type in OCaml (i.e. a type which has no values), or a way to
> simulate it?

What about
type void = { v : void };;
?

Sébastien.

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

[Basile STARYNKEVITCH]

Sébastien Hinderer wrote:
> Stefan Monnier :
>> Is there a void type in OCaml (i.e. a type which has no values), or a way to
>> simulate it?
> 
> What about
> type void = { v : void };;

You can build such a value with
let rec vv = { v = vv };;

Generally speaking, the unit type whose single value is () is used in Ocaml for what C calls the void type: unit 
returning functions are procedures.

A void type would be useful for bizarre functions like f : int -> void
this would mean that f never returns normally, i.e. that it loops indefinitely, or
calls exit (to stop the entire program), or throws an exception but never returns.

AFAIK, there is no such void type in Ocaml (but some members of Gallium did publish papers mentioning void).

However, there is one thing I did not understand: why (= what for) does Stefan Monnier want a void type?


-- 
Basile STARYNKEVITCH         http://starynkevitch.net/Basile/
email: basile<at>starynkevitch<dot>net | mobile: +33 6 8501 2359
8, rue de la Faiencerie, 92340 Bourg La Reine, France
*** opinions {are only mine, sont seulement les miennes} ***

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

[rossberg]

Chung-chieh Shan wrote:
> Stefan Monnier <monnier@iro.umontreal.ca> wrote in article
> <jwvvec5dv32.fsf-monnier+gmane.comp.lang.caml.inria@gnu.org> in
> gmane.comp.lang.caml.inria:
>> Is there a void type in OCaml (i.e. a type which has no values), or a
>> way to
>> simulate it?
>
> type void = Void of void

Dont't forget OCaml's let-rec:

  let rec v = Void v

works like a charm.

Sébastian Hinderer wrote:
> What about
> type void = { v : void };;

Same here:

  let rec v = {v = v}

Since there are no empty polymorphic variants either (there used to be in
earlier versions, IIRC), the only solution is:

Chris Kings wrote:
> type void

This is a *declaration*, and as such defines a new abstract type that is
uninhabited, as desired.

- Andreas

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

[Christophe TROESTLER]

On Sat, 28 Jul 2007 10:13:03 +0200, Basile STARYNKEVITCH wrote:
> 
> A void type would be useful for bizarre functions like f : int ->
> void this would mean that f never returns normally, i.e. that it
> loops indefinitely, or calls exit (to stop the entire program), or
> throws an exception but never returns.

And even then

  f : int -> 'a

may be more appropriate.

My 0.02€,
ChriS

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

[Brian Hurt]

On Sat, 28 Jul 2007, Basile STARYNKEVITCH wrote:

> A void type would be useful for bizarre functions like f : int -> void 
> this would mean that f never returns normally, i.e. that it loops 
> indefinitely, or calls exit (to stop the entire program), or throws an 
> exception but never returns.

The proper type for these functions would be f : int -> 'a.  Take a look 
at invalid_arg and failwith as examples.  The advantage of having them 
return an unbound 'a is that then unifies with any other given type, 
allowing you to write code like:

 	if (some_test) then
 		some_value
 	else
 		invalid_arg "some_test failed!"

and have it work for all possible return types of some_value.

Brian

Re: [Caml-list] Void type?

[Stefan Monnier]

>> Is there a void type in OCaml (i.e. a type which has no values), or a way to
>> simulate it?

> If you're looking for a "true" void (as opposed to the unit type,
> which has exactly one value), just declaring it as an abstract type:

> type void

> should do the trick.  You will be unable to instantiate any values of
> that type using pure O'Caml (i.e. no Obj.magic or C code).

But can I pass [] to a function that expects a "void list"?


        Stefan

Re: [Caml-list] Void type?

[Basile STARYNKEVITCH]

Stefan Monnier wrote:
>>> Is there a void type in OCaml (i.e. a type which has no values), or a way to
>>> simulate it?
> 
>> If you're looking for a "true" void (as opposed to the unit type,
>> which has exactly one value), just declaring it as an abstract type:
> 
>> type void
> 
>> should do the trick.  You will be unable to instantiate any values of
>> that type using pure O'Caml (i.e. no Obj.magic or C code).
> 
> But can I pass [] to a function that expects a "void list"?


Yes. It is the only list of type void list.

-- 
Basile STARYNKEVITCH         http://starynkevitch.net/Basile/
email: basile<at>starynkevitch<dot>net | mobile: +33 6 8501 2359
8, rue de la Faiencerie, 92340 Bourg La Reine, France
*** opinions {are only mine, sont seulement les miennes} ***

Re: [Caml-list] Void type?

[Arnaud Spiwack]

> But can I pass [] to a function that expects a "void list"?
>   
If you want to do this sort of things. Then you have two basic ways :

1/ using the revised syntax :
    type void = []; .
    which has an elimination principle  let void_elim x = match x with [];

2/ using an abstract module with declarations :
    type void
    val  void_elim : void -> 'a

   This module would be the generic representation of a void type. It 
can be instantiated by the concrete definitions in 1/.
   Another way is to cheat :
      type void = unit
      type void_elim = Obj.magic

  This implementation is sound since there is no way provided to build 
an element of type void, thus void elim will never be executed.


Depending on what exactly you want to do you might disregard the 
elimination principle. But it's inherently part of the void logic.


Regards,
Arnaud Spiwack

Re: [Caml-list] Void type?

[Stefan Monnier]

>>> type void
>> But can I pass [] to a function that expects a "void list"?
> Yes.  It is the only list of type void list.

Looks like what I was looking for.  Thanks,


        Stefan

Re: Void type?

[Chung-chieh Shan]

rossberg@ps.uni-sb.de wrote in article <61777.84.165.172.53.1185610925.squirrel@www.ps.uni-sb.de> in gmane.comp.lang.caml.inria:
> Chung-chieh Shan wrote:
> > type void = Void of void
> Dont't forget OCaml's let-rec:
>   let rec v = Void v
> works like a charm.

Oops!  Thanks.  I guess contravariance in charm is a curse. (:

What about:

    # type void = { v: 'a. 'a };;
    type void = { v : 'a. 'a; }
    # let rec vv = { v = vv };;
    This field value has type 'a which is less general than 'b. 'b

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
People are oddly consistent.

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

[Arnaud Spiwack]

> What about:
>
>     # type void = { v: 'a. 'a };;
>     type void = { v : 'a. 'a; }
>     # let rec vv = { v = vv };;
>     This field value has type 'a which is less general than 'b. 'b
>   
Now that's a very nice solution. You give the impredicative coding of 
the void type (forall 'a. 'a) by boxing it into record type.

You get void_elim withouth cheating :
  let void_elim x = x.v

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).

Well spotted.


Arnaud Spiwack

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

[Jon Harrop]

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?

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?e

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

[Arnaud Spiwack]

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.




Arnaud Spiwack

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

[Richard Jones]

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.

-- 
Richard Jones
Red Hat

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

[Arnaud Spiwack]

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.
>
>   

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

[Richard Jones]

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.

-- 
Richard Jones
Red Hat

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

[Arnaud Spiwack]

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

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

[Brian Hurt]

On Sun, 29 Jul 2007, 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.

This is why you can not build an element of void type (without Obj.magic)- 
as there is no value which can be (safely) used as any type.  Using 
Obj.magic to create such void types will simply lead to segfaults and 
mysterious bugs in your code, and thus nullify the main advantages of 
Ocaml.  The main reason I can see to use void types is to introduce 
Java-style nulls into Ocaml.  The lack of Java-style nulls is one of the 
main reasons I like Ocaml.

If you want to have a "nullable" type, use 'a option or the equivalent. 
If you want to have a "no value" type, use unit.  As a general rule, if 
you find yourself fighting the type system, step back, rethink the 
problem, and find a solution that works with the type system and not 
against it- you'll generally end up with better code.

Brian

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

[skaller]

On Sun, 2007-07-29 at 22:06 +0200, Arnaud Spiwack wrote:

> 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.

It is used like this in Felix:

  type void
  type proc = unit -> void
  exception Ok
  let squash () : void = raise Ok
  let call (f:proc) : unit = try ignore(f ()) with Ok -> ()
  let seq (fs: proc list): proc = 
	fun () -> squash (List.iter call fs)

  (* example *)

  let x = ref 0
  let f () : void = squash (incr x)
  let incr3 : proc = seq [f;f;f];;
  call incr3;;
  print_endline ("x=" ^ string_of_int !x);;

You can write combinators such as 'cond' and 'loop' as well.
The combinators are purely functional and lazy, except 'call'
which forces side-effecting.

The advantage is the type system prevents some accidents:

	let f () = incr x;;
	f (f ());; (* woops *)

by using the fact that void has no values, to prevent using
the application of a procedure as the argument of an function.

Given a purely functional library .. you could probably
design a purely functional camlp4/5 syntax, then you'd
actually get referential transparency. 

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: Void type?

[Geoffrey Alan Washburn]

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.

However, most realistic programming languages are not usable as 
consistent logics, and therefore have means to construct "proofs of 
falsehood", that is expressions with a void type.  If you are using a 
type-safe language, unless you are subverting the type system, for 
example by using Obj.magic, all of these "proofs" are usually a 
diverging expression or one that makes use of some kind of control 
transfer such as an abort, invoking continuation, or raising an 
exception.  So any implementation of elim_void will never actually 
return a value of any type.

Elements of a "bottom" type more closely model something that may be 
used at any type.  Bottom types show up more often in languages with 
subtyping, where they are subtypes of all types.  The null value in 
Java, while not having an explicit type of its own (to my knowledge) is 
a good example of a bottom element.

Hopefully this clarifies some confusion and conflation going on in this 
thread.

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

[Brian Hurt]

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

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

[Christopher L Conway]

I'm no expert on this subject, but I'd like to pause this thread to
point out that we  have, on the one hand, people trying to explain the
Curry-Howard isomorphism and, on the other, people trying to explain
the pragmatics of the OCaml type system, and that it does not appear
that this thread is converging towards either party comprehending the
other...

So... from the Curry-Howard perspective the "void" (uninhabited) type
represents false, because it is a proposition (=type) that has no
proofs (=values). I think (and here I'm treading on thin ice) that a
type (X -> void) would represent a reductio ad absurdum proof of (not
X) whereas a type (void -> X) would simply have no meaning. If you're
interested in the connection between ML and Curry-Howard, and you have
some spare time, you might read:
research.microsoft.com/~simonpj/papers/not-not-ml/index.htm

Chris

On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> 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
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: Void type?

[Geoffrey Alan Washburn]

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.

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

[Chris King]

On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> 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).

Hence why (as you point out) any function which inhabits that type
must either throw an exception, abort the program, or loop, each of
which are a signal that there is a logical error in the program
(ignoring the use of exceptions as control structures).  But since
O'Caml's type system is not as powerful as, say, Coq's, it must let
such propositions through and instead catch them at runtime.

Take for example List.hd: 'a list -> 'a.  This is not a valid
proposition, since it claims we can construct any value from the empty
list.  But everything's OK, since Caml deals with this situation by
raising an exception at runtime.  The type system only lets List.hd
typecheck because it's perfectly aware that, thanks to its call to
"failure", it will never follow an execution path which triggers this
inconsistency.

- Chris

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

[Jeff Polakow]

[-- Attachment #1: Type: text/plain, Size: 1482 bytes --]

Hello,

> > 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.
> 
As others have mentioned the motivation for an elimination principle comes 
from the Curry-Howard isomorphism. In case you're wondering, the actual 
phrase "elimination principle" (or rule, or form, or whatever) comes from 
the presentation of formal logic as a natural deduction system which is a 
bunch of rules describing how to create valid logical deductions. The 
rules of a natural deduction system are divided into introduction rules, 
which explain how to deduce a formula (e.g. if you can deduce A and you 
can deduce B then you can deduce A & B), and elimination rules, which 
explain how a deduced formula can be used (e.g. if you can deduce A & B 
then you can deduce A). Here is a wikipedia article with more detail: 
http://en.wikipedia.org/wiki/Natural_deduction

-Jeff


---

This e-mail may contain confidential and/or privileged information. If you 
are not the intended recipient (or have received this e-mail in error) 
please notify the sender immediately and destroy this e-mail. Any 
unauthorized copying, disclosure or distribution of the material in this 
e-mail is strictly forbidden.

[-- Attachment #2: Type: text/html, Size: 2252 bytes --]

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

[Christophe Raffalli]

>
>
> 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.
>
Personnally, I think that we should have more subtyping than in OCaml. 
Then, "void" is the smallest type (and quite equivalent to 'a.'a) 
and "unit" is the bigest type. This looks natural for "void" and more 
surprising for "unit", but you can see that you can do nothing with a 
value of type unit (except matching it, which is not much), which mean 
that is you do not match unit (you use "_" everywhere you would use "()" 
in pattern), then any value can be safely cast to the unit type ... So 
"void" is really the dual of "unit" and they are very distinct.

Christophe

PS: In PML it works like that (our server is down, so please wait 
tomorrow if you want to try PML)

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

[Markus Mottl]

On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> 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.

Indeed, this proposition is impossibly true.

> 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.

I guess you mean that one cannot form proofs of propositions that
don't have a model (i.e. an interpretation that makes the proposition
true).  There is a false dichotomy here.  It rests on the assumption
that a pure program that has such a type is a proof of the proposition
whereas in fact it isn't.  The assumption that programs are proofs
only makes sense if every program is strongly normalizing, i.e.
requires only a finite amount of evaluation (= "proof") steps.  This
is always the case with e.g. the pure, simply typed lambda calculus
without fixed-point operator, which is strongly normalizing.
Something that requires an infinite number of derivation steps cannot
be considered a proof.

If we constrained ourselves to programs that are proofs only, and if
we required soundness, too, then there would be satisfiable
propositions for which, indeed, you wouldn't be able to write down a
program of corresponding type: some solvable problems would become
unsolvable to us.

OCaml is not unsound.  It is also not incomplete in the sense that you
cannot write down a terminating program for a proposition that has a
model.  But this unfortunately necessarily implies that you can write
down programs that are not proofs, i.e. never terminate.

Note that you can also write down the type "unit -> unit", which is a
tautology and therefore trivially true in any interpretation.  But you
can still write down a program of this type that doesn't constitute a
proof of the corresponding proposition irrespective of how trivial it
may be:

  let rec f () = f (f ())

Provability and truth are two distinct concepts, you cannot conflate
the two in the general case.  This is a direct consequence of Goedel's
incompleteness theorem.

Some program may constitute a proof or not, and a type may correspond
to a satisfiable proposition or not.  We definitely don't want a
system that allows us to write down something that is a proof of a
false proposition (= unsound).  We want to be able to write down a
proof for every proposition that has a model (= completeness).  But
then we'll have to live with the presumably less awful fact that we
will be able to write down non-proofs of non-truths (and truths
alike)...

> 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.

You'll laugh, but I just actually made use of Chung-chieh Shan's trick
to use polymorphic record fields in our code base.  Here is a rough
idea of where this may be useful:

Assume you have a functor argument that defines several types and
functions operating on these types.  Now assume that I know that I
will never want to use the module resulting from the functor
application in a way that requires the use of some of these types and
associated functions in the functor argument.  How can I make sure
that nobody will ever do something with the resulting module that
violates these assumptions?  E.g.:

---------------------------------------------
module type ARG = sig
  type t
  type u

  val use_t : t -> unit
  val use_u : u -> t
end

module Func (Arg : ARG) = struct
  let propagate_t arg_t = Arg.use_t arg_t
  let propagate_u arg_u = Arg.use_u arg_u
end

type void = { void : 'a. 'a }

module Arg = struct
  type t = int
  type u = void

  let use_u u = u.void
  let use_t t = print_int t
end
---------------------------------------------

If I had specified "u" as "unit" in the above example, I would need to
e.g. raise an exception in "use_u" to indicate that my assumption was
violated, or return a dummy value (integer) which may screw up
something in the functor body, etc.  But having specified the value as
"void", I essentially get a proof at compile time that nobody will
ever be able to misuse the module resulting from the functor
application.

Of course, I could restrict the signature of the resulting module, but
this may be a non-trivial effort, e.g. if type "u" is used in sum
types of the resulting module, etc., in which case I'd have to wrap
the result in an intermediate module that translates function calls
accordingly.  The "void" solution on the other hand is just plain
awesome and solves this problem safely and conveniently.

Best regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

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

[Brian Hurt]

Just to nail this thread shut, I have been convinced of the utility of a 
void type (as distinct from the unit type) in pragmatic code.  Consider 
the following module signature:

module type Req = sig
 	type a
 	type b
end;;

module Example(Base: Req) = struct
 	type a_or_b =
 		| A of Base.a
 		| B of Base.b
 	;;

 	let foo (x: a_or_b list) = ...

end;;

An important point to notice here is that the Example module signature can 
not be factored into a "a part" and a "b part" without losing important 
capabilities- for example, being able to pass in a list that contains both 
a's and b's.  Even assuming you have full control of the source code and 
time and inclination (if needed) to refactor the code, a refactoring is 
still not possible.  So my blythe "just refactor the module" doesn't 
apply.

So how do I use that module and say, in the type system, "I will never 
pass in a b"?  This is where the void type comes in.  I can declare:

module Myreq = struct
 	type a = whatever;;
 	type b = void;;
end;;

module Myexample = Example(Myreq);;

Note that I can still call function Myexample.foo- I can call it with an 
empty list, or with a list of as many A's as I want.  But it's impossible 
for me to create a B element.

Brian

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

[Richard Jones]

On Mon, Jul 30, 2007 at 07:13:21PM -0400, Brian Hurt wrote:
> So how do I use that module and say, in the type system, "I will never 
> pass in a b"?  This is where the void type comes in.  I can declare:
> 
> module Myreq = struct
> 	type a = whatever;;
> 	type b = void;;
> end;;
> 
> module Myexample = Example(Myreq);;

Similar to Markus Mottl's practical example.  [I'm so glad that we're
getting practical uses out of this discussion ...]

The question is, which void type definition do you use?

  type void

or

  type void = { v: 'a. 'a }

It seems to me that your example could use either.  Markus uses the
second definition, but I don't understand particularly why he couldn't
use either.

Rich.

-- 
Richard Jones
Red Hat

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

[Chris King]

On 7/31/07, Richard Jones <rich@annexia.org> wrote:
> The question is, which void type definition do you use?
>
>   type void
>
> or
>
>   type void = { v: 'a. 'a }

Personally I would use the second.  That way, when you come across a
void value (say, in pattern matching a variant), you can take care of
that match case without resorting to "assert false" (whether directly
or via void_elim):

type t = A of int | B of void

match foo with
| A i -> print_int i
| B v -> v.v

It makes me feel all warm & fuzzy inside that one doesn't have to
resort to "assert false" here :)

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

[Markus Mottl]

On 7/31/07, Chris King <colanderman@gmail.com> wrote:
> Personally I would use the second.  That way, when you come across a
> void value (say, in pattern matching a variant), you can take care of
> that match case without resorting to "assert false" (whether directly
> or via void_elim):

This is the exact reason why I used this solution: the compiler
essentially proves to you that this branch will never be taken,
because it is impossible to create a value that is a member of any
type (without black magic, that is).  This is important if you want to
check your code for uncaught exceptions, especially if you eventually
want to do this mechanically.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

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

[Tom]

[-- Attachment #1: Type: text/plain, Size: 749 bytes --]

On 31/07/07, Brian Hurt <bhurt@spnz.org> wrote:
>
>
> So how do I use that module and say, in the type system, "I will never
> pass in a b"?  This is where the void type comes in.  I can declare:
>
> module Myreq = struct
>         type a = whatever;;
>         type b = void;;
> end;;
>
> module Myexample = Example(Myreq);;
>
> Note that I can still call function Myexample.foo- I can call it with an
> empty list, or with a list of as many A's as I want.  But it's impossible
> for me to create a B element.
>

I am still not convinced about the usability of the void type... Why simply
not declare type b as abstract?

module Myreq = struct
        type a = whatever
        type b
end

Essentially, it means the same, just less typing.

 - Tom

[-- Attachment #2: Type: text/html, Size: 1282 bytes --]

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

[Markus Mottl]

On 8/1/07, Tom <tom.primozic@gmail.com> wrote:
> I am still not convinced about the usability of the void type... Why simply
> not declare type b as abstract?
>
> module Myreq = struct
>         type a = whatever
>         type b
> end
>
> Essentially, it means the same, just less typing.

Less typing in the type definition, but more typing handling a
function or match branch that makes use of a value of type b.  You'd
either have to raise an exception there, or do something unsafe.  The
"void"-solution is much cleaner.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com