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

Question

我想对此进行编译：

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

这无法编译，因为编译器无法n与n + m. 我知道这是因为takefor Vect's 的签名，但我不知道如何去向编译器展示它们可以统一 if 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必须为零，但伊德里斯没那么聪明。

Answer 2

伊德里斯无法统一n，n + m因为它不知道n = n + 0。您需要通过手动证明来帮助他。

首先，为什么它需要这个证明。原因是take期望Vect (n+m) a：

Idris> :t Vect.take
Prelude.Vect.take : (n : Nat) -> Vect (n + m) a -> Vect n a

因此，这将进行类型检查

foo: Vect (n + 0) String -> Vect n String
foo {n} xs = take n xs

您需要一种转换Vect n a为Vect (n + 0) a：

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n+Z) a

可以使用replace以下功能：

Idris> :t replace
replace : (x = y) -> P x -> P y

但现在你需要一个证明n = n + 0。这是（与其余代码）：

plusAddZero : (n : Nat) -> n = n + 0
plusAddZero = proof
  intros
  rewrite (plusCommutative n 0)
  trivial

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n + 0) a
addNothing {n} {a} = replace {P = \m => Vect m a} (plusAddZero n)

foo : Vect n String -> Vect n String
foo {n} xs = Vect.take n (addNothing xs)

对于这样一个简单的功能来说似乎太多了。希望有人会提出更简洁的解决方案。