jchia_1 2017-02-17 19:52:39
I have a elementary category theory question. Can there be more than one arrow between u and v for some object u and some object v?
jle` 2017-02-17 19:52:55
yes
jchia_1 2017-02-17 19:52:59
i mean "more than one arrow from u to v"
jle` 2017-02-17 19:53:46
jchia_1: the case where there is at most one is a special case, called a thin category
jchia_1 2017-02-17 19:53:47
jle`: Then when you compose two arrows, (u -> v) and (v -> w), there could be multiple possible arrows (u -> w)?
jle` 2017-02-17 19:54:03
well, if you compose those two arrows, there is a unique result
jle` 2017-02-17 19:54:12
but that result is potentially not the only (u -> v)
jle` 2017-02-17 19:54:17
*not the only (u -> w)
jchia_1 2017-02-17 19:54:33
if there are multiple arrows (u->w), which arrow is the result of the composition?
jle` 2017-02-17 19:54:42
that depends on the category
jle` 2017-02-17 19:55:26
that's like asking "if there are multiple items in a group, which one is the result of x*y?"
jle` 2017-02-17 19:55:41
the result is a part of the definition of that group action
jchia_1 2017-02-17 19:55:52
jle`, so when you define a category, not only do you have to say what the objects and arrows are, if the category is not thin, you have to say how to compute composition?
jle` 2017-02-17 19:55:59
yes
EvanR 2017-02-17 19:56:20
that is the main question to answer, what you get when you smush two arrows together
jle` 2017-02-17 19:56:31
that's like saying if you define a group, you don't only have to say what the items are, but also what teh result of 'multiplication' is
EvanR 2017-02-17 19:56:44
and show that its associative and respects identity arrows
jle` 2017-02-17 19:56:51
so when you say that the integers is a group under +, you have to define what the result of 2 + 3, 2 + 4 is, etc.
jle` 2017-02-17 19:57:10
and that's actually the interesting part of the group
jle` 2017-02-17 19:58:00
jchia_1: are you familiar with groups/monoids?
jle` 2017-02-17 19:58:13
if you're familiar with Haskell, it's sort of like writing a Monoid instance
jchia_1 2017-02-17 19:58:19
jle`: No, only graphs, sets and some haskell types
jle` 2017-02-17 19:58:21
not only do you have to define what type is the Monoid, you also have to define (<>)
EvanR 2017-02-17 19:58:22
example, in the category of sets and functions, there are 4 functions from Bool to Bool
jchia_1 2017-02-17 19:58:29
and haskell monoids
jle` 2017-02-17 19:58:33
instance Monoid [] where
jle` 2017-02-17 19:58:45
mappend = concat
jle` 2017-02-17 19:58:56
* Monoid [a]
jle` 2017-02-17 19:59:07
* (++)
jle` 2017-02-17 19:59:22
you have to give what type you're talking about ([a]), and also what it means to 'mappend' (here, (++))
jle` 2017-02-17 20:00:24
instance Monoid Int where
jle` 2017-02-17 20:00:27
mappend = (+)
jle` 2017-02-17 20:01:26
here we define a monoid (Int, 0, (+)), which is what the items of the monoid are (values of type Int), the identity (0), and the mappending action (here, addition)
jle` 2017-02-17 20:01:30
we have to provide all three
jle` 2017-02-17 20:02:44
it's the same for defining a Category. you have to provide what the objects are, what the morphisms are, how to generate the identity morphism for each object, and the composing action
jchia_1 2017-02-17 20:03:47
jle`: I get it. I was under the impression that you can only have one arrow from u to v.
EvanR 2017-02-17 20:04:14
a basic example of a category is sets as objects and functions between them as arrows
EvanR 2017-02-17 20:04:34
you can see for many sets there are more than one possible function
jle` 2017-02-17 20:05:40
jchia_1: one way you can think of a category is as a partial monoid
EvanR 2017-02-17 20:05:52
in the case of 1 -> N, there are an infinite number of functions
jchia_1 2017-02-17 20:06:15
EvanR: OK. I suppose if you try to draw the category, it's hard to it justice. You draw one arrow from one set to another set but it's really representing a multitude of functions.
jchia_1 2017-02-17 20:06:22
"hard to do it justice"
EvanR 2017-02-17 20:06:32
if your category is simple enough you can draw it completely
EvanR 2017-02-17 20:06:46
its ok to draw more than one arrow between the same pair of objects
EvanR 2017-02-17 20:07:49
heres one http://category-theory.mitpress.mit.edu/images/Art_P216.jpg
jchia_1 2017-02-17 20:09:25
EvanR: Yeah, but in the category where (large) sets are objects and arrows are functions mapping between them, there are potentially many arrows from one object to another, so realistically it can't be drawn.
EvanR 2017-02-17 20:09:33
in diagrams one arrow means one arrow, or else "insert whatever arrow you want here"
EvanR 2017-02-17 20:10:24
for finite sets you can think about it combinatorially
EvanR 2017-02-17 20:11:28
there are n^m functions from set of size m to set of size n
jchia_1 2017-02-17 20:11:37
how are some applications of category theory in haskell? are there libraries that are easier to understand/use if i know category?
jchia_1 2017-02-17 20:11:51
EvanR: yeah, that's exactly what i mean. too many arrows to draw on paper
jle` 2017-02-17 20:12:03
jchia_1: you might not even just want to draw a bunches of arrows because to make it useful you'd also have to label them
jle` 2017-02-17 20:12:36
jchia_1: well, on one level, you can use it to help with your program refactoring
jle` 2017-02-17 20:13:02
similar to monoids, you get associativity and stuff
jle` 2017-02-17 20:13:34
jchia_1: on another level, there's http://hackage.haskell.org/package/base-4.9.1.0/docs/Control-Category.html
jle` 2017-02-17 20:13:41
which lets you write code that's polymorphic ove all Categories
jle` 2017-02-17 20:14:04
in the same way that you can use the Monoid typeclass to write monoid-polymorphic code. like for Writer, and mconcat
EvanR 2017-02-17 20:14:18
so far i have no found CT directly beneficial to haskell coding
EvanR 2017-02-17 20:14:29
its just an interesting decorative thing
jle` 2017-02-17 20:14:33
jchia_1: but, to answer your more general question, category theory extends to more than just the definition of categories
jchia_1 2017-02-17 20:14:55
jle`: Roughly speaking, how can I apply category theory to do refactoring?
jchia_1 2017-02-17 20:15:08
Control.Category looks abstract. Are there examples of how to use it?
jle` 2017-02-17 20:15:19
Control.Category should look very familiar
jle` 2017-02-17 20:15:30
the Category typeclass is more or less the Monoid typeclass
jle` 2017-02-17 20:15:32
but higher-kinded
jchia_1 2017-02-17 20:15:39
jle`: it has the elements of category, but how do i write a program with it?
jchia_1 2017-02-17 20:15:51
"elements of category theory"
jle` 2017-02-17 20:16:03
do you understand why the Monoid typeclass is useful, or why knowing that something is a monoid is useful?
EvanR 2017-02-17 20:16:14
if you have arrows a, b, c, d of the appropriate types, you can do a . b . c . d
jchia_1 2017-02-17 20:16:30
jle`: Yes, it's polymorphic, i can work with a Monoid without knowing what kind of Monoid it is
jle` 2017-02-17 20:16:40
the only reason that we can have a Writer monad is because of the Monoid typeclass abstracting over monoids
jle` 2017-02-17 20:17:00
and yeah, it's similar here; you can do category-polymorphic things with any instance of Category
jle` 2017-02-17 20:17:22
practically though there are less interesting category-polymorphic things you can do than there are interesting monoid-polymorphic things you can do
EvanR 2017-02-17 20:17:43
just like in CT, you have to add extra powers to a category to get things to be interesting
EvanR 2017-02-17 20:17:57
which is what you have in kmett libs
jle` 2017-02-17 20:18:14
yeah, if you impose more structure on your categories, you can get some more interesting polymorphic things you can do with them
jle` 2017-02-17 20:18:30
kind of like how adding extra structure to Applicative gives you Monad, which lets you do more interesting things
jle` 2017-02-17 20:18:57
jchia_1: but on a refactoring level, there are libraries like 'pipes' that give you values that they claim are morphisms in some category
jle` 2017-02-17 20:19:18
jchia_1: so with that in mind you know that their composition operator is associative
Cooler 2017-02-17 20:19:24
> fmap (10/) (4, 5)
jle` 2017-02-17 20:19:24
jchia_1: and also that you have access to an identity at any time
lambdabot 2017-02-17 20:19:27
(4,2.0)
Cooler 2017-02-17 20:19:38
why does that give 4?
Cooler 2017-02-17 20:19:43
10/4 = 4?
jchia_1 2017-02-17 20:19:44
EvanR: Yeah, Control.Category looks like a "kmett lib" to me. I look at it and wonder how exactly I'm supposed to use it, and I try to find examples.
glguy 2017-02-17 20:20:15
Cooler: The fmap instance for (,)a can't touch the first component of the tuple
jle` 2017-02-17 20:20:18
Cooler: fmap doesn't change the first item
jle` 2017-02-17 20:20:22
> fmap (10/) ('a', 5)
lambdabot 2017-02-17 20:20:26
('a',2.0)
Cooler 2017-02-17 20:20:37
why?
jle` 2017-02-17 20:20:55
Cooler: its implementation is parametrically polymorphic, so it has to be the same no matter waht the type of the first item is
fizbin 2017-02-17 20:20:56
Because tuples aren't lists?
jchia_1 2017-02-17 20:20:57
jle`: I'm not sure what 'cat' is in the Category class
jle` 2017-02-17 20:21:02
jchia_1: cat is your instance
jle` 2017-02-17 20:21:07
sort of like Monoid m, m is the instance
jle` 2017-02-17 20:21:23
the Category typeclass is more or less identical to the Monoid typeclass, so if you understand one, you should understand the other
jchia_1 2017-02-17 20:21:26
jle`: What is cat a b?
jchia_1 2017-02-17 20:21:30
a function?
jle` 2017-02-17 20:21:51
Cooler: it's a value of 'cat' applied to two type parameters
jle` 2017-02-17 20:21:59
sort of like how you have fmap :: Functor f => (a -> b) -> f a -> f b
jle` 2017-02-17 20:22:06
'f a' is f (the instance) applied to a type parameter, a
jle` 2017-02-17 20:22:12
oh sorry, that was meant for jchia_1
jle` 2017-02-17 20:22:20
Cooler: what do you think fmap (10/) ('a', 5) should do?
jle` 2017-02-17 20:22:35
fmap :: (a -> b) -> (c, a) -> (c, b)
jle` 2017-02-17 20:22:41
that's the type of fmap for tuples
Cooler 2017-02-17 20:22:49
but why?
jle` 2017-02-17 20:22:54
:t fmap
lambdabot 2017-02-17 20:22:56
Functor f => (a -> b) -> f a -> f b
narasca 2017-02-17 20:22:57
the functor is ((,) a)
jle` 2017-02-17 20:23:07
the tuple instance is `((,) c)`
dmj` 2017-02-17 20:23:15
Cooler: it can, since tuples are also bifunctors
dmj` 2017-02-17 20:23:21
> bimap (+1) (+1) (1,1)
lambdabot 2017-02-17 20:23:25
(2,2)
jle` 2017-02-17 20:23:33
Cooler: so that's fmap :: (a -> b) -> ((,) c) a -> ((,) c) b
jle` 2017-02-17 20:23:44
Cooler: do you see why? i replaced the 'f' (the Functor instance) with ((,) c)
jle` 2017-02-17 20:23:54
and so then we get fmap :: (a -> b) -> (c, a) -> (c, b)
Cooler 2017-02-17 20:24:07
ok
jle` 2017-02-17 20:24:12
the functor instance for tuples is ((,) c)
jchia_1 2017-02-17 20:24:21
jle`: I think I can use (->) as cat, correct? But then it's not that interesting, is it? I could just use regular haskell function composition. What's the point of using Category?
fizbin 2017-02-17 20:24:27
Cooler: I think part of the reasoning you're missing is that in general a 2-tuple has two different types for fst and snd.
Cooler 2017-02-17 20:24:32
so for a 3 tuple (a, b, c) it would just affect c?
jle` 2017-02-17 20:24:46
jchia_1: that's like asking what's the point of using Monoids if i can always just use (+)/(||)/(++)/(*)
jle` 2017-02-17 20:25:04
jchia_1: you can use [a] is the Monoid instance and then your mappend is (++)
jle` 2017-02-17 20:25:09
so why bother with making a monoid instance
jle` 2017-02-17 20:25:12
when you can always just use (++)
jchia_1 2017-02-17 20:25:15
jle`: Could you give me a few examples of useful things to use as cat?
fizbin 2017-02-17 20:25:22
Cooler: So the natural definition of fmap is only going to apply to one of the members
jle` 2017-02-17 20:25:33
jchia_1: do you mean, useful Category-polymorphic functions?
jle` 2017-02-17 20:25:55
jchia_1: or do you mean interesting Category instances
Cooler 2017-02-17 20:25:57
so for a 3 tuple (a, b, c) it would just affect c?
jchia_1 2017-02-17 20:26:01
Category instances
narasca 2017-02-17 20:26:08
Cooler: that you cant do
glguy 2017-02-17 20:26:25
cooler: right
jle` 2017-02-17 20:26:36
jchia_1: i can, but remember that individual category instances aren't the 'neat' thing about using Category in haskell
jle` 2017-02-17 20:26:48
jchia_1: just like individual monoid instances aren't the neat thing about the Monoid typeclass
jchia_1 2017-02-17 20:27:02
i just want to understand with some concrete examples
jle` 2017-02-17 20:27:17
jchia_1: the common instasnce people are shown next is Kleisli m
jle` 2017-02-17 20:27:28
where newtype Kleisli m a b = K (a -> m b)
fizbin 2017-02-17 20:27:45
Cooler: You could define fmap applied to (a,b,c) to mean that (affect only the last one)
jchia_1 2017-02-17 20:27:48
jle`: I'm not familiar with Control.Arrow.
jle` 2017-02-17 20:27:57
this has nothing to do with Control.Arrow
jle` 2017-02-17 20:28:05
this is just a type that has a Category instance
jle` 2017-02-17 20:28:11
can you think of what it would be?
jle` 2017-02-17 20:28:24
what would (K f) . (K g) = ??
fizbin 2017-02-17 20:28:31
Cooler: But basic haskell doesn't define what fmap on a 3-tuple is
jchia_1 2017-02-17 20:28:32
jle`: Isn't Kliesli defined in Control.Arrow?
fizbin 2017-02-17 20:28:34
> fmap (+1) (0 , 0, 0 ) :: (Int,Int,Int)
lambdabot 2017-02-17 20:28:37
error:
lambdabot 2017-02-17 20:28:37
• No instance for (Functor ((,,) Int Int))
lambdabot 2017-02-17 20:28:37
arising from a use of 'fmap'
fizbin 2017-02-17 20:28:45
Cooler: ^^^
jle` 2017-02-17 20:28:46
jchia_1: it could be, but i'm giving you the definition here
jle` 2017-02-17 20:28:55
jchia_1: you can just think of it as a newtype wrapper over an (a -> m b) function
Cooler 2017-02-17 20:29:09
fizbin, why does it define fmap on a tuple given its so weird?
jle` 2017-02-17 20:29:10
newtype Foo m a b = MkFoo (a -> m b)
jle` 2017-02-17 20:29:24
jchia_1: can you write a Category instance for Monad m => m ?
jle` 2017-02-17 20:29:33
er
jle` 2017-02-17 20:29:40
Monad m => Foo m
jle` 2017-02-17 20:29:44
id :: Monad m => Foo m a a
jle` 2017-02-17 20:29:59
(.) :: Monad m => Foo m b c -> Foo m a b -> Foo m a c
EvanR 2017-02-17 20:29:59
a 3-tuple is strictly speaking superfluous
fizbin 2017-02-17 20:30:26
Cooler: Because it's useful? Also, after using it for a while it doesn't seem that weird.
jle` 2017-02-17 20:30:28
Cooler: you can think of the Functor, Applicative, Monad, Traversable, Foldable, etc. instances of tuple as treating the tuple as a tagged value
EvanR 2017-02-17 20:30:30
if you think of (a,b) functor as being some computation with read-only environment a, then the 3-tuple from earlier would be ((a,b),c)
jle` 2017-02-17 20:30:38
Cooler: an (Int, a) is an 'a' that's "tagged" with an Int
jle` 2017-02-17 20:30:53
Cooler: so fmapping a function over an (Int, a) would be mapping over the actual value, while leaving the tag unchanged
jle` 2017-02-17 20:31:02
jchia_1: let me know if you want me to spoil the answer for you :)
EvanR 2017-02-17 20:31:27
and at the point you have (((a,b),c),d) you probably want a record in that spot
EvanR 2017-02-17 20:31:58
binary products implies all finite products
fizbin 2017-02-17 20:32:23
EvanR: Unless you've gotten yourself tied in knots and at that point are addicted to &&& and *** etc.
jchia_1 2017-02-17 20:32:28
(MkFoo x) . (MkFoo y) = MkFoo (x >=> y)
jle` 2017-02-17 20:32:48
jchia_1: yup. well actaully MkFoo (x <=< y), for the types to line up
jchia_1 2017-02-17 20:32:49
jle`: Maybe i got the direction wrong, hold on
EvanR 2017-02-17 20:32:54
arrows are sad
jle` 2017-02-17 20:33:34
jchia_1: so you found out that for the (a -> m b) instance of Category, (.) is just kleisli composition
jle` 2017-02-17 20:33:44
so kleisli arrows form a category, with (>=>) as their composition action
EvanR 2017-02-17 20:34:08
isnt it <=<
jle` 2017-02-17 20:34:24
sure :o
jchia_1 2017-02-17 20:34:25
jle`: OK, so I could write some code in terms of Category that I could use on monads and functions, among other things.
EvanR 2017-02-17 20:34:31
this is haskell we do everything backwards
EvanR 2017-02-17 20:34:35
and we like it
jle` 2017-02-17 20:34:38
jchia_1: yeah, yu can use it for kleisli arrows, and also for functions
spear2 2017-02-17 20:35:02
lol i look away for 2 minutes and "there can be more than one arrow between objects a and b" becomes "so kleisli arrows form a category, with (>=> as their composition action"
jle` 2017-02-17 20:35:05
but this is kind of yawn bc there aren't too many occasions where you think "oh i wish i could write something that is generalized for both normal functions and kleisli arrows"
jle` 2017-02-17 20:35:32
so while this is interesting, the Category typeclass ends up not being super useful for writing polymorphic code
EvanR 2017-02-17 20:35:53
bare categories dont have much going on
EvanR 2017-02-17 20:36:16
2-categories maybe
jle` 2017-02-17 20:36:27
yeah, there just isn't enough structure to take advantage of
jle` 2017-02-17 20:37:05
jchia_1: another instance in base is (:~:) or type equality
EvanR 2017-02-17 20:37:16
every weirdo category is a valid category, but the key is your polymorphic code cant know about those non-standard details without extra assumptions
EvanR 2017-02-17 20:37:47
unlike in java where every Object has a huge array of bog standard support methods
jle` 2017-02-17 20:38:21
jchia_1: if you know about (:~:), then a value of (a :~: b) is a proof that 'a' and 'b' are the same type
jle` 2017-02-17 20:38:48
so, for the (:~:) category, `id :: a :~: a`, which says, "you can always get a proof that a type is the same as itself"
jle` 2017-02-17 20:39:04
and (.) :: (b :~: c) -> (a :~: b) -> (a :~: c)
jle` 2017-02-17 20:39:40
which says, "if i have a proof that 'b' is the same as 'c', and a proof that 'a' is the same as 'b', then i can make a proof that 'a' is the same as 'c'"
jle` 2017-02-17 20:39:54
so, for the (:~:) category, (.) is the transitive property of equality
jle` 2017-02-17 20:40:34
and 'id' is the reflexive property of euqality
EvanR 2017-02-17 20:40:38
every ordered set is a category in the same way
jchia_1 2017-02-17 20:42:56
jle`: How could I make use of this in a program?
jchia_1 2017-02-17 20:43:16
jle`: To somehow test for type equality?
EvanR 2017-02-17 20:43:38
:t testEq
lambdabot 2017-02-17 20:43:39
error: Variable not in scope: testEq
jle` 2017-02-17 20:43:44
jchia_1: well, in the context of this discussion, it gives you a familiar API to work with (:~:)
jle` 2017-02-17 20:44:00
if you know that (:~:) is an instance of Category, you already know that you have (.) and id
EvanR 2017-02-17 20:44:25
:t testEquality
lambdabot 2017-02-17 20:44:25
error: Variable not in scope: testEquality
jle` 2017-02-17 20:44:25
just like if you know IO is a Monad, you know that you have 'return' and (>>=)
EvanR 2017-02-17 20:44:43
if you are resorting to runtime testing of type equality, you are likely doing something wrong
EvanR 2017-02-17 20:45:01
and if youre not, then you know so much this advice doesnt matter
