Re: [Caml-list] Problem with universal functions in a module

[Goswin von Brederlow <goswin-v-b@web.de>]

On Sat, Jan 10, 2015 at 06:49:31PM +0000, Leo White wrote:
> > I don't see anything to infere there. Only thing I see is that in the
> > case of mono the universal function has to be unified with a single
> > type function. But 'a . 'a -> 'a should unify with int -> int
> > resulting in int -> int without problems.
> 
> 'a. 'a -> 'a cannot unify with int -> int. If it did then 'a. 'a -> 'a
> wouldn't be polymorphic: it could not be used as both int -> int and
> float -> float. Instead 'a. 'a -> 'a must be instantiated to 'b -> 'b
> which can then be unified with int -> int. It is the descision whether
> or not to perform this instantiation that needs to be infered.
> 
> To understand the full range of issues associated with higher-rank and
> impredicative polymorphism I suggest reading the relevant literature
> (e.g. "MLF: raising ML to the power of system F", "Semi-explicit
> first-class polymorphism for ML", "Flexible types: robust type inference
> for first-class polymorphism", "Boxy types: inference for higher-rank
> types and impredicativity", ...).
> 
> Regards,
> 
> Leo

I acknowledge that I'm weak on the theory here but from the example
the rules seems to be pretty simple:

    When trying to unify a universal function with a polymorphic or
    monomorphic function first instantiate.

As said I don't expect ocaml to infer what functions are universal.
That can be annotated. So the question isn't if we can infer from the
mono case wether the function is universal or monomorphic. The
function must already be annotated as universal. Dropping the
universality to allow unification with other types seems to be
straight forward though.

In laymans terms: A function 'a . 'a -> 'a can always be used where 'b
-> 'b (or in this case int -> int) is expected. That doesn't change
the type of the function itself though.

MfG
	Goswin