Higher-order subtyping for dependent types

Andreas Abel

Institut für Informatik
Ludwig-Maximilians-Universität München

Thursday, 24 November 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: 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 numbers below n. In our type system, Fin 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 types +(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 x itself. We alleviate this problem by requiring x to be irrelevant for the shape of B(x). Formally, our type system is justified by an erasure semantics.

Tarmo Uustalu
Last update 29.11.2011