Есть ли у Idris не прекращающиеся условия?

Question

В неофициальном FAQ на официальной вики-странице Idris (официальной в том смысле, что она есть в git-репо языка), указано, что

на общем языке [например,Idris] у нас нет неопределенных и не заканчивающихся терминов, поэтому нам не нужно беспокоиться об их оценке.

Однако, следующее определение для ones (с использованием List вместо Stream), конечно, кажется, что оно не заканчивается:

ones: List Int
ones = 1 :: ones
-- ...
printLn(head ones) -- seg fault!

Итак, я не уверен, ошибочна ли запись в вики или я неправильно понял контекст.Обратите внимание, что Stream обходной путь уже описан в руководстве по Idris .

Answer 1

Идрис является полным, только если вы просите его быть полным.Вы можете написать одну из %default total, %default covering или %default partial (по умолчанию), и все объявления после этого будут принимать данную аннотацию совокупности:

%default total

-- implicitly total
ones1 : List Int
ones1 = 1 :: ones1
-- ERROR: ones1 is not total

-- total
ZNeverHeardOfIt : Nat -> Nat
ZNeverHeardOfIt (S n) = n
-- ERROR: missing cases in ZNeverHeardOfIt

covering
natRoulette : Nat -> Nat
natRoulette Z = Z
natRoulette (S n) = natRoulette (S (S n))
-- covering means all possible inputs are covered by an equation
-- but the function isn't checked for termination
-- natRoulette has cases for all inputs, but it might go into an infinite loop
-- it's morally equivalent to just partial, as a function that loops forever
-- on an input isn’t very different from one missing the case
-- it just gets the compiler to complain more

partial
ones : List Int
ones = 1 :: ones
-- no checks at all
-- Idris, being strict, needs to evaluate ones strictly before it can evaluate ones.
-- Oh wait, that's impossible. Idris promptly vanishes in a segfault.