hoebel (04/27/89)
From: hoebel >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) ->Louis Hoebel Computer Science Department hoebel@cs.rochester.edu University of Rochester {allegra|rutgers}!rochester!hoebel Rochester NY 14627 716 275 5414 ------------------------------------------------------------------
jack@cs.glasgow.ac.uk (Jack Campin) (05/04/89)
>> 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