Wie funktioniert rewrite in Idris

Ich habe mich kürzlich gefragt, ob rewrite direkt in den Typchecker eingebaut ist und ob das Konstrukt überhaupt nur mit (=) (Typ-equality) funktionieren kann.

Wie sich herausstellt ist die Antwort jein - rewrite als Syntaxkonstrukt ist an (=) gebunden, das Prinzip dahinter ist einfach nur eine - zugegeben etwas trickreiche - Funktion auf Typebene.

Beispiel

Um das ein wenig herauszuarbeiten möchte ich ein einfaches und wohlbekanntes Beispiel betrachten: Bei der Addition natürlicher Zahlen ist die 0 das neutrale Element und um das zu beweisen wird in der Regel rewrite benutzt.

Die natürlichen Zahlen mit Addition sind schnell definiert:

data Natural 
  = Null 
  | Succ Natural
  

plusN : Natural -> Natural -> Natural
plusN Null m = m
plusN (Succ n) m = Succ (plusN n m)

Strukturelle Gleichheit auf Typ-Ebene

Ähnlich wie in der Prelude benutze ich einen Typ mit einem einzigen Konstruktor Reflexiv:

data Gleich : { T : Type } -> (a : T) -> (b : T)  -> Type where
  Reflexiv : Gleich x x

Als Beispiel besagt Gleich 1 1 das 1 gleich 1 ist - das wird durch Reflexiv : Gleich 1 1 bezeugt bzw. bewiesen.

Diese unscheinbar erscheinende Definition hat weitreichende Konsequenzen: Der Typ Gleich a b kann zwar für alle möglichen Kombinationen von a und b angegeben werden, ein konkreter Typ wie Gleich (1+1) 2 ist aber genau dann bewohnt, wenn beide Komponenten strukturell gleich sind, weil eben nur genau dann Werte über Reflexiv erzeugt werden können, wenn das gilt.

Außerdem liefert ein Wert Reflexiv : Gleich a b dem Typchecker direkt die Einschränkung, dass a und b strukturell gleich sein müssen, was Idris beim Pattern Matching mit berücksichtigt, sofern Reflexiv links im Pattern steht.

Ich verwende hier strukturell übrigens ein wenig flachs - Idris reduziert/evaluiert totale Funktionen, die es im Typ sieht so weit wie möglich - deswegen wird the Gleich (plusN 0 n) n $ Reflexiv kein Problem machen, während the Gleich (plusN n 0) n $ Reflexiv nicht akzeptiert werden wird.

Zurück zum Beispiel

Interessant wird der Gleich Typ natürlich erst, wenn die Gleichheit nicht ganz so offensichtlich ist, so möchten ich zum Beispiel einen Wert vom Typ

plusNeutral0 : (n : Natural) -> Gleich (plusN Null n) n

konstruieren, um damit zu beweisen, dass 0 das links-neutrale Element der plusN Operation ist. Hier ist die Gleichheit schon nicht mehr so trivial, der Beweis ist aber noch so einfach, dass Idris diesen nach einem case-split auf n für beide Fälle automatisch findet:

plusNeutral0 : (n : Natural) -> Gleich (plusN Null n) n
plusNeutral0 Null = Reflexiv
plusNeutral0 (Succ n) = Reflexiv

das liegt natürlich daran, dass plusN entsprechend auf dem ersten Argument rekursiv definiert war.

Der noch fehlende Teil

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n

ist so auch ungleich schwerer.

Ein Anfang

Der gleiche case-split wie eben liefert:

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n
plusNeutral0Right Null = ?rhsNull
plusNeutral0Right (Succ m) = ?rhsSucc

und der Typ des ?rhsNull holes ist schon einmal angenehm einfach: Gleich Null Null - prima, das ist einfach Reflexiv:

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n
plusNeutral0Right Null = Reflexiv
plusNeutral0Right (Succ m) = ?rhsSucc

Das zweite Loch ?rhsSucc ist ein wenig komplizierter:

