A dependently typed calculus with polymorphic subtyping

摘要

A polymorphic subtyping relation, which relates more general types to more specific ones, is at the core of many modern functional languages. As those languages start moving towards dependently typed programming a natural question is how can polymorphic subtyping be adapted to such settings. This paper presents the dependent implicitly polymorphic calculus (λ_I~(A)): a simple depen-dently typed calculus with polymorphic subtyping. The subtyping relation in λ_I~(A) generalizes the well-known polymorphic subtyping relation by Odersky and Laeufer (1996). Because λ_I~(A) is dependently typed, integrating subtyping in the calculus is non-trivial. To overcome many of the issues arising from integrating subtyping with dependent types, the calculus employs unified subtyping, which is a technique that unifies typing and subtyping into a single relation. Moreover, λ_I~(A) employs explicit casts instead of a conversion rule, allowing unrestricted recursion to be naturally supported. We prove various non-trivial results, including type soundness and transitivity of unified subtyping. Λ_I~(A) and all corresponding proofs are mechanized in the Coq theorem prover.