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

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

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

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

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 "Sounds rough buddy"

@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"

@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

@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

@ionchy Why is being nondeterministic an issue?

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

@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

@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

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

@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

@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

@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

@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

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

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

@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

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

@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

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

@ionchy Then you get Agda I guess

@vdash Agda has mu types???

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

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

@ionchy Oh lmao

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

@ionchy Subtyping just kind of happens as a consequence, so the judgements are redundant. I feel they are elucidating tho