> to permit polymorphic recursion if
> a type signature is provided
>
> Simon
>
> PS This idea is part of the folklore, but I don't know of a reference which
> describes it. Does anyone else? (Specifically the simple type-signature
> solution; ...)
By coincidence, I was just looking up the references today.
I think the type-signature solution is at least implicit in
Henglein's paper, even though does not advocate it. He claims
that the type derivation does not diverge in practice, just
as the ordinary Milner algorithm is not exponential in practice.
A more precise statement:
"Let us say an (untyped) expression e of size n has a small typing
if it has a well-typed version e' that is at most of size p(n) for
a fixed polynomial p.
Theorem 8. Milner-Mycroft typability with small types is
polynomial-time decidable."
-- Henglein [1993, section 6.2, page 285]
Mikael
References:
A. Mycroft.
Polymorphic type schemes and recursive definition.
Int. Symp. on Programming, pp 217-228, LNCS 167, Springer 1984.
Fritz Henglein.
Type inference with polymorphic recursion.
ACM TOPLAS 15(2), pp 253-289, April 1993.
A. J. Kfoury, J. Tiuryn and P. Urzyczyn.
Type reconstrution in the presence of polymorphic recursion.
ACM TOPLAS 15(2), pp 290-311, April 1993.
A. J. Kfoury, J. Tiuryn and P. Urzyczyn.
The undecidability of the semi-unification problem.
Information and Computation 102(1), pp 83-101, Jan. 1993.
