jonsterling
commented
6 years ago As an update, I have experimented with this idea and I think it may be immortal. The only difficult thing (which is already an issue) is that we really need to make the implementation of subtyping in the unifier behave the same as whatever implementation we have for the core language. This is currently a source of confusing mismatches, and in the context of the new proposed algorithm, it gets even worse.
It's worth noting that the new subtyping algorithm must be mutually recursive with the type checking algorithm. This means in turn that the unifier must implement its own type checker, which will be a bit of a pain.
What would be very cool is if we could somehow implement it abstractly once, and then instantiate it for the core language and then for the unifier. the main difference would be that it would be filling holes as it goes.
I think I can design a monad that would suffice, but I'll need to think about it.
So far we have needed some kind of fancy subtyping rules for restriction and extension types (which I majorly bungled before)---and I was thinking that there may be a better way to do things that doesn't require such fancy rules.
There are a lot of places that the fancy subtyping algorithm can't see that something is a subtype, but where if we eta expand some code, we can see it. This happens a lot with extension types, which is why in the corrected version (which is now merged), the examples have a lot of eta-expanded things.
This makes me think about two things:
We should somehow change our type checking and subtyping algorithm so that somehow subtyping only fires at atomic and positive types (specifically, the universe). All the other cases should somehow be explained through eta expansion; what this means is that we should somehow return an eta-expanded value from
infer, and then check this against the negative type. When doing the mode switch at positive type, we would have to compare the types structurally, and then when we hit a negative type, we would again do this eta thing with a generic element.The current rules mean that eta contraction is not sound; but eta contraction is definitely needed in the unifier in order to invert a spine. So it seems like it is of the essence to come up with typing relation which makes eta contraction sound, and the thing I suggested above would probably suffice.
As a high-level philosophical point, I think that even though polarity doesn't seem play a great role in MLTT (there are not enough effects to observe differences in evaluation order, rule invertibility, etc.), polarity is actually of the essence regardless.
This reminds me of how when I was trying to come up with a theory of proof refinement for systems, it worked perfectly for negative types and was essentially impossible for positive types. It tells me that we need to think a bit about what positive types really mean in martin-lof type theories.