自定义依赖数据类型上的Idris - map函数失败
自定义依赖数据类型上的Idris - map函数失败
提问于 2018-06-09 05:55:58
我对idris和dependent-types比较陌生，我遇到了以下问题--我创建了一个类似于向量的自定义数据类型：
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是在本地定义的。
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-06-09 08:13:21
如果你在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 -> TupleVect n m b页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/50768877
复制相关文章
相似问题