On the Haskell mailing list Simon writes:
>PS This idea [of admitting polymorphic recursion if it's declared explicitly]
>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; I know there are papers about inference algorithms which allow
>polymorphic recursion; semi-unification and stuff.)
Hope [1] had explicit polymorphic recursion. Meertens's language ABC
[2] also has polymorphic recursion and uses an inference algorithm
(which turns out to be incomplete). Mycroft gives a proof that
polymorphic recursion admits principal typing in the ML-sense; the
proof also shows how to extend an Algorithm-W style inference
algorithm with a simple and pretty efficient _checking_ algorithm for
explicit polymorphic recursion [3]. He also has a semicomplete
algorithm. Semi-unification can be used to find more type errors (and
terminate in those cases) and to speed the computation of types.
Generally, whether or not polymorphically bindable identifiers have
explicit type declarations makes the complexity-theoretic difference:
ML with or without polymorphic recursion can be type checked in
low-order polynomial time as long as all the variables that can have
polymorphic types (let-bound and possibly letrec-bound) have explicit
types. The only reason why complexity in type inference gets out of
hand is because those (implicit!) types blow up, and those programs
you can't even write (practically speaking) if you insist that they be
declared explicitly [4].
Fritz
[1] @inproceedings{bms80,
AUTHOR = "Burstall, R. and MacQueen, D. and Sannella, D.",
BOOKTITLE = "Stanford LISP Conference 1980",
ENTRYDATE = "7/18/87",
KEY = "Burstall",
PAGES = "136-143",
TITLE = "Hope: An Experimental Applicative Language",
YEAR = "1980"}
[2] @inproceedings{me83,
AUTHOR = "Meertens, L.",
BOOKTITLE = "Proc. 10th ACM Symp. on Principles of Programming
Languages (POPL)",
ENTRYDATE = "7/18/87",
KEY = "Meertens",
PAGES = "265-275",
TITLE = "Incremental Polymorphic Type Checking in {B}",
YEAR = "1983"}
[3] @inproceedings{my84,
AUTHOR = "Mycroft, A.",
BOOKTITLE = "Proc. 6th Int. Conf. on Programming, LNCS 167",
TITLE = "Polymorphic Type Schemes and Recursive Definitions",
YEAR = "1984"}
[4] @Article{henglein93c,
author = "Henglein, Fritz",
title = "Type Inference with Polymorphic Recursion",
journal = "ACM Transactions on Programming Languages and
Systems (TOPLAS)",
year = "1993",
volume = "15",
number = "2",
pages = "253-289",
month = "April"
}
