Re: [Caml-list] Custom operators in the revised syntax

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

On Sat, 2007-05-12 at 06:59 +0100, Jon Harrop wrote:

> > If ANYONE knows an algorithm that can do unification with
> > sets of types, that is, with a union type, I'd sure like
> > to know it!
> 
> Isn't this exactly what polymorphic variants do?

I don't think so, but here I need a theorist to give
a proper explanation.

I suspect part of what pm-variants do does indeed rely
on the fact that you have a finite set of discrete constructors
(variant tags).

However here, you will fail to get a unique constructor a LOT
of the time .. and that is OK, you just dispatch at run time
on the tag.

But int, float, long etc don't have tags or associated RTTI
in Felix when used as values (they do if they're boxed .. but
they're boxed by using a variant .. and that's a different type).

The point is that here, we actually need to resolve to 
a single type, equivalent to pm-variants resolving to
a single constructor. So the situation is different:

	f: [`Int of int | `Float of float] -> int

makes sense, use runtime dispatch but:

	f: [int | float] -> int

is nonsense -- unless the argument is ignored --
because you *cannot* dispatch. In Felix:

	typedef nums = typesetof(int,float);
	fun f[t in nums]: t -> int = "(int)$1";

makes sense, but only because it leverages C/C++
generic programming stuff, that is, it is extensionally
polymorphic (the compiler emits the code for every
call point and relies on (int)x being a generic in C).

Particularly, this *actually* means the same as:

	fun f: int -> int = "(int)$1";
	fun f: float -> int = "(int)$1";

that is, it's sugar for a type schema (first order
universal quantification) with an intersection constraint.

In Felix this kind of 'sugar' is more than just useful
for reducing several overloaded bindings to one, it is
quite mandatory for making it possible to write bindings
to libraries like OpenGL where the types are aliases
for unknown integer types. So a function like:

	void GLsetCoord(x:GLint, y:GLint)

is modelled by

	proc GLsetCoord: !ints * !ints;

which means you can call it like:

	GLsetCoord (1, 2L);

instead of having to cast every argument to GLint.


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