--- Paul Hudak
This is a very late response to an old thread...
Tom Hawkins wrote:
In a pure language, is it possible to detect cycles in recursive data structures? For example, is it possible to determine that "cyclic" has a loop? ...
data Expr = Constant Int | Addition Expr Expr
cyclic :: Expr cyclic = Addition (Constant 1) cyclic
Or phased differently, is it possible to make "Expr" an instance of "Eq" such that cyclic == cyclic is smart enough to avoid a recursive decent?
I'm a little confused. It's one thing to demonstrate that a (possibly infinite) digraph contains a loop, but quite another to show that it does not. Carrying around a copy of the subgraph consisting of nodes actually visited is workable in a pure language, but there's no guarantee of termination.
-Tom
---
Perhaps it's obvious, but one way to do this is to make the cycle *implicit* via some kind of a fixed-point operator, which is a trick I used recently in a DSL application.
So, you imagine f to be a function that (non-deterministally) follows an edge in a digraph. The idea being that G is (possibly infinite) digraph and F is a subgraph. The "function" f would non-deterministically select a vertext of F, follow an edge in G (again chosen non-deterministically), add the (possibly new) edge to F, and return the resulting graph. Then, you are asking if f has a fixpoint in this broader context?
For example, you could define:
data Expr = Const Int | Add Expr Expr | Loop -- not exported deriving (Eq, Show)
The purpose of Loop is to "mark" the point where a cycle exists. Instead of working with values of type Expr, you work with values of type Expr -> Expr, or Fix Expr:
type Fix a = a -> a
For example:
fe1,fe2 :: Fix Expr fe1 e = Add (Const 1) (Const 1) -- non-recursive fe2 e = Add (Const 1) e -- recursive
You can always get the value of an Expr from a Fix Expr whenever you need it, by computing the fixed point:
fix f = x where x = f x
If it can be computed. Maybe I'm off-track here, but it seems to me that when you introduce laziness into the equation, you lose any guarantee of there even being a fixpoint, much less one that can be computed.
e1,e2 :: Expr e1 = fix fe1 -- finite e2 = fix fe2 -- infinite
Note that e2 is equivalent to your "cyclic". But now we can also test for equality:
instance Eq (Fix Expr) where fe1 == fe2 = fe1 Loop == fe2 Loop
For example, fe2 == fe2 returns "True", whereas e2 == e2 (i.e. your cyclic == cyclic) diverges.
Of course, note that, although fe1 == fe2 implies that fix fe1 == fix fe2, the reverse is not true, since there will always be loops of varying degrees of unwinding that are semantically equivalent, but not "syntactically", or structurally, equivalent. Thus this definition of equality is only approximate, but still, it's useful.
I'm lost. Are you saying bottom is bottom?
If you want to have multiple loops, or a loop not at the top level, then you need to add some kind of a loop constructor to Expr. I've sketched that idea below, and pointed out a couple of other useful ideas, such as showing a loop, and mapping a function over a loop without unwinding it.
I hope this helps,
-Paul
===
Gregory Woodhouse