如何改写：Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a

Question

我被 Idris 困住了（再次叹息）。我正在使用第 10 章的 Idris 书中的类型驱动开发进行合并排序练习。我有这个：

import Data.Vect
import Data.Vect.Views

sort2 : Ord a => (l: a) -> (r: a) -> (a, a)
sort2 l r = if l <= r then (l, r) else (r, l)

needHelp :  Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a
needHelp {n=(S n)} {m=(S m)} (x :: xs) = ?help

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  needHelp (f :: s :: (vectMerge xs ys))

我已经隔离了needHelp函数，所以你可以看到我想要实现的重写。我试过这个：

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  let tail = (rewrite plusSuccRightSucc n m in s :: vectMerge xs ys) in
  f :: tail

但伊德里斯抱怨道：

When checking right hand side of Main.case block in vectMerge with expected type
        Vect (S (plus n (S m))) a

rewriting S (plus n m) to plus n (S m) did not change type letty

我不明白为什么这不起作用。非常感谢帮助。

Answer 1

rewrite 与您的 当前目标 有关，而不是您试图用来解决目标的术语（我试图在 ).

所以，这是一个可能的解决方案：

import Data.Vect

sort2 : Ord a => (l: a) -> (r: a) -> (a, a)
sort2 l r = if l <= r then (l, r) else (r, l)

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  rewrite sym $ plusSuccRightSucc n m in
  (f :: s :: (vectMerge xs ys))

sym in sym $ plusSuccRightSucc n m 反转 rewrite 的方向。

如何改写：Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a

How to rewrite: Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a

idris