Andreas Abel, Higher-Order Subtyping for Dependent Types
Higher-Order Subtyping for Dependent Types
Dependent type theory allows to assign precise types to expressions, to capture invariants up to total correctness, but sometimes the precision gets in the way. Too rigid types require the programmer to apply conversion functions which obscure the computational content of the program and make it harder to reason about it. Subtyping has been a successful means in object-oriented languages to alleviate rigidity of the type system, and it has been applied in the context of dependent types to coercive subtyping, universe subtyping, sized types, singleton types and refinement types.
In this talk, we enter the uncharted territory of higher-order
subtyping for dependent types. We describe a type system that
distinguishes functions by their variance, e.g., there is a type for
monotone functions. One example is the type
Fin n of natural
n. In our type system,
is a monotone function from natural numbers to sets,
implying that an element of
Fin n is casted to
Fin (n+1) automatically.
A stumbling stone for the formulation of monotone dependent function
+(x:A) -> B(x) is the fact that the codomain
B(x) might not share the variance of the function,
i.e., might not be monotone in
We alleviate this problem by requiring
to be irrelevant for the shape of
Formally, our type system is justified by an erasure semantics.