Наткнулся.

[thesz]

У обычных векторов типы элементов не зависят от позиции. Это просто вектора, вектора векторов (матрицы) и тп.

Но можно определить вектор, у которого тип элемента от позиции зависит:
data DVec {n : Nat} {e : Nat -> Set} : Set1 where

Comments

[nivanych]

В Agda Set имеет тип Set1,
а Set1 имеет тип Set2 ?

[thesz]

По-моему, так.

[nivanych]

А вот так получится --
data TVec {T : Set1} : Nat -> Set1 where
TNil : TVec zero
TCons : {n : Nat} -> {dtp : T} -> (x : dtp) -> TVec n -> TVec (suc n)
?

[thesz]

А как ты это дело извлекать будешь?

Сравнение с образцом по (TCons x xs) какой тип присвоит x?

Это та же проблема унификации с внутренним forall.
data V =
N
| forall t . C t V

[nivanych]

Может быть, получится сравнение с образцом по
TCons (x:t) xs
?

Если не получится, то придётся
явно тип прописывать.
Надо бы уже поставить Agda,
да просмотреть снова документацию.
А то чуйствую, что вопросы дурацкие.

Ничего, после 11-12 освобожусь.

[thesz]

Это будет, вообще-то, преобразование типов.

Не пойдет. ;)

[thesz]

"Функцию вызвать нужную" - а какую?

Функция может на вход принимать квадратные матрицы и считать, что элементы выше диагонали нулевые. Можно ли это показать в её типе? Можно. Как этот тип будет выглядеть? А вот примерно так, как показано выше.

Можно сэкономить память, опять же.

[thesz]

Специальный тип лучше тем, что лучше обозначает контракт.

Ты просто не сможешь вызвать fooLowerT для плотной матрицы, в которой каждый элемент может быть не равен 0. Тебе придётся соорудить доказательство, что твоя матрица нижнетреугольная и только после этого ты сможешь вызвать fooLowerT.

[nealar]

Вкуришь меня в Агду на MskHUG?
Ещё я ttfp заканчиваю читать, что взять следующей книжкой?

[thesz]

Уж насколько я её сам осилил, не более. ;)