Why is it worth spending time on type theory? (2013)
7 comments
·August 4, 2025fellowniusmonk
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
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
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?
ttoinou
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
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.
null
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.