vector - Idris - 自定义相关数据类型的映射函数失败

Question

我对 idris 和依赖类型相对较新，遇到了以下问题 - 我创建了一个类似于向量的自定义数据类型:

infixr 1 :::

data TupleVect : Nat -> Nat -> Type -> Type where
    Empty : TupleVect Z Z a
    (:::) : (Vect o a, Vect p a) ->
            TupleVect n m a ->
            TupleVect (n+o) (m+p) a

exampleTupleVect : TupleVect 5 4 Int
exampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: Empty

它是通过添加向量元组来归纳构造的，并通过每个元组位置的向量长度之和进行索引。

我尝试为我的数据类型实现映射函数:

tupleVectMap : ((Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->
               TupleVect n m a -> TupleVect n m b
tupleVectMap f Empty = Empty
tupleVectMap f (x ::: xs) = let fail = f x
                            in ?rest_of_definition

这会产生以下类型错误:

   |
20 | tupleVectMap f (x ::: xs) = let fail = f x
   |                             ~~~~~~~~~~~~~~ ...
When checking right hand side of tupleVectMap with expected type
        TupleVect (n + o) (m + p) b

Type mismatch between
        (Vect o a, Vect p a)
and
        (Vect k a, Vect l a)

类型检查器似乎无法统一向量的长度在提取的元组 x 中以及 f 的参数中所需的长度。然而我不理解为什么会这样，因为 k 和 l 只是类型名称，表明f 不会改变给定向量的长度。

由于以下类型检查，我更加困惑:

tupleVectMap' : TupleVect n m a -> TupleVect n m b
tupleVectMap' Empty = Empty
tupleVectMap' (x ::: xs) =
    let nonfail = f x
    in ?rest_of_definition
      where
        f : ((Vect k a, Vect l a) -> (Vect k b, Vect l b))

这里 f 具有完全相同的类型签名。唯一的区别是 f 是本地定义。

Answer 1

如果您:set showimplicits在引用中您将看到这两个函数之间的差异。

在 tupleVectMap是

f : (Data.Vect.Vect k a, Data.Vect.Vect l a) ->
    (Data.Vect.Vect k b, Data.Vect.Vect l b)
x : (Data.Vect.Vect o a, Data.Vect.Vect p a)

因为k和o ( l 和 p )不一定相等， x不能应用于f 。基本上，如果您调用tupleVectMap ，您已经确定 f只接受Vect长度k .

在tupleVectMap'期间这是

f : {k : Prelude.Nat.Nat} -> {l : Prelude.Nat.Nat} ->
    (Data.Vect.Vect k a, Data.Vect.Vect l a) ->
    (Data.Vect.Vect k b, Data.Vect.Vect l b)
x : (Data.Vect.Vect o a, Data.Vect.Vect p a)

这里f使用两个隐式参数来设置 Vect 的长度每当它被调用时。所以f x {k=o} {l=p}有效(尽管您不必指定隐式参数)。

如果您将函数类型定义为

，它也会起作用

tupleVectMap : ({k, l : Nat} -> (Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->
               TupleVect n m a -> TupleVect n m b