# Nominal subtyping in ΠΣ-calculus / Contravariant casts considered harmful

ΠΣ-calculus by T. Altenkirch et al. is dependently typed Turing-complete extension of lambda calculus which is intended serve as a core language for various rich dependently typed languages such as Agda and Coq.

Since ΠΣ-calculus contains enumeration types, it's quite natural to define nominal subtyping relation on some of the types representable in ΠΣ. In general, a type A is called nominally smaller than B if any valid term of type A is also a valid term of type B without any change.

Enumeration type A = {l} is subtype of enumeration type B iff it contains only labels contained in B:
A <: B.
Obviously, we can apply x: A everywhere we can apply x: B which is the main property of subtyping.

Nominal subtyping relation easily generalizes covariantly to (dependent) function types:
(x: T) -> A(x) <: (x: T) -> B(x) iff A(x) <: B(x) for all x:T.
and (dependent) tuple types:
(x: A) * G(x) <: (x: B) * H(x), iff A <: B and G(x) <: H(x) for all x: A.
For example the type {'a, 'b} * {'c, 'd} has the following nominal subtypes:
{'a, 'b} * {'c, 'd}, {'a} * {'c}, {'a} * {'d}, {'b} * {'c}, {'b} * {'d},
{'a} * {'c, 'd}, {'b} * {'c, 'd}, {'a, 'b} * {'c}, {'a, 'b} * {'d}.

A lot more illustrative example is the recursive type
Nat = {'zero | 'succ} * {'zero => 'unit, 'succ => Rec [Nat]}.
It obviously has the has the nominal subtype
Zero = {'zero} * {'unit}
containing only zero. We could also introduce rules for recursion elaboration which would allow subtypes containing all number singletons (e.g. One = {'Succ} * Zero) and typelevel-definable natural number sequences (e.g. PositiveNat = {succ'} * Nat). Desirability of recursion elaboration rules is however questionable since it immediately renders the subtyping relation nondecidable.

Implicit contravariant casts considered harmful

It's true that if A <: B then functions f: B -> T can be narrowed and used anywhere where g: A -> T is accepted,
i.e. (B -> T) is a subtype of (A -> T) in structural sense; but not in nominal sense: Inhabitants of function types are defined using lambda expressions with specified type of the range. Some programming languages (e.g. Scala) perform narrowing implicitly which leads to very unintuitive behavior and should be considered design failure. Consider for example the functions
f : {'a} -> {'x, 'y}
f = {'a => 'x}
g : {'a, 'b} -> {'x, 'y}
g = {'a => 'x, 'b => 'y}
and expression
isEqual f g
which compares the functions. In a language without implicit narrowing it would produce a typechecking error since the values to compare have different types. In a language with implicit narrowing, the function g would be restricted to the domain {'a} and the result would be true despite the fact that f and g are actually different.

The renowned inability of Scala to warn the programmer about wrong usage of the "contains" method in
List(1,2,3) contains ((n:Int) => n > 0)
also trace to implicit narrowing.
• #### Towards Univalent Construction Calculus

Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning. By “modern”…

• #### (no subject)

Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

• #### Прогресс

Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

• Post a new comment

#### Error

default userpic

When you submit the form an invisible reCAPTCHA check will be performed.