dependent-type - 如何在 Idris 中重写函数体，以便类型对应于函数签名并且整个事物都可以编译

Question

我想编译这个:

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

这编译失败，因为编译器无法统一 n与 n + m .我知道这是因为take的签名对于 Vect，但我不知道如何向编译器展示它们可以统一，如果 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'

Idris 在统一方面的困难是因为它不愿意推断 m在take的应用中:

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

你给了它一个 Vect n String它想要一个 Vect (n + m) a - 它愉快地统一了a与 String , 因为 Vect是类型构造器，但不愿统一n与 n + m因为，一般来说，它不能反转函数。你我都看得出来 m必须为零，但 idris 并不那么聪明。