10
votes
Accepted
What subtyping rules does Agda support?
The current subtyping rules that Agda uses are for sized types (when --sized-types is enabled) and cumulativity (when ...
- 506
8
votes
Formal description of algorithmic subtyping/cumulativity
See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.
- 11.1k
8
votes
Accepted
What's the benefit of having pi and sigma types with an invariant parameter?
There are subtleties here, when type annotations are present, depending in quite a brittle way on where they must be placed. (I'm half-remembering conversations about this with Zhaohui Luo.) Suppose ...
- 771
5
votes
Accepted
Formal description of algorithmic subtyping/cumulativity
For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ...
- 6,028
4
votes
Accepted
Why inductive types (or variants) are so rigid in terms of the set of constructors
There are two components to your question.
The first, corresponds to the idea of constructor subtyping (actually, non-empty lists are the first example of the paper). I don't think there are any hard ...
- 6,028
4
votes
What's the benefit of having pi and sigma types with an invariant parameter?
As pointed out in the comments already, even if you do allow for cumulativity (in one direction or the other) in your domain type, you do not need to record the two types in your context: only the ...
- 6,028
Only top scored, non community-wiki answers of a minimum length are eligible