Функция работает только при переворачивании

Почему ошибка?

import Data.Vect
import Data.Vect.Quantifiers

get : (i : Fin n) -> All (flip Vect t) ls -> Vect (index i ls) t
get FZ (y :: z) = y
get (FS y) (z :: w) = get y w

nproject : Vect l (n : _  ** Fin (index n ls)) -> All (flip Vect t) ls -> Vect l t
nproject [] _ = []
nproject ((n ** i)::fs) vs = index i (get n vs) :: nproject fs vs

Это работает, только если я переверну nproject:

*VectExtensions> flip nproject [[0]] [(0 ** 0)]
[0] : Vect 1 Integer
*VectExtensions> nproject [(0 ** 0)] [[0]]
When checking argument pf to constructor Builtins.MkDPair:
        Type mismatch between
                IsJust (Just x)
        and
                IsJust (integerToFin 0 n)

Но это работает с явным ls:

*VectExtensions> nproject {ls=[_]} [(0 ** 0)] [[0]]
[0] : Vect 1 Integer

idris
person michaelmesser    schedule 05.02.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Ошибки исходят от integerToFin : Integer -> (n : Nat) -> Maybe (Fin n). Он используется REPL, потому что вы используете (0 ** 0) вместо (FZ ** FZ). REPL знает, что это всего лишь синтаксис, и вам действительно нужен Fin n, а не Integer. Таким образом, REPL сначала пытается преобразовать, и (0 ** 0) становится внутренним (integerToFin 0 n ** integerToFin 0 m). Из-за реализации вывода типа он думает о случае n=Z. А так integerToFin 0 Z = Nothing вместо Just Fin n.

Чтобы решить эту проблему, вы можете немного помочь:

> nproject [(FZ ** 0)] [[0]] 
[0] : Vect 1 Integer

Or

> nproject [(0 ** FZ)] [[0]] 
[0] : Vect 1 Integer

Итак, почему эта ошибка?

Это зависит от реализации вывода типа компилятора, и если я вижу это правильно, то он просто недостаточно умен для этого случая. :-)

Думаю проблема примерно в следующем:

Это :t nproject:

nproject : Vect l (n : Fin n ** Fin (index n ls)) -> All (flip Vect t) ls -> Vect l t

n может быть 0 и, следовательно, integerToFin 0 0 = Nothing.

В перевернутом случае известно, что n равно 1, потому что он пытается вывести неявные аргументы и [[0]] перед (0 ** 0). Тогда REPL может сделать вывод, что integerToFin 0 (S Z) = Just FZ

person xash    schedule 06.02.2018