idris 中隐式参数的顺序答案

【问题标题】：Order of implicit arguments in idrisidris 中隐式参数的顺序
【发布时间】：2019-12-13 14:03:29
【问题描述】：

How does the order of implicit arguments affect idris?

我刚刚阅读了这篇文章，我对 MkPair 的类型签名感到好奇。我在 REPL 上尝试了MkPair 10，我得到了

（输入）：无法将参数 B 推断为 Builtins.MkPair

这正是我所期望的。从它的类型签名Builtins.MkPair : {A : Type} -> {B : Type} -> (a : A) -> (b : B) -> (A, B)，我必须在为a 应用值之前传递B（无论是隐式还是显式）。同时，我希望q 10 可以工作，因为它的类型是q : {A : Type} -> (a : A) -> {B : Type} -> (b : B) -> (A, B)，这告诉我在为A 和a 应用值之前，我不需要B 的任何值。

但同样的消息也失败了！

（输入）：无法将参数 B 推断为 Main.q

q 会发生什么？

我还有一个问题。在我发现 q 两者都不起作用之前，我要问 Idris 编译器更喜欢 MkPair 的签名而不是 q 的签名的原因。 MkPair 看起来对我来说是不必要的渴望。为什么过早要求B？

【问题讨论】：

标签： functional-programming idris

【解决方案1】：

在没有任何上下文来指导编译器的情况下，我猜 Idris 在默认情况下保持其渴望的态度，并在执行自动部分应用程序之前尝试推断出现在最后一个指定的“显式”参数之前的所有隐式参数。

请注意，您可以通过将表达式放置在适当类型的孔中来抑制这种行为：

the ({b : Type} -> b -> (Nat, b)) (q 10)

-- or

r : {b : Type} -> b -> (Nat, b)
r = q 10

【讨论】：