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

这本书使用 Idris 进行类型驱动开发 https://www.manning.com/books/type-driven-development-with-idris提出这个练习：

定义一个适合签名的可能方法：

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

I tried:

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 的向量，那么将其附加到自身似乎是合理的。

我究竟做错了什么？

简短回答

将类型签名更改为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 and 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 is n, mult根本无法减少。multCommutative将帮助我们扭转局面：

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

我们应用平等的最佳工具是rewrite，就像我的定义一样two'. (run :t replace如果你想看看如何以困难的方式做到这一点，请在 REPL 中）rewrite foo in bar建造，foo是某种类型的东西a = b and bar具有外部表达式的类型，但与所有as 替换为bs。在我的two'上面我先用它来改变Vect (n * 2) to Vect (2 * n)。这让mult减少。如果我们看一下mult上面，并将其应用到2 i.e. S (S Z) and 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 again.

: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）