RE: Haskell 2 -- Dependent types?

[Nick Kallen]

> > > 2) Yes, I agree that the possibility that user-supplied type
> > > declarations can change the meaning of the program is a strike against
> > > the idea.
> > I don't find that so strange.  If there are no principal types
> > (which we can't hope for), then user added signatures can
> > have the effect of changing the meaning of a program.
>
> I've lost track of what we're talking about here.  In what system can
> we not hope for principal types?  (I believe that there are type
> theories with dependent types, such as the one in Thompson's _Type
> Theory and Functional Programming_, where each term has at most one
> type; so it can't just be dependent types that disallow principal
> types.)

It's not that principal types don't exist, its that it's in general
impossible to infer them (I believe, correct me if I'm wrong).