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: ...
Tiago Campos's user avatar
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 ...
ice1000's user avatar
  • 5,972
5 votes
1 answer
364 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 ...
ice1000's user avatar
  • 5,972
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 ...
ionchy's user avatar
  • 1,026