## September 12th, 2013

### Хроники

Вчера пришёл с работы домой с мыслью "всё завтра", вырубился, врубился (продолбав все будильники) в 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.

### Suspended contexts in ΠΣ-calculus: A handy tool for typeclasses, ornaments and restrictions

ΠΣ-calculus by T. Altenkirch et al. is typed turing-complete calculus of partial functions with an exceptionally rich type structure able to accommodate the type-level structure and computational expressiveness of Martin-Löf-style type-theories and their known extensions. It is intended to serve as a core ("sugar-free") language for various dependently typed languages such as Agda and Coq, which lambda calculus fails short to serve as base for. Being partial, ΠΣ allows for the type of all types Type:Type and treats terms and types on equal footing, it fails, however, to treat contexts as first-class citizens.

)