Phil suggests that Haskell 1.3 might:
| Remove the restriction that type synonym
| declarations must not be recursive.
|
| In other words, one could write things like
|
| type Stream a = (a, Stream a)
|
| which is equivalent to the type (a, (a, (a, ...))).
I have some reservations about this. As things stand, a type synonym is just
an abbreviation for another type. Synonyms are convenient because they allow
us to write shorter, more informative types. But, if necessary, we can
always eliminate them from a given type expression.
The proposed change would give us types that (a) are not currently available
to the Haskell 1.2 programmer, and (b) cannot be expressed without using a
type synonym. Of course, one argument for dropping the restriction is that
the new types introduced would actually be useful to the Haskell 1.3
programmer. However, I find (b) a little worrying.
To get some idea for the problems that we're dealing with, consider the
definition of a stream of zeros:
zeros = (0, zeros)
What type should we assign to zeros? A Haskell 1.2 system will reject this
because it requires zeros :: t where t = (Int,t), which will not get past the
occurs check in the unifier. I suppose that we could allow this if the user
(i.e. programmer) gave an explicit type signature such as:
zeros :: Stream Int
Of course, we can't expect the definition to type check without an explicit
type declaration unless a new type synonym is generated just for the purpose.
Dropping the restriction on recursive type synonyms gives a poor man's
version of recursive types. Maybe we could find a way to support full
recursive types instead, using explicit mu's in type expressions? For
example, the stream type might become:
type Stream a = mu s . (a, s)
This seems much more elegant and general.
| Guy Steele has since pointed out several compelling examples
| where it would be *much* easier not to have the restriction,
| and I've encountered a few myself.
I've played with some of Guy's examples and found that the recursive types
can be avoided for some of the specific applications that he has in mind.
I certainly would be interested to see more examples, and I'd also be
surprised if they couldn't be dealt with using mu types.
| The obvious way to go is for someone to implement it first, to
| make sure it's not difficult. Mark Jones, have you tried this
| in Gofer yet?
In fact, the current version of Gofer actually requires the complete
expansion of all type synonyms during static analysis, so recursive
type synonyms would be rather difficult for me to implement.
On the other hand, I suspect that it may be possible to get somewhere with
proper recursive mu types. I've seen several papers about recursive types,
but I'm not sure if I know of any work about type inference in the presence
of recursive types; perhaps somebody can remind me? Informally, it's easy
enough to see how mu types would be produced during unification. I suppose
that there could also be an awkward interaction with overloading, but my
intuition tells me that this is unlikely.
It might also be worth mentioning that constructor classes actually give you
a weak form of the mu operator. For example, we can define:
data Mu f = In (f (Mu f))
However, with this treatment, you have to write an explicit `In' operation.
For example, if I define:
zeros = In (0, zeros)
then the type inference system tells me that zeros :: Mu ((,) Int). What
we'd really like is for the `coercion' from f (Mu f) to Mu f to be inferred
automatically. (And, with recent discussions in mind, I'd also like the In
constructor to be strict, or defined by Phil's newtype construct, so that it
is actually an isomorphism ...)
Looking forward to further comments,
Mark
