Circular pure data structures?

Hello, Is it possible to create a circular pure data structure in Haskell? For example: a :: Data let b = getNext a let c = getNext b c == a -- Gives True Thanks, -John

On Jul 14, 2009, at 18:27 , John Ky wrote:
Is it possible to create a circular pure data structure in Haskell? For example:
http://haskell.org/haskellwiki/Tying_the_knot -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

Yes, using lazy semantics. http://www.haskell.org/haskellwiki/Tying_the_Knot -Ross On Jul 14, 2009, at 6:27 PM, John Ky wrote:
Hello,
Is it possible to create a circular pure data structure in Haskell? For example:
a :: Data
let b = getNext a let c = getNext b
c == a -- Gives True
Thanks,
-John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

John,
Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this... ones = 1 : ones ones' = 1 : ones' Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating. "Pointer equality" (ie. testing if the values are represented by the same bits in memory) is no good, since it's entirely up to the compiler whether ones and ones' use the same bits. (They won't, but that's not important.) In general "pointer equality" of Haskell values, such as ones and (tail ones) interferes with referential transparency, which is held in high regard around here. Although, for the record, when pointer equality is really what you want, I'm sure there's ways to Force It. For your purposes, does it matter if you can actually do the comparison? Is it enough to know that ones and (tail ones) are equal? Regards, John

John Dorsey wrote:
John,
Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this...
ones = 1 : ones ones' = 1 : ones'
Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating.
That depends on what you mean by "proof" or "comparison". Usually large proofs are constructed by induction (breaking the problem apart bit by bit), but that only works for arbitrarily large but nevertheless finite problems. If you try induction on a (possibly) infinite structure you'll get a (possibly) non-terminating proof/program. Instead, for infinite structures we must use "coinduction" to reason about them. In a sense, this changes the definition of proof from "yes this is the case" into "yes this is the case as far as you know", since in finite time we can only look at a finite portion of any structure (and conversely, differences that we can't/don't observe "don't matter"). Often this results in semidecidable properties from the inductive world becoming co-semidecidable in the coinductive world (if two infinite streams are unequal this can be discovered in finite time, but discovering that they are equal is trickier). -- Live well, ~wren

