[Haskell-cafe] Very freaky

[Jonathan Cast]

On Thursday 12 July 2007, Andrew Coppin wrote:
> Stefan O'Rear wrote:
> > On Thu, Jul 12, 2007 at 07:19:07PM +0100, Andrew Coppin wrote:
> >> I'm still puzzled as to what makes the other categories so magical that
> >> they cannot be considered sets.
> >>
> >> I'm also a little puzzled that a binary relation isn't considered to be
> >> a function...
> >>
> >> From the above, it seems that functors are in fact structure-preserving
> >> mappings somewhat like the various morphisms found in group theory. (I
> >> remember isomorphism and homomorphism, but there are really far too many
> >> morphisms to remember!)
> >
> > Many categories have more structure than just sets and functions.  For
> > instance, in the category of groups, arrows must be homomorphisms.
>
> What the heck is an arrow when it's at home?

A homomorphism is just a function that preserves the group operation (addition 
or multiplication, depending on the group); i.e., one that does what you 
expect when presented with addition or multiplication (or whatever).

> > Some categories don't naturally correspond to sets - consider eg the
> > category of naturals, where there is a unique arrow from a to b iff a ≤
> > b.
>
> ...um...

Meditate on this at greater length.  Here lies the path to enlightenment.

Incidentally, I think this lies behind the Curry-Howard isomorphism mentioned 
earlier.  In a category C, the product (a, b) of two objects is the triple 
(p, p1 :: p -> a, p2 :: p -> b) such that for all triples (c, c1 :: c -> a, 
c2 :: c -> b) there is precisely one arrow h :: c -> p such that p1 . h = c1 
and p2 . h = c2.  So, taking Prop to be the category of propositions such 
that, for all propositions p, q, the pair (p, q) is an arrow from p to q iff 
p => q, the product (p, q) is the proposition c such that c => p, c => q, and 
for all propositions d such that d => p and d => q, d => c.  Of course, c is 
just p /\ q.

> > Binary relations are more general then functions, since they can be
> > partial and multiple-valued.
>
> What's a partial relation?

Let P, Q be sets, let r `subset` (P, Q) be a relation on P and Q, and for p 
`elem` P, r(p) = { q `elem` Q | (p, q) `elem` r }.  Then r is:

* total iff for all p `elem` P. r(p) contains at least one element,
* partial iff r is not total,
* a partial function iff for all p `elem` P. r(p) contains at most one 
element,
* multi-valued iff r is not a partial function, and
* a function iff r is a partial function and total.

> > indeed, it is possible to form
> > the "category of small categories" with functors for arrows.  ("Small"
> > means that there is a set of objects involved; eg Set is not small
> > because there is no set of all sets (see Russel's paradox) but Nat is
> > small.)
>
> OK, see, RIGHT THERE! That's the kind of sentence that I read and three
> of my cognative processes dump sort with an "unexpected out of neural
> capacity exception". o_O

I'd think you'd expect it by now :)  Lessa answered this one competently 
enough, I think.

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs