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