Categories (cont.)

Christopher Howard

20 Dec 2012 20 Dec '12

6:42 a.m.

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 (.) :: 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

Attachments:

signature.asc (application/pgp-signature — 553 bytes)

Show replies by date

Petr P

20 Dec 20 Dec

7:35 a.m.

Hi Christopher, a data type can be an instance of Category only if it has kind * -> * -> *. It must have 2 type parameters so that you could have types like 'cat a a'. Some simple examples: import Prelude hiding (id, (.)) import Control.Category import Data.Monoid -- See https://en.wikipedia.org/wiki/Opposite_category newtype Op c a b = Op (c b a) instance Category c => Category (Op c) where id = Op id (Op x) . (Op y) = Op (y . x) -- A category whose morphisms are bijections between types. data Iso a b = Iso (a -> b) (b -> a) instance Category Iso where id = Iso id id (Iso f1 g1) . (Iso f2 g2) = Iso (f1 . f2) (g2 . g1) -- A product of two categories forms a new category: data ProductCat c d a b = ProductCat (c a b) (d a b) instance (Category c, Category d) => Category (ProductCat c d) where id = ProductCat id id (ProductCat f g) . (ProductCat f' g') = ProductCat (f . f') (g . g') -- A category constructed from a monoid. It -- ignores the types. Any morphism in this category -- is simply an element of the given monoid. newtype MonoidCat m a b = MonoidCat m instance (Monoid m) => Category (MonoidCat m) where id = MonoidCat mempty MonoidCat x . MonoidCat y = MonoidCat (x `mappend` y) Many interesting categories can be constructed from various monads using Kleisli. For example, Kleisli Maybe is the category of partial functions. Best regards, Petr 2012/12/20 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

(.) :: 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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

wren ng thornton

7:59 a.m.

On 12/20/12 6:42 AM, Christopher Howard wrote:

...

code: -------- instance Category Integer where

id = 1

(.) = (*)

-- and

instance Category [a] where

id = [] (.) = (++) -------

But these lead to kind mis-matches.

As mentioned in my other email (just posted) the kind mismatch is because categories are actually monoid-oids[1] not monoids. That is: class Monoid (a :: *) where mempty :: a mappend :: a -> a -> a class Category (a :: * -> * -> *) where id :: a i j (.) :: a j k -> a i j -> a i k Theoretically speaking, every monoid can be considered as a category with only one object. Since there's only one object/index, the types for id and (.) basically degenerate into the types for mempty and mappend. Notably, from this perspective, each of the elements of the carrier set of the monoid becomes a morphism in the category--- which some people find odd at first. In order to fake this theory in Haskell we can do: newtype MonoidCategory a i j = MC a instance Monoid a => Category (MonoidCategory a) where id = MC mempty MC f . MC g = MC (f `mappend` g) This is a fake because technically (MonoidCategory A X Y) is a different type than (MonoidCategory A P Q), but since the indices are phantom types, we (the programmers) know they're isomorphic. From the category theory side of things, we have K*K many copies of the monoid where K is the cardinality of the kind "*". We can capture this isomorphism if we like: castMC :: MonoidCategory a i j -> MonoidCategory a k l castMC (MC a) = MC a but Haskell won't automatically insert this coercion for us; we gotta do it manually. In more recent versions of GHC we can use data kinds in order to declare a kind like: MonoidCategory :: * -> () -> () -> * which would then ensure that we can only talk about (MonoidCategory a () ()). Unfortunately, this would mean we can't use the Control.Category type class, since this kind is more restrictive than (* -> * -> * -> *). But perhaps in the future that can be fixed by using kind polymorphism... [1] The "-oid" part just means the indexing. We don't use the term "monoidoid" because it's horrific, but we do use a bunch of similar terms like semigroupoid, groupoid, etc. -- Live well, ~wren

Christopher Howard

7:07 p.m.

On 12/20/2012 03:59 AM, wren ng thornton wrote:

