Wenn Reverse :: [k] -> [k] eine Typfamilie ist, kann Haskell das (Reverse (Reverse xs)) ~ xs nicht sagen. Gibt es eine Möglichkeit, dies dem Typsystem ohne Laufzeitkosten mitzuteilen?Informieren Sie Haskell, dass `(Reverse (Reverse xs)) ~ xs`
Ich bin versucht, nur unsafeCoerce zu verwenden, aber das scheint eine Schande.
Der einzige Weg, die ich kenne, das Verhalten von ~ in GHC zu beeinflussen ist, um tatsächlich eine Instanz von a :~: b zu konstruieren (oder ähnlichem, das Wichtigste ist, einen Begriff zu konstruieren, die dies auf den typechecker „beweist“) und dann Musterübereinstimmung für den Refl-Konstruktor, für den es erforderlich wäre, den Beweisträger zur Laufzeit zu bewerten. Mein Verständnis ist, dass das aktuelle Design für abhängige Typen in GHC immer noch die Ausführung aller Beweise für die Typgleichheit erfordert. Man könnte jedoch die Umschreibregeln von GHC verwenden, um nach der Typprüfung den Beweiszeugen durch eine sehr kostengünstige Funktion (z. B. unsafeCoerce Refl :: Reverse (Reverse a) :~: a) zu ersetzen, was die Auswertung sehr kostengünstig macht, aber immer noch sicher ist (da der Beweiszeuge bereits eine Überprüfung vorgenommen hat), zeigen, dass, wenn es endet, wird es einen korrekten Beweis produzieren). https://typesandkinds.wordpress.com/2016/07/24/dependent-types-in-haskell-progress-report/
AFAICS, keine Möglichkeit, dass zur Zeit zu tun:
Viel mehr Informationen über den aktuellen Zustand der abhängigen Typisierung in Haskell sind hier zu finden. Aus diesem Grund würde ich gerne sehen, dass GHC eines Tages einen Termination-Checker integriert und intern jede beliebige beendbare Beendigung von x: T in x = unsafeCoerce() 'optimiert, wenn' T' genau einen Konstruktor ohne Argumente hat (wie ' : ~: 'tut). Man müsste immer noch einen Beweis durch Induktion schreiben, aber es wird zumindest keine Laufzeitstrafe eingeführt. – chi
Irgendwann muss es praktischer sein, eine Sprache zu benutzen, die eigentlich für so etwas gedacht ist ... –