🚀 go-pugleaf

>> The mathematical basis for polymorphic type systems comes from Robinson's
>> article on unification in the JACM, from around '67 (sorry, can't remember
>> the title). From here, there's Milner's work, the LCF system, and of course
>> (fanfare:) ML.
> I believe the correct reference is:
> Robinson, J.A., "A machine-oriented logic based on the resolution
> principle," Journal of the ACM 12(1) p23 (1965)

No.  Unification is an IMPLEMENTATION technique for typecheckers, not a
mathematical basis for anything.  The mathematics is from Hindley's 1969 paper
on principal type schemes; see Barendregt's "The Lambda Calculus" for the
exact reference.  If the *basis* was unification, what would correctness of
the typechecker mean?

Incidentally, has any implemented polymorphic typechecker ever been proved
correct?  Is there one that is even a plausible contender for being proved
correct (i.e. no known bugs)?

-- 
Jack Campin  *  Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, SCOTLAND.    041 339 8855 x6045 wk  041 556 1878 ho
INTERNET: jack%cs.glasgow.ac.uk@nsfnet-relay.ac.uk  USENET: jack@glasgow.uucp
JANET: jack@uk.ac.glasgow.cs     PLINGnet: ...mcvax!ukc!cs.glasgow.ac.uk!jack