On Thu, 20 Dec 2012, Christopher Howard
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.