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

[skaller <skaller@users.sourceforge.net>]

On Fri, 2004-11-26 at 11:44, Jacques Garrigue wrote:

> But by definition 'a unifies with everything, including your void
> type, or you get a noncommutative notion of unification...

BTW: I still don't have a clear understanding of exactly
how problems arise with void with intensional polymorphism.
The typing with a distributive category is clearly sound.
AFAIK this extends to a cartesion closed category.

One might think that extra checks would be needed
which would have to be done at run time with intensional
polymorphism. For example:

let snd (x,y) = y

Here, 'a * 'b is isomorphic to void if 'a or 'b is void.
The definition of snd then doesn't make sense.
The actual problem, however, isn't void, but the incorrect
assumption that a pair can represent a polymorphic tuple:
it isn't the typing that is unsound, but the
choice of canonical representation of product.

The problem would go away if the pointer to the heap
block was NULL for void, but this would require
extra NULL checks at run time.

However, this particular example cannot ever lead
to a problem, since you can't actually create a variable
of void type (there's no value to put in it) so no
possible instantiation of 'snd' can fail.

[There is a clearly related issue with unit: the
types 'a and 1 * 'a are isomorphic, but the definition
of numbered projections prevents the useless unit
being optimised away -- the language guarrantees
not to apply this isormorphism simply because it
would break the run time representation.]

However I don't know if this argument can be extended
in the presence of function types. It would seem that
without a primitive function returning void, there's
no way to encode one that returns void either.

However if you have a primitive f:'a-> void you can
obviously create new functions returning void, for
example:

let g f x = f x
let h x = g f x

However I still don't see how you can ever call such a function
in a way that actually tries to pass a value of type void.
That value has to come from somewhere and there is no way
to make one: a call 

   f x

is manifestly of type void, and so, for example,

	(f x, 99)

is manifestly of type void.

My thinking is that if you can't catch an improper use
of void at compile time, then there can't be one
at run time either (in other words its quite sound).

I would like to see an example where this is not the case.
I'm suspicious, because void is the categorical initial,
and a fundamental part of many of the models for computing
I've seen based on category theory -- and my understanding
is that the CT approach is just an alternative to lambda calculus
(i.e. they're equivalent).

So it looks to me that not providing an algebraic void
is a way to simplify the representation -- not a matter
of unsoundness.

BTW: Ocaml unification must already handle void: it supports
intersection types internally, and int & float is void.
How is it that this also doesn't lead to non-commutative unification?

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net