Live data from Hacker News

What Is Applied Category Theory? (2018)

arxiv.org

41–50 of 71 posts

Re: What Is Applied Category Theory? (2018)

#41

Just a nice set of ideas to be used for social signalling. In with type systems, a typeclass is all you need. The mantra is "to be an X (being substituted for an X) is to be able to perform (implement) such and such actions (or have this or that biochemical properties). It is that general, that deep, it could be even seen in molecular biology. Category theory, on the other hand, is just a few nested abstract concepts…

Every type theory gives a categorical logic [0]. Category theory is all about describing the structures which definitely exist around mathematical objects even if we don't acknowledge them very often. This isn't social signalling; I'm not posting under my real name and I'm not trying to get accolades. This is mathematics; we teach it to each other.

[0] https://mikeshulman.github.io/catlog/catlog.pdf

Re: What Is Applied Category Theory? (2018)

#42
post #10

I've never actually gotten around to diving into this topic before, but every time one of Tai-Danae Bradley's publications pops up I am awed by how much care she puts into crafting these from the layout to the illustrations

I think she's using the LaTeX package for Edward Tufte's style:

https://edwardtufte.github.io/

(If you like the design, you'd like Tufte's books.) Anyway, her paper is fun to read and one of the most beautiful papers I've read in terms of layout and design - I like the contrast between the hand-drawn illustrations and the abstract content. It reminds me of Lin Clark's Code Cartoons (https://code-cartoons.com/) .

Re: What Is Applied Category Theory? (2018)

#44

Earlier quoted context omitted.

Not addressing your question, but the Yoneda Lemma is kind of a charlatan. On first reading, it seems magical and deep, but once you grok the proof, it feels like a relatively trivial observation. The whole thing is just about arrow composition! In a way, once you're on the other side, the Yoneda Lemma feels a bit like a checkpoint during the accimatization period where your brain gets used to thinking in categories…

"On first reading, it seems magical and deep, but once you grok the proof, it feels like a relatively trivial observation. The whole thing is just about ____ composition!" I think if you replace _____ with the right word almost every result I've seen in my (albeit somewhat limited) exposure to category theory can be described this way. (not that that detracts from your answer!)

Well yeah, because category theory studies composition. That's what it's for. That's why a category is defined the way it is: a bunch of objects, identity arrows from each to itself, and arrows between them, which enjoy an associative composition operator.

Re: What Is Applied Category Theory? (2018)

#45

Category Theory is one of those things which I know are important and has applications in many engineering fields. I also have an intuition that its obviously because things need to flow into each other and composability is how we achieve that. But man, whenever I try to get into this I feel like someone is hitting me on the head with equations.

Maybe for a value of "has applications" that doesn't necessarily include anyone actually applying it. As a generalisation, I don't think anyone by people into category theory actually cares about or applies category theory.

I'm applying it.

Re: What Is Applied Category Theory? (2018)

#46
post #16

Earlier quoted context omitted.

Not addressing your question, but the Yoneda Lemma is kind of a charlatan. On first reading, it seems magical and deep, but once you grok the proof, it feels like a relatively trivial observation. The whole thing is just about arrow composition! In a way, once you're on the other side, the Yoneda Lemma feels a bit like a checkpoint during the accimatization period where your brain gets used to thinking in categories…

> The whole thing is just about arrow composition! There's much much more to it. For example, a version of the yoneda lemma also holds for metric spaces (instead of a set of arrows between to things, you simply have a number indicating a distance between two things). Here's how I like to think about the yoneda lemma: If you have some kind of objects you want to talk about, one way to do this is by relating these obje…

That almost describes discourse about politics and social issues, too.

Re: What Is Applied Category Theory? (2018)

#47

Earlier quoted context omitted.

Maybe for a value of "has applications" that doesn't necessarily include anyone actually applying it. As a generalisation, I don't think anyone by people into category theory actually cares about or applies category theory.

Shouldn't it be easier to explain a general concept than a specific one? The only reason I can think of why this isn't happening is because you need to learn a large amount of information before any of the category theory stuff can be applied in real life. But honestly speaking, that can't be true because languages like Haskell exist and isn't that on the whole programming using category theory? (I am be completely w…

> languages like Haskell exist and isn't that on the whole programming using category theory?

It's not. However claims like that get thrown around a fair amount so the confusion is understandable.

That said, some important Haskell abstractions were designed using category theory. So it can be helpful to know some of the lingo (since it will show up in abstraction names and descriptions).

And if you're looking to design the next breakthrough Haskell abstraction it might be extremely helpful, but that's not 99% of programmers. However, the people who can do that are super cool, eg https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors....

Re: What Is Applied Category Theory? (2018)

#48

Earlier quoted context omitted.

Maybe for a value of "has applications" that doesn't necessarily include anyone actually applying it. As a generalisation, I don't think anyone by people into category theory actually cares about or applies category theory.

Shouldn't it be easier to explain a general concept than a specific one? The only reason I can think of why this isn't happening is because you need to learn a large amount of information before any of the category theory stuff can be applied in real life. But honestly speaking, that can't be true because languages like Haskell exist and isn't that on the whole programming using category theory? (I am be completely w…

> Shouldn't it be easier to explain a general concept than a specific one?

It depends. Are you an abstract or a concrete thinker? That's one axis of one the standard ways of describing personalities. (Yeah, I know, psychology... but it does seem to describe an actual difference in how people think.)

Now, people with one kind of personality can learn to think in the other way, but they won't find it as easy.

Re: What Is Applied Category Theory? (2018)

#49

In re: CT see also Conal Elliott's "Compiling to categories" http://conal.net/papers/compiling-to-categories/ Also, "concatinative" languages like Joy. https://en.wikipedia.org/wiki/Joy_(programming_language)

FWIW, here's an example of a simple programming task in Joy, the derivation of the step combinator. It might not make a lot of sense without familiarity with Joy, however, the thing to notice is the smooth algebraic form of programming. Making simple obvious decisions at each point leads to a concise and correct program. That's "the function-level programming style of John Backus's FP." in action. You can do it in Haskell (et. al.) too but I find it much easier in Joy. YMMV.

The step combinator accepts a list and a quoted program and runs the program on each item in the list in turn. (Use it to write e.g. sum of list of ints, etc.)

     [] [P] step
  -----------------  Empty list, no-op.


     [X|Xs] [P] step
  -----------------------  Non-empty list, run P and recur.
     X P [Xs] [P] step

 In terms of branch and x:

   step == [F] x

 So:

   [L] [P] step
   ------------------
   [L] [P] [F] x
   ------------------
   [L] [P] [F] F

 First, get the flag value and roll

Re: What Is Applied Category Theory? (2018)

#50

Earlier quoted context omitted.

Not addressing your question, but the Yoneda Lemma is kind of a charlatan. On first reading, it seems magical and deep, but once you grok the proof, it feels like a relatively trivial observation. The whole thing is just about arrow composition! In a way, once you're on the other side, the Yoneda Lemma feels a bit like a checkpoint during the accimatization period where your brain gets used to thinking in categories…

Yoneda just says that we may exchange an object for all of the arrows which point to (dually, from) it. This is extremely deep; it is rather surprising that objects and arrows would have such a duality or exchange!

+1. The lemma is trivial not because the result isn't deep but because we have the right definitions.
Post reply on HN