Erhalte 'Show a' aus dem Kontext 'Show (a, b)'

8

Wie der Titel sagt, bin ich daran interessiert, Show a in einem Kontext zu verwenden, in dem ich Show (a,b) habe. Dieses Problem tritt bei GADTs wie folgt auf:

%Vor%

Der Fehler ist:

%Vor%

Ich würde denken, dass die Instanzdeklaration instance (Show a, Show b) => Show (a,b) Show element beweist, aber ich kann mir auch vorstellen, dass das Problem auch etwas damit zu tun hat, wie die Typklassenmaschinerie zur Laufzeit implementiert wird.

Ich habe entdeckt, dass, wenn wir die Klassendefinition ändern können, es möglich ist, dies zu lösen:

%Vor%

Dann holen wir auf der Benutzungsseite das Wörterbuch explizit:

%Vor%

Ich habe mich gefragt, ob es eine nicht-intrusive (oder einfach andere) Möglichkeit gibt, Show element zu erhalten. Wenn nicht, könnten Sie erklären, warum genau dieses Problem auftritt?

    
enobayram 22.09.2016, 13:03
quelle

3 Antworten

2

Wenn es Ihnen nichts ausmacht, dass b immer eine Instanz von Show sein muss, dann ist dies eine einfache Lösung:

%Vor%     
user2297560 22.09.2016 13:40
quelle
1

Ich habe immer wieder versucht zu sehen, ob ich etwas Besseres finden kann, und hier ist das Beste, was ich mir vorstellen kann:

In meinem ursprünglichen Versuch habe ich die Typklasse Show' mit der Instanzdeklaration für Paare gekoppelt. Obwohl ich keine Möglichkeit gefunden habe, die Typklasse zu ändern, habe ich es zumindest geschafft, dies für jede Instanzdeklaration zu verallgemeinern.

Wie in den Kommentaren der Frage erwähnt, ist instance (Show a, Show b) => Show (a,b) eine einseitige Implikation, aber ich nahm an, dass sie auch in der anderen Richtung angewendet werden könnte, da keine überlappenden Instanzen vorhanden sind. Leider verlässt sich GHC nicht darauf, aber wir können das selbst behaupten. Meine Intuition kann in Code übersetzt werden: ( :=> stammt von Data.Constraint aus dem constraints Paket und a :=> b bedeutet, dass irgendwo ein instance a => b ist)

%Vor%

Hier ist die Funktion noOverlap ein Versprechen, dass, wenn Sie eine Einschränkung b finden, die zu einer Instanz Show' a führt, ich b gegeben Show' a beweisen kann. Dieses Versprechen entspricht der Aussage, dass es keine überlappenden Instanzen für Show'

geben wird

Jetzt brauchen wir eine Hilfsfunktion, um noOverlap

tatsächlich zu implementieren %Vor%

Wenn diese Funktion in einem Kontext aufgerufen wird, in dem Sie eine Instanz k :=> Show' a haben, gibt diese Funktion eine Funktion zurück, die Dict b für any Instanz zurückgibt b :=> Show' a . Wir müssen unsafeCoerce verwenden, um GHC davon zu überzeugen, dass Dict k und Dict b identisch sind, aber soweit ich sehen kann, ist dies eine sichere Verwendung von unsafeCoerce, da die funktionale Abhängigkeit a :=> b | b -> a dafür sorgt sei nur eine Instanz von k :=> Show' a für eine gegebene Show' a .

Mit diesem Helfer können Sie Instanzen folgendermaßen definieren:

%Vor%

Wir müssen die :=> Instanzen manuell definieren, da GHC das nicht automatisch macht, aber dort ist kein Platz für Fehler. Wenn wir links von einer manuell definierten :=> eine zu schwache Einschränkung geben, wird ins = Sub Dict nicht kompilieren und wenn wir eine zu starke Einschränkung geben, dann wird noOverlap = basedOn nicht kompilieren, so dass boilerplate von der Compiler.

Wir können dann noOverlap wie folgt verwenden:

%Vor%

Das Schöne ist, dass wir jetzt auch von Show' [a] zu Show' a oder jeder anderen Instanzdeklaration gehen können.

Hinweis: Sie benötigen {-# LANGUAGE FlexibleContexts, TypeOperators, RankNTypes, ConstraintKinds, AllowAmbiguousTypes #-} , um diese zu kompilieren.

    
enobayram 23.09.2016 12:08
quelle
1

Hier ist eine Verallgemeinerung von user2297560 , die keine feste Codierung Show in der GADT erfordert:

%Vor%

Dann können Sie

%Vor%     
leftaroundabout 23.09.2016 12:16
quelle

Tags und Links