Идрис: Написание функции начальных сегментов для векторов с длиной как фин, а не как натуральный

Question

Я пытаюсь написать функцию начальных сегментов для векторов, которая хранит длину вектора в виде Fin, а не Nat, следующим образом:

vectorsInits : Vect n t -> Vect n (p ** Vect (finToNat p) t)
vectorsInits Nil = Nil
vectorsInits (x::xs) = ((FS FZ) ** (x::Nil)) :: map (\(p ** ys) => ((FS p) ** x::ys)) (vectorsInits xs)

Это определение не работает, однако, как я получаю следующую ошибку типа:

When checking right hand side of vectorsInits with expected type

    Vect (S len) (p : Fin n ** Vect (finToNat p) t)

When checking argument pf to constructor Builtins.MkDPair:

    Type mismatch between

            Vect 1 t (Type of [x])

    and

            Vect (finToNat (FS FZ)) t (Expected type)

    Specifically:

            Type mismatch between

                    1

            and

                    finToNat (FS FZ)

Но из определения finToNat ясно, что finToNat (FS FZ) будет равен 1,. даже если я напишу следующую функцию, чтобы попытаться заставить idris понять, что они равны, я получу ошибку:

intproof : Vect 1 t -> Vect (finToNat (FS FZ)) t 
intproof x = x
...
vectorsInits (x::xs) = ((FS FZ) ** intproof (x::Nil)) :: map (\(p ** ys) => ((FS p) ** x::ys)) (vectorsInits xs)

дает мне ошибку:

When checking right hand side of vectorsInits with expected type
        Vect (S len) (p : Fin n ** Vect (finToNat p) t)
When checking argument pf to constructor Builtins.MkDPair:
    Type mismatch between
            Vect (finToNat (FS FZ)) t (Type of intproof [x])
    and
            (\p => Vect (finToNat p) t) (FS FZ) (Expected type)
    Specifically:
            Type mismatch between
                    1
            and
                    finToNat (FS FZ)

даже писать:

intproof : Vect 1 t -> (\p => Vect (finToNat p) t) (FS FZ)
intproof x = x

получает ту же ошибку, что и выше

У меня есть% по умолчанию всего, и я импортирую Data.Vect в начале моего файла.

Есть ли способ заставить Idris признать, что finToNat (FS FZ) равен 1 (то есть S Z))?

Спасибо

Answer 1

У вас есть проблема:

vectorsInits : Vect n t -> Vect n (p ** Vect (finToNat p) t)

Какой тип p? Вы не дали это, и это на самом деле заканчивается

vectorsInits : Vect n t -> Vect n (p : Fin m ** Vect (finToNat p) t)

То есть тип FinОн работает рядом с вашими данными, совершенно не связан с вводом. Это не правильно. Это должно быть (по крайней мере)

vectorsInits : Vect n t -> Vect n (p : Fin n ** Vect (finToNat p) t)

Однако это не совсем верно. Что должно произойти, так это то, что FinСчитать от FZ в last по мере того, как вы переходите к выводу, но ваша текущая реализация этого не делает. Если вы измените его, вы заметите, что каждый выходной вектор в конечном итоге будет иметь длину на единицу больше, чем индекс:

vectorsInits : Vect n t -> Vect n (p : Fin n ** Vect (S (finToNat p)) t)
vectorsInits [] = []
vectorsInits (x :: xs) = (FZ ** [x]) :: map (\(idx ** ixs) => (FS idx ** x :: ixs)) (vectorsInits xs)

Или вы можете прикрепить [] к началу вывода (в конце концов, [] является префиксом каждого списка), и, таким образом, получить версию, которая соответствует идентичности index n (vectorInits xs) = take n xs (некоторые искажения опущены):

vectorsInits : Vect n t -> Vect (S n) (p : Fin (S n) ** Vect (finToNat p) t) 
vectorsInits [] = [(FZ ** [])] 
vectorsInits (x :: xs) = (FZ ** []) :: map (\(idx ** ixs) => (FS idx ** x :: ixs)) (vectorsInits xs)