> From: Simon L Peyton Jones <[EMAIL PROTECTED]>
> [...]
> The standard Hindley-Milner restriction is that a recursive function
> can only be called monomorphically in its own body. Here's an
> example (from an earlier posting to the SML list, which can't typecheck
> under this restriction.
>
> data Foo a = A | B (Foo [a])
>
> -- f :: Foo a -> ()
> f A = ()
> f (B thing) = f thing
>
> Why doesn't it work? Because the recursive call to f is at type
> [a] rather than a.
>
> There's a fairly standard extension to the HM type system which says that
> if f is given an explicit type signature (so that the type of f need only
> be checked, not inferred), then the program can be typechecked.
If we allow a data type constructor like Foo, how would we do equality
for it? It seems that we would need to write something like
instance Eq a, Eq (Foo [a]) => Eq (Foo a) where
A == A = True
(B thing1) == (B thing2) = thing1 == thing2
_ == _ = False
which cannot be handled by the current type inference system (the explicit
typing of (==) does not help avoid the need for the context Eq (Foo [a])
in any way that I can see).
Satish
