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.