Idris是否有非终止条款？

Question

关于官方伊德里斯维基的非官方常见问题解答(官方的,因为它是关于语言的git repo),它被声明

在总语言[例如Idris]中,我们没有未定义和非终止术语,因此我们不必担心评估它们.

但是,ones(使用List而不是Stream)的以下定义肯定似乎是非终止的:

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

所以,我不确定wiki条目是否错误,或者我是否误解了上下文.请注意,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.