Очень зависимые типы

[akuklev]

Николай Краус и коллеги недавно высказали гипотезу, что HoTT можно дополнить ещё одним полезным в хозяйства конструктором зависимых типов данных, впервые упомянутым в 1996 году под названием "очень зависимая функция". Этот конструктор является одновременным обобщением зависимой суммы и зависимого произведения, из-за чего он крайне симпатичен.

Смотрите, это тип пары двух натуральных чисел:
(Nat, Nat)

А вот это тип пары двух натуральных чисел, таких что второе не больше
первого:
(n : Nat, Fin(n))

А вот это тип натуральнозначной функции на натуральных числах:
Nat -> Nat

А вот это более рестриктивный тип, он требует чтобы значение было не больше аргумента:
(n : Nat) -> Fin(n)

Существует совершенно фундаментальная эквивалентность между кортежами (парами, тройками и т.д.) и списками конечной длинны. Для однородных списков это вообще тривиально, (Nat, Nat, Nat) == (Fin(3) -> Nat), для кодирования гетерогенных списков справа потребуются уже зависимые функции:
(A, B, C) == (selector : Fin(3)) -> selector |>
  0 => A
  1 => B
  2 => C

Наша цель в том, чтобы можно было и зависимый кортеж вида
(a : A, b : B(a), c : C(a, b),..)
представить в виде функции. Для этого нам понадобится, чтобы тип значения функции на более старших аргументах мог зависеть от значений этой же самой фукнции на более младших аргументах.
(a : A, b : B(a), c : C(a, b),..) == (sel : Fin(3) -> (\fs => sel |>
  0 => A
  1 => B(fs(0)
  2 => C(fs(1))
))

Именно эта конструкция называется "очень зависимым типом". Она обобщает понятие "зависимого кортежа" на случай кортежей бесконечной длины, индексированных индуктивным семейством типов. Такой конструктор типов позволяет формулировать алгебраические структуры, которые не могут быть конечно аксиоматизированы, и, предположительно, пучки над категорями Риди, в том числе семи-симплициальные и симплициальные типы, слабые омега-группоиды (симплициальные типы Кана), Г-пространства. На данный момент конструкция проработана только для обратных категорий, т.е. случая семи-симплициальных, семи-кубических и т.д. типов.

Указанный выше синтаксис позволяет в теле выражения после -> применять f к любым аргументам, т.е. мы лишены синтаксической защиты от циркулярных определений. При определении конкретной функции f вместе с её типом такую защиту легко организовать. Для начала рассмотрим случай, когда каждый последующий тип кортежа T(n) зависит только от предыдущего значения (а не от всех предыдущих):
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (f(n))


Тип Fin(3), разумеется, можно заменить на любой другой индуктивный тип, добавив в тело t разбор всех его конструкторов. Тут видно, что как только мы заполним многоточие телом функции f, функция f и её тип будут корректно определены взаимно рекурсивно-индуктивно. Мы без особого труда можем расширить зависимость на ситуацию, когди тип T(n) элемента кортежа зависит от всех предыдущих значений:
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (fs(n))

  ts: Fin(3) -> Type
    0 => t(0)
    succ(n) => ts(n) × t(n + 1)

  fs: (s: Fin(3)) -> ts(s)
    0 => f(0)
    succ(n) => (fs(n), f(n + 1))


Как и выше, Fin(3) легко обобщается до произвольного индуктивного семейства типов. Как мы видим, синтаксическое определение очень зависимого типа совместно с конкретным представителем такого типа не представляет проблем. Как сформулировать синтаксическое определение очень зависимого типа в отрыве от конкретного представителя? Выше приведён способ развязать этот узел примитивно -- раз тип очень зависимых функций из W определяется функцией t(s: W, fs: subterm(s) -> ...): Type, то и будем писать в качестве формера (s : W) -> (\fs => well-formed type expression), однако возникают вопросы, нет ли более элегантного способа развязать этот узел в духе контейнеров.