Наткнулся.
У обычных векторов типы элементов не зависят от позиции. Это просто вектора, вектора векторов (матрицы) и тп.
Но можно определить вектор, у которого тип элемента от позиции зависит:
Это нижне-треугольные матрицы, ленточные матрицы (ну, нижняя часть ленты).
Вроде, полезная штука.
Однако реализацию операции reverse я для неё придумать не могу.
reverse можно определить для векторов фиксированной длины. Наверное. ;)
Но можно определить вектор, у которого тип элемента от позиции зависит:
data DVec {n : Nat} {e : Nat -> Set} : Set1 where DNil : DVec zero (e zero) DCons : {n : Nat} -> {e : Nat -> Set} -> (e (succ n)) -> DVec n e -> DVec (succ n) (e (succ n))(Agda2, не проверял за отсутствием на компьютере)
Это нижне-треугольные матрицы, ленточные матрицы (ну, нижняя часть ленты).
Вроде, полезная штука.
Однако реализацию операции reverse я для неё придумать не могу.
reverse можно определить для векторов фиксированной длины. Наверное. ;)