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.