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