idris - 为什么 idris 需要相互？

Question

为什么 Idris 要求函数按照定义的顺序出现，并使用 mutual 声明的相互递归?

我希望 Idris 执行函数之间的第一次依赖分析，并自动对它们进行重新排序。我一直相信 Haskell 是这样做的。为什么这在 idris 是不可能的？

Answer 1

在 tutorial它说(强调我的):

In general, functions and data types must be defined before use, since dependent types allow functions to appear as part of types, and their reduction behaviour to affect type checking. However, this restriction can be relaxed by using a mutual block, which allows data types and functions to be defined simultaneously.

(Agda 也有这个限制，但现在有 removed the mutual keyword in favour of giving types then definitions 。)

对此进行扩展:当您有依赖类型时，Haskell 的自动依赖分析将是困难或不可能的，因为类型级别的依赖顺序可能与值级别的依赖顺序非常不同。 Haskell 没有这个问题，因为值不能出现在类型中，所以它可以只进行依赖分析，然后按顺序进行类型检查。这就是 Idris 教程关于类型检查所需的值的减少行为的内容。

我不知道这个问题通常是否可以通过依赖类型解决(一方面，你失去了 Hindley-Milner)，但我敢打赌，即使是这样，它也不会有效。