Re: polymorphic recursion

[Pierre Weis <Pierre.Weis@inria.fr>]

> This might be the case for OCaml, but note that SML97 disallows more
> general type-constraints than the type apparent in the expression without
> the constraint (cf. rule (9) and comment in the 97 Definition - p22) 

That's a good point. It's simple to state and understand.

> This makes sense in the filosophy that type constraints are only supposed
> to be programmer documentation or to help the type-inference engine to
> detect type-errors "earlier" (the latter is practical while debugging
> type-errors).

Yes, but furthermore it can be used to help the typechecker to find
types more general than it will normally find.

> Unfortunately, SML is not very consistent on this matter as well, since it
> might require type annotations to succeed its type inference (e.g. at
> top-level monomorphism and the resolution of variable record patterns) A
> SML type-constraint cannot be more general, but is allowed to be more
> specific. e.g:
> 
> - val (f : 'a -> 'a -> 'a) = fn x => fn y => y;
> val f = fn : 'a -> 'a -> 'a

This is necessary to ``constrain'' the types of programs, when you
want to obtain a type more specific than the one synthetized by
the typechecker, in order to get more precise typing
verifications. This is also useful to get rid of spurious type
unknowns at modules boundaries, since you cannot let them escape from
the module.

> And if SML "would" follow this filosophy properly, there is no room for
> polymorphic recursion in general since, as you indicate, type-inference
> for this is undecidable. 

Yes polymorphic recursion type-inference is undecidable.
No, ``exact'' type constraints do not preclude polymorphic recursion.

Starting with the ``exact'' type annotation as hypothesis, it is easy
to verify that the polymorphic recursion is sound. This is simple and
easy. The only drawback is that you have to find the type yourself,
and that you may indicate a too specific type.

> I don't know why Caml allows more general type constraints, but it might
> be a good idea to follow SML on this matter (and I am interested to know
> if there are good reasons for not doing this)

If we use it to get polymorphic recursion, there is a good reason to
do this.

Another problem is the scope of type variables in type
constraints. What's the meaning of

let f (x : 'a) (y : 'a) = y;;

We may need explicit Forall keywords to express type schemes in constraints.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/