> (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 belie
The key issue in Lennart's example, I think, is monomorphic recursion.
For the function
f _ =
let y = f 'a'
in undefined
Haskell incorrectly (IMHO) infers the type `f :: Char -> a'
instead of the more general type `f :: b -> a'.
This occurs because in the absens
John Hughes :
>
> Everybody agrees the monomorphism restriction is a pain:
...
> So, let's make it visible, in the simplest possible way. Let there be TWO
> forms of binding: x = e, and x := e (say). A binding of the form `x = e' is
> interpreted using call-by-name, and may of course be overloa
On 25-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
>
> > Certainly a language with dependent types should define exactly what
> > types the type checker will infer. But when generating code, the
> > compiler ought to be able to make use of mor
> This occurs because in the absense of type declarations,
> Haskell assumes that any recursion will be monomorphic,
> which is in general not necessarily the case.
As I'm sure you know, type inference is in general impossible
for polymorphic recursion, and since Haskell insists on
decidable type
