为什么不能解决`n`和`plus n 0`之间的约束？

问题描述

我正在尝试在 REPL 上重新加载包含以下 Idris 2 函数的源文件：

||| Apply a function across all elements of a vector.
||| @function The function to apply.
||| @input_vector The vector whose elements will be given as an argument to the function.
my_vect_map : (function : a -> b) -> (input_vector : Vect n a) -> Vect n b
my_vect_map function Nil = Nil
my_vect_map function (head :: tail) =
  (my_vect_map' ((function head) :: Nil) tail) where
    my_vect_map' : (accumulator : Vect length_b b) -> Vect length_a a -> Vect (length_b + length_a) b
    my_vect_map' accumulator Nil = accumulator
    my_vect_map' accumulator (head' :: tail') =
      my_vect_map' (accumulator ++ ((function head') :: Nil)) tail'

但它无法通过错误进行类型检查：

Error: While processing right hand side of my_vect_map. While processing right hand side
of my_vect_map,my_vect_map'. Can't solve constraint
between: length_b (implicitly bound at page_75_section_3_2_exercises_solutions.idr:89:5--89:47) and plus length_b 0.

page_75_section_3_2_exercises_solutions.idr:89:36--89:47
    |
 89 |     my_vect_map' accumulator Nil = accumulator
    |                                    ^^^^^^^^^^^

Error(s) building file page_75_section_3_2_exercises_solutions.idr

为什么类型检查器不能解决 length_b 和 plus length_b 0 之间的约束？我做错了什么，我该如何纠正？我尝试手动完成一些示例，似乎成功了：

my_vect_map id [] => Nil => []

my_vect_map id ['a'] => my_vect_map id ('a' :: Nil) => my_vect_map' ((id 'a') :: Nil) Nil => my_vect_map' ('a' :: Nil) Nil => ('a' :: Nil) => ['a']
                                                                                                          ^length_b=1  ^length_a=0            ^length=1=length_b+length_a

my_vect_map id ['a','b'] => my_vect_map id ('a' :: ('b' :: Nil)) => my_vect_map' ((id 'a') :: Nil) ('b' :: Nil) => my_vect_map' ('a' :: Nil) ('b' :: Nil) => my_vect_map' (('a' :: Nil) ++ ((id 'b') :: Nil)) Nil => my_vect_map' (('a' :: Nil) ++ ('b' :: Nil)) Nil => my_vect_map' ('a' :: ('b' :: Nil)) Nil => ('a' :: ('b' :: Nil)) => ['a','b']
                                                                                                                                 ^length_b=1  ^length_a=1                                                                                                                             ^length_b=2           ^length_a=0                     ^length=2=length_b+length_a

另外，我如何让类型检查器意识到 length_b + length_a 等于 n（因为我认为我没有设法将这种关系编码到函数中）？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）