Idris语言是否存在非终止项？

首先得明确：非官方FAQ里的描述并没有错，只是你可能误解了它的适用上下文——它说的是“在Idris这样的完全语言中，我们没有未定义和非终止项”，这里的“项”特指通过Idris终止检查器的总函数/合法定义，而你写的List版ones并不属于这个范畴。

下面拆解几个关键点：

1. List vs Stream的本质区别 #

• List是有限序列的类型，Idris要求List的构造必须遵循结构递归：每次递归调用必须处理原数据的子结构（比如递归处理tail xs而不是整个xs）。你写的ones = 1 :: ones是无限递归构造List，完全违背了List的有限性定义，Idris的终止检查器会直接拒绝这个定义（除非你用%assert_total强行绕过检查）。
• Stream是无限序列的类型，它支持核心递归（也叫guarded recursion）：构造时的递归调用被包裹在构造器里（比如1 :: ones中的ones是被::包裹的），Idris会认可这种定义，而且Stream是惰性求值的——求值head ones时只会构造第一个元素，不会递归求值整个无限序列，所以能正常返回1。

2. Idris“完全性”的真实含义 #

Idris作为完全语言，核心保证是：所有通过类型检查和终止检查的总函数，在求值时一定会终止，且不会出现未定义行为。但这个保证是有前提的——你必须遵守Idris的递归规则，写合法的总函数。

如果你绕过终止检查（比如用%assert_total）或者写了不满足结构/核心递归的部分函数，那Idris就无法保证你的代码不会出现非终止或未定义行为——你写的List版ones就是这种情况，强行运行head ones会导致无限递归，最终栈溢出触发段错误。

3. 编译器的直接提示 #

如果你尝试在Idris中直接定义ones : List Int; ones = 1 :: ones，编译器会抛出类似这样的错误：

Can't find a way to break the cycle:
ones = 1 :: ones

这说明Idris已经识别出这个定义是非终止的，不允许它通过检查。只有当你用%assert_total跳过检查时，才会让这个定义通过，但这相当于你手动放弃了Idris的完全性保证，出问题也就不奇怪了。

总结一下：FAQ的描述是针对Idris的总函数场景，而你的代码是一个未通过终止检查的部分函数，不属于FAQ所描述的范畴，所以才会出现看似矛盾的情况。

内容的提问来源于stack exchange，提问作者bbarker