[Prev][Next][Index][Thread]No Subject
Received: From ITOINFO(MAILER) by IBOINFN with RSCS id 0000 for MAILER@(&; Thu, 14 Apr 88 12:45 N Message-id: <001> Date: THU, 14-APR-88 13:11 N From: <DEZANI@ITOINFO.BITNET> Subject: To: <TYPES@THEORY.LCS.MIT.EDU> Received: by leonardo.uucp (ITOINFO) (4.12/3.14 ) id AA27209; Thu, 14 Apr 88 11:42:53 GMT Date: Thu, 14 Apr 88 11:42:53 GMT From: dezani@ITOINFO (Dezani Mariangela) To: types%THEORY.LCS.MIT.EDU@IBOINFN Subject: Typed versus untyped (Albert's April 10 note). From: Roger Hindley (majrh%pyramid.swansea.ac.uk@rl.earn but temporarily c/o Mariangiola Dezani, address as header) Henk's slogan "Church vs Curry" sounds a good approximation, though "Typed terms vs Type-assignment" gives the flavour of the distinction better. One important advantage of type-assignment (TA) systems is that in TA language, one can ask (and answer) questions of a kind that cannot be expressed at all in typed-term language. For example (1) "If we assumed that this part of a term X has a certain type, what type would the whole of X have?" Also the question mentioned in Albert's note: (2) "Is a given term, for example S(KK)K, an erasure of a typed one? It is this extra expressive power that makes TA-systems interesting; they are, roughly speaking, like Meta-Languages for languages of typed terms. (cf. Milner's choice of name "ML".) By the way, the Hindley-Milner typing algorithm mentioned in Albert's note has a long history; Curry used it informally in the 1950's, perhaps even 1930's, before he wrote it up formally as an equation-solving procedure in 1967 (published 1969). Curry's algorithm includes a unific- ation algorithm. The algorithm of Hindley, dating from 1967, depends on Robinson's unification algorithm. The Milner algorithm depends on Robinson too. J.H. Morris gave an equation-solving algorithm in his thesis at MIT (1968, but presumably devised some time before then); it includes a unification algorithm in the same way Curry's does. Carew Meredith, working in propositional logics, used a Hindley-like algorithm in the 1950's; by the formulas-as-types correspondence, this is a principal-type-scheme algorithm, in today's language. Tarski had used, it is rumoured, a p.t.s. or unification algorithm in early work in the 1920's. There must be a moral to this story of continual re-discovery; perhaps someone along the line should have learned to read. Or someone else learn to write.
