Idris Dependent Pairs：编译的程序和REPL之间的意外行为

Question

在Idris中使用依赖对进行练习时，我在编译程序和REPL之间遇到了意想不到的行为差异。我正在测试以下数据类型：

(a : Type ** b : Type ** Arrow a b)

这应该代表a类型和b类型之间的某种关系。鉴于上述情况，我想提取该类型的“证明”术语。我可以使用DPair.snd $ DPair.snd <some-instance>从REPL做到这一点，一切正常。但是，如果我尝试创建一个函数：

unwrap : (a ** b ** Arrow a b) -> Arrow a b
unwrap x = DPair.snd $ DPair.snd x

程序将编译，但当我尝试调用它时将失败。返回的错误消息是

(input): No such variable b

有没有人遇到这个或知道解决方案？

Answer 1

你想要实现的目标是不可能的。如果你看一下unwrap : (a1 : Type ** b1 : Type ** Arrow a b) -> Arrow a b的类型，你会发现它使用的是与(a : Type ** b : Type ** Arrow a b)不同的数据类型。这是因为参数a，b是事先量化的 - 设置结果类型（这也是与REPL情况的区别;你没有绑定参数）。所以用:set showimplicit就可以了

Main.unwrap : {b : Type} -> {a : Type} ->
              (a1 : Type ** b1 : Type ** Main.Arrow a b) ->
              Main.Arrow a b

关于依赖对的问题，你不能轻易地限制它们。看看Vect.filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem) - 如果我们有像unwrap : (p : Nat ** Vect p elem) -> Vect p elem这样的函数，我们首先不需要依赖对。

相反，一个调用unwrap的函数需要检查p，然后相应地处理Vect。遗憾的是，我们不能轻易地检查类型（至少如果你想要推广所有类型）。所以你最好的选择是：不要在这里使用依赖类型。