4 ms·

I had a limited interest in exploring type theories for their own sake some time ago but it receded when I was unable to resolve, or find a resolution to, a con

I had a limited interest in exploring type theories for their own sake some time ago but it receded when I was unable to resolve, or find a resolution to, a conceptual problem that seems extremely foundational. Each type theory has a hierarchy of types: 1-types, 2-types, 3.1*10^62-types, etc. but some niche type theories allow for types indexed by transfinite ordinals: ω-types, ω+5-types, I even found a construction of a theory that supports φ_α-types. There is apparently at least one very counterintuitive type theory where the hierarchy of indexable types provably continues past the proof-theoretic ordinal of the theory, somehow, but I haven't seen it myself. These have real implications of what kinds of proofs you can do with a given type theory. . The problem is deciding which of these theories to permit, or possibly even deciding how to decide which theories to permit, if you'll pardon the pun. I decided to give it up and get back to PDEs.

turminal 3y ago
I think this is on some level very much like deciding which programming language to use. It really depends on what problems you're trying to solve and there isn't a single one that is the best. The difference is that type theories are much less of a "solved" problem and a lot of the variations are subject to ongoing research. As a consequence we're still at the stage where we're trying to figure out the "deciding how to decide", as opposed to programming languages, where decision criteria are relatively well understood.
deleted 3y ago
[deleted]
armchairhacker 3y ago
Reminds me of "rzk: an experimental proof assistant for synthetic ∞-categories" (https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#fn:1 https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction...) and the ∞-categories paper (https://arxiv.org/abs/1705.07442 https://arxiv.org/abs/1705.07442)

turminal 3y ago

I think this is on some level very much like deciding which programming language to use. It really depends on what problems you're trying to solve and there isn't a single one that is the best. The difference is that type theories are much less of a "solved" problem and a lot of the variations are subject to ongoing research. As a consequence we're still at the stage where we're trying to figure out the "deciding how to decide", as opposed to programming languages, where decision criteria are relatively well understood.

deleted 3y ago

[deleted]

armchairhacker 3y ago

Reminds me of "rzk: an experimental proof assistant for synthetic ∞-categories" (https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#fn:1 https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction...) and the ∞-categories paper (https://arxiv.org/abs/1705.07442 https://arxiv.org/abs/1705.07442)