Хроники

Вчера пришёл с работы домой с мыслью "всё завтра", вырубился, врубился (продолбав все будильники) в 10:22, подпрыгнул на работу, как раз к 10:55 успел (в 11:00 планерка). Ужин и завтрак как-то не успелись, это меня печалит. Всё-тки к доктору.

(no subject)

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

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.