## Higher-order subtyping for dependent types

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