[Haskell-cafe] bug in ghci ?
Alexander Solla
ajs at 2piix.com
Fri Jul 9 22:01:53 EDT 2010
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.
More information about the Haskell-Cafe
mailing list