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.