Hello,
Actually, I wanted to be able to create a tree structure when I can navigate
both leaf-ward and root-ward. I didn't actually care for equality.
I think the tying the knot technique as mentioned by others is sufficient
for this purpose.
Cheers,
-John
On Wed, Jul 15, 2009 at 8:55 AM, John Dorsey
John,
Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this...
ones = 1 : ones ones' = 1 : ones'
Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating.
"Pointer equality" (ie. testing if the values are represented by the same bits in memory) is no good, since it's entirely up to the compiler whether ones and ones' use the same bits. (They won't, but that's not important.) In general "pointer equality" of Haskell values, such as ones and (tail ones) interferes with referential transparency, which is held in high regard around here. Although, for the record, when pointer equality is really what you want, I'm sure there's ways to Force It.
For your purposes, does it matter if you can actually do the comparison? Is it enough to know that ones and (tail ones) are equal?
Regards, John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Sufficient, but not good. Try zippers instead. On 15 Jul 2009, at 08:29, John Ky wrote:
Hello,
Actually, I wanted to be able to create a tree structure when I can navigate both leaf-ward and root-ward. I didn't actually care for equality.
I think the tying the knot technique as mentioned by others is sufficient for this purpose.
Cheers,
-John
On Wed, Jul 15, 2009 at 8:55 AM, John Dorsey
wrote: John, Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this...
ones = 1 : ones ones' = 1 : ones'
Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating.
"Pointer equality" (ie. testing if the values are represented by the same bits in memory) is no good, since it's entirely up to the compiler whether ones and ones' use the same bits. (They won't, but that's not important.) In general "pointer equality" of Haskell values, such as ones and (tail ones) interferes with referential transparency, which is held in high regard around here. Although, for the record, when pointer equality is really what you want, I'm sure there's ways to Force It.
For your purposes, does it matter if you can actually do the comparison? Is it enough to know that ones and (tail ones) are equal?
Regards, John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Hello,
If I use zippers, do all my nodes need to be the same type? My tree doesn't
have the same type for every node. For example:
Modules -> Module -> Types -> Type -> Members -> Member -> Type -> ...
Thanks
-John
On Wed, Jul 15, 2009 at 2:41 PM, Miguel Mitrofanov
Sufficient, but not good.
Try zippers instead.
On 15 Jul 2009, at 08:29, John Ky wrote:
Hello,
Actually, I wanted to be able to create a tree structure when I can navigate both leaf-ward and root-ward. I didn't actually care for equality.
I think the tying the knot technique as mentioned by others is sufficient for this purpose.
Cheers,
-John
On Wed, Jul 15, 2009 at 8:55 AM, John Dorsey
wrote: John, Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this...
ones = 1 : ones ones' = 1 : ones'
Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating.
"Pointer equality" (ie. testing if the values are represented by the same bits in memory) is no good, since it's entirely up to the compiler whether ones and ones' use the same bits. (They won't, but that's not important.) In general "pointer equality" of Haskell values, such as ones and (tail ones) interferes with referential transparency, which is held in high regard around here. Although, for the record, when pointer equality is really what you want, I'm sure there's ways to Force It.
For your purposes, does it matter if you can actually do the comparison? Is it enough to know that ones and (tail ones) are equal?
Regards, John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Zippers come up as the "derivative" of the type; if you haven't yet
encountered this trick, then first find it :)
Try differentiating your datastructure.
2009/7/15 John Ky
Hello,
If I use zippers, do all my nodes need to be the same type? My tree doesn't have the same type for every node. For example:
Modules -> Module -> Types -> Type -> Members -> Member -> Type -> ...
Thanks
-John
On Wed, Jul 15, 2009 at 2:41 PM, Miguel Mitrofanov
wrote: Sufficient, but not good.
Try zippers instead.
On 15 Jul 2009, at 08:29, John Ky wrote:
Hello,
Actually, I wanted to be able to create a tree structure when I can navigate both leaf-ward and root-ward. I didn't actually care for equality.
I think the tying the knot technique as mentioned by others is sufficient for this purpose.
Cheers,
-John
On Wed, Jul 15, 2009 at 8:55 AM, John Dorsey
wrote: John, Is it possible to create a circular pure data structure in Haskell? For example:
Creating the data structure is easy; as other respondents have pointed out. A simple example is this...
ones = 1 : ones ones' = 1 : ones'
Comparing these values is harder. All of (ones), (ones'), (tail ones), and so forth are equal values. But I don't know how to compare them. My Spidey-sense tells me there's probably a simple proof that you can't, if you care about the comparison terminating.
"Pointer equality" (ie. testing if the values are represented by the same bits in memory) is no good, since it's entirely up to the compiler whether ones and ones' use the same bits. (They won't, but that's not important.) In general "pointer equality" of Haskell values, such as ones and (tail ones) interferes with referential transparency, which is held in high regard around here. Although, for the record, when pointer equality is really what you want, I'm sure there's ways to Force It.
For your purposes, does it matter if you can actually do the comparison? Is it enough to know that ones and (tail ones) are equal?
Regards, John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Web IR developer, market.yandex.ru

On Wed, Jul 15, 2009 at 12:13 AM, Eugene Kirpichov
Zippers come up as the "derivative" of the type; if you haven't yet encountered this trick, then first find it :)
Try differentiating your datastructure.
Here's a paper with a good introduction to the concept and bibliography: http://strictlypositive.org/dfordata.pdf My take on it: A zipper is the one-hole-context of your data-type plus a focused-on payload. Data-structure differentiation is the method for deriving the one-hole-context. Antoine

John,
If I use zippers, do all my nodes need to be the same type?
No, zippers can also be defined for mutually recursive data types. In a paper to be presented at ICFP, next September, Alexey Rodriguez, Andres Löh, Johan Jeuring, and I show how zippers for mutually recursive data types can be derived in Haskell: Alexey Rodriguez, Stefan Holdermans, Andres Löh, and Johan Jeuring. Generic programming with fixed points for mutually recursive datatypes, 2009. To appear in the proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, Edinburgh, Scotland, August 31–September 2, 2009. http://people.cs.uu.nl/stefan/pubs/rodriguez09generic.html . An implementation is available on Hackage: http://hackage.haskell.org/package/zipper . HTH, Stefan
participants (10)
-
Antoine Latter
-
Brandon S. Allbery KF8NH
-
Eugene Kirpichov
-
Felipe Lessa
-
John Dorsey
-
John Ky
-
Miguel Mitrofanov
-
Ross Mellgren
-
Stefan Holdermans
-
wren ng thornton