如何重写: Vect (S (S (n +m)a -> Vect (S (+n (S )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

但Idris抱怨道：

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与你当前的目标有关，而不是你试图用来解决目标的术语的wrt (我试图用this answer来说明它)。

因此，这里有一个可能的解决方案：

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 $ plusSuccRightSucc n m中的sym与rewrite的方向相反。