Iso-type systems : simple dependent type theories for programming

Abstract

Dependent types have been drawing a lot of attention in programming language designs. A key reason is that they allow unifying types and terms that are usually distinct syntactic levels in traditional language designs. Unified syntax brings some interesting advantages over separate syntax, including added expressiveness and less duplication of concepts. However, it is challenging to combine dependent types with common programming features, such as unrestricted general recursion and object-oriented programming (OOP) features including subtype polymorphism and abstract type members. To address these challenges, we propose three novel dependently typed calculi with both simplicity and expressiveness, namely Pure Iso-Type Systems (PITS), the λI≤ calculus and the λIΣ calculus.

PITS is a generic language framework that employs unified syntax, supports general recursion and preserves decidable type checking. It is comparable in simplicity to pure type systems (PTS), and is useful to serve as a foundation for functional languages that stand in-between traditional ML-like languages and full-spectrum dependently typed languages. The key to retain decidable type checking in the presence of general recursion is a generalization of iso-recursive types called iso-types. Iso-types replace the implicit conversion rule typically used in dependently typed calculi and make every computation explicit via cast operators. We study three variants of PITS that differ on the reduction strategy employed by the cast operators and prove type-safety and decidability of type checking for all variants.

The λI≤ calculus is a variant of PITS with unified subtyping, a novel technique that unifies typing and subtyping and enables the combination of dependent types and subtyping. In λI≤, there is only one judgment that is akin to a typed version of subtyping. Both the typing relation, as well as type well-formedness are just special cases of the unified subtyping relation. λI≤ supports essential features for modeling OOP, such as high-order subtyping, bounded quantification and top types. It can fully subsume System F≤ and enjoys several standard and desirable properties, such as type-safety and transitivity of subtyping.

The λIΣ calculus is a variant of λI≤ with strong dependent sums. Strong sums are useful to model Scala-like traits with type members. λIΣ adopts a novel treatment of strong sums called iso-strong sums. The destructors of iso-strong sums are typed using intermediate type-level applications instead of standard direct substitutions. The necessary type-level computation can be done by just call-by-value casts. λIΣ supports impredicativity and enjoys the same desirable properties as λI≤, including type-safety and transitivity.