Idris有非终止项吗？

Question

在官方Idris wiki的非官方FAQ（官方指该wiki位于语言的git repo上）中，指出：

在一个完整的语言中（例如Idris），我们没有未定义和不终止的术语，因此我们无需担心对它们进行评估。

然而，以下ones的定义（使用List而不是Stream）显然是不终止的：

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

所以，我不确定维基百科的条目是错误的，还是我误解了上下文。请注意，Stream 解决方法已经在 Idris 教程中 描述。

- bbarker

Answer 1

只有在你要求它是total时，Idris才会是total的。你可以写其中之一：%default total、%default covering或者%default partial（默认值），之后所有的声明都将采用给定的totality注释：

%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.

- HTNW