automatisch ableiten zeigen Instanzen für GADTs

Question

Angenommen ich eine komplexe GADT haben, die mit vielen versteckten Typ Parameter als Erbauer:

data T where 
    A :: Num n => n -> T 
    B :: (Num n, Integral m) => n -> m -> T 
    C :: Floating a => [a] -> T 
    -- and so on 
    Z :: Num n => n -> n -> T 

ich ohne diesen Datentyp sendefähiges machen wollen, die manuell die Instanz zu schreiben. Problem ist, dass seit Show keine Oberklasse von Num mehr ist, das Hinzufügen einer einfachen deriving instance Show T ist nicht genug für den Compiler zu schließen, dass es Show Constraints zu allen internen versteckten Typ Parameter hinzufügen müssen.

Für jeden versteckten Typ-Parameter gibt es so etwas wie

Could not deduce (Show n) arising from a use of 'showsPrec' 
from the context Num n 
    bound by a pattern with constructor 
      A :: forall n. Num n => n -> T 
... 
Possible fix: 
    add (Show n) to the context of the data constructor 'A' 

eine Show Einschränkung in den Datentyp hinzuzufügen, ist keine Option, da sie die möglichen Bewohner von T begrenzt. Es scheint wie deriving instanec Show T sollte die Einschränkung Show auf die versteckten Datentypen einführen, obwohl ich mir nicht sicher bin.

Wie kann ich darüber gehen?

Answer 1

Ich hatte einen interessanten Gedanken, nicht sicher, wie praktisch es ist. Wenn Sie jedoch möchten, dass T als darstellbar angezeigt werden kann, wenn die Parameter zwar darstellbar, aber auch mit nicht darstellbaren Parametern verwendbar sind, können Sie T über eine Integritätsbedingung mit ConstraintKinds parametrisieren.

{-# LANGUAGE GADTs, ConstraintKinds #-} 

import Data.Kind 

data T :: (* -> Constraint) -> * where 
    A :: (Num n, c n) => n -> T c 
    B :: (Num n, c n, Integral m, c m) => n -> m -> T c 
    ... 

Dann wird T Show sendefähiges sein ... vielleicht

deriving instance Show (T Show) 

(mit StandaloneDeriving Erweiterung) funktionieren wird, aber zumindest, T ist sendefähiges grundsätzlich und man konnte die Instanz schreiben manuell.

Obwohl mein praktischer Rat ist, die existentials zu vergegenständlichen. Ein existentieller Typ entspricht der Sammlung seiner Beobachtungen. Zum Beispiel, wenn Sie

class Foo a where 
    getBool :: a -> Bool 
    getInt :: a -> Int 

dann die existentielle

data AFoo where 
    AFoo :: Foo a => a 

eine Klasse wie hatte genau entspricht (Bool,Int), denn das einzige, was Sie mit einem Foo deren Art tun können Sie nicht wissen, ist Rufen Sie getBool darauf oder getInt darauf an. Sie verwenden Num in Ihrem Datentyp und Num hat keine Beobachtungen, denn wenn man eine unbekannte a mit Num a haben, das einzige, was man durch den Aufruf von Methoden von Num tun können, ist mehr bekommen a s aus, und nichts jemals Beton. Also Ihr A Konstruktor

A :: (Num n) => n -> T 

gibt Ihnen nichts und man könnte genauso gut sagen

A :: T 

Integral, auf der anderen Seite, hat toInteger als Beobachtung.So könnte man wahrscheinlich

ersetzen

B :: (Num n, Integral m) => n -> m -> T 

mit

B :: Integer -> T 

(wir verloren das n Argument und ersetzt m mit Integer). Ich denke nicht, dass dies technisch äquivalent ist, da wir seine Operationen anders implementiert haben könnten als Integral, aber wir werden an dieser Stelle ziemlich technisch und ich bezweifle, dass Sie das brauchen (ich wäre daran interessiert, wie Sie es tun würden)).