{size-annotated types, untyped reduction, subject reduction} really is a game of "pick two", huh

Follow

Size annotations breaking subject reduction, size arguments requiring shape irrelevance, subtyping depending on size polarities
These are all related phenomena but I can't see what the underlying cause it but I can feel it

Here is the problem
I will tell you the problem

Just gotta ramble don't even worry about it 

Suppose you had explicit size application
Let f be the identity function on Nats, and let x: Nats
Then (f s x) is well-typed
But by subtyping, x: Nats+1 is perfectly valid (and it should be, or else we get problems like being unable to define pred)
So (f (s+1) x) is also well-typed
But these terms, despite reducing to the same thing, are not equal
The NbE for sized dependent types paper fixes this by allowing you to arbitrarily indicate when an argument should be shape-irrelevant
I don't like this because it feels too arbitrary

Suppose instead you did not have explicit size application but you did have explicit size abstractions
Now the problem is that typing is nondeterministic due to needing to solve size variables, but reduction tries to be deterministic even though you wouldn't know what the size variables you need to substitute in are yet
So the Sacchini stuff solves this by erasing size annotations
I think
I lost my train of thought in the middle of this post

re: Just gotta ramble don't even worry about it 

Plot twist: I do need size application or else I can't let-bind sized types (which is something I realized originally and then somehow convinced myself I was wrong about even though I was actually right)
And the NbE paper was right after all I do need size irrelevance via shape irrelevance annotations I can't believe it

re: Just gotta ramble don't even worry about it 

The proof would go through if Agda ignored sizes where they act as type argument, i.e., in constructors and term-level function applications, but not in types where they act as regular argument, e.g. in Nat i.

hmmm

re: Just gotta ramble don't even worry about it 

If I want size annotations and therefore size abstractions then I need either typed reduction or size applications. If I want size applications then I need shape irrelevance. It's all there is to it, these are all things I knew before

ramble pt. 2 

I was thinking about making my fixpoints recursive only in the first argument but then I realized that I can't do that because the first argument's type might have indices that change as I recur
Dependent types keep breaking things hrmph

re: ramble pt. 2 

Not having some available some number of arguments before your recursive argument breaks even a simple recursion on dependent vectors because its length index varies
You could enforce that all the arguments before the recursive one are "forced" from the type of the recursive argument but that sounds hard and pointless

re: ramble pt. 2 

It's ugly. Inductive types are ugly. If I had time and knew that they would compile well I would look into mu types, but I'm not convinced they would compile well
Also they seem to require yet another form of subtyping, and with universe and size subtyping I think I've had enough of it

@ionchy Size polarities sounds like subtyping to me

@ionchy Like to me that sounds like "subtyping depending on subtyping"

@vdash if only subtyping didn't depend on subtyping and could simply subtype without subtyping

Just gotta ramble don't even worry about it 

@ionchy Oh I see what's going on. I have no soln for you but it reminds me of... lots of things actually

Just gotta ramble don't even worry about it 

@ionchy "Sounds rough buddy"

Just gotta ramble don't even worry about it 

@vdash I know right??? There's a few couple different problems that all feel like they're related and they probably are but I don't know how and all of the existing solutions feel like approximations or "I pretend I do not see it"

Just gotta ramble don't even worry about it 

@ionchy I think this is like one of those ancient problems which just keeps coming back in different forms. Things are irrelevant but also, they are relevant

Just gotta ramble don't even worry about it 

@vdash I don't like it very much. Someone else should've solved it ages ago in a way that I can deem to be elegant and aesthetic

Just gotta ramble don't even worry about it 

@ionchy Why is being nondeterministic an issue?

Just gotta ramble don't even worry about it 

@ionchy Like why not allow nondeterministic reduction (at compile time)

Just gotta ramble don't even worry about it 

@vdash How would, like, a closed term reduce to a value then though
I guess you'd have two different reductions
But like... there's still those size abstractions and it's the type that determines what sizes should be applied but reduction isn't typed
Reduction would work as a relation instead of a computation (or, like, an equality I guess) but ultimately I still need it to run to smth
I... think? I mean... these are programs... idk brain no work

Just gotta ramble don't even worry about it 

@ionchy Well the size is irrelevant to reduction at runtime right? So if this nondeterminism is "irrelevant" in the sense that whichever way it reduces you get the same result, then like in terms of meaning it seems like it would be fine

Just gotta ramble don't even worry about it 

@ionchy Unless sizes are relevant to reduction, in which case nondeterministic reduction sounds like a bad idea

Just gotta ramble don't even worry about it 

@vdash well it's like
nondeterministic in the sense that for typing to go through, the reduction has to magically know what size expressions to apply to the size abstractions
and it does matter because the right sizes have to be applied for the term to be well typed
it really does sound like the size applications should be explicit instead of them being conjured up somehow in the typing derivation lol but like
then you have the first issue I mentioned in the toot lol

Just gotta ramble don't even worry about it 

@vdash idk I feel like I'm running around in circles
we've discussed this so many times like if you do this then you have to have that, if you don't have that then you have to do this, on and on
it's the same things and every time I feel like I can fix it but I can't

Just gotta ramble don't even worry about it 

@vdash like if I have size applications then the problem with terms that should be the same aren't the same. ultimately this is due to subtyping of inductive types with sizes but if you disallow subtyping then you can't define a simple predecessor function for Nats, because in the zero case the type doesn't change while in the succ case the size shrinks, so the shrunk return value has to be cast up a size

Just gotta ramble don't even worry about it 

@vdash come to think of it, I should probably write this down
but actually I think we do already have this written down I'm just revisiting it over and over again

re: ramble pt. 2 

@ionchy Idk about compilation but they don't require subtyping that's just me

re: ramble pt. 2 

@vdash really?? I thought NuPRL needed subtyping to get things right

re: ramble pt. 2 

@ionchy Nuprl does have subtyping but not like explicitly it just kinda happens as a consequence of things being what they are. The μ types do have a monotonicity subgoal which is basically subtyping but strict positivity is a syntactic approximation of this

re: ramble pt. 2 

@ionchy Basically strict positivity is a subtyping thing but unlike monotonicity it is decidable

re: ramble pt. 2 

@ionchy But at the end of the day, if you have any kind of subtyping, then you need to ensure it respects the subtyping which is already present implicitly in the type system even if for whatever reason we prefer to not see it

re: ramble pt. 2 

@vdash Hmm. Don't like invisible subtypings
I would make it explicit, in the hypothetical universe where I was investigating them

re: ramble pt. 2 

@ionchy Then you get Agda I guess

re: ramble pt. 2 

@vdash Agda has mu types???

re: ramble pt. 2 

@ionchy What no. Universes are not cumulative is what I was referring to

re: ramble pt. 2 

@vdash oh
by explicit subtyping I meant, like, there is a judgement for it lol

re: ramble pt. 2 

@vdash I have no idea what an implicit subtyping is but if there is no judgement it doesn't sound good

Show newer
Sign in to participate in the conversation
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.