[HN Gopher] Why is it worth spending time on type theory? (2013)
___________________________________________________________________
Why is it worth spending time on type theory? (2013)
Author : mindcrime
Score : 66 points
Date : 2025-08-04 16:46 UTC (2 days ago)
(HTM) web link (math.stackexchange.com)
(TXT) w3m dump (math.stackexchange.com)
| ttoinou wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Legal means mostly and yeah indeed networks effects are the
| biggest obstacle.
| fellowniusmonk wrote:
| 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 wrote:
| 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.
| benrutter wrote:
| 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?
| voxl wrote:
| 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.
| doppelgunner wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| This is the type of snark that's HN appropriate.
| AnimalMuppet wrote:
| 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 wrote:
| 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 wrote:
| 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).
| lovich wrote:
| 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
| JonChesterfield wrote:
| 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).
| louthy wrote:
| 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).
|
| [1]
| https://youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa...
|
| [2] https://github.com/hmemcpy/milewski-ctfp-pdf
| joe_the_user wrote:
| 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).
|
| [1] https://mathoverflow.net/questions/8731/categorical-
| foundati...
| auggierose wrote:
| It is not worth spending time on type theory. It is quite
| meaningless, literally.
| js8 wrote:
| 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.
| labrador wrote:
| 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 wrote:
| 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.
___________________________________________________________________
(page generated 2025-08-06 23:00 UTC)