lomeo | typechecker для dependent types system (Reply)

Заинтересовал меня всё таки

kurilka тотальным ФП, а у

thesz я понахватался ссылок и умных слов. Ну, ещё и dependent types в стороне не остались.

Подумал, что total fp будет неплохо смотреться для программирования на типах - гарантия завершения будет тут очень кстати.

К сожалению, "по семейным обстоятельствам" я сейчас не в силах заняться чем нибудь серьёзно, поэтому всё, что я здесь пишу - скорее для себя, чтобы не забыть. Написано очень нудно (это тоже для себя, извините - я тупой) и сумбурно (а это так получилось).

Итак что здесь? (чтобы вы решили читать или нет)
Здесь размышления о том, как должен работать тайпчекер в системе с зависимыми типами. Я пытаюсь придумать приёмы, позволяющие строить гарантировано завершающиеся доказательства/опровержения.

Допустим, у нас есть тайп чекер, который разбирает следующее определение:

append :: List a n -> List a m -> List a (n + m)
append []     ys = ys
append (x:xs) ys = x : (xs `append` ys)

Это вы наверняка уже сто раз видели, но я для проформы повторю основные определения: List имеет тип (kind в терминах Haskell) - * -> Nat -> *:

data List :: * -> Nat -> *
    = []  :: List a 0
    | (:) :: a -> List a n -> List a (n + 1)

Nat - тип натуральных чисел:

data Nat :: *
    = Z :: Nat
    | S :: Nat -> Nat

Запись вида 0, 1, 2... всего лишь синтаксический сахар для Z, S Z, S (S Z)... А запись (n + 1) - сахар для S n. Вот, например, как этот сахар используется в определении функции (+):

(+) :: Nat -> Nat -> Nat
0 + m = m                   -- аналогично Z + m = m
(n + 1) + m = (n + m) + 1   -- аналогично (S n) + m = S (n + m)

Итак, нашему тайпчекеру надо проверить тип функции append.

Для первой части определения вроде бы всё просто (на самом деле нет, но мы это рассмотрим дальше). Из [] мы сопоставляем типы List a n и List b 0, находим, что наиболее общий тип, который входит в эти два - это List a 0 (подробности, как мы это делаем, неважны). ys :: List a m, а значит, нам надо убедиться, что результат (ys справа) имеет тип List a (0 + m). Для этого мы должны доказать, что List a m (выведенный тип выражения ys) будет равен List a (0 + m) (тип из сигнатуры). Разбирая конструкторы получим m == 0 + m, а это равенство у нас уже есть в определении (+).

Итак, вроде простая задача, но тут мы применили три приёма:
1. Подстановка (n == 0, m == n + m => m == 0 + m)
2. Разбор конструктора (декомпозиция? структурный декремент?)
3. Подстановка из равенства из определения функции (частный случай пункта 1, но из-за него нам надо знать определения функций над типами во время компиляции)

Пока не будем на этом останавливаться, поехали дальше.

Вторая часть определения

append (x:xs) ys = x : (xs `append` ys)

Откуда

x :: a
xs :: List a k
ys :: List a m
k + 1 == n
xs `append` ys :: List a (k + m)
x : (xs `append` ys) :: List a ((k + m) + 1)

Итак, мы должны сравнить List a (n + m) == List a ((k + m) + 1)
1. n + m == (k + m) + 1 (разбор конструктора)
2. (k + 1) + m == (k + m) + 1 (подстановка)
3. (k + m) + 1 == (k + m) + 1 (подстановка из функции)

Вроде бы пары приёмов - подстановки и разбора конструктора (эдакой эта-редукции уровня типов) нам хватает. На самом деле тут самое интересное. Допустим, что программист определил тип для append как List a n -> List a m -> List a (m + n). Т.е. рокировка n и m. Как тут будет проходить доказательство?

Для первой части имеем (после вытаскивания из конструкторов)

m == m + 0

А вот это доказать простой подстановкой уже не получается. Единственное, что пришло мне в голову использовать метод индукции. Проверяем для всех конструкторов типа Nat, начиная с простых (нерекурсивных, т.к. это data - они обязательно должны быть).

Для Z: m == 0, 0 + 0 = 0. ОК
Для S: m = k + 1
1. k + 1 == (k + 1) + 0 (подстановка)
2. k + 1 == (k + 0) + 1 (подстановка из функции)
3. k == k + 0 (разбор конструктора)
4. ОК (по индукции)

С индукцией тоже могут быть проблемы, о которых надо подумать: много переменных в равенствах, много параметров в конструкторах.

Тем не менее, мы получили три приёма - подстановка, разбор конструктора и индукция. Последние два, очевидно, никак не могут препятствовать проверке типа завершиться. Подстановка из функции - тоже, т.к. функции у нас терминируемы, только брать надо подстановки слева направо. Остаётся просто подстановка, из типа, выведенного из выражения и из типа, описанного программистом. Может ли здесь возникнуть такая ситуация, что в системе равенств будет присутствовать n = m + 1, m = n + 1? Если да, можем ли мы легко определять такие ситуации и грязно ругаться?

В общем, резюмирую.

Проверка типа заключается в доказательстве, что тип, описанный программистом является таким же или более конкретным, чем тип, выведенный из выражения в правой части. При доказательстве используются три приёма:
1. подстановка
2. разбор конструктора (может деструкция? надо в статьях посмотреть)
3. индукция

Проблемы возникают с подстановкой:
1. Надо знать содержание функций, применяющихся в описании типа.
2. Неясно как быть с подстановками, ведущими к нетерминируемости.

По первому пункту: видимо, надо знать именно равенства, а не паттерн -> case, разбирать проще. Правда, не представляю, как это может выглядеть.

Если у кого то есть материалы по теме, накидайте сюда плз - потом как руки дойдут обязательно прочту всё-всё-всё :-)