ornaments-memo

Сабтайпинг как он представлен в замечательной работе <a href="http://lampwww.epfl.ch/~amin/drafts/dissertation_eval.pdf">“Dependent Object Types”, N. Amin</a> касается только (слегка обобщённых) сигма-типов, которые можно рассматривать как индуктивные типы с одним конструктором, как например pair (a : A) (b : B). Вообще говоря этот подход можно расширить для любых индуктивных типов, в результате отношение подтипизации сможет отражать орнаментацию типов.

Подход представленный в вышеописанной работе позволяет выводить утверждение S <: T, когда S получен из T последовательным применением одного из трёх механизмов:
– extending = добавление новых полей
– narrowing = сужение типов существующих полей
– infilling = заполнение части полей значениями (перемещение идентификатора из параметров конструктора в индексы)
Обобщение подхода на индуктивные типы с бОльшим количеством конструкторов добавляет ещё один механизм:
– omission = опускание одного из конструкторов.

Как это работает легче всего описать на примере. Возьмём например тип
  @Family Nat:
    Zero
    Succ (n : Nat)

Тип
  @Family List[T : *]:
    Nat.Zero
    Nat.Succ (n : List[T], item : T)
является подтипом Nat, тут были использованы механизмы extending (у конструктора Succ добавлено
лишнее поле item : T) и (рекурсивно) narrowing: в предположении, что List[T] <: Nat мы имеем право
сузить тип аргумента n у конструктора Succ до List[T], стало быть определение List[T]
гарантирует List[T] <: Nat по определению в предположении List[T] <: Nat аргументах
конструкторов.

Мы можем легко получить и гетерогенный список:
  @Family HList:
    Nat.Zero
	  Nat.Succ (n : HList, X : *, item : X)
а List можем реализовать так, что он будет являтся подтипом HList при помощи механизма infilling:
  @Family List[T : *]:
    HList.Zero
	  HList.Succ(n : List[T], X: T, item : T)}

При помощи механизма infilling, мы можем также получить другой важный подтип Nat:
  @Family Vec[T : *, length : Nat]:
    List[T].Zero(length: Zero)
	  List[T].Succ(n : Vec[T], item : T, length: Succ(n.length))

Кроме того, мы можем не работать с конструкторами по-отдельности, а добавить во все сразу
какое-нибудь дополнительное поле, используя макрос ‹with›, например
  @def EvenNat: (n : Nat) ‹with› (evenness : n ‹mod› 2 = 0)
  @def OddNat: (n : Nat) ‹with› (oddness : n ‹mod› 2 = 1)

В связи с этим приведём ещё один интересный пример: взаимно-индуктивное семейство типов EvenNatI и OddNatI:
  @Family EvenNatI, OddNatI:
    Nat.Zero : EvenNatI
	  Nat.Succ(n : OddNatI) : EvenNatI
	  Nat.Succ(n : EvenNat) : OddNatI

На этом примере мы видим, что во-первых есть ещё один механизм сужения (запретить часть конструкторов),
во-вторых что когда индуктивные типы взаимозависимы, убедиться в том, что они являются подтипами некоторого
другого типа можно только рассматривая их определения в совокупности. Ещё отметим, что несложно определить
типы EvenNatI, OddNatI так, чтобы они наследовались от EvenNat и OddNat соответственно, пользуясь механизмом
fill и по ходу определения доказывая что значение n ‹mod› 2 обращается при каждом применении Succ (с чем
автоматически сприваляется SAT-solver F*):
  @Family EvenNatI, OddNatI:
    EvenNat.Zero(evenness: @derive) : EvenNatI
	  EvenNat.Succ(n : OddNatI, evenness: @derive) : EvenNatI
	  OddNat.Succ(n : EvenNat, @derive) : OddNatI

Несложно убедиться, что механизмы extend/refine, narrow и fill позволяют определять в точности орнаменты над
индуктивными типами, а сабтайпинг таким образом гарантирует возможность применять орнаментированные значения
в контексте где о части дополнительной структуры можно забыть, таким образом сабтайпинг не более чем удобный
синтаксический сахар для работы с орнаментами. Впрочем, номинальный сабтайпинг описанный здесь недостаточен:
наличие в контексте доказательств того что тривиальные отображения Vec -> List, EvenNatI -> EvenNat,
OddNatI -> OddNat cледующие из Vec <: List, EvenNatI <: EvenNat, OddNatI <: OddNat должно расцениваться как
наличие в контексте суждений List <: Vec, EvenNat <: EvenNatI, OddNat <: OddNatI, схлапывающих иерархию в 
точности там, где это нужно.