我试图在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)
但是我在最后一行得到了这个错误:
06001
有没有办法让这个功能起作用?
最佳答案 问题是insertAt(FS i)在不知道任何类型的情况下不能减少类型.如果我们知道types = t :: ts那么它可以简化为t :: insertAt i ts.
但是在mapN的第二种情况下,我们知道类型正是这种形式:
>我们的第一个论点是FS i
>暗示n = S m对于某些m …
>意味着我们的隐式类型参数具有类型Vect(S m)Type
>这意味着它的形式为t :: ts!
一旦我们将其指向Idris,它很乐意减少insertAt(FS i)类型,因此,您的代码类型检查:
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