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

Applied Category Theory Course

math.ucr.edu

Post reply on HN
Print view View original

81–90 of 100 posts

Re: Applied Category Theory Course

#81

Post by getpost »

mikhailfranco wrote: post #78

Surely Baez's even in American English (yeah, I know it's a Spanish name). British English almost always adds 's for the singular possessive, even when the name ends in s, so Dickens's and St. James's. However, American English often uses the plural possessive suffix ' for names ending in s. One Spanish name example I have seen is Bezos' for something of Jeff's (his billions, or his wives, I forget which). But Baez'…

Made me look it up: https://www.merriam-webster.com/grammar/what-happens-to-name...

Re: Applied Category Theory Course

#82

Post by [deleted] »

mikhailfranco wrote: post #78

Surely Baez's even in American English (yeah, I know it's a Spanish name). British English almost always adds 's for the singular possessive, even when the name ends in s, so Dickens's and St. James's. However, American English often uses the plural possessive suffix ' for names ending in s. One Spanish name example I have seen is Bezos' for something of Jeff's (his billions, or his wives, I forget which). But Baez'…

[deleted]

Re: Applied Category Theory Course

#83

Post by catgary »

shanusmagnus wrote: post #74
catgary wrote: post #66

Earlier quoted context omitted.

So, just to offer a few counterpoints there is Tom Leinster’s work on diversity/entropy [1], where people working in mathematical ecology have been happy with his contributions. I’ve also see the Penn robotics group start to use categorical machinery to nail down concepts like bisimulation of dynamical systems and develop a ‘type theory’ for motion plans that has its semantics in a category of dynamical systems [2].…

Semi-related: I read the first page of your second reference and really can't make any sense of it, despite having what I would have thought to be enough knowledge to at least orient: "We aim to construct a physically-grounded compositional framework for hybrid system synthesis, particularly targeted at applications in robotics. Compositionality lies at the heart of language in general [WHM12] and its formalization u…

It’s basically just saying notions of compositionality from software doesn’t really translate over to analogue computers, and by extension robots that interact with their environment. It seems like they’re being careful to make atomic statements that are supported by the individual papers they’re citing. They may have been dealing with some particularly obstinate reviewers and adopted a defensive writing style (it can be a tough habit to kick, I’ve definitely given overly precise seminar talks because someone brought up size issues the week before and I just didn’t want to deal with any pedantry).

Re: Applied Category Theory Course

#84

Post by _a_a_a_ »

mikhailfranco wrote: post #78

Surely Baez's even in American English (yeah, I know it's a Spanish name). British English almost always adds 's for the singular possessive, even when the name ends in s, so Dickens's and St. James's. However, American English often uses the plural possessive suffix ' for names ending in s. One Spanish name example I have seen is Bezos' for something of Jeff's (his billions, or his wives, I forget which). But Baez'…

It's fine & I've used that. Given a name (say Jones) then the possessive is with a "'s" suffix (Jones's) but for by convention you can elide the final "s" to avoid duplication (so: Jones'). I'm happy that can be done with a "z", hence Baez' is fine.

Re: Applied Category Theory Course

#86

Post by mjburgess »

almostdeadguy wrote: post #77
mjburgess wrote: post #28

Earlier quoted context omitted.

Programming is also applied physics. But understanding the kinetic forces behind typing is no guide to improved programming. To say that learning a field is useful is to say that knowing these abstractions is useful. Much of Haskell's "category theory" is a reuse of terms. Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". This says littl…

> Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". I'm not sure an "Appendable" Int or IO type, or a "Runnable" / "Composable" List type is any less confusing to Joe Programmer. These descriptions do not articulate the same things implied by the Monoid, Functor, and Monad laws. Some of these aren't even correct (i.e. not all Functors ar…

I take it all Functors are runnable if you see (1) map as generalised function application and (2) functors as lifted map.

The concepts, at the level of abstraction i just use there, are confusing. Thinking this abstractly about programs actively impairs programming in many cases.

This level of 'unification of syntax via abstraction' is relevant only really to language designers.

Re: Applied Category Theory Course

#87

