[Haskell-cafe] Categories (cont.)

[Jay Sulzberger]

On Thu, 20 Dec 2012, Christopher Howard <christopher.howard at frigidcode.com> wrote:

> I've perhaps been trying everyones patiences with my noobish CT
> questions, but if you'll bear with me a little longer: I happened to
> notice that there is in fact a Category class in Haskell base, in
> Control.Category:
>
> quote:
> --------
> class Category cat where
>
> A class for categories. id and (.) must form a monoid.
>
> Methods
>
> id :: cat a a
>
> the identity morphism
>

Here we run into at least one general phenomenon, which wren ng thornton
discusses in this thread.  One phenomenon is:

1. Different formalizations of the same concept, here "category",
strike the student when they are first seen, as completely
different things.  In particular, different formalisms often have
different types, where by "types" here, we mean types in the
implicit type system the student assumes.  The Haskell
declaration

   id :: cat a a

declares that id is an element of type (cat a a), that is, that
given any (suitable) type a, there is an element which we call
"id" of the type (cat a a).  Here (cat a a) might be read as "the
type of all morphisms between an element of type *anything* and
another element of type *anything*, where the two types are
the same.  Now in most category theory textbooks we have an axiom

   For each object obj in the category, we have a morphism
   identity(obj): obj -> obj
   That is, we have a map defined on Obj the set of objects
   of our category, which takes values in the Mor, the (disjoint)
   union of Mor(a,b) over all objects of our category.

One natural-to-the-beginner idea is that to do a
translation^Winterpretation of this into Haskell, we would need a
a Haskell procedure defined on (approximately) all types a which,
once we fix our category C, will hand us back a procedure of type
(C a a).  Note that this Identity procedure takes as input a type
and hands back a "lower level" thing, namely a value of type
(C a a).  So the "type" of Identity in our approximation of Haskell
would be:

   * -> (C * *)

where we have the constraint

   All the textual "*"s appearing in above line,
   refer to the same type

Now, I am a beginner in Haskell, and I am not sure whether we can
make such a declaration in Haskell.  In my naive type system
(id :: cat a a) gives id a different type from Identity.
Identity takes one input, patently, but id seems to take no
inputs.  Admittedly we may pass easily by means of a functor
(imprecision here, what are the two categories for this functor?)
from id to Identity, and by another functor, back.  I do think
that Haskell's handling of "universally polymorphic" types does
indeed provide for automatic, behind the source code, application
of these two functors.

To be painfully explicit: (id :: cat a a) says, in my naive type
theory, that "id" is a name for some particular element of
(cat a a).  Identity(a) is the result of applying Identity to the
type a.  A name is at a different level from the thing named, in
my naive type theory.

2. The above is a tiny example of the profusion of swift
apparently impossible conflations and swift implicit, and often
also explicit, distinctions which are sometimes offered in
response to the beginner's puzzlement.

> (.) :: cat b c -> cat a b -> cat a c
>
> morphism composition
> --------
>
> However, the documentation lists only two instances of Category,
> functions (->) and Kleisli Monad. For instruction purposes, could
> someone show me an example or two of how to make instances of this
> class, perhaps for a few of the common types? My initial thoughts were
> something like so:
>
> code:
> --------
> instance Category Integer where
>
>  id = 1
>
>  (.) = (*)
>
> -- and
>
> instance Category [a] where
>
>  id = []
>  (.) = (++)
> -------
>
> But these lead to kind mis-matches.
>
> -- 
> frigidcode.com

Ah, OK, let us actually apply some functors.  I shall make some
mistakes in Haskell, I am sure, but the functors are not due to
me, are well known, and I believe, debugged:

Let us rewrite

> instance Category Integer where
>
>  id = 1
>
>  (.) = (*)

as

> instance Nearcat0 Integer where
>
>  id = 1
>
>  (.) = (*)

This is surely a category, ah, well just about, after we apply
some functor^Wtransformation.  What Nearcat0 is a Haskell thing,
ah, I just now see wren's explication, with Haskell code, in which,
I think Nearcat0 Integer is a thing of type Monoid in Haskell.  I
do not know what a "phantom type" is, but without the constraint
of having to produce a Haskell interpretation, let us just repeat
the standard category theory textbook explication:

A monoid may "be seen as" a category as follows:

Let M be a monoid with constant 1, and multiplication *.

Then we may define a category C with one object, which object we
will call, say, theobj.  To each element m of the monoid, we
define a morphism cat(m) in Mor(C) such that

   head(cat(m)) = theobj
   tail(cat(m)) = theobj

and for all m, n in the monoid

   cat(m) <<*>> cat(n) = cat(m * n)

where we have written "<<*>>" to mean the composition of morphisms
in C.  Note that once we have specified that C has only one
object, then the head and tail functions of C are determined,
and, so also, every pair of morphisms may be composed, because
the head of the first is guaranteed to be also the tail of the
second.

Now the above quote, from many textbooks, does not mention
Haskell.  wren's post presents an implementation of the above in
Haskell.  Another implementation might have different parts and
their motions might differ, and the way of explicating why it is
an implementation might also differ.  In reading Haskell mailing
lists and blogs I am struck by how often there are several
different translations of one concept into Haskell code.  In some
cases, when Haskell has a more flexible type system, different
translations will naturally collapse to fewer.

oo--JS.