Gibt es eine einfache Möglichkeit, Gleichheit ( DecEq ) Instanzen für Datentypen zu schreiben? Zum Beispiel möchte ich, dass das Folgende in seiner DecEq -Deklaration O (n) -Zeilen enthält, wobei ?p etwas Einfaches ist:
David Christiansen arbeitet an etwas, um dies im Allgemeinen zu automatisieren, und er ist im Wesentlichen fertig; Es kann in seinem GitHub-Repository gefunden werden . In der Zwischenzeit ist hier ein Ansatz, der Sie in dieser Situation von O (n ^ 2) Fällen zu O (n) Fällen führen kann. Zuerst einige Vorbemerkungen. Wenn Sie etwas mit Decidable-Gleichheit haben und eine Injektion vom Typ Ihrer Wahl zu diesem Typ haben, können Sie eine Entscheidungsprozedur für diesen Typ treffen:
%Vor%Leider führt der direkte Nachweis, dass Ihre Funktion eine Injektion ist, zu O (n ^ 2) Fällen, aber im Allgemeinen ist jede Funktion mit einer Retraktion injektiv:
%Vor%Wenn Sie also eine Funktion vom Typ Ihrer Wahl zu einer mit entscheidbaren Gleichheit und einer Zurückziehung für sie haben, dann haben Sie eine entscheidbare Gleichheit für Ihren Typ:
%Vor%Schließlich können Sie die Fälle für das schreiben, was Sie gewählt haben:
%Vor% Beachten Sie, dass die natToFoo Funktion zwar ziemlich große Muster hat, aber dort ist nicht wirklich viel los. Es sollte wahrscheinlich möglich sein, die Muster klein zu machen, indem man sie verschachtelt, obwohl das hässlich sein kann.
Verallgemeinerung: Zuerst dachte ich, das würde nur für Sonderfälle funktionieren, aber ich denke jetzt, dass es ein bisschen besser sein könnte. Insbesondere wenn Sie einen algebraischen Datentyp haben, der Typen mit dezidierbarer Gleichheit enthält, sollten Sie in der Lage sein, ihn in ein verschachteltes Either von verschachteltem Pair zu konvertieren, das Sie dorthin bringt. Zum Beispiel (mit Maybe , um Either (Bool, Nat) () zu verkürzen):
Tags und Links idris