[Haskell-cafe] bug in ghci ?

[Alexander Solla]

On Jul 9, 2010, at 5:46 PM, Kevin Quick wrote:

> That's probably an interesting assertion that one of the category  
> theorists around here could prove or disprove.  ;-)

It's not too hard.  I don't like thinking about it in terms of  
category theory, though.  It's easier to think about it in terms of  
universal quantification.  The assertion is equivalent to the claim  
that (forall x, forall y, P x y) iff (forall y, forall x, P x y),  
though you have to do quite a bit of packing and unpacking to get there.

Another way to see it is in terms of recursion on initial algebras.   
Given an initial algebra A, and an initial algebra B, we'll say that A  
-> B represents the construction of attaching a copy of B to every  
element of A.  We can assume that A and B are disjoint, because we can  
find a normal form A' -> B' for which A' and B' are disjoint, and such  
that A -> B is isomorphic to A' -> B'.  (To see that, assume that some  
subalgebra C is contained in both A and B.  Attaching a copy of B to  
every element of A means attaching a copy of C to each element, and  
also B \ C.  But A already contains C.  So A -> B is isomorphic to A - 
 > B \ C).  Note that since we can assume A and B are disjoint, we can  
also assume A and B are NOT mutually recursive.  We can always find a  
way to break that mutual recursion up.

I'm not sure how to prove that A -> B and B -> A, as I defined them,  
are isomorphic.  But they are.  I guess we can re-interpret A and B as  
meet semi-lattices, and A -> B and B -> A as their products.