Der Vereinheitlichungsalgorithmus leitet zu konkrete Typen ab

Question

Ich habe versucht, Tupel der Größe n in Idris zu erstellen:

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)

Aber ich erhalte in der letzten Zeile diesen Fehler:

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

Gibt es eine Möglichkeit, diese Funktion zum Laufen zu bringen?

Answer 1

Das Problem ist, dass insertAt (FS i) a types kann nicht reduziert werden, ohne etwas darüber zu wissen types.Wenn wir es wüssten types = t :: ts dann könnte es reduziert werden auf t :: insertAt i ts.

Aber im zweiten Fall von mapN, Wir Tun weiß das types hat genau diese Form:

1. Unser erstes Argument ist FS i
2. Implizieren n = S m für einige m...
3. Das heißt unser implizites types Argument hat Typ Vect (S m) Type
4. Das heißt, es hat die Form t :: ts!

Sobald wir Idris darauf aufmerksam machen, wird es gerne reduziert insertAt (FS i) a types und somit überprüft Ihr Code Folgendes:

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