> Dear people interested in Haskell 1.3,
Disclaimer: I'm *not* a member of any "Haskell 1.3" committee,
if any such committee has been formed.
> One modest extension we could make to the Haskell type system is
>
> to permit polymorphic recursion if
> a type signature is provided
I agree that this would be a good idea! Both for the reason you give
and the reason below:
Having done this change, one could (should!) remove section 4.5.1
(Dependency Analysis). This would have the consequence that some
more type signatures may sometimes be required when using version 1.3
compared to using version 1.2. I don't think that would to too bad...
To get consistency between implementations one should (instead!)
require that a declaration group is type checked in its entirety,
*not* splitting it up into smaller declaration groups, even
when possible.
The reason for removing section 4.5.1 (except that I don't like it) is:
Even though the split up of let-expressions into declaration cliques
can be expressed as a source code transformation, the same cannot be
done for where-declarations (modules, classes, instances, value-
declaration clauses, case-clauses). The latter two can be expressed
as source code transformations, but only after doing other source
transformations making then into let-expressions (including trans-
forming away guards). These transformations may not be desirable in
all implementations. In particular it may make it hard to produce good
type error messages. For modules, classes (with default declarations),
and instances the split into declaration cliques cannot be expressed
as a *source* transformation.
(Note that classes and instances already have type signatures, so there
would be no need to add any extra type signatures in these cases.)
So if we (you!) permit the use of a polymorphic function at different,
smaller or equal (rather than just equal), instances of the type
of the function within the declaration group *if* a type signature
is provided, then we can actually get a *simpler* type system!
That is, the requirement to transform to declaration cliques before
type checking can be removed, a transformation that cannot always be
expressed as a source transformation. We get the added benefit
of being able to write recursive functions for which the trans-
formation to declaration cliques does not do the trick.
Also, giving type signatures and checking that the types are a
fixed point is more obviously correct than deriving some (non-greatest!)
fixed-point types for a recursive declaration group. Deriving the
*greatest* fixed point types would of course be ideal, if that had
been decidable. But since it isn't (the greatest fixed point types
may be infinite), I support Simon's proposal.
/kent k
