Исправление balsoft, (текущая версия) :
«взять из массива элемент по индексу со смещением» будет полнейшим угаром.
Нет, это как раз угаром не будет. Основной угар там будет с тем, чтобы всегда доказывать типы функций (т.е. если ты говоришь, что у тебя ф-ция doubleVect : Vect n Int -> Vect (n*2) Int, то тебе это нужно доказать). После этого имея Vect n Int и Fin n получить Int уже очень просто: Data.Vect.index
Исходная версия balsoft, :
«взять из массива элемент по индексу со смещением» будет полнейшим угаром.
Нет, это как раз угаром не будет. Основной угар там будет с тем, чтобы всегда доказывать типы функций (т.е. если ты говоришь, что у тебя ф-ция Vect n Int -> Vect (n*2) Int, то тебе это нужно доказать). После этого имея Vect n Int и Fin n получить Int уже очень просто: Data.Vect.index