![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Очень-очень интересно!
Aug. 23rd, 2014 11:59 pmВ предикативных типизированных исчислениях построений встречаются много разных способов определять типы, самый универсальный предикативный (т.е. избегающей неразрешимой рекурсии) известный на сегодня способ определять типы — расслоенные индуктивно-рекурсивные определения, таким образом можно определять не только индексированные контейнеры (эквивалентно: индуктивные семейства типов), их зависимые суммы и произведения, но и вселенные (типы типов), замкнутые относительно построения в них индексированных контейнеров, зависимых сумм и произведений. В общем это такой зверь, которого достаточно для всех известных применений, не считая высших типов. Именно индуктивно-рекурсивно (и заведомо только так) можно построить модель зависимо-типизированного языка в нём самом, т.е. пару из зависимого типа Expr[T] (валидное выражение языка типа T) и функции execute: Expr[T] => T.
Ничего нормального для высших типов на эту тему ещё не изобрели, в частности в HoTT стоит адова проблема построения симплициалных типов (это важно потому что показано, что если в HoTT можно смоделировать её саму, то с необходимостью можно сэмулировать и симплициальные типы). С другой стороны, с колокольни HoTT вообще непонятно, как могут строиться в одномерной теории вселенные типов, доказано что уважающая унивалентность вселенная n-типов в HoTT неизбежно имеет h-уровень больше n. То есть понятно, что индукция-рекурсия очень поверхностно совместима с HoTT, унивалентных вселенных так не построишь, да и другие интересности получаются неэквивариантными.
В недавней статье Neil Ghani et al. вводят очень интересную (красивую с категорной точки зрения) положительную индукцию-рекурсию: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/positive_calco2013.pdf.
Крайне интересным образом, вселенная, замкнутая относительно построения П-типов, методами IR+ не получишь, однако можно получить группоид, обладающий нужными свойствами, это как раз то что в HoTT должно получиться. Наверняка за этим делом скрывается обобщение – некая высшая положительная индукция-рекурсия HIR+, методами которой можно как раз получать всякие там симплициальные типы.
Ничего нормального для высших типов на эту тему ещё не изобрели, в частности в HoTT стоит адова проблема построения симплициалных типов (это важно потому что показано, что если в HoTT можно смоделировать её саму, то с необходимостью можно сэмулировать и симплициальные типы). С другой стороны, с колокольни HoTT вообще непонятно, как могут строиться в одномерной теории вселенные типов, доказано что уважающая унивалентность вселенная n-типов в HoTT неизбежно имеет h-уровень больше n. То есть понятно, что индукция-рекурсия очень поверхностно совместима с HoTT, унивалентных вселенных так не построишь, да и другие интересности получаются неэквивариантными.
В недавней статье Neil Ghani et al. вводят очень интересную (красивую с категорной точки зрения) положительную индукцию-рекурсию: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/positive_calco2013.pdf.
Крайне интересным образом, вселенная, замкнутая относительно построения П-типов, методами IR+ не получишь, однако можно получить группоид, обладающий нужными свойствами, это как раз то что в HoTT должно получиться. Наверняка за этим делом скрывается обобщение – некая высшая положительная индукция-рекурсия HIR+, методами которой можно как раз получать всякие там симплициальные типы.
