It is not clear to me how we would construct models for cyclic types
(then, I'm just starting to learn how to do it for acyclic types :-).
That is: What do the domains for these types look like? The reason I'm
worrying about this is that when I do abstract interpretation over
structured datatypes (such as lists, trees, ASTs), I need to construct
finite, abstract domains that model the infinite, concrete domains.
I do this from the type (i.e. type expression) associated with the
domain, and I have always used the finite, acyclic property of the
type expressions to guarantee that I get finite abstract domains that
really model the underlying concrete ones. The same seems to be true
of all abstract interpretations that construct their domains from
types, but maybe techniques meant for untyped languages can be used.
On a more cheerful, less please-don't-do-that note, could the type
checker perhaps transform the types of the program, perhaps by
introducing new algebraic datatypes, back to an acyclic form? So that
I can deal with this in the type checker and forget about it later?
Like, in the case of Guy's example:
data FooTree a b = Leaf b | Node a (FooTree a b) a (FooTree a b)
Now, let's say we use this in such a way that the type checker finds
the type:
mu a . [FooTree a Int] -- Ints in the leaves
Then the type checker could (for the benefit of later passes) break
the cycle by creating the new algebraic datatype A defined by:
data A = A_Constructor [FooTree A Int] !
where the "!" indicates that the constructor A_Constructor is strict
in its argument. This means that we don't actually have to implement
the constructor at run-time, so the introduction of this type carries
no performance penalty.
Now, of course, we could find the type
mu a . [FooTree a Float]
somewhere else during typechecking and construct a corresponding type,
but a better idea would be to try to construct the most general cycle
breaking algebraic datatype instead. In this case (I think) it would
be:
data A b = A_Constructor [FooTree (A b) b]
Then the first type would be (A Int) and the second (A Float).
In order for this to work, the typechecker would have to transform the
program both by generating these new type declarations and by
inserting the appropriate constructors in the code (in this case
A_Constructor). Right off the top of my head (which is where the idea
came from) I don't know if this is possible, there might be some
subtle reason why the type system of cyclic types is in some sense
stronger than the acyclic system, but since this technique can in
general be used to code a model for the untyped lambda calculus in
e.g. Haskell, it seems likely to me that it would work.
Cheers,
Karl-Filip
Make the cyclic case acyclic, and the acyclic case fast!
