(xs : Vect n elem) -> Vect (n * 2) 元素

Question

本书 Type Driven Development with Idris 介绍了这个练习：

Define a possible method that fits the signature:

two : (xs : Vect n elem) -> Vect (n * 2) elem

我试过了：

two : (xs : Vect n elem) -> Vect (n * 2) elem
two xs = xs ++ xs

但是我得到以下错误：

*One> :r
Type checking ./One.idr
One.idr:9:5:When checking right hand side of two:
Type mismatch between
        Vect (n + n) elem (Type of xs ++ xs)
and
        Vect (mult n 2) elem (Expected type)

Specifically:
        Type mismatch between
                plus n n
        and
                mult n 2
Holes: Hw1.two

如果我有一个大小为 N 的向量，并且需要一个大小为 N*2 的向量，那么将它附加到自身似乎是合理的。

我做错了什么？

Answer 1

简答

将类型签名更改为 two : (xs : Vect n elem) -> Vect (n + n) elem。

如果你真的需要那样

要达到 Vect (n * 2) elem 有点复杂。这里：

two' : Vect n elem -> Vect (n * 2) elem
two' {n} xs = rewrite multCommutative n 2 in rewrite plusZeroRightNeutral n in xs ++ xs

您收到该错误消息的原因是类型检查中的相等性是还原为正常形式后的相等性。 n + n 和 mult n 2 相等，但它们的正常形式不同。（mult n 2 是 n * 2 解析类型类后的结果。）

你可以这样看mult的定义：

*kevinmeredith> :printdef mult
mult : Nat -> Nat -> Nat
mult 0 right = 0
mult (S left) right = plus right (mult left right)

它通过对第一个参数进行模式匹配来工作。由于 two 类型签名中的第一个参数是 n，因此根本无法减少 mult。 multCommutative 将帮助我们翻转它：

*kevinmeredith> :t multCommutative 
multCommutative : (left : Nat) ->
                  (right : Nat) -> left * right = right * left

我们应用平等的最佳工具是 rewrite，就像我对 two' 的定义一样。（运行 :t replace 在 REPL 中，如果你想看看如何以困难的方式做到这一点）在 rewrite foo in bar 结构中，foo 是 a = b 类型的东西bar 具有外部表达式的类型，但所有 a 都被 b 替换。在我上面的two'中，我首先用它把Vect (n * 2)改成了Vect (2 * n)。这让 mult 减少。如果我们查看上面的 mult，并将其应用于 2，即 S (S Z) 和 n，您会得到 plus n (mult (S Z) n，然后是 plus n (plus n (mult Z n))，然后然后 plus n (plus n Z)。你不必自己计算减少量，你可以只应用重写并在末尾打一个洞：

two' : Vect n elem -> Vect (n * 2) elem
two' {n} xs = rewrite multCommutative n 2 in ?aaa

然后问伊德里斯：

*kevinmeredith> :t aaa
  elem : Type
  n : Nat
  xs : Vect n elem
  _rewrite_rule : plus n (plus n 0) = mult n 2
--------------------------------------
aaa : Vect (plus n (plus n 0)) elem

plus n Z 不会归约，因为 plus 是由第一个参数的递归定义的，就像 mult 一样。 plusZeroRightNeutral 为您提供所需的平等：

*kevinmeredith> :t plusZeroRightNeutral 
plusZeroRightNeutral : (left : Nat) -> left + 0 = left

我再次使用与 rewrite 相同的技术。

:search 可让您在图书馆中搜索特定类型的居民。你会经常发现有人已经为你完成了证明事情的工作。

*kevinmeredith> :s (n : Nat) -> n + 0 = n
= Prelude.Nat.multOneLeftNeutral : (right : Nat) ->
                                   fromInteger 1 * right = right


= Prelude.Nat.plusZeroRightNeutral : (left : Nat) ->
                                     left + fromInteger 0 = left


*kevinmeredith> :s (n, m : Nat) -> n * m = m * n
= Prelude.Nat.multCommutative : (left : Nat) ->
                                (right : Nat) -> left * right = right * left

（此答案适用于 Idris 版本 0.9.20.1）

(xs : Vect n elem) -> Vect (n * 2) 元素

(xs : Vect n elem) -> Vect (n * 2) elem

idris

简答

如果你真的需要那样