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

Question

" 使用Idris进行类型驱动开发 "一书介绍了此练习:

定义适合签名的可能方法:

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具有外部表达式的类型,但是所有as都被s替换b.在我two'上面,我第一次用它来改变Vect (n * 2)到Vect (2 * n).这让我们mult减少.如果我们看一下mult上面,并将它应用于2ie,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)