函数只在翻转时起作用。
函数只在翻转时起作用。
提问于 2018-02-05 22:51:40
为什么会出错？
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回答 1
Stack Overflow用户
回答已采纳
发布于 2018-02-06 12:54:28
错误来自于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 tn可以是0，因此也可以是integerToFin 0 0 = Nothing。
在翻转的情况下，n被称为1，因为它试图在(0 ** 0)之前推断隐式参数和[[0]]。然后，REPL可以推断出integerToFin 0 (S Z) = Just FZ
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/48632794
复制相关文章
相似问题
腾讯云开发者
