Lennart Augustsson <[EMAIL PROTECTED]> writes:
> > (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).
Sorry; I wasn't thinking clearly. You're quite right; Thompson's
theory does achieve its at-most-one type property by putting lots of
type information in the terms (although not quite as bad as an
annotation on each subterm).
Carl Witty
[EMAIL PROTECTED]
