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.