Haskell GADT ‚Show'- Instance-Typ-Variable Abzug

Question

Dieser Code

{-# LANGUAGE GADTs #-} 

data Expr a where 
    Val :: Num a => a -> Expr a 
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool 

eval :: Expr a -> a 
eval (Val x) = x 
eval (Eq x y) = (eval x) == (eval y) 

instance Show a => Show (Expr a) where 
    show (Val x) = "Val " ++ (show x) 
    show (Eq x y) = "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")" 

mit der folgenden Fehlermeldung kompilieren fehlschlägt:

Test.hs:13:32: error: 
    * Could not deduce (Show a1) arising from a use of `show' 
     from the context: Show a 
     bound by the instance declaration at test.hs:11:10-32 
     or from: (a ~ Bool, Eq a1) 
     bound by a pattern with constructor: 
        Eq :: forall a. Eq a => Expr a -> Expr a -> Expr Bool, 
       in an equation for `show' 
     at test.hs:13:11-16 
     Possible fix: 
     add (Show a1) to the context of the data constructor `Eq' 
    * In the first argument of `(++)', namely `(show y)' 
     In the second argument of `(++)', namely 
     `(show y) ++ ") (" ++ (show x) ++ ")"' 
     In the expression: "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")" Failed, modules loaded: none. 

die letzte Zeile behebt das Problem, kommentiert und Inspektion der Der Typ von Expr in GHCi zeigt, dass GHC, anstatt Eq vom Typ Eq a => (Expr a) -> (Expr a) -> Expr Bool zu folgern, es tatsächlich zu Eq a1 => (Expr a1) -> (Expr a1) -> Expr Bool für data Expr a where ... wird. Dies erklärt die Fehlermeldung, da instance Show a => Show (Expr a) where ...a1 nicht als Instanz von Show erzwingen wird.

aber ich nicht verstehen, warum GHC wählt, dies zu tun. Wenn ich eine Vermutung abgeben müsste, würde ich sagen, es hat etwas damit zu tun, dass Eq einen Wert zurückgibt, der nicht von a überhaupt abhängt und somit GHC "vergisst" über a, sobald Eq einen Expr Bool zurückgibt. Ist das - zumindest was - hier passiert?

Gibt es auch eine saubere Lösung? Ich habe versucht, verschiedene Dinge, einschließlich versuchen, den gewünschten Typen zu „zwingen“ über InstanceSigs und ScopedTypeVariables so etwas wie dies zu tun:

instance Show a => Show (Expr a) where 
    show :: forall a. Eq a => Expr a -> String 
    show (Eq x y) = "Eq (" ++ (show (x :: Expr a)) ++ ") (" ++ (show (y :: Expr a)) ++ ")" 
    ... 

, aber ohne Erfolg. Und da ich immer noch ein Haskell-Neuling bin, bin ich mir nicht einmal sicher, ob das irgendwie irgendwie funktionieren könnte, aufgrund meiner ersten Vermutung, warum GHC überhaupt nicht den "richtigen"/gewünschten Typ ableitet.

EDIT:

Ok, so habe ich beschlossen, eine Funktion

extract (Eq x _) = x 

in die Datei hinzuzufügen (ohne Typen Signatur), nur um zu sehen, welcher Rückgabetyp es haben würde. GHC weigerte sich erneut zu kompilieren, aber diesmal enthielt die Fehlermeldung einige Informationen über Variablen vom Skolem-Typ. Eine schnelle Suche ergab this question, was (glaube ich?) Formalisiert, was ich glaube das Problem zu sein: Sobald Eq :: Expr a -> Expr a -> Expr Bool eine Expr Bool zurückgibt, geht a "out of scope". Jetzt haben wir keine Informationen mehr über a, also extract müsste die Signatur exists a. Expr Bool -> a haben, da forall a. Expr Bool -> a nicht für jede a gilt. Da GHC exists nicht unterstützt, schlägt die Typprüfung fehl.

Answer 1

Eine Option ist nicht erfordert eine Show a Supraleitung.

instance Show (Expr a) where 
    showsPrec p (Eq x y) = showParen (p>9) 
     $ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y 

Natürlich ist dies etwas den Stein schlägt die Straße hinunter, denn jetzt können Sie nicht

schreiben

showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x 

mehr - jetzt das Blatt Wert nicht Show eingeschränkt.Aber hier können Sie Ihren Weg, um dieses hacken, indem die Num Zwang etwas stärker:

data Expr a where 
    Val :: RealFrac a => a -> Expr a 
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool 
instance Show (Expr a) where 
    showsPrec p (Val x) = showParen (p>9) $ ("Val "++) 
      . showsPrec 10 (realToFrac x :: Double) 

Nun, das ist ein großer Hack, und an diesem Punkt könnte man genauso gut verwenden Sie einfach

data Expr a where 
    Val :: Double -> Expr Double 
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool 

(oder welcher andere einzelne Typ am besten zu Ihren Nummern passt). Das ist keine gute Lösung.

Um die Fähigkeit zu speichern Anzahl von jede Art in Expr Blätter behalten, doch in der Lage sein, sie zu Show zu beschränken, falls gewünscht, müssen Sie polymorph auf die Einschränkung sein.

{-# LANGUAGE ConstraintKinds, KindSignatures #-} 

import GHC.Exts (Constraint) 

data Expr (c :: * -> Constraint) a where 
    Val :: (Num a, c a) => a -> Expr a 
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool 

Dann können Sie

instance Show (Expr Show a) where 
    showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x 
    showsPrec p (Eq x y) = showParen (p>9) 
     $ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y 

Answer 2

tun werde ich nur diesen Punkt erklären.

Allerdings verstehe ich nicht, warum GHC dies tut.

Das Problem ist, man einen benutzerdefinierten Typ mit einem Num und Eq Beispiel schreiben können, aber keine Show ein.

newtype T = T Int deriving (Num, Eq) -- no Show, on purpose! 

Dann wird dieser Typ überprüft:

e1 :: Expr T 
e1 = Val (T 42) 

wie dies tut:

e2 :: Expr Bool 
e2 = Eq e1 e1 

Es sollte jedoch klar sein, dass e1 und e2 nicht show ziert werden können. Um diese zu drucken, benötigen wir Show T, was fehlt.

Ferner ist die Einschränkung

instance Show a => Show (Expr a) where 
     -- ^^^^^^ 

ist hier nutzlos, da wir Show Bool haben, aber das ist nicht genug e2 :: Expr Bool zu drucken.

Dies ist das Problem der existentiellen Typen: Sie bekommen, was Sie bezahlen. Wenn wir e2 = Eq e1 e2 konstruieren, müssen wir nur die Bedingung Eq T "bezahlen". Wenn wir also das Muster Eq a b erreichen, erhalten wir nur Eq t zurück (wobei t eine geeignete Typvariable ist). Wir erfahren nicht, ob Show t gilt. In der Tat, selbst wenn wir uns an t ~ T erinnern würden, würde uns immer noch die erforderliche Show T Instanz fehlen.