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