DrSyzygy and Category Theory

DrSyzygy_and_category_theory.txt

<hiptobecubic> @src Maybe
<lambdabot> data Maybe a = Nothing | Just a
<hiptobecubic> @src Monad
<lambdabot> class  Monad m  where
<lambdabot>     (>>=)       :: forall a b. m a -> (a -> m b) -> m b
<lambdabot>     (>>)        :: forall a b. m a -> m b -> m b
<lambdabot>     return      :: a -> m a
<lambdabot>     fail        :: String -> m a
<hiptobecubic> @src [] (>>)
<lambdabot> xs >> ys      = concatMap (const ys) xs
<hiptobecubic> @src [] (>>=)
<lambdabot> xs >>= f     = concatMap f xs
<hiptobecubic> So are lists a category? 
<hiptobecubic> well it's a monad i guess
<hiptobecubic> also a monoid i would think? with "." being concatenation?
<byorgey> hiptobecubic: the list constructor is a monad.  There is a category (the Kleisli category) that corresponds to any monad.
<byorgey> lists are a monoid, yes.
<byorgey> but it doesn't make sense to ask whether "lists are a category".
<hiptobecubic> byorgey, yeah. i feel like i'm one level of abstraction too low, or maybe more
<byorgey> the Kleisli category for lists is the category where arrows from a to b  are functions of type   a -> [b]
<hiptobecubic> why a -> [b] and not [a] -> [b]?
<monochrom> so that >>> is >=>
<DrSyzygy> hiptobecubic: Because that's what the Kleisli category is.
<parcs`> why [a] -> [b] and not a -> [b]?
<hiptobecubic> parcs`, from lists to other lists?
<DrSyzygy> If M is a monad, then the Kleisli category for M has as objects the objects of the category outside, and a morphism a -> b is a function a -> M b
<hiptobecubic> The category outside?
<DrSyzygy> hiptobecubic: In this case Hask, the category of haskell types.
<DrSyzygy> so if M is a Haskell monad, you have objects of the Kleisli category being simply haskell types.
<hiptobecubic> So... M is in Hask as well of course?
<DrSyzygy> Composition g . f is join . fmap g . f
<DrSyzygy> M is  amonad.
<DrSyzygy> over Hask.
<DrSyzygy> so a monad in the sense you're used to.
<hiptobecubic> DrSyzygy, there is no sense that I'm used to.
<monochrom> M is a monadic functor from Hask to Hask
<DrSyzygy> For lists, this says that functions in a Kleisli category are maps a -> [b] (by definitino) and function composition takes f::a -> [b] and g::b -> [c] and does join . map g . f
<DrSyzygy> if you're not familiar with monads, thoguh, it's not entirely clear to me that learning about the Kleisli category will help you further.
<hiptobecubic> DrSyzygy, leaving parts out makes it harder to understand though. It's better this way.
<DrSyzygy> hiptobecubic: what parts are you worrying about seeing left out?
<hiptobecubic> maps are from a -> [b], where a is "outside" the monad and b is in it?
<rostayob> hiptobecubic: you're not leaving anything out if you're learning monads and you don't learn about arrows :P
<hiptobecubic> DrSyzygy, rostayob perhaps not, but that's not something you would know until it's too late
<DrSyzygy> hiptobecubic: a morphism from a to b in the Kleisli category for Hask is the same thing as a Haskell function a -> M b.
<rostayob> hiptobecubic: if you want to learn about arrows, read Wadler's paper
<rostayob> that was the best resource I could find
<hiptobecubic> I'll take your word for it, of course. I'm just tired of people throwing crappy analogies around everytime anyone writes a blog post or asks a question about monads
<DrSyzygy> hiptobecubic: You don't want crappy analogies? Okay then.
<DrSyzygy> 1. Do you know what a category is? (if you say no, I will follow up with a definition and a discussion of its implications)
<monochrom> there is no analogy here so far
<hiptobecubic> like this astronaut <-> spacestation garbage I found last time I was searching
<DrSyzygy> hiptobecubic: Christ, yeah, no.
<monochrom> right, we are all past that
<DrSyzygy> hiptobecubic: http://www.haskell.org/haskellwiki/User:Michiexile/MATH198
<DrSyzygy> Not a space station anywhere.
<hiptobecubic> DrSyzygy, I know of them, in that I very slowly read the wikipedia article four times in the last hour
<DrSyzygy> hiptobecubic: Okay. Here's my short spiel on a category.
<rostayob> hiptobecubic: you don't need to know about category theory either....
<hiptobecubic> rostayob, perhaps not, but now i'm interested :)
<rostayob> well, ok then
<DrSyzygy> A category is a thing that looks like what people in algebra and topology had been doing for a couple of decades already. It abstracts out the mathematical concept of a Function in a way that turns out to apply to all sorts of cases.
<DrSyzygy> Fundamentally, a category consists of Objects and Morphisms. Each morphism is associated to two objects -- a source and a target.
<DrSyzygy> And if you take a chain of morphism you can "compose" them - much like you would with functions -- to get a new morphism.
<hiptobecubic> DrSyzygy, yes. So far I think I got that part.
<DrSyzygy> Concretely, in our context we tend to talk about one category in particular: Hask. This has objects <Haskell types> and morphisms <Haskell functions>.
<DrSyzygy> So an object is something like Bool or Char or [String] -> (Int -> String)
<hiptobecubic> Ok
<parcs`> if Kleisli were [a] -> [b] it would be just a specialized function arrow
<DrSyzygy> A morphism is just any function you can write down.
<rostayob> [a] -> [b] is a useful arrow
<DrSyzygy> You'll notice that morphisms are members of haskell types as well -- this is a specific and kinda neat property that categories may or may not have.
<tzxn3> https://en.wikibooks.org/wiki/Haskell/Understanding_monads/State#Introducing_State
<DrSyzygy> hiptobecubic: With me so far?
<ion> hiptobecubic: You could make a category of lists of functions. I’m not sure if that would be very useful, though. :-)
<hiptobecubic> DrSyzygy, yes
<hiptobecubic> so functions are objects and morphisms ?
<hiptobecubic> in Hask?
<DrSyzygy> hiptobecubic: objects in Hask are _datatypes_.
<ion> newtype LoF a b = LoF [a -> b]
<hiptobecubic> DrSyzygy, ohhh sorry. yes. that makes more sense
<DrSyzygy> hiptobecubic: morphisms in Hask are haskell functions.
<DrSyzygy> A function has an input datatype and an output datatype.
<ion> id = LoF (pure id); (LoF fs) . (LoF gs) = LoF (liftA2 (.) fs gs) :-P
<DrSyzygy> hiptobecubic: Now, the next step is functors.
<hiptobecubic> DrSyzygy, pause
<DrSyzygy> hiptobecubic: Sure.
<hiptobecubic> DrSyzygy, So is the morphism just referring to source and target type? or the actual computation that the function does
<DrSyzygy> hiptobecubic: The morphism is the function. But part of what a morphism is is that it knows where it starts and where it ends.
<DrSyzygy> hiptobecubic: Now what we basically have so far is a definition of an algebraic object. A category is a thing with objects and morphisms, such that things behave nicely.
<DrSyzygy> hiptobecubic: Behaving nicely here means things like "function composition is associative" and "id exists"
<DrSyzygy> hiptobecubic: In particular, it seems almost ridiculously obvious when we discuss the Haskell category.
<hiptobecubic> DrSyzygy, so the morphism "odd" is from the object Int to the object Bool, but it also includes the logic of the function to differentiate it from the other morphisms with the same source and target?
<DrSyzygy> hiptobecubic: Yes.
<DrSyzygy> hiptobecubic: In particular, odd :: Int -> Bool is a different morphism from even :: Int -> Bool.
<hiptobecubic> DrSyzygy, yes that's what I was thinking. ok
<hiptobecubic> DrSyzygy, is there a word for the set of morphisms of type Int -> Bool?
<DrSyzygy> hiptobecubic: Sure. It's the set of morphisms Hom(Int, Bool)
<hiptobecubic> DrSyzygy, Hom? 
<DrSyzygy> hiptobecubic: Or, in Haskell, it's the morphisms of type Int -> Bool.
<DrSyzygy> hiptobecubic: In particular, all this makes Category into an essentially algebraic idea.
<DrSyzygy> hiptobecubic: So we can apply algebraic techniqeus to them.
<DrSyzygy> hiptobecubic: We can, for instance, ask what a map between categories should look like.
<DrSyzygy> hiptobecubic: Hom = Homomorphisms. Comes from the algebraic heritage of category theory.
<hiptobecubic> DrSyzygy, ok
<DrSyzygy> hiptobecubic: A map between categories should map objects to new objects. And it should map morphisms to morphisms. And things that compose should still compose. And the source/target should follow along.
<hiptobecubic> DrSyzygy, so between categories, would be object -> object?
<hiptobecubic> DrSyzygy, yes ok
<DrSyzygy> hiptobecubic: So in particular, a map from Hask to Hask should assign to each data type t a new datatype F t, and to each function s -> t a new function F s -> F t.
<DrSyzygy> hiptobecubic: Since datatypes behave the way they do, in Haskell it is enough to have a constructor of kind * -> * to build the object side of a functor.
<hiptobecubic> DrSyzygy, so if Int maps to A and Bool maps to B and even to C, then C should be of type A -> B?
<DrSyzygy> hiptobecubic: and the function side shows up from fmap :: (a -> b) -> (F a -> F b)
<DrSyzygy> hiptobecubic: If you have a functor it will map each datatype to exactly one datatype.
<DrSyzygy> So Bool cannot map to both B and C.
<DrSyzygy> Because the functor changes datatypes.
<DrSyzygy> Here is when you want to start thinking about [].
<DrSyzygy> hiptobecubic: If you have a datatype t, then [t] is a datatype.
<rostayob> but it's still similar
<DrSyzygy> hiptobecubic: and if you have a map s -> t, there is a particularly nice function map :: [s] -> [t].
<hiptobecubic> DrSyzygy, ok let me digest for a minute
<ion> drsyzygy: Are there other sensible maps from Hask to Hask than adding F in front of data types and the function’s input and output types?
<hiptobecubic> DrSyzygy, so i'm clear. [t] is the same as m t where m is lists, yes?
<DrSyzygy> hiptobecubic: Yes.
<DrSyzygy> ion: It's actually kinda difficult to write down functor-ish things that aren't functors in Haskell.
<DrSyzygy> I'm sure we can figure one out, but they tend to have a slightly artificial feel to them.
<DrSyzygy> ion: Basically, just like you tend to want linear maps between vector spaces, you kinda really want functors between categories.
<hiptobecubic> DrSyzygy, "* -> *" is a kind? Meaning ... thing from a thing to a thing?
<ion> drsyzygy: How about an illustrative example outside Haskell?
<DrSyzygy> hiptobecubic: Yes.
<ion> or outside Hask
<DrSyzygy> ion: Sure! One nice bunch of categories show up from partially ordered sets.
<DrSyzygy> ion: So you have the partial order a < b < c, right? and another partial order d > e < f.
<ion> I get (a -> b) -> (F a -> F b) but i have no understanding of functors outside Hask.
<hiptobecubic> :t map
<lambdabot> forall a b. (a -> b) -> [a] -> [b]
<hiptobecubic> :t fmap
<lambdabot> forall a b (f :: * -> *). (Functor f) => (a -> b) -> f a -> f b
<DrSyzygy> ion: So both these have three elements. one of them have all elements in a row, the other orders them so that e is smaller than both d and f, but we cannot compare d and f directly.
<DrSyzygy> Here is one functor from abc to def: a->e b->d c->f.
<DrSyzygy> wait.
<DrSyzygy> first of all: here is how you make categories out of partial orders.
<DrSyzygy> objects are the elements of the poset. and there is EXACTLY one morphism x -> y iff x <= y.
<hiptobecubic> poset?
<DrSyzygy> partially ordered set.
<hiptobecubic> ok
<DrSyzygy> So in abc we have morphisms a->a, a->b, a->c, b->b, b->c, c->c.
<DrSyzygy> In def we have morphisms d->d, e->e, e->d, e->f, f->f.
<DrSyzygy> Now, a functor from abc to def is for instance a->e, b->d, c->f and all the maps go where they need to.
<DrSyzygy> no wait.
<DrSyzygy> I'm stupid. sorry.
<DrSyzygy> what I wrote up there earlier is an example of a non-functor function between the object sets.
<DrSyzygy> because there IS a moprhism b->c, but there is no morphism d->f.
<hiptobecubic> DrSyzygy, so we can only map to larger values?
<DrSyzygy> A functor def -> abc is d->b e->a f->c and all morphisms go where they need to.
<DrSyzygy> hiptobecubic: you have to be able to map morphisms.
<DrSyzygy> You can construct examples where all objects map, all morphisms map, but the composition breaks down.
<hiptobecubic> DrSyzygy, need to read that again...
<DrSyzygy> shergill: I started out as a pure mathematician, doign stuff close to category theory. I took up haskell BECAUSE categories are so useful and closely related to the language.
<cmccann> shergill, I think the rule of thumb is that Haskell enthusiasts are people who programmers think are mathematicians and mathematicians think are programmers
<ion> drsyzygy: Ok, thanks, i can see how the map works. What would be an example of a use case for the map between posets?
<hiptobecubic> rostayob, I started out as an environmental biologist :) Don't feel bad
<DrSyzygy> ion: Suppose the poset structure is accidential, and what you really care about is some other property.
<DrSyzygy> ion: Or suppose there are several valid poset structures on a set together with whatever other structure you are interested in.
<hiptobecubic> DrSyzygy, ok so we're limited to x <= y because otherwise we can't bring the morphisms from one category to the other?
<DrSyzygy> hiptobecubic: exactly
<DrSyzygy> ion: For instance, you can define a total order on complex numbers; but in very many ways, none of which are always appropriate.
<hiptobecubic> DrSyzygy, Is each poset it's own category in this example? And we're mapping between categories when we map between posets?
<DrSyzygy> ion: But you can still do, say, complex analysis in spite of this, and you may well have complex analytic functions that might or might not agree with the orderings involved.
<DrSyzygy> hiptobecubic: Every poset is a category with the construction I talked about above.
<DrSyzygy> A total order is a poset in which any pair of objects are comparable.
<hiptobecubic> DrSyzygy, are "posets" also a category?
<DrSyzygy> hiptobecubic: Yup. And morphisms for the category of posets are maps that respect ordering.
<DrSyzygy> hiptobecubic: So that if a < b then f(a) < f(b)
<DrSyzygy> so exactly the functor condition, really.
<hiptobecubic> DrSyzygy, ok yes. I'm feeling it.
<hiptobecubic> DrSyzygy, I think I'm caught up with you so far. If you were intending to continue
<DrSyzygy> hiptobecubic: Right. So if you are starting to get a feeling for functors, I want to start talking about endofunctors.
<DrSyzygy> hiptobecubic: Or in other words, functors from Hask back to Hask again.
<DrSyzygy> hiptobecubic: Here's one nice thing about functors Hask -> Hask: almost all of them make sense as "data containers".
<DrSyzygy> hiptobecubic: Because 1. a functor assigns to each data type a new data type -- the type contained.
<hiptobecubic> DrSyzygy, what do you mean?
<DrSyzygy> hiptobecubic: 2. functions between datatypes act on the "inside" by the fmap property of functors.
<DrSyzygy> hiptobecubic: 3. id has to fix things for a functor.
<DrSyzygy> hiptobecubic: 4. function composition has to work.
<_mpu> rostayob: heck,  Result signatures are no longer supported in pattern matches
<DrSyzygy> These 4 observations together force something that looks a lot like a data type container.
<DrSyzygy> hiptobecubic: So if F is a functor, and t is some datatype, we know that F t is some datatype.
<hiptobecubic> Also, you called "a -> e, b->d, c->f" a functor before, but it is also a morphism in the category of posets, right?
<DrSyzygy> hiptobecubic: Yes. And because each poset is a category, we get functoriality.
<DrSyzygy> hiptobecubic: There is a category of all categories, and morphisms in this category are functors.
<DrSyzygy> hiptobecubic: ... actually, I realized that this abc -> def wasn't a morphism - it was the function def -> abc that was.
<hiptobecubic> DrSyzygy, ok. So functors specifically refer to the morphisms in the category of categories
<DrSyzygy> hiptobecubic: EXACTLY!
<hiptobecubic> DrSyzygy, and endofunctors are morphisms for which the source and target are the same object?
<ion> What would be an example of a non-endo functor?
<DrSyzygy> hiptobecubic: Yup.
<hiptobecubic> let me try
<DrSyzygy> ion: Anything where source and target category are different.
<cmccann> ion, half of ContT is an interesting, Haskell-relevant example
<cmccann> ion, i.e. "newtype F r m a = F (a -> m r)"
<cmccann> where composing F with itself gives you ContT
<hiptobecubic> So for example the one you mentioned earlier, between posets
<hiptobecubic> is a non-endofunctor
<DrSyzygy> hiptobecubic: Yup. Because the posets are different and therefore form different categories.
<DrSyzygy> hiptobecubic: So if F is a functor and t is a datatype, F t is some datatype.
<DrSyzygy> hiptobecubic: You know that id :: F t -> F t exists, and doesn't change things.
<hiptobecubic> Whereas Haskell functions (morphisms in Hask) are all endofunctors?
<DrSyzygy> hiptobecubic: Haskell Functors are all endofunctors.
<DrSyzygy> hiptobecubic: Haskell functions are all morphisms.
<DrSyzygy> hiptobecubic: You know that fmap :: (t -> s) -> (F t -> F s) exists, and that fmap id :: F t -> F t has to be the same as id.
<DrSyzygy> hiptobecubic: And you know that fmap (g . f) is what you expect it to be. So fmap lets you operate inside F automatically.


----------------------------------- Side note ----------------------------------
<cmccann> also, Functor instances necessarily define proper subcategories of Hask, so you could also imagine functors between those subcategories
<DrSyzygy> cmccann: _proper_ subcategories?
<DrSyzygy> cmccann: Oh wait .. yeah, even a trivial functor adds a constructor wrapping, so I guess it's prudent to talk about proper subcategories for Functor instances.
<DrSyzygy> cmccann: As opposed to actual endofunctors.
<tomprince> DrSyzygy: They are endofunctors, but they just aren't essentially surjective.
<tomprince> Or maybe, not surjective, but potentially essentially surjective.
<cmccann> DrSyzygy, obviously if you squint a bit and look through any newtype wrappers then that's not the case though
<DrSyzygy> cmccann: There are several ways in which actual haskell is not a perfect reification of category theory.
<cmccann> DrSyzygy, that's probably an understatement but yes :]
<DrSyzygy> cmccann: What fascinates me is the extent to which it fails to be more of an understatement than you'd think.
<cmccann> DrSyzygy, it mostly manifests as _|_ undermining properties you'd expect to have, plus things being unclear because anything morphism-like getting flattened down to some sort of function
<cmccann> DrSyzygy, like type for (>>=) vs. its counterpart for a comonad. some of the arrows flip and others don't and it's not clear why unless you step away from Haskell and look at the "real thing"
--------------------------------- End Side Note --------------------------------


<DrSyzygy> hiptobecubic: Any category needs to have a concept of what it means to be a morphism.
<DrSyzygy> hiptobecubic: Morphisms in Hask are haskell function.
<DrSyzygy> hiptobecubic: Morphisms in the category of categories are functors.
<hiptobecubic> Morphisms in hask are definitely functions. Very clear on that.
<hiptobecubic> Morphisms in category of categories are the functors. So *some* functions are also functors, if their source and targets an be called categories?
<DrSyzygy> hiptobecubic: Yeeah.
<hiptobecubic> the Monads, are thus, a category?
<DrSyzygy> weeeeell...
<ion> The kleisli monad is, right?
<hiptobecubic> Which are also a haskell data type, making them objects in Hask?
<DrSyzygy> where we started was the observation that given a monad M, there IS a category associated to it.
<hiptobecubic> "associated to it"?
<DrSyzygy> yes.
<DrSyzygy> The Kleisli category of a monad is a NEW category that uses the monad in its definition.
<DrSyzygy> hiptobecubic: So we can build new categories by just describing objects and morphisms.
<DrSyzygy> and morphisms don't HAVE to be functions. Nor do they have to be the functions you think they are.
<DrSyzygy> So here is a category you can build using a monad M.
<DrSyzygy> Objects are just datatypes.
<hiptobecubic> can you give me an example of a morphism which isn't a function?
<hiptobecubic> in any sense? not in haskell
<DrSyzygy> hiptobecubic: a->b in the poset as a category.
<DrSyzygy> that one isn't a function, it's an ordering relation.
<hiptobecubic> oh
<ion> Ooh, i was thinking of it as a function.
<hiptobecubic> me too
<DrSyzygy> Now a morphism s -> t in the Kleisli category is defined to be a function s -> M t in Hask.
<shergill> DrSyzygy: a->b being defined iff a <= b?
<DrSyzygy> shergill: Yup.
<byorgey> shergill: composition in that category just corresponds to the transitivity law.
<cmccann> looking at a monoid as a single-object category is instructive here I think
<DrSyzygy> cmccann: To disabuse people of the morphism=function idea?
<cmccann> where the arrows are actually the "values" and the monoid operation is composition
<DrSyzygy> Okay. So pause in the kleisli exposition.
<DrSyzygy> hiptobecubic: You know what a monoid is?
<hiptobecubic> DrSyzygy, yes
<DrSyzygy> So a monoid gives rise to a category.
<DrSyzygy> This category has one "virtual" object.
<DrSyzygy> Call it o
<DrSyzygy> And the set of all morphisms o->o is exactly the set of elements in the monoid.
<hiptobecubic> why is it virtual?
<DrSyzygy> hiptobecubic: Because it doesn't play any role other than placeholder.
<DrSyzygy> hiptobecubic: All the action is among the morphisms.
<DrSyzygy> the identity morphism is the identity element of the monoid.
<DrSyzygy> and the composition of morphisms is given by the operation in the monoid.
<hiptobecubic> So if we take the monoid of integers with addition
<DrSyzygy> there is a morphism called 3 and another one called 5.
<ion> o → o is a natural number?
<DrSyzygy> Well...
<hiptobecubic> an integer
<DrSyzygy> each natural number is an o->o.
<hiptobecubic> how is 3 a morphism?
<DrSyzygy> hiptobecubic: You said we would consider the monoid of integers.
<ion> It satisfies the laws. (3 . 4) . 5 = 3 . (4 . 5) and 3 . id = id . 3 = 3
<DrSyzygy> hiptobecubic: I said that if we have a monoid, it makes a category with just one object, and where the morphisms are just the elements of the monoid.
<DrSyzygy> hiptobecubic: So 3 is a morphism o->o because each monoid element becomes a morphism o->o.
<DrSyzygy> hiptobecubic: And we need for composition to be defined.
<DrSyzygy> You said monoid under addition; so 3 . 4 is going to be 7, and (3.4).5 is going to be 12.
<DrSyzygy> similarily 3.(4.5) = 12.
<hiptobecubic> DrSyzygy, ok yes. You did say that. But this example suggests that i'm not following it. For some reason I expected (+) to be the morphism. I guess that doesn't work though, as it's binary
<hiptobecubic> ohhhh wait
<DrSyzygy> cmccann: :-P
<hiptobecubic> the composition of morphisms is the binary relation
<DrSyzygy> hiptobecubic: Exactly!!
<hiptobecubic> oh wow
<DrSyzygy> :-)
<hiptobecubic> OK
<cmccann> hm, would something like "\x -> Endo (mappend x)" amount to explicitly constructing this view of monoids in Haskell?
<DrSyzygy> hiptobecubic: So you understand how monoid-as-category works?
<DrSyzygy> cmccann: Possibly.
<hiptobecubic> DrSyzygy, i think so. The elements of the monoid are actually morphisms in the category, with composition defined as the binary operator
<DrSyzygy> exactly
<DrSyzygy> and here we see how morphisms need not have ANYTHING to do with functions.
<hiptobecubic> so lists ARE a category :D
<DrSyzygy> sure.
<hiptobecubic> well "the lists"
<hiptobecubic> the actual lists are morphisms
<hiptobecubic> with composition being (++)
<DrSyzygy> yup
<hiptobecubic> ok
<DrSyzygy> Now to kleisli, shall we?
<hiptobecubic> Lets
<DrSyzygy> So, given a monad M in Hask, we can construct a new category entirely.
<ion> Btw, can you encode this as an instance of Category any way? You’d have to pass * -> * to something that wants * -> * -> *, saying the two parameters are the same. :-P
<DrSyzygy> ion: Probably...
<DrSyzygy> Kleisli(M) has as objects datatypes in Haskell.
<DrSyzygy> But a morphism from s to t in Kleisli(M) is a function s -> M t
<DrSyzygy> and function composition works by g . f = join . fmap g . f
<hiptobecubic> DrSyzygy, a monad M in Hask is also a data type, yes?
<DrSyzygy> hiptobecubic: No. A monad M is a functor equipped with extra structure.
<hiptobecubic> DrSyzygy, ah ok.
<DrSyzygy> hiptobecubic: In particular, a functor M is a monad if it has 1. return :: t -> M t, 2. join :: M M t -> M t
<DrSyzygy> such that these things obey laws that are VERY similar to the monoid laws.
<DrSyzygy> THIS is what people mean when they say "monoid in category of endofunctors" btw.
<DrSyzygy> So now you can verify that in this definition of composition we get
all the things we need -- composition is associative. composition with identity is as if you hadn't done anything.
<DrSyzygy> oh btw. id in Kleisli(M) is the same as return for M.
<hiptobecubic> DrSyzygy, return maps from Hask to M, right?
<DrSyzygy> yup.
<DrSyzygy> Weeelll, return is a natural transformation from Id to M.
<hiptobecubic> oh wait
<hiptobecubic> what?
<DrSyzygy> So _functors_ with fixed source and target also form a category.
<DrSyzygy> And a morphism from F to G in this category is a collection of morphisms that transform any F s -> F t in to an G s -> G t in a good way.
<hiptobecubic> There are functors that don't have a fixed source and target? I thought functors were morphisms in the category of categories? And morphisms were inherently associated with a source and target?
<DrSyzygy> hiptobecubic: Nono, but any pair of functors don't have to have the same sources and targets.
<DrSyzygy> But if we consider ALL functors from C to D, then this collection forms a category.
<hiptobecubic> Oh you mean many different functors, each of which happening to have the same source objects and target objects?
<DrSyzygy> yes
<hiptobecubic> for which source and target are not necessarily the same object
<Saizan> source and target categories (objects of Cat)
<DrSyzygy> yup
<hiptobecubic> If we back track for a moment
<hiptobecubic> 3 was a morphism with source and target 'o'
<hiptobecubic> what *is* 'o' there?
<DrSyzygy> yeah
<DrSyzygy> hiptobecubic: Just a symbol.
<hiptobecubic> 3 is a morphism with source '' and target ''? where the source and target are just irrelevant?
<byorgey> o was the name we happened to pick for the single object in the monoid category
<DrSyzygy> hiptobecubic: Not entirely irrelevant. source and target has to be the same thing.
<hiptobecubic> yes
<hiptobecubic> ok
<hiptobecubic> But there's only one thing
<DrSyzygy> sure
<hiptobecubic> ok
<hiptobecubic> So back to functors from C to D
<DrSyzygy> Right.
<DrSyzygy> Let F and G both be functors from C to D.
<ion> How is the set of all functors from C to D a category? How do you compose f :: C -> D and g :: C -> D?
<ion> How do you get id :: C -> D?
<DrSyzygy> ion: That's what I'll tell you about.
<ion> :-)
<DrSyzygy> Now the OBJECTS are functors C -> D. The MORPHISMS are an entirely new thing that I'll tell you about now.
<ion> ah
<DrSyzygy> A _natural transformation_ from F to G is a collection of morphisms in D.
<DrSyzygy> Namely, for any object s in C, there is a resulting morphism F s -> G s.
<hiptobecubic> i need a pencil and paper
<DrSyzygy> And for any morphism s -> t in C we require that if we first go F s -> G s and then go G s -> G t, or first F s -> F t and then F t -> G t, the resulting map F s -> G t should always be the same both ways.
<Aune> DrSyzygy, Am I understanding this correctly? Hask is a category where the types {Int, Bool, Char} are objects and the functions {a -> b, Bool -> [Int] } are the morphisms. But arent some things both objects and morphisms, IE the arguments to {(Bool -> Int) -> (Int -> Char) -> Char}? Does this have any implications or do we just choose to view the object (a -> b) and the morphism (a -> b) as different entities?
<DrSyzygy> Aune: Yes, in Haskell there is an _internal hom_, i.e. morphisms are members of objects.
<DrSyzygy> Aune: And this is a particularly pleasant thing when it happens in a category.
<hiptobecubic> so we have a category that is made of morphisms from category C to category D
<DrSyzygy> hiptobecubic: Yup.
<Aune> DrSyzygy, havent seen any of that in my book, do you have a link to something about that?
<hiptobecubic> and that means that the morphisms are now objets
<DrSyzygy> Aune: I write a bit about it in my lecture notes. http://www.haskell.org/haskellwiki/User:Michiexile/MATH198
<DrSyzygy> hiptobecubic: Yup.
<quintessence> hiptobecubic: there's an object corresponding to the collection of morphisms between two given objects.  So there's an object (type) Int -> Int, but not an object corresponding to the individual morphism (+1).
<Aune> Is terminal object the same as bottom in Hask?
<DrSyzygy> Aune: Nooo, usually not, not quite.
<DrSyzygy> Aune: Terminal object is different depending on where you look for it.
<DrSyzygy> Aune: Bottom doesn't fit neatly into the category semantics.
<ion> drsyzygy: Could you give an example of C, D, F, G, s and t? C = Id, D = M for instance?
<ion> Or s = Id, t = M?
<DrSyzygy> ion: Okay. C = Hask, D = Hask, F = Id, G = [].
<DrSyzygy> s = Int, t = Bool.
<ion> Thanks
<DrSyzygy> So a natural transformation F -> G is a collection of maps s -> [s] and such that these commute with the fmaps.
<hiptobecubic> DrSyzygy, F = id?
<DrSyzygy> F = Id. The identity endomorphism.
<DrSyzygy> Now, here's one neat thing about a natural transformation:
<DrSyzygy> it's what gives us polymorphism in Haskell.
<hiptobecubic> we're looking at it as a morphism from C to D?
<DrSyzygy> as a morphism from F to G.
<hiptobecubic> Id is a morphism from Id to [] ?
<DrSyzygy> nooo, Id is a functor Hask -> Hask.
<DrSyzygy> And return is a morphism from Id to [].
<hiptobecubic> from Id to M ?
<DrSyzygy> Yup.
<ion> f :: Id Int -> Id Bool, g :: Id Bool -> [] Bool, g . f :: Id Int -> [] Bool
<hiptobecubic> so is F id in Klielsi(m) or is it the id in Hask?
<ion> f :: Id Int -> [] Int, g :: [] Int -> [] Bool, g . f :: Id Int -> [] Bool
<DrSyzygy> hiptobecubic: All of this is in Hask.
<DrSyzygy> hiptobecubic: Kleisli is of surprisingly little use in mainstream haskell
<DrSyzygy> though the way the Monad class is usually presented uses the Kleisli idea to get from join :: M M t -> M t to bind :: (t -> M t) -> M t -> M t
<ion> > (permutations <=< subsequences) "hai"
<lambdabot>   ["","h","a","ha","ah","i","hi","ih","ai","ia","hai","ahi","iah","aih","iha"...
<DrSyzygy> http://www.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf << uses the natural transformation property of polymorphic functions to do all sorts of awesome things.
<Aune> Is  unit  "()" a terminal object in Hask, any morphism (a -> ()) ought to be competely isomorphic to (const ())? Also, is there any initial objects in Hask. Seems to me there shouldnt be.
<tgeeky_> DrSyzygy: so what is:  (C,D) = Hask, F= id X id, G= [[]], S=Int with the same statement?
<DrSyzygy> Aune: sounds about right I think...
<DrSyzygy> tgeeky_: So your F t = (t,t) ?
<DrSyzygy> And your G t = [[t]] ?
<byorgey> Aune: if you don't pay attention to _|_ then () is a terminal object  and   data Void   is an initial object.  But _|_ complicates matters.
<byorgey> Aune: for example, there could actually be many morphisms  (a -> ()) depending on how much of 'a' is forced to be evaluated
<byorgey> Aune: and you can tell the difference when a contains _|_.
<tgeeky_> DrSyzygy: I didn't define it, because you didn't use t anywhere?
<DrSyzygy> ....
<DrSyzygy> so your F s = (s,s) and your G s = [[s]] ?
<DrSyzygy> tgeeky_: Then a natural transformation F -> G is a polymorphic function f :: (s,s) -> [[s]]
<tgeeky_> DrSyzygy: is this the stuff covered in Wadlers paper?
<DrSyzygy> tgeeky_: To some extent. Might be hidden in type theory language.
<singpolyma> Is there a good resource on the difference between a Monoid and a MonadPlus ?
<hiptobecubic> So a natural transformation is a morphism in the category of functors-with-identical-types?
<rostayob> the best book is Acowley right?
<byorgey> rostayob: hahaha, I think you mean Awodey
<DrSyzygy> rostayob: Awesome
<DrSyzygy> rostayob: I'd like to think that my draft does a decent job. ;-)
<DrSyzygy> rostayob: But yeah, Awodey is a really nice book. A bit logic-and-maths-heavy.
<ion> Do you mean <http://www.haskell.org/haskellwiki/User:Michiexile/MATH198> by your draft? I didn’t read it yet.
<DrSyzygy> ion: I'm considering making a book out of that.
<Aune> byorgey, Ok, if f :: a -> () forces the evaluation of its argument then the result will not be () but _|_ in the case where the argument evaluates to bottom. But if we restrict oursefls to Hask*, the 'subcategory' of Hask not including _|_, then it is () is terminal.
<Aune> In this case, why is Void initial?
<hiptobecubic> DrSyzygy, was my last statement correct?
<hiptobecubic> "So a natural transformation is a morphism in the category of functors-with-identical-types?"
<DrSyzygy> hiptobecubic: Yup.
<byorgey> Aune: oh, hmm, I guess you're right about Void
<DrSyzygy> Also, a natural transformation between endofunctors of Hask is a polymorphic function.
<byorgey> Aune: an imaginary Haskell-without-bottom might be expected to have a primitive  Void -> a
<byorgey> Aune: but it doesn't
<rostayob> DrSyzygy: I have some background in type theory (I'm almost done with understanding "type theory for functional programmers") and I'd like a book that relates the two
<DrSyzygy> rostayob: Then pierce might be worth looking at.
<shergill> DrSyzygy: your lecture notes present a nice overview (i just made my way through the first lecture). thanks for putting them up!
<hiptobecubic> DrSyzygy, is this analogy correct?  Hask : Cat :: Function : Functor?
<DrSyzygy> hiptobecubic: Sure.
<ion> drsyzygy: Thanks for your time, i’ll be sure to read your lecture notes.
<hiptobecubic> DrSyzygy, ok i'm off for tonight. Thanks so much for this talk. Category theory is a lot more interesting than I had imagined
<hiptobecubic> "3 is a morphism" really woke me up.
<DrSyzygy> ion, hiptobecubic: thanks for your interest and attention.
<Aune> Mathematical functors have the law: F(g∘f) = F(g) ∘ F(f), how does this translate into haskell? This more reminds me more of applicative than functor. pure(f∘g) = pure(f) <*> pure(g)...
<ion> aune: fmap (g . f) = fmap g . fmap f
<cmccann> Aune, also, pure f <*> x = fmap f x
<cmccann> so the Applicative part is more about saying that pure behaves appropriately with respect to the functor law
<cmccann> also, you're probably thinking of something like (.) <$> pure f <*> pure g
<cmccann> Aune, the F is both the type constructor and fmap
<hiptobecubic> DrSyzygy, categories require morphisms with composability and an identity?
<DrSyzygy> hiptobecubic: yup.