On Thu, May 1, 2008 at 9:54 AM, Wouter Swierstra wrote:

...

Where could I find a good treatment on data vs. codata & the difference between well-founded recursion & well-founded(?) corecursion?

Bart Jacobs has some good papers on the subject. I found the draft of his book "Introduction to Coalgebra" quite good:

http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf

Indeed. I'd also recommend Varmo Vene's thesis, Categorical Programming with Inductive and Coinductive Types: http://www.cs.ut.ee/~varmo/papers/thesis.pdf Matt -- Matt Hellige / matt@immute.net http://matt.immute.net

I'm not sure there's a proof as such, more like a definitional absence of distinction between initiality and finality. In other words, the CPO framework is orthogonal to such extremality considerations. Perhaps someone here knows about work enriching CPOs in that direction. -- Kim-Ee Michael Karcher-7 wrote:

Wouter Swierstra wrote:

...

Hi Creighton,

...

Where could I find a proof that the initial algebras & final coalgebras of CPO coincide? I saw this referenced in the "Bananas.." paper as a fact, but am not sure where this comes from.

Probably he was referring to the last paragraph of the introduction:

Working in CPO has the advantage that the carriers of intial algebras and final co-algebras coincide, thus there is a single data type that comprises both finite and infinite elements.

-- View this message in context: http://www.nabble.com/Couple-of-formal-questions-tp16974927p17020475.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

On Mon, May 5, 2008 at 9:53 AM, Wouter Swierstra wrote:

On 1 May 2008, at 16:58, Michael Karcher wrote:

Wouter Swierstra wrote:

...

...

Hi Creighton,

...

Where could I find a proof that the initial algebras & final coalgebras of CPO coincide? I saw this referenced in the "Bananas.." paper as a fact, but am not sure where this comes from.

I couldn't find the statement you are referring to in "Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire" - but I'm not sure if this holds for every CPO.

Probably he was referring to the last paragraph of the introduction:

Working in CPO has the advantage that the carriers of intial algebras and final co-algebras coincide, thus there is a single data type that comprises both finite and infinite elements.

Ah - thanks for pointing that out. According to my more categorically inclined office mates, Marcelo Fiore's thesis is a good reference:

https://www.lfcs.inf.ed.ac.uk/reports/94/ECS-LFCS-94-307/

Hope that answers your question,

Wouter

I've had a lot of good reading material from this thread, and I greatly appreciate it: As a more background reading on this, I think Meijer & Fokkinga's "Program Calculation Properties of Continuous Algebras" is good, though the notation is a little idiosyncratic. http://citeseer.ist.psu.edu/717129.html I've also liked Baez et al's Rosetta Stone paper as food for thought http://math.ucr.edu/home/baez/rosetta.pdf Creighton Hogg