Pinned toot

🎉 My thesis is officially submitted! 🎉 (this will be my tweet thread lmao)

🎉 My thesis is officially submitted! 🎉

Sized Dependent Types via Extensional Type Theory: http://hdl.handle.net/2429/82209

I syntactically model Sizey ᴍᴄType Theory (STT) with higher-rank, bounded sizes in an extensional CIC (CIC🄔). A little more detail in 🧵 0/5

If you're familiar with sized types in Agda, there's 2 big features:

- Higher-rank quantification (e.g. (∀α. τ) → σ) so you can pass around size-preserving functions
- Bounded quantification (e.g. ∀α < s. τ) to make pattern-matching work and to avoid "semicontinuity" reqs 1/5

These two in particular are important bc a bunch of past work have one or the other (or neither, like our preprint on CIC^{*)} but not both! So one of the goals of STT is to be a foundation for sized dependent types with both features and good metatheory, i.e. consistency 2/5

Proven w/ a syntactic model into CIC🄔: If well-typed STT terms translate to CIC🄔 terms with the translated type, then consistency of CIC🄔 implies that of STT

A neat thing is that fixpoints are well-founded induction on sizes bc they use bounded sizes

(Slide from SRC talk) 3/5

Since ∞ < ∞ isn't wf, I exclude ∞ from STT (that's what makes Agda's sized types inconsistent)

I talk a little about problems with that and failed solution attempts (some of it in my earlier blog post https://ionathan.ch/2021/08/04/sized-types.html)

So replacing ∞ is still an open problem 👀 4/5

But to conclude:

✅ Sizey ᴍᴄType Theory

✅ higher-rank and bounded sizes

✅ logical consistency

✅ syntactic model of sized dependent types works!

❌ ∞ bad. but ∞ useful... 5/5

Pinned toot

One day I'll figure out how ppl are quantifying the "power" of theories (or was it logics?) by assigning ordinals to them. Ordinal analysis or whatever

Okay maybe that's not a great example bc I think the way ppl were proving that was to define ordinals lol. Which are a set theory thing

He'll casually drop things like "the more universes you have the more endofunctions on naturals you have" and I'm like WHAT. how do you even BEGIN to prove something like that. and then not understand a single reply in the thread

Type theory has a lot of structure to it but disappointingly doesn't seem to have the same kind of semantic content as other branches of math without appealing to those branches. Except for those diagonal arguments which look like sleight of hand tricks, and every single tweet Martin Escardo makes about type theory that I don't understand

Every single "counterexample" in type theory that produces an inconsistency always does so via some other mathematical concept. Hurken's paradox is about set-theoretical universes and powersets. Berardi's paradox is about retracts which I think is some sort of topology thing. My proof using unrestricted large elimination of ordinals uses ordinals which is a set theory thing. Non-strictly positive types with impredicativity uses an injection from a powerset to itself which is a set theory thing. Then every other contradiction arises from a sort of diagonalization argument which I presume generalizes across all such instances but idk what the connection is, only that they all kind of look the same and have a sort of clever diagonal trick to them

You can't really define an eliminator for Fix f can you

From an f (Fix f) there isn't really an interior Fix f you can apply to your predicate? idek what the type would be

Somehow learned about recursors and eliminators seperately after foldr foldl and never made the connection lmaooo

I mean, a dependent recursion scheme that would then allow me to express an eliminator

Wait do dependent folds exist?

`cata: forall P. (forall x. (fpx: f (P x)) -> P (In (? x fpx))) -> (x: Fix f) -> P x`

but there's no f (Fix f) to stick into In, only f (P x) and (Fix f)

How do you express a dependent elimination principle using a recursion scheme bc I'm having trouble adding a dependency for the return type on the element of Fix itself

Like it's supposed to look like

`cata: forall P. (f (P ?) -> P ?) -> (x: Fix f) -> P x`

I imagine you'd need to fold it up once somewhere

Do you think paramorphisms deserve their own nLab page? I don't think they deserve their own page. It can be seen as a "generalization" of catamorphisms but it doesn't really count since you can literally implement a paramorphism using a catamorphism so there isn't really any extra expressivity

Now a histomorphism is different bc it's genuinely more expressive, and anamorphisms need their own page so that the eventual page on hylomorphisms can link to the two

Admin

Jon(athan)? | ionchy ("YON-tchy") 🏳️🌈

MSc ⇒ PhD student in PL doing type theory things

@ionathanch on most places 🐦

PoGo: 8336 6654 0984

#WaterDrinker 💧

emoji boy of types.pl

I have been blessed with admin powers on this instance and I will do my best not to muck things up

pfp: https://picrew.me/share?cd=6rKy0AQ4I3

header: https://doi.org/10.1145/2578855.2537850

Joined Oct 2020