Questions tagged [subtyping]

Use this tag for polymorphism that restrict the range of types that can be used in a particular case.

Filter by
Sorted by
Tagged with
0 votes
1 answer
147 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: ...
9 votes
2 answers
298 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 votes
1 answer
365 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 ...
14 votes
2 answers
124 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 ...