definieren Gleichheit von Listen Funktion

Question

Typ Getriebene Entwicklung mit Idris präsentiert diese Übung:

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys 

Allerdings habe ich versucht, es zu implementieren über:

data EqList : (xs : List a) -> (ys : List a) -> Type where 
    Same : (xs: List a) -> EqList xs xs 

sameS : (xs : List a) -> (ys : List a) -> (x: a) -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
sameS xs xs x (Same xs) = Same (x :: xs) 

same_cons : {xs : List a} -> {ys : List a} -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons {xs} {ys} eq = sameS xs ys _ eq 

ich die x in EqList (x :: xs) (x :: ys) gefolgert, weil ich m verwirrt, wie man x erhält, wenn xs und ys leer sind.

Auch die oben kompiliert, aber es scheiterte, als ich versuchte, es zu nennen:

*Exercises> same_cons (Same [1,2,3]) 
(input):Can't infer argument x to same_cons 

Answer 1

Das implizite Argument x kann nicht in Ihrem Anwendungsfall geschlossen werden, weil es keine Informationen in dem Aufruf ist same_cons (Same [1,2,3]) es zu beschränken zu irgendetwas. Wenn Sie den Typ des Ergebnisses korrigieren, erhalten Sie die Wahl x, z.

λΠ> the (EqList [0,1,2,3] [0,1,2,3]) (same_cons (Same [1,2,3])) 
Same [0, 1, 2, 3] : EqList [0, 1, 2, 3] [0, 1, 2, 3] 

seit der Wahl von [0,1,2,3] für x:xs vereint x mit 0.

BTW können Sie die Definition von same_cons da der Typ des eq Argument vereinfachen bestimmt xs und ys so können Sie Idris es ableiten lassen:

same_cons : (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons eq = sameS _ _ _ eq 

Answer 2

Um zu klären, wie man erhalten die x: Alles in Klein in Die Typendeklaration wird zu einem impliziten Argument, wenn es nicht bereits explizit ist. So

same_cons : {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

ist die gleiche wie

same_cons : {a : Type} -> {x : a} -> {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

Das ist, wo die x versteckt ist. So könnten Sie {x} auf der linken Seite der Definition verwenden, um es zu bekommen. Oder lass Idris einfach alles verarbeiten und benutze die Definition von Cactus. Bei zukünftigen Problemen mit Argumenten können Sie in der REPL :set showimplicits verwenden, um alle impliziten Argumente anzuzeigen, wenn Sie nach Typen fragen, z. :t same_cons.

Und wenn Idris den Wert für ein implizites Argument nicht ableiten kann, können Sie es, indem die resultierende Art wie Cactus hat oder stellen Sie die implizite Argument auf einen Wert helfen kann:

*> same_cons {x=0} (Same [3,2,5]) 
Same [0, 3, 2, 5] : EqList [0, 3, 2, 5] [0, 3, 2, 5]