Typ-Ebene Peano Zahlen und UndecidableInstances

Question

Nach this tutorial, ich habe den folgenden Code:

{-# LANGUAGE DataKinds, TypeFamilies #-} 

data Nat = Z | S Nat 

type family Plus (n :: Nat) (m :: Nat) :: Nat 
type instance Plus Z  m = m 
type instance Plus (S n) m = S (Plus n m) 

So weit so gut. Ich weiß, dass DataKinds automatische Förderung von Typen zu Arten, und TypeFamilies aktivieren Sie Funktionen auf Typenebene.

Dann füge ich:

type family Mul (m :: Nat) (n :: Nat) :: Nat 
type instance Mul Z  m = Z 
type instance Mul (S n) m = Plus m (Mul n m) 

compilieren gibt mir:

Nested type family application 
    in the type family application: Plus m (Mul n m) 
(Use UndecidableInstances to permit this) 
In the type instance declaration for ‘Mul’ 

Der Name dieser Erweiterung ist beängstigend. Manche Leute sagen zu avoid es, und Erklärungen dieser Erweiterung, die ich versucht habe zu lesen, machen keinen Sinn für mich.

die Suche nach einem wenig Hilfe in den Fehler zu verstehen, warum es in diesem Beispiel zeigt mich, was ist der Sinn des unentscheidbar in diesem Zusammenhang und in welchen Fällen diese Erweiterung so beängstigend ist, wie es klingt?

Answer 1

Es ist nicht wirklich beängstigend. Es deaktiviert die (eher schwachen) GHC-Prüfungen, die sicherstellen sollen, dass Typfamilien- und Instanzdefinitionen beendet werden. Das Worst-Case-Verhalten ist also die nicht-terminierende Typprüfung. In den meisten Fällen erhalten wir jedoch Fehlermeldungen anstelle von tatsächlichen Schleifen, da Schleifen die Stapelgrenzen in der Typüberprüfung oft überschreiten. Wir erhalten keine Unsicherheit, Inkohärenz oder andere Eigenschaften, die die Robustheit oder Inferenz des Programms beeinträchtigen können.

"Unentscheidbar" ist wahrscheinlich ein stärkerer Ausdruck als gerechtfertigt, da es nur anzeigt, dass GHC nicht entscheiden kann, ob eine Definition endet. In vielen Fällen ist GHC für diesen Job zu schwach, und andere Compiler für abhängige Sprachen können die Terminierung problemlos überprüfen. Bei GHC wird UndecidableInstances oft auch für offensichtlich terminierende Definitionen benötigt, in welchen Fällen seine Verwendung durchaus gerechtfertigt ist.

Answer 2

UndecidableInstance ist in Ordnung zu verwenden. Zugegeben, man sollte immer einen einen Moment berücksichtigen, ob etwas wirklich benötigt wird, oder es wäre idiomatischer, einen anderen Weg zu wählen.

Luke macht den Punkt, dass UndecidableInstances nicht verwendet werden sollte, um Superklassen zu implementieren. Nun, das stimmt, aber es hat nicht wirklich viel mit unentscheidbaren Instanzen zu tun. – Superclassing ist einfach immer ein Hack und ziemlich genau umgekehrt wie Abstraktionen entworfen werden sollten.

Es ist IME nicht wahr, zumindest nicht mehr, dass Superklassen ist die häufigste Verwendung von UndecidableInstances. Es gibt viele Dinge, die Sie mit dieser Erweiterung tun können, aber nicht ohne. Am sichersten, es kann nicht möglich sein, eine Halte-Proof-Bedingung auferlegen, wenn Sie tatsächlich Turing-vollständige abhängige Typisierung zur Compile-Zeit, die im Grunde, was alle DataKinds Fuzz ist, zu gehen.

Also, mach dir keine Sorgen zu viel; in der Tat werden Sie wahrscheinlich nicht umgehen UndecidableInstances. Wie gesagt von Andr & aacute; s Kov & aacute; cs, ist diese Erweiterung vollkommen sicher WRT Korrektheit, das Schlimmste, was passieren kann, ist eine Schleife/Fehler.

Wenn das für Ihren Geschmack zu gruselig ist, verwenden Sie eine Sprache, die von vornherein als abhängig typisiert und insgesamt entworfen wurde, d.Agda.