System S
Любители функционального программирования среди нас, наверное знают, что не только вычислимые функции, но и данные можно кодировать лямбда-выражениями, например булевы значения можно закодировать как функции двух аргументов, tt возвращает первый и игнорирует второй, а ff игнорирует первый, а возвращает второй, тогда конструкция if (condition) a else b превращается просто в condition(a, b). Натуральные числа можно кодировать нумералами Чёрча: это такие штуки, которые принимают произвольную функцию и применяют её саму к себе некоторое количество раз, которое как раз и соответствует кодируемому числу.
В интуиционистских зависимых теориях типов существует понятия индуктивных типов данных. Каждый такой тип T данных снабжается правилом исчерпания T-elim, принимающим по функции перехода на каждый конструктор, и возвращающим функции из T куда угодно. Например для натуральных чисел Nat = {Zero: Nat, Succ(n: Nat): Nat}, чтобы задать функцию (n: Nat) -> X(n), нужно использовать Nat-elim с параметрами
step-Zero: X(Zero)
step-Succ(n: Nat): X(n) -> X(Succ(n)),
совокупность данных для задания функции (в данном случае, пара step-Zero и step-Succ) называется рекурсором.
Для любого такого типа данных* можно изготовить представление данных, такое что терм t: T представляется лябмда-термом code-t, таким что T-elim recursor t = code-t recursor, это называется представления Parigot. Некоторая проблема состоит в том, что силами обычного полиморфного лямбда-исчисления типировать эти термы не представляется возможным. Не так давно вышла публикация, описывающая очень занятное обобщение (на зависимые типы) полиморфного лямбда-исчисления высшего порядка (System F-omega), названное авторами System S, способная типировать все такие представления: http://homepage.cs.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf
Фактически, такие типы там определяются заданным в явном виде правилом исчерпания. Судя по первому впечатлению после прочтения, на языке этой штуки возможно описывать не только индексированные контейнеры (indexed inductive type families), но и индуктивно-рекурсивные. Меня же больше всего занимает вопрос, нельзя ли в рамках System S определить very dependent types с правилом исчерпания на основе открытой индукции. На первый, опять же взгляд, синтаксис позволяет...
На второй взгляд очень интересно, как бы это дело обобщить для кодирования высших индуктивных типов в духе cubical type theory (на уровень термов кроме обычных лямбд добавятся path abstractions, а нужно ли что-то добавлять на уровень типов непонятно, может быть непредикативное равенство из их публикации само сработает).
___
* Не совсем любого, есть ограничение что термы не должны содержать типы.
В интуиционистских зависимых теориях типов существует понятия индуктивных типов данных. Каждый такой тип T данных снабжается правилом исчерпания T-elim, принимающим по функции перехода на каждый конструктор, и возвращающим функции из T куда угодно. Например для натуральных чисел Nat = {Zero: Nat, Succ(n: Nat): Nat}, чтобы задать функцию (n: Nat) -> X(n), нужно использовать Nat-elim с параметрами
step-Zero: X(Zero)
step-Succ(n: Nat): X(n) -> X(Succ(n)),
совокупность данных для задания функции (в данном случае, пара step-Zero и step-Succ) называется рекурсором.
Для любого такого типа данных* можно изготовить представление данных, такое что терм t: T представляется лябмда-термом code-t, таким что T-elim recursor t = code-t recursor, это называется представления Parigot. Некоторая проблема состоит в том, что силами обычного полиморфного лямбда-исчисления типировать эти термы не представляется возможным. Не так давно вышла публикация, описывающая очень занятное обобщение (на зависимые типы) полиморфного лямбда-исчисления высшего порядка (System F-omega), названное авторами System S, способная типировать все такие представления: http://homepage.cs.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf
Фактически, такие типы там определяются заданным в явном виде правилом исчерпания. Судя по первому впечатлению после прочтения, на языке этой штуки возможно описывать не только индексированные контейнеры (indexed inductive type families), но и индуктивно-рекурсивные. Меня же больше всего занимает вопрос, нельзя ли в рамках System S определить very dependent types с правилом исчерпания на основе открытой индукции. На первый, опять же взгляд, синтаксис позволяет...
На второй взгляд очень интересно, как бы это дело обобщить для кодирования высших индуктивных типов в духе cubical type theory (на уровень термов кроме обычных лямбд добавятся path abstractions, а нужно ли что-то добавлять на уровень типов непонятно, может быть непредикативное равенство из их публикации само сработает).
___
* Не совсем любого, есть ограничение что термы не должны содержать типы.