Dear people interested in Haskell 1.3,
One modest extension we could make to the Haskell type system is
to permit polymorphic recursion if
a type signature is provided
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.
This program looks a little odd, but I can personally testify to having
tripped over this problem in programs that I Really Wanted to write.
I propose we adopt the extension for Haskell 1.3.
Simon
PS This idea is part of the folklore, but I don't know of a reference which
describes it. Does anyone else? (Specifically the simple type-signature
solution; I know there are papers about inference algorithms which allow
polymorphic recursion; semi-unification and stuff.)
