Re: [Caml-list] What is "principal typing"?

[Jeff Polakow <jeff.polakow@db.com>]

[-- Attachment #1: Type: text/plain, Size: 1514 bytes --]

Hello,

  There are two notions, often conflated,  which you might be referring
to: principal types and principal typings. The following is taken from [1]
which is worth reading if you're interested in this topic.

    Principal Types
      Given: a term M typable with type assumptions A.
      There exists: a type sigma representing all possible types for M in
A.

    Principal Typings
      Given: a typable term M.
      There exists: a judgement A |- M : tau \x1c representing all possible
typings for M.

Principal types, which ML has, are useful because, for a given context,
there is a most general type for any typeable term. This is a useful
property to have for languages which attempt type inference.

Principal typeings, which ML does not have, are useful because they allow
for compositional type inference (i.e. each piece of the program can be
analyzed separately).

[1] J. B. Wells. The essence of principal typings. In Proc. 29th Int'l
Coll. Automata, Languages, and Programming, volume 2380 of LNCS, pages
913-925. Springer-Verlag, 2002.
(http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:ICALP-2002.pdf)

--Jeff

---

This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.

[-- Attachment #2: Type: text/html, Size: 2678 bytes --]