Re: Haskell 2 -- Dependent types?

[Lennart Augustsson]

>   (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.)
The more I think about this, the less I believe it. :-)
I don't think each term can have a at most one type (unless all
terms have a type annotation, in which case it is trivial).

There might still be principal types, but I can't recall seeing
such a thing, but then my memory isn't what it used to be...

Which version of type theory is Simon Thompson using?

      -- Lennart