> I also think its neat that you seem to have found a use for cyclic
> unification. This is definitely an impetus to extend the language to
> include cyclic types. (I don't expect we'll do this for a while
> though. You might consider modifying the Glasgow Haskell compiler to
> include this yourself -- it may not be too difficult.)
I'm not sure with it's possible to do this with the substitution
algorithm used in our compiler, I thought the occurs check helped
preserve the idempotency of substitions? It's certainly possible in
the graph-based algorithm I describe in my 1991 Glasgow FP workshop
paper (in fact, you get this "for free" and end up adding an occurs
check just to match the normal algorithm!). The paper describes
[informally] how to transform a substitution algorithm written using
monads (such as the one in our compiler) into the graph version. You
can also use a parallel algorithm if you use the right monad. Apart
from the changes to the underlying monad, the differences are quite
minor. The paper is (still) a draft version, so may be buggy, but
please ask if you'd like a copy.
Oh if you did this, you'd also need to change the type output
routines, and you might like to allow explicitly cyclic types in type
signatures [may as well as existential types while you're there, too
:-) -- it's a pain when not all expressions can be given a type
signature].
Apart from the implementation (which doesn't seem to be a problem if
the right alg. is used[*]) does anyone know of more subtle problems with
cyclic types [such as not being able to define the type system using
the traditional sequent style]? Is this a well-studied area?
Kevin
[*] Though if substitions couldn't be used, I wouldn't like to have
to reimplement the type checkers in all existing Haskell compilers.