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

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

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