Christopher Howard | 20 Dec 12:42 2012

Categories (cont.)

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:
--------
(Continue reading)

Petr P | 20 Dec 13:35 2012
Picon

Re: Categories (cont.)

  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

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 <christopher.howard <at> frigidcode.com>
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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
wren ng thornton | 20 Dec 13:59 2012

Re: Categories (cont.)

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 | 21 Dec 01:07 2012

Re: Categories (cont.)

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Jay Sulzberger | 21 Dec 04:05 2012
Picon

Re: Categories (cont.)


On Thu, 20 Dec 2012, Christopher Howard <christopher.howard <at> frigidcode.com> 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 | 21 Dec 04:36 2012
Picon

Re: Categories (cont.)

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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Jay Sulzberger | 21 Dec 04:48 2012
Picon

Re: Categories (cont.)


On Thu, 20 Dec 2012, Gershom Bazerman <gershomb <at> gmail.com> 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 | 22 Dec 05:26 2012

Re: Categories (cont.)

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 23:56 2012
Picon

Re: Categories (cont.)


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.
ok | 21 Dec 03:40 2012
Picon

Re: Categories (cont.)

> 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 15:35 2012
Picon

Re: Categories (cont.)

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 | 21 Dec 20:35 2012
Picon

Re: Categories (cont.)

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" <rendel <at> informatik.uni-marburg.de> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Jay Sulzberger | 21 Dec 22:21 2012
Picon

Re: Categories (cont.)


On Fri, 21 Dec 2012, Chris Smith <cdsmith <at> gmail.com> 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" <rendel <at> informatik.uni-marburg.de>
> 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 <at> haskell.org
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>
wren ng thornton | 22 Dec 05:59 2012

Re: Categories (cont.)

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
     --  <at> c <at> -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.hs>

--

-- 
Live well,
~wren
Conal Elliott | 8 May 18:14 2013
Picon

Re: Categories (cont.)

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 <wren <at> freegeek.org> 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
    -- <at> c <at> -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.hs>

--
Live well,
~wren


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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
wren ng thornton | 12 May 00:24 2013

Re: Categories (cont.)

On 5/8/13 12:14 PM, Conal Elliott wrote:
> 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).

I haven't investigated further since my previous emails on the idea. When
working with them, though, I did notice that things work out a lot better
with separate unary constraints on domains and codomains, as opposed to
having a binary constraint that relates domains to codomains. (The latter
is, of course, strictly more powerful; which may be the problem.)

As another part of that project, however, I've been working on type-level
arithmetic, and that also leads to a frightening proliferation of
constraints. The problem is that even though we can implement the
definitions of addition, comparison, etc, there's no good way to teach the
constraint solver facts like:

    m <  S m
    m <= m+n  -- For natural numbers, not integers.
    m <= n -> exists o. n == m+o
    m <= n -> n <= o -> m <= o
    etc

The introduction of these facts would introduce nondeterminism into the
resolution of constraints--- since the solver would need to decide between
using the inductive definitions vs these auxilliary facts.

My impression is that the difficulties here are the same for both cases...

--

-- 
Live well,
~wren

Gmane