...

On 12/20/12 6:42 AM, Christopher Howard wrote:

As mentioned in my other email (just posted) the kind mismatch is because categories are actually monoid-oids[1] not monoids. That is:

class Monoid (a :: *) where mempty :: a mappend :: a -> a -> a

class Category (a :: * -> * -> *) where id :: a i j (.) :: a j k -> a i j -> a i k

Theoretically speaking, every monoid can be considered as a category with only one object. Since there's only one object/index, the types for id and (.) basically degenerate into the types for mempty and mappend. Notably, from this perspective, each of the elements of the carrier set of the monoid becomes a morphism in the category--- which some people find odd at first.

In order to fake this theory in Haskell we can do:

newtype MonoidCategory a i j = MC a

instance Monoid a => Category (MonoidCategory a) where id = MC mempty MC f . MC g = MC (f `mappend` g)

This is a fake because technically (MonoidCategory A X Y) is a different type than (MonoidCategory A P Q), but since the indices are phantom types, we (the programmers) know they're isomorphic. From the category theory side of things, we have K*K many copies of the monoid where K is the cardinality of the kind "*". We can capture this isomorphism if we like:

castMC :: MonoidCategory a i j -> MonoidCategory a k l castMC (MC a) = MC a

but Haskell won't automatically insert this coercion for us; we gotta do it manually. In more recent versions of GHC we can use data kinds in order to declare a kind like:

MonoidCategory :: * -> () -> () -> *

which would then ensure that we can only talk about (MonoidCategory a () ()). Unfortunately, this would mean we can't use the Control.Category type class, since this kind is more restrictive than (* -> * -> * -> *). But perhaps in the future that can be fixed by using kind polymorphism...

[1] The "-oid" part just means the indexing. We don't use the term "monoidoid" because it's horrific, but we do use a bunch of similar terms like semigroupoid, groupoid, etc.

Finally... I actually made some measurable progress, using these "phantom types" you mentioned: code: -------- import Control.Category newtype Product i j = Product Integer deriving (Show) instance Category Product where id = Product 1 Product a . Product b = Product (a * b) -------- I can do composition, illustrate identity, and illustrate associativity: code: -------- h> Product 5 >>> Product 2 Product 10 h> Control.Category.id (Product 3) Product 3 h> Control.Category.id <<< Product 3 Product 3 h> Product 3 <<< Control.Category.id Product 3 h> (Product 2 <<< Product 3) <<< Product 5 Product 30 h> Product 2 <<< (Product 3 <<< Product 5) Product 30 -------- -- frigidcode.com

Jay Sulzberger

10:05 p.m.

On Thu, 20 Dec 2012, Christopher Howard wrote:

...

On 12/20/2012 03:59 AM, wren ng thornton wrote:

...
On 12/20/12 6:42 AM, Christopher Howard wrote:

As mentioned in my other email (just posted) the kind mismatch is because categories are actually monoid-oids[1] not monoids. That is:

class Monoid (a :: *) where mempty :: a mappend :: a -> a -> a

class Category (a :: * -> * -> *) where id :: a i j (.) :: a j k -> a i j -> a i k

Theoretically speaking, every monoid can be considered as a category with only one object. Since there's only one object/index, the types for id and (.) basically degenerate into the types for mempty and mappend. Notably, from this perspective, each of the elements of the carrier set of the monoid becomes a morphism in the category--- which some people find odd at first.

In order to fake this theory in Haskell we can do:

newtype MonoidCategory a i j = MC a

instance Monoid a => Category (MonoidCategory a) where id = MC mempty MC f . MC g = MC (f `mappend` g)

This is a fake because technically (MonoidCategory A X Y) is a different type than (MonoidCategory A P Q), but since the indices are phantom types, we (the programmers) know they're isomorphic. From the category theory side of things, we have K*K many copies of the monoid where K is the cardinality of the kind "*". We can capture this isomorphism if we like:

