Idris - 自定义依赖数据类型的映射函数失败 [英] Idris - map function on custom dependent data type fails

问题描述

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

中缀 1 :::数据元组向量:Nat ->纳特->类型 ->输入哪里空:TupleVect Z Z a(:::) : (Vect o a, Vect p a) ->TupleVect n m a ->TupleVect (n+o) (m+p) a示例TupleVect : TupleVect 5 4 IntexampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: 空

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

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

tupleVectMap : ((Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->TupleVect n m a ->元组向量 n m btupleVectMap f Empty = EmptytupleVectMap f (x ::: xs) = 让失败 = f x在 ?rest_of_definition 中

这会产生以下类型错误:

<代码> |20 |tupleVectMap f (x ::: xs) = 让失败 = f x|~~~~~~~~~~~~~~~~~~使用预期类型检查 tupleVectMap 的右侧时TupleVect (n + o) (m + p) b类型不匹配(Vect o a, Vect p a)和(向量 k a, 向量 l a)

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

自从以下类型检查后，我更加困惑:

tupleVectMap' : TupleVect n m a ->元组向量 n m btupleVectMap' 空 = 空tupleVectMap' (x ::: xs) =让非失败 = f x在 ?rest_of_definition 中在哪里f : ((Vect k a, Vect l a) -> (Vect k b, Vect l b))

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

解决方案

如果你在 refl 中 :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 只接受长度为 k 的 Vects.>

虽然在 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 ->元组向量 n m b

I am relatively new to idris and dependent-types and I encountered the following problem - I created a custom data type similar to vectors:

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

It is inductively constructed by adding tuples of vectors and indexed by the sum of the vector lengths in each tuple position.

I tried to implement a map function for my data type:

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

This yields the following type error:

   |
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)

It seems that the typechecker can't unify the lengths of the vectors in the extracted tuple x and the required lengths in the argument of f. However I don't understand why that is since k and l are just the type names indicating that f doesn't change the length of the given vectors.

I am even more perplexed since the following typechecks:

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))

Here f has the exact same type signature. The only difference being that f is defined locally.

解决方案

If you :set showimplicits in the refl you'll see the difference between the two functions.

In tupleVectMap is

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)

Because k and o (l and p) are not necessary equal, x cannot be applied to f. Basically, if you call tupleVectMap, you already determined that f only accepts Vects of length k.

While in tupleVectMap' it is

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)

Here f takes two implicit arguments to set the length of the Vects whenever it gets called. So f x {k=o} {l=p} works (though you don't have to specify the implicit arguments).

It will work as well if you define your function type as

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

这篇关于Idris - 自定义依赖数据类型的映射函数失败的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！