Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why I am learning category theory

the.scapegoat.dev

Post reply on HN
Print view View original

211–220 of 224 posts

Re: Why I am learning category theory

#211

Post by solomatov »

solomatov wrote: post #75
khazhoux wrote: post #72

As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that. Like, CT describes a set of rules but very little emerges from those rules. My complaint has nothing to do with whether CT is useful or practical. By contras…

> As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that One of the most interesting things in CT are adjoints. They happen literally everywhere. For example, static analysis via abstract interpretation is an exam…

Sine there're a lot of discussion in this tread. My opinion about category theory and programming is:

- You don't need category theory to be a programmer (or good or 10x or 100x programmer)

- It makes sense to learn category theory because its beautiful like it makes sense to study arts, literature or philosophy. Not because it useful, but because it gives you pleasure.

Re: Why I am learning category theory

#212

Post by ukj »

charcircuit wrote: post #184
larve wrote: post #177

Earlier quoted context omitted.

I'm not sure if this is supposed to be sarcastic, but taking it at face value, mathematics are the underpinning of both computer hardware and computer science. Since we are talking about more abstract mathematics, it is what gave us the lambda calculus, complexity analysis of algorithms, type theory, relational algebra, distributed systems. more pragmatically, libraries like redux, react are heavily influenced by con…

>redux, react are heavily influenced by concepts from functional programming Functional programming concepts don't require learning category theory >rust has novel concepts from type theory Type theory isn't category theory. Rust's borrow checker was not inspired by affine types. https://smallcultfollowing.com/babysteps//blog/2012/02/15/re... >data engineering in the cloud age leverages a lot of algebraic concepts to…

>Functional programming concepts don't require learning category theory

This is such a reductionist world-view. Programming concepts don't require you to learn the theory of computation either, but having a theoretical/abstract grounding for what computation is disconnected from any particular programming language/model of computation helps. A lot.

>Type theory isn't category theory

It depends on what you mean by "isn't".

There is a 1:1 correspondence between type theory and category theory constructs.

https://ncatlab.org/nlab/show/computational+trilogy#rosetta_...

Re: Why I am learning category theory

#213

Post by btilly »

zozbot234 wrote: post #193
Tainnor wrote: post #162

Earlier quoted context omitted.

> I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen…

You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfect…

In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.)

As for choice, try doing much functional analysis without Zorn's lemma.

There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.

Re: Why I am learning category theory

#214

Post by wisnesky »

zasdffaa wrote: post #203
wisnesky wrote: post #197

Earlier quoted context omitted.

Bi-directional data exchange has many uses. For example, given a set of conjunctive queries Q, because coeval_Q is left adjoint to eval_Q, the composition coeval_Q o eval_Q forms a monad, whose unit can be used to quantify the extent to which the original query Q is "information preserving" on a particular source (so query/data quality). As another example, we use the technique to load data into OWL ontologies from S…

Can you point to some examples of owl/sql transforms being flipped? I have trouble believing that an invertible transformation is hard (presumably each step is invertible, right), and certainly "never would have been able to discover" seems inconceivable to me. Looking at the paper it is very dense and abstract, also 50 pages long. Edit: on reflection I am doing a bit of sealioning which was not my intention but it d…

You might try pages 8-16 of this presentation: https://www.categoricaldata.net/cql/lambdaconf.pdf . The examples are relational to relational and simplistic but they do illustrate running the same transformation both forward and backward, as well as show the "unit" of such a "monad". We implemented everything in public software, so hopefully the software is even better than my word! As for loading SQL to RDF specifically, I'd be happy to share that technique, but it isn't public yet- please ping me at ryan@conexus.com.

Re: Why I am learning category theory

#215

Post by MockObject »

wisnesky wrote: post #197
charcircuit wrote: post #133

Earlier quoted context omitted.

So what is coevaluation and why is it useful? Please don't just point at the paper again.

Bi-directional data exchange has many uses. For example, given a set of conjunctive queries Q, because coeval_Q is left adjoint to eval_Q, the composition coeval_Q o eval_Q forms a monad, whose unit can be used to quantify the extent to which the original query Q is "information preserving" on a particular source (so query/data quality). As another example, we use the technique to load data into OWL ontologies from S…

Could this possibly be explained to the average programmer, who doesn't have the foggiest notion what conjunctive queries, coevaluation, or monads are?

Re: Why I am learning category theory

#216

Post by Karrot_Kream »

Koshkin wrote: post #167
SleekEagle wrote: post #158

Earlier quoted context omitted.

> It's a common observation that many mathematicians and maths students tend to fall into either the algebraic or the analytic camp (we don't talk about the topologists)

Aren’t all topologists algebraic topologists today?

No way? It's a pretty even split between analysts and algebraists from what I can tell. Really depends on what you're researching. Only the internet and online CS-adjacent communities have these crazy algebra-dominated communities.

Re: Why I am learning category theory

#218

Post by zozbot234 »

btilly wrote: post #213
zozbot234 wrote: post #193

Earlier quoted context omitted.

You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfect…

In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.) As for choice, try doing much functional analysis without Zorn's lemma. There are parts of math that you can do constructively. But most of it you really can't. And choice…

> In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is.

Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.

Re: Why I am learning category theory

#219

Post by Tainnor »

zozbot234 wrote: post #218
btilly wrote: post #213

Earlier quoted context omitted.

In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.) As for choice, try doing much functional analysis without Zorn's lemma. There are parts of math that you can do constructively. But most of it you really can't. And choice…

> In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is. Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsens…

That's why for me, constructivism - or in general mathematics with different axioms - are additions to classical mathematics, not replacements. And in that sense, they're fine for me. You'll definitely find people online defending the position that all classical maths is bullshit - I'm not saying that actual researchers behave like that, though.

But I'm also a strict formalist, or more accurately, I think whichever axioms happen to be useful should be used, without much need for there to be a epistemological commitment.

Re: Why I am learning category theory

#220

Post by z5h »

yakshaving_jgt wrote: post #23
nnoitra wrote: post #4

Will it make you a better React dev tho?

I think the best way to become a better React developer is to learn Elm, and then build your React apps the same way Elm would have forced you to.

I gave an Elm talk years ago at the shared office space I used to work at. A few devs there later told me the talk helped them better understand React.
Post reply on HN