castMC :: MonoidCategory a i j -> MonoidCategory a k l castMC (MC a) = MC a

but Haskell won't automatically insert this coercion for us; we gotta do it manually. In more recent versions of GHC we can use data kinds in order to declare a kind like:

MonoidCategory :: * -> () -> () -> *

which would then ensure that we can only talk about (MonoidCategory a () ()). Unfortunately, this would mean we can't use the Control.Category type class, since this kind is more restrictive than (* -> * -> * -> *). But perhaps in the future that can be fixed by using kind polymorphism...

[1] The "-oid" part just means the indexing. We don't use the term "monoidoid" because it's horrific, but we do use a bunch of similar terms like semigroupoid, groupoid, etc.

Finally... I actually made some measurable progress, using these "phantom types" you mentioned:

code: -------- import Control.Category

newtype Product i j = Product Integer

deriving (Show)

instance Category Product where

id = Product 1

Product a . Product b = Product (a * b) --------

I can do composition, illustrate identity, and illustrate associativity:

code: -------- h> Product 5 >>> Product 2 Product 10

h> Control.Category.id (Product 3) Product 3

h> Control.Category.id <<< Product 3 Product 3 h> Product 3 <<< Control.Category.id Product 3

h> (Product 2 <<< Product 3) <<< Product 5 Product 30 h> Product 2 <<< (Product 3 <<< Product 5) Product 30 --------

Thank you for this code! What does the code for going backwards looks like? That is, suppose we have an instance of Category with only one object. What is the Haskell code for the function which takes the category instance and produces a monoid thing, like your integers with 1 and usual integer multiplication? Could we use a "constraint" at the level of types, or at some other level, to write the code? Here by "constraint" I mean something like a declaration that is a piece of Haskell source code, and not something the human author of the code uses to write the code. Maybe "Categorical Programming for Data Types with Restricted Parametricity" by D. Orchard and Alan Mycroft http://www.cl.cam.ac.uk/~dao29/drafts/tfp-structures-orchard12.pdf has something to do with this. oo--JS.

...

-- frigidcode.com

Gershom Bazerman

10:36 p.m.

On 12/20/12 10:05 PM, Jay Sulzberger wrote:

...

What does the code for going backwards looks like? That is, suppose we have an instance of Category with only one object. What is the Haskell code for the function which takes the category instance and produces a monoid thing, like your integers with 1 and usual integer multiplication? Could we use a "constraint" at the level of types, or at some other level, to write the code? Here by "constraint" I mean something like a declaration that is a piece of Haskell source code, and not something the human author of the code uses to write the code. instance C.Category k => Monoid (k a a) where mempty = C.id mappend = (C..)

The above gives witness to the fact that, if I'm using the language correctly, if we choose any object (our "a") in any given category, this induces a monoid with the identity morphism as unit and composition of endomorphisms as append. The standard libraries in fact provide this instance for the function arrow category (under a newtype wrapper): newtype Endo a = Endo { appEndo :: a -> a } instance Monoid (Endo a) where mempty = Endo id Endo f `mappend` Endo g = Endo (f . g) --Gershom

Jay Sulzberger

10:48 p.m.

On Thu, 20 Dec 2012, Gershom Bazerman wrote:

...

On 12/20/12 10:05 PM, Jay Sulzberger wrote:

...
What does the code for going backwards looks like? That is, suppose we have an instance of Category with only one object. What is the Haskell code for the function which takes the category instance and produces a monoid thing, like your integers with 1 and usual integer multiplication? Could we use a "constraint" at the level of types, or at some other level, to write the code? Here by "constraint" I mean something like a declaration that is a piece of Haskell source code, and not something the human author of the code uses to write the code. instance C.Category k => Monoid (k a a) where mempty = C.id mappend = (C..)

The above gives witness to the fact that, if I'm using the language correctly, if we choose any object (our "a") in any given category, this induces a monoid with the identity morphism as unit and composition of endomorphisms as append.

