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

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

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

> > I have only seen one algorithm for this an it was
> > extremely complicated. If you know a better way I'd
> > sure like to know what it is.
> 
> AFAIK, you just change the unify to intersect sets of types. 

I have no idea how to unify in the presence of (undiscriminated)
setwise union of polymorphic types. It seems a little easier
if the types are restricted to a finite set of non-polymorphic
types.

> I assume the 
> implementation of polymorphic variants already does this, so take that and 
> make it enforce a single type contructor at function boundaries (maybe 
> defaulting in some cases). If you "polymorphic variant" has more than one 
> constructor then there is an ambiguity and you flag an error asking for a 
> type annotation.

The difference is that polymorphic variants HAVE constructors.
But we're talking about types *without* constructors.

In Felix, the (Ocaml) term combinators actually support typesets.
But the unification engine just throws up when it sees them :)

During overload resolution, you CAN use typesets as constraints.
For example:

	typedef ints = typesetof(int, long);
	fun f[t in ints]: t * t -> t = "$1+$2";

	print$ f 1; // OK!
	print$ f 1L; // OK!
	print$ f 1.0; // ERROR

	fun g[t in ints](x:t)=> f x; // ERORR

The last line illustrates the lack of propagation: the type
of x is actually just 't' at the point f is applied,
and t isn't in the set ints.

The way it works is the argument is first matched against the
unconstrained type (by unification), and then the constraint
such as:

	int in typeset(int,long)

is checked: if it fails that overload candidate is rejected
(but another may still match).

In principle the correct 'subtyping' rule is to use a subset
(or superset depending on +/- position I guess) so that
it should be possible in this case to propagate and make
the function g above work.

The problem is that once you introduce polymorphism,
the type of one function can depend on the type of another,
but that type isn't known until that other is actually
instantiated.

This can not be handled 'properly' by just adding typesets to the 
type system because that would be too general: it fails to
record the dependencies. For example in the f/g case above,
the type of g is NOT

	g: ints -> ints

but rather

	g: { int -> int; long -> long }

and now consider a harder case like:

	t in ints. t * t = { int * int; long * long }

which is quite different to

	ints * ints = { int * int; int * long; long * int; long * long }

So roughly .. we're talking about a unification engine that
can propagate constraints, and a type system which would
seem to at least need to be second order. 

As I said I think this is possible for finite ground types,
but in the presence of polymorphism unification would not be
able to reduce many terms. In turn, this would make overloading
such cases impossible.

In Felix, overloading is done polymorphically, and can't
vary depending on the instantiation of type variables
(you can do that with typeclasses though).

But unless you instantiate the type variables, you can't
reduce the terms. It isn't clear it is even possible to
normalise them for equality check, let alone tell if
one is a specialisation of another.

The result, in Felix, is that overloading would have to
return a SET of functions instead of a single one,
since several functions 'might' match the argument type.
And the set could be large -- it seems exponential in
the length of a call chain. Ouch.

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!

> .NET provides run-time type information so I assume the compiler specializes 
> when types are static and resorts to run-time dispatch otherwise.

That seems right. I think G'Caml tried to do that was well.

> > and this kind of constraint, unfortunately, doesn't propagate
> > (i.e. the above isn't really a type). Propagating ground
> > type sets is actually easy, but once you have higher orders
> > it is probably undecidable.
> 
> I hadn't thought of that. I just discovered that you cannot add vectors of 
> vectors in F#, so it is probably 1st order only.

Hmm, that's a bit surprising if your explanation above is correct,
that is, if it resorts to dynamic typing if it can't resolve
statically.


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