Блог

Я пытаюсь перезагрузить исходный файл, содержащий следующую функцию Idris 2 в REPL:

 ||| 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 (потому что я не думаю, что мне удалось закодировать это отношение в функцию)?

Вы можете доказать это n 0 = n , используя правило перезаписи plusZeroRightNeutral в Data.Nat .

Возможно, вы захотите немного переосмыслить эту функцию.

Вы можете создать векторную карту довольно тривиально:

 my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map fn [] = []
my_vect_map fn (x :: xs) = fn x :: my_vect_map fn xs
 

Редактировать

Вот хвостовая рекурсивная версия map :

 mutual
  rhs : {m : Nat} -> (a -> b) -> a -> Vect m b -> Vect len a -> Vect (plus m (S len)) b
  rhs f x acc xs = rewrite sym $ plusSuccRightSucc m len in my_vect_map' f (f x :: acc) xs

  my_vect_map' : {m : Nat} -> (a -> b) -> Vect m b -> Vect n a -> Vect (m   n) b
  my_vect_map' f acc [] = rewrite plusZeroRightNeutral m in acc
  my_vect_map' f acc (x :: xs) = rhs f x acc xs

my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map f = reverse . my_vect_map' f []
 

Единственная цель rhs — показать len размер xs .

Мы также использовали {} для приведения переменных типа в область видимости на уровне значений.

Надеюсь, это поможет.