如何在Idris中重写函数体,以便类型对应于函数签名和整个事物编译

Question

我想要编译:

foo: Vect n String -> Vect n String
foo {n} xs = take n xs

这不能编译,因为编译器不能统一n用n + m.据我所知,这是因为takeVect的签名,但我无法弄清楚如何向编译器展示他们可以统一的编译器m = 0.

Answer 1

只是为了添加上一个答案,另一种可能性是使用plusZeroRightNeutral库中现有的引理进行内联重写:

foo: Vect n String -> Vect n String
foo {n} xs = let xs' : Vect (n + 0) String
                     = rewrite (plusZeroRightNeutral n) in xs in
                 take n xs'

伊德里斯在统一中遇到的困难是因为它不愿意m在应用中推断:

take : (n : Nat) -> Vect (n + m) a -> Vect n a

你给它一个Vect n String它想要一个Vect (n + m) a-它已经愉快地统一a用String,因为Vect是一类的构造函数,但就是不愿统一n使用n + m,因为在一般情况下,它不能反转的功能.你和我可以说它m必须为零,但伊德里斯并不那么聪明.