What is "principal typing"?

What is "principal typing"?

[Tom]

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

Now, this may sound a stupid question, but I am no guru of mathematics and
type theory... Could somebody point me to some documents explaining what the
principal typing is and why is it useful? (Supposedly, this is some property
that type inference systems should have...)

- Tom

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

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

[Jeff Polakow]

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

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

[Tom]

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

Thanks!

On 21/12/06, Jeff Polakow <jeff.polakow@db.com> wrote:
>
>
>
> 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.



Could you give some concrete example of a type inference engine and a
typable term, but which does not have a principal type?

- Tom

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

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

[Jeff Polakow]

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

Hello,

> Could you give some concrete example of a type inference engine and 
> a typable term, but which does not have a principal type?
> 
Here is a silly example. Consider a simply typed lambda calculus with 
subtyping on base types (e.g. int < real) but no structural subtyping 
(i.e. no subtype relation between functions). Then things like the 
identity function have no principal type. 

There are less trivial systems out there where, usually involving subtying 
and/or type classes, where principal types either don't exist or were 
tricky to figure out. But I am several years removed from actively 
thinking about this stuff and can't recall off hand more specific details.

-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: 1810 bytes --]

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

[Christophe Dehlinger]

On 12/21/06, Jeff Polakow <jeff.polakow@db.com> wrote:
>
> 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).
>
>

According to a 2005 paper by Camarao and Figueiredo (found at
http://www.dcc.ufmg.br/~camarao/ml-has-pt.pdf ), there is a variation
of the usual Damas-Milner type system for core-ML that types the same
terms and also has principal typings.

So the language ML does have principal typings, in the sense that it
has a useful type system with principal typings, but afaik no ML
implementation uses a such a type system.

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

[Jeff Polakow]

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

Hello,

> According to a 2005 paper by Camarao and Figueiredo (found at
> http://www.dcc.ufmg.br/~camarao/ml-has-pt.pdf ), there is a variation
> of the usual Damas-Milner type system for core-ML that types the same
> terms and also has principal typings.
> 
I hadn't heard of this work before. I'll try to take a look at it 
sometime.

> So the language ML does have principal typings, in the sense that it
> has a useful type system with principal typings, but afaik no ML
> implementation uses a such a type system.
> 
Yes, I should have been more careful with my assertion. The paper I 
referenced actually shows that Hindley/Milner has no principal typings.

-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: 1809 bytes --]