idris - Idris 是否有不终止条款？

Question

在官方 Idris wiki 上的非官方常见问题解答(官方是因为它在该语言的 git 仓库中)，它是 stated that

in a total language [e.g. Idris] we don't have undefined and non-terminating terms so we need not worry about evaluating them.

但是，ones 的以下定义(使用 List 而不是 Stream)显然看起来是非终止的:

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

因此，我不确定维基条目是否有误，或者我是否误解了上下文。注意 Stream 解决方法已经是 described in the Idris tutorial .

Answer 1

如果你要求 Idris 是完整的，那么它就是完整的。您可以编写 %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.