Post by nextaccountic »

j2kun wrote: post #56
JHonaker wrote: post #49

Earlier quoted context omitted.

It really depends on what your idea of applied is, but Conal Elliot's work is really interesting. His paper on Compiling to Categories [1] pitches programming language semantics as a cartesian closed category [2] allows for really cool stuff by mapping typical evaluation semantics to alternatives like building a computational graph visualization, a pretty printer, and imbuing the original program with automatic diffe…

This does not appear to pass the criterion I gave: > used by someone in a production software setting to solve a problem not related to category theory If this stuff or its derivative work is used in production in a mainstream compiler (GHC, perhaps?), then I would see it differently.

there was a startup that used this to compile functional programs into circuits

not sure if it went anywhere, but it even included self modifying fpga-like circuits iirc

Re: Applied Category Theory Course

#88

Post by umutisik »

j2kun wrote: post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

This agrees with my experience when I was a young mathematician looking for math that is useful.

Re: Applied Category Theory Course

#89

Post by amboo7 »

j2kun wrote: post #58
tutfbhuf wrote: post #23

Earlier quoted context omitted.

> And when I talk to people who are actually on the front lines that try to use category theory to solve some problem, they tell me that it ended up being completely useless. I'm open to having my mind changed. I aim to provide an example of applied category theory in computer science. Your understanding may differ due to the encompassing time frame, however, I ensure that even the most recent findings can rapidly tr…

I understand those concepts well, but I find the casual chain of events questionable, especially when the story is told by category theorists. For example, I was once told by a prominent category theorist that certain aspects of the API design for C++ futures was informed by category theory. When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. This is what i…

I would appreciate if someone wrote here their opinion on Matriarch [1], an application of category theory to biology/physics via software.

[1] https://web.mit.edu/matriarch/

Re: Applied Category Theory Course

#90

Post by j2kun »

tutfbhuf wrote: post #65
j2kun wrote: post #58

Earlier quoted context omitted.

I understand those concepts well, but I find the casual chain of events questionable, especially when the story is told by category theorists. For example, I was once told by a prominent category theorist that certain aspects of the API design for C++ futures was informed by category theory. When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. This is what i…

> ... but I find the casual chain of events questionable ... When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. I think you missed one level of indirection in my argument. I'm not claiming that language designers employ Category Theory explicitly when designing new language features (although this is indeed the case with Haskell, PureScript, and similar la…

> Often, they refer to programming language tutorials where these mathematical ideas are already implemented, for example, in Python or C++.

The difference is that _someone_ is actually implementing the features they're relying on, and those people know the math, understand its importance, and deliberately apply it. I know because I dig through their git commits so I can interview them about their work for my book.

Your argument puts a lot of faith in Haskell. Let me take one path in your example to make this concrete. Rust was influenced by Haskell, how specifically? [1] claims it was mainly in "typeclasses, type families." Picking one randomly, the GHC user guide [2] describes type families as originating from three specific papers, [3], [4], [5], none of which mention category theory (nor does the much longer Haskell Wiki [6]). It seems to suggest, what is obvious to me, that not _all_ features of Haskell are related to category theory.

If every time I trace claims of applied CT I find big holes, how could I possibly believe that so many great ideas that programmers use every day are secretly deliberately based on CT?

There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no. Math is a modeling language and if nobody models their problems with it then theorems do nothing. And so, if all of the category theory is lost in the translation from some (perhaps itself far removed) language feature of Haskell and later inspired language design, then that tells me category theory is the _wrong_ modeling language for that design problem. If it were good, and if the resulting theorems were essential and useful, then the practitioners would adopt it. That is a failure of CT.

[1]: https://doc.rust-lang.org/reference/influences.html [2]: https://downloads.haskell.org/ghc/latest/docs/users_guide/ex... [3]: https://www.microsoft.com/en-us/research/wp-content/uploads/... [4]: https://www.microsoft.com/en-us/research/wp-content/uploads/... [5]: https://www.microsoft.com/en-us/research/wp-content/uploads/... [6]: https://wiki.haskell.org/GHC/Type_families

Post reply on HN