Есть фактически две причины, по которым Идрис не признает функцию fibo как итог. Во-первых, как вы указали, он не определен для целых чисел меньше 1, а во-вторых, он называет себя рекурсивно. Хотя Идрис способен распознавать всю совокупность рекурсивных функций, обычно это может сделать только тогда, когда можно показать, что аргумент рекурсивного вызова «меньше» (т. Е. Ближе к базовому случаю *), чем исходный аргумент (например, , если функция получает список в качестве аргумента, он может называть себя хвостом списка без необходимости жертвовать тотальностью, потому что хвост является подструктурой исходного списка и, следовательно, ближе к Nil). Проблема с выражениями типа (n-1) и (n-2), когда они типа Int, является то, что, хотя они численно меньше п, они не структурно меньше, потому что 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 представляет собой правило, которое, если п ≤ м, а затем (преемник п) ≤ (правопреемник м). Ключевое слово 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, где это возможно, в противном случае мы все равно должны предоставить его сами.
* Там также может быть некоторые CODATA тонкости, связанные что я замазывания здесь, не понимая, но это широкий принцип.