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

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

我试图为我的数据类型实现一个map函数:

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)

似乎typechecker无法统一提取的元组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在refl中,你会看到两个函数之间的区别.

在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只接受Vects长度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有两个隐式参数来设置Vects被调用时的长度.这样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