Ограничение входных аргументов функцией

На самом деле есть две причины, по которым Идрис не распознает функцию fibo как общую. Во-первых, как вы указали, он не определен для целых чисел меньше 1, а во-вторых, он вызывает себя рекурсивно. Хотя Idris способен распознавать все рекурсивные функции, обычно он может это делать только тогда, когда можно показать, что аргумент рекурсивного вызова «меньше» (т.е. ближе к базовому случаю*), чем исходный аргумент (например, , если функция получает список в качестве аргумента, она может вызвать себя с хвостом списка, не обязательно жертвуя целостностью, потому что хвост является подструктурой исходного списка и, следовательно, ближе к Nil). Проблема с такими выражениями, как (n-1) и (n-2), когда они имеют тип Int, заключается в том, что хотя они численно меньше n, они не структурно меньше, потому что Int не равно определено индуктивно и поэтому не имеет базовых случаев. Поэтому средство проверки целостности не может убедиться, что рекурсия всегда в конце концов достигает базового случая (даже если это может показаться нам очевидным), и поэтому оно не будет считать fibo полным.

Прежде всего, давайте решим проблему рекурсии. Вместо Int мы можем использовать индуктивно определенный тип данных, такой как Nat:

data Nat =
  Z | S Nat

(Натуральное число либо равно нулю, либо является преемником другого натурального числа.)

Это позволяет нам переписать fibo как:

fibo : Nat -> Int
fibo (S Z)     = 1
fibo (S (S Z)) = 2
fibo (S (S n)) = fibo (S n) + fibo n

(Обратите внимание, что в рекурсивном случае вместо явного вычисления (n-1) и (n-2) мы получаем их путем сопоставления с образцом аргумента, тем самым демонстрируя Идрису, что они структурно меньше.)

Однако это новое определение fibo все еще не является полностью полным, поскольку в нем отсутствует случай для Z (т. е. ноль). Если мы не хотим предусмотреть такой случай, то мы должны дать Идрису некоторые гарантии, что этого не допустят. Один из способов сделать это — потребовать доказательства того, что аргумент fibo больше или равен единице (или, что то же самое, единица меньше или равна аргументу):

fibo : (n : Nat) -> LTE 1 n -> Int
fibo Z LTEZero impossible
fibo Z (LTESucc _) impossible
fibo (S Z) _ = 1
fibo (S (S Z)) _ = 2
fibo (S (S (S n))) _ = fibo (S (S n)) (LTESucc LTEZero) + fibo (S n) (LTESucc LTEZero)

LTE 1 n — это тип, значения которого являются доказательством того, что 1 ≤ n (в пределах натуральных чисел). LTEZero представляет аксиому, согласно которой ноль ≤ любого натурального числа, а LTESucc представляет правило, что если n ≤ m, то (последователь n) ≤ (последователь m ). Ключевое слово impossible указывает, что данный случай не может произойти. В приведенном выше определении невозможно, чтобы первый аргумент fibo был равен нулю, потому что нет способа доказать, что 1 ≤ 0. Для любого другого натурального числа n мы можем доказать, что 1 ≤ n используя (LTESucc LTEZero).

Теперь, наконец, fibo является полным, но довольно громоздко предоставлять ему явное доказательство того, что его аргумент больше или равен 1. К счастью, мы можем пометить аргумент доказательства как автоматически неявный:

fibo : (n : Nat) -> {auto p : LTE 1 n} -> Int
fibo Z {p = LTEZero} impossible
fibo Z {p = (LTESucc _)} impossible
fibo (S Z) = 1
fibo (S (S Z)) = 2
fibo (S (S (S n))) = fibo (S (S n)) + fibo (S n)

Идрис теперь автоматически найдет доказательство того, что 1 ≤ n, где это возможно, в противном случае нам все равно придется предоставить его самим.

_{* Вполне могут быть некоторые тонкости, связанные с кодовыми данными, которые я здесь не замечаю, но это общий принцип.}