为什么Idris要求函数按照它们的定义顺序出现并且相互递归声明mutual？
我希望Idris在函数之间执行依赖性分析的第一遍,并自动重新排序.我一直相信Haskell会这样做.为什么在伊德里斯这不可能？
在教程中它说(强调我的):
通常,必须在使用之前定义函数和数据类型,因为依赖类型允许函数作为类型的一部分出现,并且它们的缩减行为会影响类型检查.但是,可以通过使用相互块来放宽此限制,该相互块允许同时定义数据类型和功能.
(Agda也有这个限制,但现在已经删除了相互关键字,转而给出类型然后定义.)
为了扩展这一点:当你有依赖类型时,Haskell的自动依赖性分析将是困难的或不可能的,因为类型级别的依赖顺序可能与值级别的依赖顺序不同.Haskell没有这个问题,因为值不能出现在类型中,所以它可以只进行依赖性分析,然后按顺序进行类型检查.这就是Idris教程关于类型检查所需的值的减少行为的内容.
我不知道问题是否甚至可以通过依赖类型来解决(一方面你会失去Hindley-Milner),但我敢打赌它即使有效也不会有效.