5 ms·
> eventually you realize this is the ultimate abstraction (category theory), and it cannot go more abstract than that This is exactly the kind of false sense o
by j2kun 9y ago
> eventually you realize this is the ultimate abstraction (category theory), and it cannot go more abstract than that
This is exactly the kind of false sense of intellectual superiority to avoid. Mathematicians and category theorists don't talk like this. Even the parts of Haskell that have the flavor of category theory aren't really all that much like category theory.
- proc0 9y agoMaybe you can expand on that, and/or show me something more abstract than category theory. Programming = abstracting information processing. Category theory = the mathematics of abstract functions (or morphisms a.k.a. changing something)... so it makes sense that CT captures something very fundamental about computation.
- Koshkin 9y agoTechnically, category theory is not more abstract than the rest of (abstract) algebra.
- proc0 9y agoYou can derive all other math branches with CT, so yes, it is more abstract. It is "higher level" (in the same sense of programming languages) than other maths.
- fyi1183 9y agoPlease point out where somebody genuinely puts an effort to found math on category theory? The standard way to do so is set theory, and the more recent hype is type theory. Category theory in itself is pretty useless. Categories are a bit like graphs in that: they are too general. There are serious mathematical theories using category theory as their language (mostly commutative algebra and whatever it touches) just as there are serious theories using the language of graphs, but in both cases the meat of the math is not in the underlying language.
- mbid 9y agoThere are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the properties of sets in terms of the "is element" relation, you can give first order axioms for how the morphisms and objects of an elementary topos behave. Then you may add more axioms to assert that the elementary topos you're talking about is really a category of sets in the sense of ZFC. If you want to research more about this, I can recommend sheaves in geometry and logic by Maclane and Moerdijk. You can also search for "algebraic set theory" and go from there. And btw, type theory is essentially the same thing. The axioms are IMO uglier and more ad-hoc, but there are (some proven, some conjectured) equivalence results.
- scentoni 9y agohttps://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
- lmm 9y agoThat is a) a great project b) not category theory.
- infty 9y ago>Please point out where somebody genuinely puts an effort to found math on category theory? What about the following: https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM Even if the meat of the math is not in the categorical aspects of a theory, the categorical input can be useful - if nothing else, then as a convenient language.
- dsacco 9y agoNo, you can’t. The vast majority of analysis cannot usefully be represented in category theory. You can’t express everything in analysis using morphisms and maps. When you’re working with structures (algebra, geometry, topology, etc), sure, you can construct them in the language of categories. But that’s very far from “all of math”.
- Retra 9y agoYou can derive all other math from any Turing complete system. Category theory is no more powerful than that.
- tathougies 9y agoGiven that turing complete systems are not total, you can actually derive anything, including falsehood, from them. The point being that a general 'turing complete' system is about as useful to use as the basis of mathematics as a banana. Category theory is not a great basis for mathematics, but at least it's not inconsistent.
- FridgeSeal 9y agoCT exists at the same level as some other "fundamental level" fields of maths like topology and abstract algebra (/algerbraic topology). It's certainly very abstract and fundamental, but it's definitely not the root field.
- madmax96 9y agoYou can't derive CT with CT. Though that has nothing to do with your point, just suggesting that we aren't there yet.
- Eire_Banshee 9y agoYou are missing his entire point.
- proc0 9y agoI know, which is why I asked for some clarification. I actually think haskell is able to directly implement CT, there is HASK category after all. If it's that this is too pretentious to even mention in HN, then I'm completely lost.
- jonnybgood 9y agoHask is not a real category.
- dragonwriter 9y ago> there is HASK category after all. This is disputed and seems to be at best conjecture/intuition without adequate formal definition supporting it.
- j2kun 9y ago1. Just because we have not thought of something more abstract does not mean category theory is the "ultimate" abstraction that cannot be surpassed. You would have said the same thing about sets before category theory was invented. 100% guaranteed there will be another, more abstract paradigm when the need arises. 2. Just because one thing captures something fundamental about computation does not mean it captures everything fundamental about computation, nor does it mean nothing else can capture fundamental aspects of computation (disjoint from what may or may not be captured by category theory). For example, category theory does a terrible job representing the mathematical subfield of complexity theory, despite it being entirely about computation. For that matter, "how abstract" is not always comparable, and the intellectual dick measuring of what is the most abstract is counterproductive. Even basic questions in particle physics have no known model in mathematics that doesn't break under gentle prodding, so is particle physics more abstract than mathematics? 3. Haskell does a lousy job representing the majority of ideas that make category theory useful to mathematicians. For example, universal properties are neglected Haskell, and at best they're implicit. Nobody actually thinks about the math when they're writing Haskell programs, they just think about Haskell types and programs, which makes the "techniques and patterns" of Haskell programming just as arbitrary as the conventions in random Javascript libraries. It's just that there are fewer names for the same thing because fewer people write serious programs in Haskell.
- dsacco 9y ago> Haskell does a lousy job representing the majority of ideas that make category theory useful to mathematicians. For example, universal properties are neglected Haskell, and at best they're implicit. Nobody actually thinks about the math when they're writing Haskell programs, they just think about Haskell types and programs, which makes the "techniques and patterns" of Haskell programming just as arbitrary as the conventions in random Javascript libraries. It's just that there are fewer names for the same thing because fewer people write serious programs in Haskell. That’s an excellent point. So many people think they’re doing category theory when they’re writing Haskell, but Haskell is essentially nothing like the mathematics it borrows terminology from. They’re really not comparable. Which is absolutely fine, but then people shouldn’t draw parallels to the actual mathematics when the terminology is similar in name only.
- runT1ME 9y ago>Even the parts of Haskell that have the flavor of category theory aren't really all that much like category theory. Can you expound on this? Just because the type classes defined in Haskell can't represent a wider range of categorical structures they purport to capture, does not mean that more structure doesn't exist throughout a Haskell code base. For instance, many argue that the only type of functors used in Haskell are endofunctors, but thats not really true unless we have a narrow definition of 'functors used in haskell', no?
- tome 9y agoThe typeclass Functor represents endofunctors from * to *. That's a pretty limited notion of "functor" when considered mathematically but also extremely useful for programming!