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...
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...
Gradual types
I'm going to bed
@ionchy Agda does it by giving up and making it an unsafe feature
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.