4

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

有没有办法让这个功能发挥作用？

4

1 回答 1

2

问题是，insertAt (FS i) a types如果不知道任何关于types. 如果我们知道types = t :: ts，那么它可以简化为t :: insertAt i ts.

但在 的第二种情况下mapN，我们确实知道这types正是这种形式：

  1. 我们的第一个论点是FS i
  2. 暗示n = S m一些m...
  3. 意味着我们的隐式types参数具有类型Vect (S m) Type
  4. 这意味着它的形式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
于 2014-12-09T01:56:13.097 回答