The standard libraries in fact provide this instance for the function arrow category (under a newtype wrapper):

newtype Endo a = Endo { appEndo :: a -> a }

instance Monoid (Endo a) where mempty = Endo id Endo f `mappend` Endo g = Endo (f . g)

--Gershom

Thanks, Gershom! I think I see. The Haskell code picks out the "isotropy/holonomy" monoid at the object a of any Haskell Category instance. actual old fashioned types remark: To get the holonomy semigroup^Wmonoid, interpolate a functor. I am glad that Haskell today smoothly handles this. ad paper on polymorphisms: I hope to post a rant against the misleading distinction between "parametric polymorphism" and "ad hoc polymorphism". Lisp will be used as a bludgeon in the only argument in the rant. The Four Things Which Must Be Distinguished will perform the opening number. oo--JS.

wren ng thornton

21 Dec 21 Dec

11:26 p.m.

On 12/20/12 7:07 PM, Christopher Howard wrote:

...

On 12/20/2012 03:59 AM, wren ng thornton wrote:

...
In order to fake this theory in Haskell we can do:

newtype MonoidCategory a i j = MC a

instance Monoid a => Category (MonoidCategory a) where id = MC mempty MC f . MC g = MC (f `mappend` g)

This is a fake because technically (MonoidCategory A X Y) is a different type than (MonoidCategory A P Q), but since the indices are phantom types, we (the programmers) know they're isomorphic. From the category theory side of things, we have K*K many copies of the monoid where K is the cardinality of the kind "*". We can capture this isomorphism if we like:

castMC :: MonoidCategory a i j -> MonoidCategory a k l castMC (MC a) = MC a

but Haskell won't automatically insert this coercion for us; we gotta do it manually. In more recent versions of GHC we can use data kinds in order to declare a kind like:

MonoidCategory :: * -> () -> () -> *

which would then ensure that we can only talk about (MonoidCategory a () ()). Unfortunately, this would mean we can't use the Control.Category type class, since this kind is more restrictive than (* -> * -> * -> *). But perhaps in the future that can be fixed by using kind polymorphism...

Finally... I actually made some measurable progress, using these "phantom types" you mentioned:

Yep, everything should work fine with the phantom types. The only problem is, as I mentioned, that you're not really getting the category associated with the underlying monoid, you're getting a whole bunch of copies of that monoid (one copy for each instantiation of the phantom types). -- Live well, ~wren

Jay Sulzberger

20 Dec 20 Dec

5:56 p.m.

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

(.) = (*)

...

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.

ok＠cs.otago.ac.nz

9:40 p.m.

...

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

This says that 'cat' must be a type constructor with two type arguments. In an instance of this type, a and b will refer to objects of the category and cat a b to the morphisms. Integer is NOT a type constructor with two type arguments, so instance Category Integer makes no sense. [] is a type constructor with one type argument, not two, so instance Category [] makes no sense either. Can you make Either an instance of Category? Can you make (,) an instance of Category? Can you make (a copy of) -> an instance of Category a different way?

Tillmann Rendel

21 Dec 21 Dec

9:35 a.m.

Hi, Christopher Howard wrote:

...

instance Category ...

The Category class is rather restricted: Restriction 1: You cannot choose what the objects of the category are. Instead, the objects are always "all Haskell types". You cannot choose anything at all about the objects. Restriction 2: You cannot freely choose what the morphisms of the category are. Instead, the morphisms are always Haskell values. (To some degree, you can choose *which* values you want to use). These restrictions disallow many categories. For example, the category where the objects are natural numbers and there is a morphism from m to n if m is greater than or equal to n cannot be expressed directly: Natural numbers are not Haskell types; and "is bigger than or equal to" is not a Haskell value. Tillmann

Chris Smith

2:35 p.m.

