Блог

Я выбираю между параметризацией моего типа на Vect r Nat «и List Nat «. Сначала я подумал, что с помощью первого я могу ограничить длину вектора следующим образом

 foo : Vect m Nat -> Vect m Nat -> Vect (2 * m) Nat
 

и это делает Vect его более мощным, но потом я понял, что могу сделать то же самое, хотя и более подробно, со списками и доказательствами

 foo : (x : List Nat) -> (y : List Nat)
      -> {auto _ : length x = length y} -> List (2 * length x) Nat
 

Теперь мне интересно, является ли это в целом правдой. Отличается ли параметризация со значениями от использования функций уровня типа с доказательствами?