Re: [Caml-list] Why doesn't ocamlopt detect a missing ; after failwith statement?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: skaller <skaller@users.sourceforge.net>
> > But by definition 'a unifies with everything, including your void
> > type, or you get a noncommutative notion of unification...
> 
> Can you give an example? I presume you mean that 
> the invariant U(t1,t2) == U(t2,t1) would break?

Not exactly, I rather meant that unification steps would not commute.
This happens sometimes when you allow unification between specialized
forms, but not with type variables.
However, I do not understand completely what you mean by void type,
and how they would relate to type variables, so it is not clear
whether this is the problem.

For instance, you say that (void * t) should be void, which suggests
that void is really the type with 0 elements (i.e. not unit.)
However, from a logical point of view (i.e. intuitionistic logic), no
function can be allowed to return such a type. It may accept it as
input, but this just means it is unusable.
Note that void in C is definitely not zero. You cannot have variables
of type void, but you can have non-null pointers to void. If void were
really zero, then a void pointer would necessarily be NULL.
It looks more like an existential type, (\exists a.a), which is
actually equivalent to unit, with special rules to deal with the fact
its physical representation is unknown.

Concerning intersection types in ocaml, int&bool is not a type by
itself.  It may only appear as a variant argument. In that case this
just means that this variant case cannot be used. In the past, [ ] was
a valid variant type, and would have been zero, but I removed it as it
does not make sense, and may delay some type errors. Types with only
one variant may not be conjunctive either. So the closest you can get
to zero now is a polymorphic type like [< `A of int&bool | `B of int&bool].
Even with [ ] there was no problem of commutation, because
unification with 'a was allowed, i.e. ([ ] * int) and [ ] were
different types; which was why it was clumsy to have
zero in the language: there is nothing as stupid as moving provably
non-existing data around, as it means that the code will never be used
anyway.

Jacques Garrigue

P.S.
I believe the problem with failwith is solvable, albeit rather
complicated. The idea is that you want to be warned when you apply a
function of type (\forall 'a. 'a) to something, because no such
function may exist, so that this application will never actually take
place.
This could be done attempting to generalize the type of the function,
once we now it is a type variable.
I'll have a try.