Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!unmvax!pprg.unm.edu!hc!lll-winken!uunet!mcvax!ukc!strath-cs!glasgow!jack
From: jack@cs.glasgow.ac.uk (Jack Campin)
Newsgroups: comp.lang.misc
Subject: Re: Robinson article
Message-ID: <2896@crete.cs.glasgow.ac.uk>
Date: 4 May 89 13:13:59 GMT
References: <1989Apr26.224726.12558@cs.rochester.edu>
Reply-To: jack@cs.glasgow.ac.uk (Jack Campin)
Organization: COMANDOS Project, Glesga Yoonie, Unthank
Lines: 24
Summary:
Expires:
Sender:
Followup-To:
Keywords:


>> 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