功能仅在翻转时有效

Question

为什么会出错？

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

Answer 1

错误来自 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

或

> 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

功能仅在翻转时有效

Function only works when flipped

idris