我试图在 Idris 中创建大小为 n 的元组:
module NTuple
data Tuple : Vect n Type -> Type where
EmptyTuple : Tuple Nil
TupleItem : a -> Tuple types -> Tuple (a :: types)
mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN fZ f (TupleItem x xs) = TupleItem (f x) xs
mapN (fS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
但我在最后一行收到此错误:
When elaborating left hand side of mapN: When elaborating an application of NTuple.mapN: Can't unify Tuple (a :: types) with Tuple (insertAt (fS i) a types) Specifically: Can't unify a :: types with insertAt (fS i) a types
有没有办法让这个功能起作用?
最佳答案
问题是insertAt (FS i) a types
无法在不了解 types
的情况下减少.如果我们知道 types = t :: ts
那么它可以减少到t :: insertAt i ts
.
但在 mapN
的第二种情况下,我们确实知道 types
正是这种形式:
FS i
n = S m
一些 m
... types
参数类型为 Vect (S m) Type
t :: ts
! 一旦我们向 idris 指出这一点,很高兴减少
insertAt (FS i) a types
因此,您的代码类型检查:mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN FZ f (TupleItem x xs) = TupleItem (f x) xs
mapN {types = _ :: _} (FS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
mapN {types = []} (FS i) _ _ = absurd i
关于idris - 统一算法推断出过于具体的类型,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25063219/