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

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

0 голосов
/ 29 апреля 2018

Я пытаюсь написать функцию начальных сегментов для векторов, которая хранит длину вектора как фин, а не как 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))?

Спасибо

1 Ответ

0 голосов
/ 30 апреля 2018

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

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)
...