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: 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 ionathan.ch/2021/08/04/sized-t)
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

✨ 𝓲𝓽 𝓲𝓼 𝓪𝓵𝔀𝓪𝔂𝓼 𝓪𝓵𝓵 𝓽𝓱𝓮 𝓽𝔂𝓹𝓮𝓼 ✨

Pinned toot

"Computers are rocks we tricked into thinking" is entirely incorrect. Computers are rocks we tricked ourselves into believing they could think

I swear it's harder to fall asleep the more important it is that you do

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

Show thread

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

Show thread

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

Show 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

Show thread

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

Show thread

I want a book like Counterexamples in Topology but it's a subject I understand

elim: forall P. (p: (x: f (Fix f)) -> f (P ?) -> P (In x)) -> forall x. P x

? ?

Show thread

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

Show thread

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

Show thread

I mean, a dependent recursion scheme that would then allow me to express an eliminator
Wait do dependent folds exist?

Show thread
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)

Show thread

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

Should I bring my Bachelor's diploma with me lmao
idk what the point would be, I'm gonna get my Master's diploma in the mail

No it'll wash off
I've had sharpie wash off of ceramic before

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.