Does syntax need to be finite?

The set of syntactically allowable terms I mean. I don't think so. There's an infinite number of variables at my disposal, presumably

Does syntax need to be countably infinite?

Hmm. I am going to hard code every countable ordinal directly in my syntax of sizes

Don't need an uncountably infinite size if your syntax has an uncountably infinite number of terms

I will demand that every programmer learn about all the ordinals before even touching a Code

It's hopeless

Bold of me to try to pair up everything with a size when there are an uncountably infinite number of things

This is why they use set theory for everything. They've got ridiculous things like "the (first limit ordinal)th uncountable ordinal" and other nonsense

The thing is that only relative size changes matter, not absolute size, but the relative size difference between a concrete construction and its base case is the absolute size

If only there were some way of looking out for changes in relative size.. to prevent recursion on things that were too big... to guard against such things so to speak...

Time to prove a fire triangle theorem for sized typing but it's a... well with two points it's a line
A firewalk, so to speak

Theorem: No sufficiently expressive dependent type theory can have enough sizes.

Sufficiently expressive: higher-order sizes, general inductive types
Enough sizes: uncountably infinite? or a upper "closure" size where inf < inf? smth like that
Oh the third side of the triangle is consistency. But people usually assume consistency is desired

I just remembered that sizes aren't part of my terms, maybe that's the missing piece (ew)

I forgot the title of that gradual typing paper so I looked up "death of gradual types" and that very much did not give me what I was looking for

The Next 700 Type System Deaths

If sizes are part of the terms there's no hope in automatically checking that less-than relation
Then you'd have to provide all the proofs yourself
Which defeats the purpose of having a sized typing system because you can literally just index your CIC inductives with a measure

• consistency
• decidable size checking
• enough sizes
• expressivity

fire pyramid (vertices)

I wonder how Agda does it
I guess if it can't deduce that a size is less than another it complains and you have to somehow shove in a term that proves it

Okay so I guess making sizes sufficiently first class, and then doing some constraint solving for some sizes

So the terms aren't always fully annotated with sizes. But also the terms aren't always devoid of sizes... there are just some holes where sizes should be... and sometimes the holes can be filled in... and sometimes they remain holes that need to be filled in...