idris - 为什么伊德里斯需要相互？

Question

为什么 Idris 要求函数按照它们的定义和相互递归的顺序出现mutual？

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

Answer 1

在教程中它说（强调我的）：

一般来说，函数和数据类型必须在使用前定义，因为依赖类型允许函数作为类型的一部分出现，并且它们的归约行为会影响类型检查。但是，可以通过使用互块来放宽这种限制，它允许同时定义数据类型和函数。

（Agda 也有这个限制，但现在删除了mutual 关键字，支持先给出类型然后给出定义。）

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

我不知道这个问题是否可以用依赖类型来解决（一方面你失去了 Hindley-Milner），但我敢打赌，即使它是有效的。