It would definitely be nice to be able to work with a partial Category class, where for example the objects could be constrained to belong to a class. One could then restrict a Category to a type level representation of the natural numbers or any other desired set. Kind polymorphism should make this easy to define, but I still don't have a good feel for whether it is worth the complexity. On Dec 21, 2012 6:37 AM, "Tillmann Rendel" wrote:

...

Hi,

Christopher Howard wrote:

...
instance Category ...

The Category class is rather restricted:

Restriction 1: You cannot choose what the objects of the category are. Instead, the objects are always "all Haskell types". You cannot choose anything at all about the objects.

Restriction 2: You cannot freely choose what the morphisms of the category are. Instead, the morphisms are always Haskell values. (To some degree, you can choose *which* values you want to use).

These restrictions disallow many categories. For example, the category where the objects are natural numbers and there is a morphism from m to n if m is greater than or equal to n cannot be expressed directly: Natural numbers are not Haskell types; and "is bigger than or equal to" is not a Haskell value.

Tillmann

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

Jay Sulzberger

4:21 p.m.

On Fri, 21 Dec 2012, Chris Smith wrote:

...

It would definitely be nice to be able to work with a partial Category class, where for example the objects could be constrained to belong to a class. One could then restrict a Category to a type level representation of the natural numbers or any other desired set. Kind polymorphism should make this easy to define, but I still don't have a good feel for whether it is worth the complexity.

Indeed this sort of thing can obviously be done. But it will require some work. The question is where, when, and how much effort, which may mean money, it will take. One encouraging thing is that recently more people understand that type checking/inference in the style of ML/Haskell/etc. is not so hard, and that general constraint solvers/SMT systems can do the job. Getting the compiler to make use of the results of such type estimates/assignments is the hard part today I think. Last night I discovered the best blurb for the program: http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf via the subReddit: http://www.reddit.com/r/dependent_types/ oo--JS.

...

On Dec 21, 2012 6:37 AM, "Tillmann Rendel" wrote:

...
Hi,

Christopher Howard wrote:

...
instance Category ...

The Category class is rather restricted:

Restriction 1: You cannot choose what the objects of the category are. Instead, the objects are always "all Haskell types". You cannot choose anything at all about the objects.

Restriction 2: You cannot freely choose what the morphisms of the category are. Instead, the morphisms are always Haskell values. (To some degree, you can choose *which* values you want to use).

These restrictions disallow many categories. For example, the category where the objects are natural numbers and there is a morphism from m to n if m is greater than or equal to n cannot be expressed directly: Natural numbers are not Haskell types; and "is bigger than or equal to" is not a Haskell value.

Tillmann

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

wren ng thornton

11:59 p.m.

On 12/21/12 2:35 PM, Chris Smith wrote:

...

It would definitely be nice to be able to work with a partial Category class, where for example the objects could be constrained to belong to a class. One could then restrict a Category to a type level representation of the natural numbers or any other desired set. Kind polymorphism should make this easy to define, but I still don't have a good feel for whether it is worth the complexity.