- + rhsSucc [E]
 `--  m : Natural
     ------------------------------------------------------------
      rhsSucc : Gleich (Succ (plusN m Null)) (Succ m)

hier hat Idris keine Chance die Lösung automatisch zu finden, einfach schon, weil kein Konstruktor von plusN direkt passt und so plusN nicht weiter reduziert werden kann.

Induktiv

Innerhalb steht ja aber plusN m Null, was ziemlich genau dem entspricht, was ich beweisen möchte, nur das hier m statt n = Succ m steht.

Offensichtlich hilft also Induktion weiter:

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n
plusNeutral0Right Null = Reflexiv
plusNeutral0Right (Succ m) =
  let induktion = plusNeutral0Right m in ?rhsSucc

mit einem verfeinerten Loch:

- + rhsSucc [E]
 `--  m : Natural
      induktion : Gleich (plusN m Null) m
     ------------------------------------------------------------
      rhsSucc : Gleich (Succ (plusN m Null)) (Succ m)

irgendwie, muss ich also noch das Succ da rein bekommen, was genau die Aufgabe von rewrite wäre!

auf dem Weg zum rewrite

Was ich also möchte ist folgendes:

  • Wenn ich weiß, dass Gleich a b ist
  • Dann möchte ich folgern, dass Gleich (Succ a) (Succ b) ist.

Als Funktion ausgedrückt ist das recht einfach:

gleichSuccGleich : (Gleich a b) -> (Gleich (Succ a) (Succ b))
gleichSuccGleich Reflexiv = Reflexiv

damit ist der Beweis dann eigentlich fertig:

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n
plusNeutral0Right Null = Reflexiv
plusNeutral0Right (Succ m) =
  let induktion = plusNeutral0Right m in gleichSuccGleich induktion

Verallgemeinerung

rewrite ist aber etwas flexibler - es geht nicht unbedingt um Succ es geht darum von einem Typ-Ausdruck, in dem b vorkommt auf einem Ausdruck zu schließen, in dem alle b durch a ersetzt wurden, wenn ich nur weiß, dass Gleich a b ist.

Die Richtung ist mag hier etwas willkürlich anmuten - ich habe sozusagen geschummelt: Ich weiß was ich brauche ;)

Als Funktion ausgedrückt ist das in etwa:

umschreiben : (Ausdruck : x -> Type) -> (Gleich a b) -> (Ausdruck b -> Ausdruck a)

Der Beweis ist recht simpel, sobald man einen case-split auf das zweite Argument (für Gleich a b) gemacht hat - hierfür kommt ja nur Reflexiv in Frage (das ist der einzige Konstruktor von Gleich) und der schränkt dann den Ausdruck so ein, dass a gleich b sein muss, somit ist natürlich auch Ausdruck a genau das gleiche wie Ausdruck b und mit ausdruck wurde schon ein entsprechender Wert angegeben:

umschreiben : (Ausdruck : x -> Type) -> (Gleich a b) -> (Ausdruck b -> Ausdruck a)
umschreiben _ Reflexiv ausdruck = ausdruck

Der Ausdruck ist jetzt ein wenig trickreich: induktion liefert Gleich (plusN m Null) m also a = plusN m Null und b = m und gesucht ist Gleich (Succ (plusN m Null)) (Succ m)

Damit muss ausdruck = \x -> Gleich (Succ x) (Succ m) sein, was auch zum Ziel führt:

plusNeutral0Right : (n : Natural) -> Gleich (plusN n Null) n
plusNeutral0Right Null = Reflexiv
plusNeutral0Right (Succ m) =
  let induktion = plusNeutral0Right m in
  umschreiben (\x => Gleich (Succ x) (Succ m)) induktion Reflexiv

Die Suche nach diesem Ausdruck erspart mir Idris natürlich mit dem eingebauten rewrite:

plusNeutral0Right : (n : Natural) -> plusN n Null = n
plusNeutral0Right Null = Refl
plusNeutral0Right (Succ m) =
  let induktion = plusNeutral0Right m in
  rewrite induktion in Refl

aber im Prinzip funktioniert das genau so.