Because once you understand type theory, you unlock the ability to win arguments on the internet using words like "monoid" and "dependent elimination". Also, it's comforting to know that while your life may lack structure, your types never will.
derriz · 3h ago
I know this is supposed to be a joke but I don’t get it? Type theory isn’t particularly heavy in terms of jargon compared to other foundational theories like category theory or set theory. These are highly technical fields of study so of course they’re going to need specific language. It would like complaining about a doctor using “fancy terms” when discussing complex medical procedures.
To give a non-cynical answer: a good reason to look at type theory - if you’ve been exposed to computer science - is that it treats syntax and syntactical manipulation as foundational and can be viewed as the branch of mathematics that ties syntax and with the notion of computation.
JadeNB · 1h ago
> Type theory isn’t particularly heavy in terms of jargon compared to other foundational theories like category theory or set theory.
And anyone who thinks their own area doesn't have jargon has just forgotten how to recognize it.
ninetyninenine · 1h ago
This is the type of snark that's HN appropriate.
js8 · 1h ago
I think the answer is yes. Modern efforts to formalize mathematics use type theory a lot, specifically calculus of inductive constructions, rather than ZFC.
At around 2000, I studied applied mathematics. I was curious about automated theorem proving, but I didn't understand the language (being, as most mathematicians, trained in proving with classical logic rather than type theory). Years later I discovered Haskell, which became a "gateway drug" to type theory. I wish something like Lean had existed 25 years ago, when I was a student.
I think fully formal methods in mathematics are the future, and every math student should learn a bit of Lean (or a similar tool, but IMHO Lean has the best tutorials, aimed at people with traditional education). Hence, everybody should learn basics of type theory.
fellowniusmonk · 5h ago
As a mereological nihilist I like type theory but I wish it was type and schema theory.
Treating complex types, structure, arrangement, entanglement, etc. as if it has the same realness or priority as primitive types is a mistake.
It's like acting like recursion is physically real (it's not) when it smuggles in the call stack.
nyrikki · 5h ago
Topos theory can be added to type theory to provide a categorical semantics.
But even with Grothendieck topology (total and co-total categories) requires sets with least upper bound (join) and a greatest lower bound (meet).
The problem is that you get semi-algorthms, thus will only halt if true.
IMHO it is better to think of recursion as enabling realizability, and forcing fixed points. The ycombinator can be used for recursion because it is a fixed point combinator.
From descriptive complexity FO+LFP=SO+Krom=P, while FO by itself is AC^0 IIRC?
Using model logic+relations is another path.
The problem I have found is those paths tend to require someone to at least entertain intuitionistic concepts and that is a huge barrier.
Mostly people tend to use type theory to convert symantic properties to trivial symantic properties for convenience.
Blackburn/Rijke/Venema's “Modal Logic” is the most CS friendly book for that if you want to try.
voxl · 2h ago
Yes well we all have our pet theories about the world. Thankfully the people that think the natural numbers aren't "real" or that recursion isn't "real" haven't won out and destroyed our ability to make meaningful progress.
benrutter · 5h ago
I'm curious about what you mean by recursion not being physically real? Do you mean it doesn't convert to CPU instructions, or something around occurence in nature?
labrador · 1h ago
I'm just an old country imperative programmer, not a big city functional programmer, so excuse my ignorance, but I had an ephiphany the other day. Functional programmers with strict types organize their data with complex types, while I do the same with classes. I need to do more research to verify this, but it explains the focus on types in functional languages to me.
js8 · 1h ago
One of the core concepts in type theory is the function type. It's a kind of building block. So perhaps better would be to say functional programmers organize everything using functions.
I suggest you look at simply typed lambda calculus, it gives a basic rationalization of types in functional programming.
ttoinou · 5h ago
OT but is this kind of well researched user content be disappearing with AI content filling the web ? Will some places / forums keep power users interested in spending time researching and answering ? When what they produce will be ingested in future models and not sourced back to them
HappyPanacea · 5h ago
I'm a very small time MSE user but indeed such concerns made me reluctant to answer recently or even participate in general. The CC BY-SA requires both Attribution and ShareAlike which doesn't happen. I expect people will move to private silos of information as much as possible.
ttoinou · 4h ago
Yeah but how do you make sure no robots subscribe to the private silos ?
Also, there's always some kind of minimal size required for spaces to be interesting for people to participate. And networks effects.
HappyPanacea · 3h ago
Legal means mostly and yeah indeed networks effects are the biggest obstacle.
joe_the_user · 4h ago
The OP goes on to immediate ask whether category theory or type theory can serve as a foundation for mathematics (they give a link to an article that talks of "foundational styles" but which doesn't give a process of explicitly "cutting the cord" from set theory).
I think the answer by (perhaps infamous) Paul Taylor in this mathoverflow post[1] is a clearer expression of the positions of those who want to jettison traditional set theory as the foundation of mathematics.
"The crucial issue is whether you are taken in by the Great Set-Theoretic Swindle that mathematics depends on collections (completed infinities)"
Yes, it's important to remember that everything labeled "infinity" in math doesn't "exist-exist" but rather is some combination of unending process and arbitrary labeling (see Skolem's paradox etc). But that doesn't mean such nominally completed infinities aren't useful or even necessary for a human being to grasp mathematics.
Anyway, for this debate it's worth reading all of Taylor's comment (which isn't to say I share his position but it's good to understand where the "finitests" are coming from).
Where does one even start learning type theory or category theory? I’ve had a passing interest from listening in on conversation between Rust friends, but never found a place to do a like type theory 101 for software engineers
louthy · 3h ago
Bartosz Milewski’s Category Theory for Programmers lectures [1] are good. Especially paired with his book [2].
I actually find that category theory is remarkably simple. At least at the level where it applies to day-to-day programming concepts. The one major benefit I got from it, was that it helped me reason about high level/abstract structure better (which helps my architectural designs/thinking).
I watched these https://www.youtube.com/@hottlectures5237, at least up to the point where they seemed to be diverging from things I could see application in. There's an associated book which is fairly tough going but enlightening (easier after watching some of the videos).
AnimalMuppet · 4h ago
Let's say I ask, "Why is it worth spending time in Baltimore?"
I could get answers about the national anthem, about Camden Yards, about good restaurants and bars. Those are "tourist" answers.
Or I could get answers about job availability and cost of housing. Those are "move there" answers.
It seems to me that this article (if you can call it that) gives mostly "tourist" answers, not "move there" answers. Well, that's all right in a way - for an academic topic, you probably have to get tourists before you get people moving there. But the problem is that mathematicians have a large number of areas that they could visit as tourists, and nothing here tells them why type theory is better to visit than, say, algebraic topology.
And that doesn't solve the original complaint. Why are so few people working in type theory? Because more of the action is in set theory and category theory, and type theory offers too little that the others don't, so nobody's going to switch.
I mean, most mathematicians aren't really in foundations anyway. They're in differential equations or prime numbers or complex analysis or algebraic topology or something like that, and making your foundation type theory instead of set theory makes no difference whatsoever to those people. Only the people working on foundations care, and as I said, most of those people already work in set theory or category theory, and type theory doesn't give them a good enough reason to uproot and move.
derriz · 4h ago
I’m not sure Set theory and Type theory compete for the same foundations people.
Type theory’s stomping ground is in the foundations of computation. I’m guessing if you sampled a theoretical comp. sci. audience, I’m pretty sure type theory would “win” the popularity contest.
Somewhat similar to intuitionism and constructivism - interesting to people interested in computability but considered almost silly or at least niche by “mainstream” math theoreticians.
AnimalMuppet · 3h ago
Fair enough, though TFA seemed to be focused on the "foundations of mathematics" angle. If you want to say it's good for foundations of CS... I can probably agree (though the category theory folks may want a word).
auggierose · 2h ago
It is not worth spending time on type theory. It is quite meaningless, literally.
To give a non-cynical answer: a good reason to look at type theory - if you’ve been exposed to computer science - is that it treats syntax and syntactical manipulation as foundational and can be viewed as the branch of mathematics that ties syntax and with the notion of computation.
And anyone who thinks their own area doesn't have jargon has just forgotten how to recognize it.
At around 2000, I studied applied mathematics. I was curious about automated theorem proving, but I didn't understand the language (being, as most mathematicians, trained in proving with classical logic rather than type theory). Years later I discovered Haskell, which became a "gateway drug" to type theory. I wish something like Lean had existed 25 years ago, when I was a student.
I think fully formal methods in mathematics are the future, and every math student should learn a bit of Lean (or a similar tool, but IMHO Lean has the best tutorials, aimed at people with traditional education). Hence, everybody should learn basics of type theory.
Treating complex types, structure, arrangement, entanglement, etc. as if it has the same realness or priority as primitive types is a mistake.
It's like acting like recursion is physically real (it's not) when it smuggles in the call stack.
But even with Grothendieck topology (total and co-total categories) requires sets with least upper bound (join) and a greatest lower bound (meet).
The problem is that you get semi-algorthms, thus will only halt if true.
IMHO it is better to think of recursion as enabling realizability, and forcing fixed points. The ycombinator can be used for recursion because it is a fixed point combinator.
From descriptive complexity FO+LFP=SO+Krom=P, while FO by itself is AC^0 IIRC?
Using model logic+relations is another path.
The problem I have found is those paths tend to require someone to at least entertain intuitionistic concepts and that is a huge barrier.
Mostly people tend to use type theory to convert symantic properties to trivial symantic properties for convenience.
Blackburn/Rijke/Venema's “Modal Logic” is the most CS friendly book for that if you want to try.
I suggest you look at simply typed lambda calculus, it gives a basic rationalization of types in functional programming.
Also, there's always some kind of minimal size required for spaces to be interesting for people to participate. And networks effects.
I think the answer by (perhaps infamous) Paul Taylor in this mathoverflow post[1] is a clearer expression of the positions of those who want to jettison traditional set theory as the foundation of mathematics.
"The crucial issue is whether you are taken in by the Great Set-Theoretic Swindle that mathematics depends on collections (completed infinities)"
Yes, it's important to remember that everything labeled "infinity" in math doesn't "exist-exist" but rather is some combination of unending process and arbitrary labeling (see Skolem's paradox etc). But that doesn't mean such nominally completed infinities aren't useful or even necessary for a human being to grasp mathematics.
Anyway, for this debate it's worth reading all of Taylor's comment (which isn't to say I share his position but it's good to understand where the "finitests" are coming from).
[1] https://mathoverflow.net/questions/8731/categorical-foundati...
No comments yet
I actually find that category theory is remarkably simple. At least at the level where it applies to day-to-day programming concepts. The one major benefit I got from it, was that it helped me reason about high level/abstract structure better (which helps my architectural designs/thinking).
[1] https://youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa...
[2] https://github.com/hmemcpy/milewski-ctfp-pdf
I could get answers about the national anthem, about Camden Yards, about good restaurants and bars. Those are "tourist" answers.
Or I could get answers about job availability and cost of housing. Those are "move there" answers.
It seems to me that this article (if you can call it that) gives mostly "tourist" answers, not "move there" answers. Well, that's all right in a way - for an academic topic, you probably have to get tourists before you get people moving there. But the problem is that mathematicians have a large number of areas that they could visit as tourists, and nothing here tells them why type theory is better to visit than, say, algebraic topology.
And that doesn't solve the original complaint. Why are so few people working in type theory? Because more of the action is in set theory and category theory, and type theory offers too little that the others don't, so nobody's going to switch.
I mean, most mathematicians aren't really in foundations anyway. They're in differential equations or prime numbers or complex analysis or algebraic topology or something like that, and making your foundation type theory instead of set theory makes no difference whatsoever to those people. Only the people working on foundations care, and as I said, most of those people already work in set theory or category theory, and type theory doesn't give them a good enough reason to uproot and move.
Type theory’s stomping ground is in the foundations of computation. I’m guessing if you sampled a theoretical comp. sci. audience, I’m pretty sure type theory would “win” the popularity contest.
Somewhat similar to intuitionism and constructivism - interesting to people interested in computability but considered almost silly or at least niche by “mainstream” math theoreticians.