Тип отбивной Идрис

Question

Я пытаюсь написать функцию chop в Идрисе.Эквивалент Haskell будет выглядеть так:

chop :: Int -> [t] -> [[t]]
chop n [] = []
chop n v = take n v : chop n (drop n v)

моя первоначальная попытка в Идрисе выглядит так:

chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop n Nil = Nil
chop n v = (take n v) :: (chop n (drop n v))

ошибка проверки типа:

Type mismatch between
               Vect 0 a (Type of [])
       and
               Vect (mult k n) a (Expected type)

       Specifically:
               Type mismatch between
                       0
               and
                       mult k n

Answer 1

k все еще может быть установлен в качестве аргумента, то есть chop {k=3} Z [] приведет к [[], [], []] : Vect 3 (Vect Z a).Ваша реализация вернет chop n Nil = [], поэтому система типов Идриса правильно жалуется.: -)

Вам необходимо учитывать k:

chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop {k} n v = ?hole

Если вы хотите фактическую реализацию, вот спойлер:

Другой подход заключается в том, чтобы указать, какмного блоков, которые вы хотите, а не размер каждого блока.

chop' : (k : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop' Z v = []
chop' {n} (S k) v = take n v :: chop k (drop n v)

n должен находиться в области видимости для вызова take и drop.