[I hear cries of Haskell 2]
Phil Wadler writes:
> The suggestion is:
>
> Remove the restriction that type synonym
> declarations must not be recursive.
>
> [...]
>
> 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?
It's not a big deal if you use a graph algorithm for unification -- you
just don't bother checking whether the result of unification is
recursive! I implemented recursive types this way in 1987, and I'm
sure this wasn't new then. A graph algorithm is arguably the "right
way" to implement type inference, anyway (Patrick Sansom has achieved
significant speedup for type inference in GHC by adopting a graph-based
algorithm). I have a paper in the 1991 Glasgow FP Workshop which
describes this algorithm in a functional style
K. Hammond,
"Efficient Type Inference Using Monads",
Proc 1991 Glasgow Workshop on Functional Programming,
Portree, Skye, 1991,
Springer-Verlag Series of Workshops in Computing Science.
and adds the occurs check to obtain normal types. The same
thing is also sketched out in my thesis (as a programming example
for DACTL).
It is slightly harder to do with substitutions, but to compensate
you can remove the horrible occurs check. I don't know the state
of theoretical work on substitutions for recursive types. Anyone?
The really big issue is how you represent recursive types for printing
or to define new types. Coming from a graph rewriting world, I prefer
explicit labelling (with type variables as labels) to implicit
recursion via synonyms. For example
e :: a:(Int -> a)
defines "e" to have the recursive type (Int -> Int -> ....).
If you think in terms of mu types, this is just syntactic sugar for:
e :: mu a . Int -> a
There's a nice relationship between types represented this way and
graph-based unification.
The other nice things about using explicit labels rather than
implicit synonyms are that
1) They can be used in arbitrary signatures without
needing to predeclare type synonyms.
2) They have a uniform printable representation
(not true for synonyms, since you might be
able to unify a type with more than one synonym).
3) With the right algorithm, it's easy to generate
recursive types -- which makes type inference
straightforward (essentially you *remove* the
"occurs check" but make sure you "tie a knot"
at this point -- trivial with a graph, slightly
harder with substitutions).
4) It's easy to introduce multiple recursions in the same
type (you need multiple mutually recursive synonyms
to achieve the same effect):
e :: a: ((b:Int -> Char -> b) -> a)
The big disadvantage of recursive types seems to be that you may
not be able to detect when a function is applied to the wrong
number of arguments, since a type variable will now unify with a
recursive function type:
f :: a -> a unifies with f :: a -> a: (b -> b)
Either John Launchbury or Simon Marlow had a convincing example of
how this could cause problems.
Kevin
