shooting off your leg with class

[thedeemon]

Захотелось мне недавно реализовать циклический сдвиг непустого вектора (списка с длиной в типе) на Идрисе. Пишу:

rotLeft : Vect a (S n) -> Vect a (S n)
rotLeft v = tail v ++ [head v]
А компилятор мне отвечает, что он хоть и умный, но ленивый, и ему не очевидно, что n+1 это n+1, ну в смысле что результат применения функции сложения натурального числа n с константой 1 это следующее за n число.
"Can't unify Vect a (m + n) with Vect a (S n)
Specifically: Can't unify plus m with S"
Для случаев, когда код правильный, но компилятор не убежден в корректности типов, в Идрисе есть специальные доказательства и интерактивный режим их построения посредством тактик. Пишем так:

rotLeft v ?= tail v ++ [head v]
Знак вопроса перед равенством означает, что корректность типов будет доказана отдельной леммой. Запускаем REPL. Он такой код принимает, а по команде :m показывает, что есть одна незакрытая лемма:

Global metavariables: [Main.rotLeft_lemma_1]
Спрашиваем ее тип:

> :t rotLeft_lemma_1
rotLeft_lemma_1 : (a : Type) -> (n : Nat) -> (Vect a (S n)) -> (Vect a (n + (S O)))
-> Vect a (S n)
Тип ее говорит, что это функция, принимающая на вход аргументы исходной функции и ее результат в том виде, который смог вывести компилятор (Vect a (n + (S O)), где S O - это натуральная единица в унарной записи), а на выходе должна выдать значение того типа, что мы указали выходным типом исходной функции (Vect a (S n)). Перехожу в интерактивный режим доказательств: :p rotLeft_lemma_1, после чего как та мартышка с печатной машинкой пробую разные тактики (это был мой первый опыт, я тогда об этих тактиках почти ничего не знал). Вижу, что последовательность из двух тактик intros и trivial лемму закрывает:

> :p rotLeft_lemma_1
---------- Goal: ----------
{ hole 0 }:
(a : Type) ->
(n : Nat) ->
(Vect a (S n)) ->
(Vect a (n + (S O))) -> Vect a (S n)
-Main.rotLeft_lemma_1> intros
---------- Other goals: ----------
{ hole 3 }
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
a : Type
n : Nat
v : Vect a (S n)
value : Vect a (n + (S O))
---------- Goal: ----------
{ hole 4 }:
Vect a (S n)
-Main.rotLeft_lemma_1> trivial
rotLeft_lemma_1: No more goals.
-Main.rotLeft_lemma_1> qed
Main.rotLeft_lemma_1 = proof {
intros;
trivial;
}
Команда qed там выводит запись доказательства, которую можно скопировать в исходник. Копирую, компилирую, все проходит успешно, ура! Пробую запустить и вижу, что работает-то код неправильно: rotLeft [1,2,3] выдает [1,2,3] вместо ожидаемого [2,3,1]. Вот так, используя зависимые типы и теорем-прувинг, можно неожиданно заставить корректный код работать некорректно. А дело тут вот в чем. Команда intros последовательно вводит все входные параметры в качестве предпосылок доказательства, записывает их в графу "дано". А команда trivial ищет среди уже доказанного терм, подходящий по форме к доказываемой цели. Поскольку на выходе мы хотим получить значение такого же типа, какое было на входе, прувер просто взял входное значение. Получилось, что лемма эта забивает на вычисленный телом функции результат и возвращает вместо него аргумент функции. Типы сошлись, все чудесно, но результат неверный.
Если же подойти к делу более осмысленно, то можно тактиками подсказать компилятору, что следует попытаться произвести вычисления (развернуть функцию сложения), затем ввести нужные парамерты в графу "дано", а потом применить лемму из стандартной библиотеки о коммутативности сложения. Тогда цель и вычисленное функцией значение окажутся с одинаковыми типами, и можно тактикой trivial взять нужное, на этот раз то самое. Вот так выглядит рабочее доказательство:

rotLeft_lemma_1 = proof {
compute; intro; intro; intro; intro;
rewrite plusCommutative n (S O); trivial;
}
C ним уже код работает правильно. Так-то.