5 ms·

Sometimes, wondering if your type is an example of some particular abstraction can reveal unexpected useful operations, when you fill in the gaps. For example,

Sometimes, wondering if your type is an example of some particular abstraction can reveal unexpected useful operations, when you fill in the gaps. For example, there's a Haskell library that defines a type called "Fold a b" [1]. It's basically a little state machine which you feed values of type "a" until you close it and then it returns an output of type "b". Turns out these Folds are examples of an abstraction called a "Comonad". This basically means that there is a function > extract:: Fold a b -> b That runs a fold without giving it any input, and a function > duplicate :: Fold a b -> Fold a (Fold a b) That turns a Fold that takes as and returns b into a Fold that takes as and returns another Fold that takes as and returns b. But what on earth could this be useful for? Turns out that "duplicate" lets you keep a Fold "open" when you pass it to functions that run the Fold and only return its result (say, a function that feeds the Fold with values read from a file). If you pass a "duplicated Fold" to such functions, you will get another Fold as result that you can keep feeding. The Applicative instance is even more useful: it lets you combine two Folds into one so that their results can be calculated in a single run. This kind of useful discovery doesn't always happen, though. Sometimes the new functions turn out to be useless, or too inefficient. [1] http://hackage.haskell.org/package/foldl-1.2.1/docs/Control-Foldl.html#t:Fold http://hackage.haskell.org/package/foldl-1.2.1/docs/Control-...

conistonwater 10y ago
I, for one, think that Fold's documentation can be seriously improved by describing its behaviour in terms of code, rather than category theory. All I'm saying is that when even you describe a Fold, you do so in terms of non-category-theory terms, and that nothing is added by category theory itself. This is much the same way lenses have some kind of category-theoretic interpretation, but exactly the same level of understanding can be achieved by thinking about them in terms of code. And if there's no difference, that means category theory is essentially unnecessary. I also want to say that I don't believe Fold was discovered from category theory, it seems to me more like a neat generalization of foldl, and then once they had an idea, they asked questions like "is this a comonad?". Indeed, it's far easier to me to figure out what's going on by reading http://hackage.haskell.org/package/foldl-1.2.1/docs/src/Control-Foldl.html http://hackage.haskell.org/package/foldl-1.2.1/docs/src/Cont... to see the Applicative instance itself.
- lomnakkus 10y ago
  Honestly, it just requires a certain familiarity with the general concepts. Once it's internalized you'll often be thinking in terms of the abstractions themselves. E.g. "If I can make my <domain-object-X> into a <Monoid/whatever>, I can apply <all-these-laws>!" type thing. For a concrete example, I've been doing this in an (unreleased) game to just regularize all the special cases of "effects" (poison, slowness, etc.) affecting the player. Bundling it all up into an Effect data type and defining a Monoid for it means that I don't have to care at all when or how they get applied, whether they have a timer, etc. > and that nothing is added by category theory itself In some sense you're right. CT is really just a systematic way of describing patterns. Theoretically we could just prove loads of special cases and never have to resort to CT to prove anything... but it sure helps when you can just invoke the Yoneda Lemma for some special case that you're working with rather than going through the whole process of re-proving the Yoneda Lemma for the umteenth time. (Btw, this isn't specific to CT. It's just that math-level specification/proof basically always tends towards generalization... for really good reasons.) EDIT: I should say that I'm not yet close to the level where I can say that a "Monad is just a monoid in the category of endofunctors". I'm still just a muggle in this whole CT thing and yet it's even helping me!

conistonwater 10y ago

I, for one, think that Fold's documentation can be seriously improved by describing its behaviour in terms of code, rather than category theory. All I'm saying is that when even you describe a Fold, you do so in terms of non-category-theory terms, and that nothing is added by category theory itself. This is much the same way lenses have some kind of category-theoretic interpretation, but exactly the same level of understanding can be achieved by thinking about them in terms of code. And if there's no difference, that means category theory is essentially unnecessary. I also want to say that I don't believe Fold was discovered from category theory, it seems to me more like a neat generalization of foldl, and then once they had an idea, they asked questions like "is this a comonad?". Indeed, it's far easier to me to figure out what's going on by reading http://hackage.haskell.org/package/foldl-1.2.1/docs/src/Control-Foldl.html http://hackage.haskell.org/package/foldl-1.2.1/docs/src/Cont... to see the Applicative instance itself.

lomnakkus 10y ago
Honestly, it just requires a certain familiarity with the general concepts. Once it's internalized you'll often be thinking in terms of the abstractions themselves. E.g. "If I can make my <domain-object-X> into a <Monoid/whatever>, I can apply <all-these-laws>!" type thing. For a concrete example, I've been doing this in an (unreleased) game to just regularize all the special cases of "effects" (poison, slowness, etc.) affecting the player. Bundling it all up into an Effect data type and defining a Monoid for it means that I don't have to care at all when or how they get applied, whether they have a timer, etc. > and that nothing is added by category theory itself In some sense you're right. CT is really just a systematic way of describing patterns. Theoretically we could just prove loads of special cases and never have to resort to CT to prove anything... but it sure helps when you can just invoke the Yoneda Lemma for some special case that you're working with rather than going through the whole process of re-proving the Yoneda Lemma for the umteenth time. (Btw, this isn't specific to CT. It's just that math-level specification/proof basically always tends towards generalization... for really good reasons.) EDIT: I should say that I'm not yet close to the level where I can say that a "Monad is just a monoid in the category of endofunctors". I'm still just a muggle in this whole CT thing and yet it's even helping me!