Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

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.
Subscribe

  • (no subject)

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

  • Прогресс

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

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 16 comments

  • (no subject)

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

  • Прогресс

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

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…