[Haskell-cafe] Circular pure data structures?

wren ng thornton wren at freegeek.org
Tue Jul 14 22:49:00 EDT 2009


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


More information about the Haskell-Cafe mailing list