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

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' 的定义一样。 (在 REPL 上运行 :t replace，如果你想看看如何以困难的方式做到这一点)在 rewrite foo in bar 构造中， foo 是 a = b 类型的东西， bar 具有外部表达式的类型，但所有 a s 都被 b s 替换。在上面的 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

然后问 idris :

*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)