Questions tagged [subtyping]
Use this tag for polymorphism that restrict the range of types that can be used in a particular case.
4
questions
14
votes
2
answers
123
views
Formal description of algorithmic subtyping/cumulativity
Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the ...
- 906
9
votes
2
answers
289
views
What's the benefit of having pi and sigma types with an invariant parameter?
Ulf Norell wrote this in his PhD thesis (figure 1.6):
This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda ...
- 5,877
5
votes
1
answer
343
views
What subtyping rules does Agda support?
Andrea Vezzosi said Cubical Agda made cubical subtyping coercion-based (inS and outS) because it's a bad idea to introduce more ...
- 5,877
0
votes
1
answer
132
views
Why inductive types (or variants) are so rigid in terms of the set of constructors
An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined.
For instance:
...
- 125