idris – 统一算法推断出太具体的类型

我试图在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
点赞