Actually, what you really want is ConstraintKinds. The following works just fine in GHC 7.6.1: {-# LANGUAGE KindSignatures , ConstraintKinds , PolyKinds , TypeFamilies , MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , FlexibleContexts #-} class Category (c :: k -> k -> *) where -- | The kind of domain objects. type DomC c x :: Constraint -- | The kind of codomain objects. type CodC c x :: Constraint -- | The identity morphisms. id :: (ObjC c x) => c x x -- | Composition of morphisms. (.) :: (DomC c x, ObjC c y, CodC c z) => c y z -> c x y -> c x z -- | An alias for objects in the centre of a category. type ObjC c x = (Category c, DomC c x, CodC c x) -- | An alias for a pair of objects which could be connected by a -- @c@-morphism. type HomC c x y = (Category c, DomC c x, CodC c y) Notably, we distinguish domain objects from codomain objects in order to allow morphisms "into" or "out of" the category, which is indeed helpful in practice. Whether there's actually any good reason for distinguishing DomC and CodC, per se, remains to be seen. In Conal Elliott's variation[1] he moves HomC into the class and gets rid of DomC and CodC. Which allows constraints that operate jointly on both the domain and codomain, whereas the above version does not. I haven't run into the need for that yet, but I could easily imagine it. It does add a bit of complication though since we can no longer have ObjC be a derived thing; it'd have to move into the class as well, and we'd have to somehow ensure that it's coherent with HomC. The above version uses PolyKinds as well as ConstraintKinds. I haven't needed this myself, since the constraints act as a sort of kind for the types I'm interested in, but it'll definitely be useful if you get into data kinds, or want an instance of functor categories, etc. [1] https://github.com/conal/linear-map-gadt/blob/master/src/Control/ConstraintK... -- Live well, ~wren

Conal Elliott

8 May 8 May

12:14 p.m.

Hi Wren, Have you taken this "constrained categories" experiment further, particularly for adding products? As I mentioned in a haskell-cafe note yesterday, I tried and got a frightening proliferation of constraints when defining method defaults and utility functions (e.g., left- or right-associating). -- Conal On Fri, Dec 21, 2012 at 8:59 PM, wren ng thornton wrote:

...

On 12/21/12 2:35 PM, Chris Smith wrote:

...
It would definitely be nice to be able to work with a partial Category class, where for example the objects could be constrained to belong to a class. One could then restrict a Category to a type level representation of the natural numbers or any other desired set. Kind polymorphism should make this easy to define, but I still don't have a good feel for whether it is worth the complexity.

Actually, what you really want is ConstraintKinds. The following works just fine in GHC 7.6.1:

{-# LANGUAGE KindSignatures , ConstraintKinds , PolyKinds , TypeFamilies , MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , FlexibleContexts #-}

class Category (c :: k -> k -> *) where

-- | The kind of domain objects. type DomC c x :: Constraint

-- | The kind of codomain objects. type CodC c x :: Constraint

-- | The identity morphisms. id :: (ObjC c x) => c x x

-- | Composition of morphisms. (.) :: (DomC c x, ObjC c y, CodC c z) => c y z -> c x y -> c x z

-- | An alias for objects in the centre of a category. type ObjC c x = (Category c, DomC c x, CodC c x)

-- | An alias for a pair of objects which could be connected by a -- @c@-morphism. type HomC c x y = (Category c, DomC c x, CodC c y)

Notably, we distinguish domain objects from codomain objects in order to allow morphisms "into" or "out of" the category, which is indeed helpful in practice.

Whether there's actually any good reason for distinguishing DomC and CodC, per se, remains to be seen. In Conal Elliott's variation[1] he moves HomC into the class and gets rid of DomC and CodC. Which allows constraints that operate jointly on both the domain and codomain, whereas the above version does not. I haven't run into the need for that yet, but I could easily imagine it. It does add a bit of complication though since we can no longer have ObjC be a derived thing; it'd have to move into the class as well, and we'd have to somehow ensure that it's coherent with HomC.

The above version uses PolyKinds as well as ConstraintKinds. I haven't needed this myself, since the constraints act as a sort of kind for the types I'm interested in, but it'll definitely be useful if you get into data kinds, or want an instance of functor categories, etc.

[1] <https://github.com/conal/**linear-map-gadt/blob/master/** src/Control/ConstraintKinds/**Category.hshttps://github.com/conal/linear-map-gadt/blob/master/src/Control/ConstraintK...

...
-- Live well, ~wren

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

4395

Age (days ago)

4534

Last active (days ago)

List overview

Download

14 comments

9 participants

participants (9)

Chris Smith
Christopher Howard
Conal Elliott
Gershom Bazerman
Jay Sulzberger
ok＠cs.otago.ac.nz
Petr P
Tillmann Rendel
wren ng thornton

Categories (cont.)

wren ng thornton

wren ng thornton

Tillmann Rendel

wren ng thornton

tags

participants (9)