typechecker для dependent types system

[lomeo]

Заинтересовал меня всё таки kurilka тотальным ФП, а у deni_ok и 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, разбирать проще. Правда, не представляю, как это может выглядеть.


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

Comments

[thesz.livejournal.com]

http://citeseer.ist.psu.edu/364350.html

Type Inference and Reconstruction for First Order Dependent Types

[lomeo.livejournal.com]

спасибо! там про тайп чекинг тоже есть или только вывод типов? или это сильно связанные темы?

[thesz.livejournal.com]

Связанные. Вроде, вывод типов - это алгоритм проверки типов в отсутствие аннотаций.

[lomeo.livejournal.com]

Не уверен, по мне так проверка типа должна быть проще, чем вывод.
Ладно буду разбираться.

[deni-ok.livejournal.com]

В общем случае - да, но это от системы типов зависит. Для чистого Хиндли-Милнера это практически одно и то же. Правда я не знаю, можно ли придумать систему, в которой вывод гарантированно завершается, а проверка - нет.

[lomeo.livejournal.com]

Да дело не в завершении. Мне кажется, что сопоставление типов с выражением должно проходить проще.
Хотя это, наверное, действительно, зависит от системы типов.

[deni-ok.livejournal.com]

Если язык целиком на лямбде или комбинаторах (мы же о таких говорим?), то составление системы уравнений на типы по последовательности абстракций/аппликаций - вроде как тривиально всегда. А вот решение - не знаю. Ты скорее всего прав в том смысле, что проще проверить, является ли данная сигнатура типа решением системы, чем искать общее решение.

Но с зависимыми типами, да, проблема есть и при подстановке сигнатуры - свойство коммутативности: m+n=n+m - теорема сложения, которая следует из введенной тобой аксиоматики Пеано, но тайпчекер об этом не знает :(

[lomeo.livejournal.com]

Да нехай его не знает, главное, чтобы он мог вывести коммутативность :-)

[deni-ok.livejournal.com]

А потом дистрибутивность умножения относительно сложения, и т.д. и т.п. вплоть до теоремы Ферма? ;)

Ты ввёл всю аксиоматику Пеано для Nat, вроде так.

http://ru.wikipedia.org/wiki/%D0%90%D0%BA%D1%81%D0%B8%D0%BE%D0%BC%D1%8B_%D0%9F%D0%B5%D0%B0%D0%BD%D0%BE

Разбор конструктора S :
S a = S b => a = b - это четвертая аксиома, индукция - пятая. Остальные вроде зашиты в определении data.

[lomeo.livejournal.com]

Спасибо!!

Единственное что, я хочу узнать можно ли расширить эти аксиомы для любых data-типов (initial algebra).

[deni-ok.livejournal.com]

Не за что :-)

Мне не очень нравится индукция у тебя: Нужно из P(n) вывести P(n+1), а ты редуцируешь P(n+1) к P(n). Я не уверен, что это не придирка, но как-то меня это смущает.

> Единственное что, я хочу узнать можно ли расширить эти аксиомы для любых data-типов (initial algebra).

Это я не очень понимаю. Что значит расширить?

[lomeo.livejournal.com]

Да ты прав, с индукцией там надо прямое доказательство использовать.

> Это я не очень понимаю. Что значит расширить?

Распространить на все data-типы, не только на Nat.

[thesz.livejournal.com]

http://www.dcs.st-and.ac.uk/~eb/ivor.php

Ivor is a type theory based theorem prover, with a Haskell API, designed for easy extending and embedding of theorem proving technology in Haskell applications. It provides an implementation of the type theory (which I call TT) and tactics for building terms in the type theory, more or less along the lines of systems such as Coq or Agda, and taking much of its inspiration from Conor McBride's presentation of OLEG in his thesis. The primary aim of Ivor is to support research in generative programming and resource bounded computation in Hume (see, e.g. this paper), but it is more generally applicable.

Вот. ;)

[lomeo.livejournal.com]

О! Спасибо!

[thesz.livejournal.com]

Вот исчо: http://www.cs.nott.ac.uk/~txa/talks/plpv07.pdf - презентация идей вот из этой статьи: http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf

В презентации я углядел вопрос "как получить Vec a (x+y) из Vec a (y+x)?" и тут же вспомнил про тебя. ;)

[lomeo.livejournal.com]

Спасибо большое, сегодня вечером почитаю.
Судя по всему легко и просто это не получается, ну и второй момент - мне ещё копать и копать :-)

[thesz.livejournal.com]

А вот: http://community.livejournal.com/ru_deptypes/412.html