Idris - 自定义相关数据类型的映射函数失败
Idris - map function on custom dependent data type fails
我对 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 是
本地定义。
如果您 :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
只接受长度为 k
.
的 Vect
s
而在 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
我对 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 是 本地定义。
如果您 :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
只接受长度为 k
.
Vect
s
而在 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