隐含的位置重要吗？答案

【问题标题】：Does the position of implicits matter?隐含的位置重要吗？
【发布时间】：2021-12-26 20:20:58
【问题描述】：

有没有区别

foo: {len : _} -> Int -> Vect len Int

和

foo: Int -> {len : _} -> Vect len Int

对于数据构造函数、类型构造函数等类似吗？有时我发现我的代码在一个位置使用隐式编译，但在另一个位置却没有，我不太清楚为什么。

【问题讨论】：

标签： idris

【解决方案1】：

如果你使用一个隐含在另一个类型中的值会很重要，比如：

x : {n : Nat} -> {ts : Vect n Type} -> HVect ts

在这种情况下，n 必须在 ts 之前。

【讨论】：

【解决方案2】：

一个小区别：如果前面的参数也在范围内，那么隐式似乎只在范围内。例如，在

foo : {len : _} -> Int -> Vect len Int
foo = ?rhs -- len IS in scope here

同时

foo : Int -> {len : _} -> Vect len Int
foo = ?rhs -- len is NOT in scope here

和

foo : Int -> {len : _} -> Vect len Int
foo x = ?rhs -- len IS in scope here

【讨论】：