condizionale derivano Show per tipo esistenziale con parametri del tipo di costruttore

Question

Supponiamo che io sono un tipo di dati come questo:

{-# LANGUAGE RankNTypes #-} 
data X a = forall b. Show b => X (a b) 

vorrei ricavare Show (X a), ma naturalmente io solo posso fare quindi se c'è un caso di Show (a b). Sono tentato di scrivere

{-# LANGUAGE StandaloneDeriving #-} 
deriving instance Show (a b) => Show (X a) 

ma purtroppo il tipo di variabile b non è disponibile nel contesto esempio perché esso è vincolato dalla forall.

Il mio prossimo tentativo è stato quello di spostare il contesto Show (a b) nel forall nella definizione del tipo di dati, in questo modo:

data X a = forall b. Show (a b) => X (a b) 
deriving instance Show (X a) 

Questo compila, ma purtroppo ora ho perso la capacità di costruire un X con una irraggiungibile (a b).

Esiste un modo per consentire X da costruire con qualsiasi (a b), e quindi condizionalmente derivano Show (X a) solo se (a b) è showable?

Answer 1

Questa è una deficienza nelle classi Prelude. C'è un bel modo per aggirarlo anche se incarnato nel pacchetto prelude-extras. Lo traccerò qui sotto.

Vorremmo creare una classe Show di livello superiore. Sembra che questo

class Show1 a where 
    show1 :: Show b => a b -> String 

Allora possiamo almeno alcune inesattezze nostro vincolo desiderato come

deriving instance Show1 a => Show (X a) 

Purtroppo, il compilatore non hanno ancora sufficienti informazioni per raggiungere questa derivazione. Dobbiamo dimostrare che (Show b, Show1 a) è sufficiente per derivare Show (a b). Per fare questo avremo bisogno di attivare alcune estensioni (spaventosi, ma in modo sano-utilizzate)

{-# LANGUAGE FlexibleInstances   #-} 
{-# LANGUAGE OverlappingInstances  #-} 

instance (Show b, Show1 a) => Show (a b) where 
    show = show1 

Ed ora che abbiamo la prova che il compilatore sarà in grado di ricavare quello che ci serve

data X a = forall b . Show b => X (a b) 
deriving instance Show1 a => Show (X a) 

Answer 2

Prenderò un approccio simile ma leggermente diverso alla risposta di J. Abrahamson.

Proprio quello che chiedi non può essere fatto, perché le classi di tipo devono essere risolti staticamente, ma l'esistenza di Show (a b) potrebbe essere dinamica a seconda della instantation di b. Questa istanziazione è nascosta all'interno del valore X e pertanto non è visibile per il controllo di tipo quando non si ha nient'altro che uno X b di origine sconosciuta.

Sarebbe bello scrivere una condizione sulla a come Show (a b) esiste ogni volta Show b fa, perché allora l'esistenza di Show (a b) non è in realtà dipende da b come già sappiamo che Show b è sempre vero.

Non possiamo scrivere che condizioni direttamente, ma siamo in grado di esprimere qualcosa di simile utilizzando GADTs:

{-# LANGUAGE GADTs #-} 
data ShowDict a where 
    ShowDict :: Show a => ShowDict a 

Il tipo ShowDict a fornisce una sorta di reificazione della classe Show a - è qualcosa che possiamo passare intorno e definire le funzioni sopra.

In particolare possiamo ora definire una classe Show1 che esprime la condizione Show (a b) ogni volta che abbiamo un Show b:

class Show1 a where 
    show1Dict :: ShowDict b -> ShowDict (a b) 

e ora possiamo definire Show (X a) in termini di Show1, costruendo ShowDict (a b) e quindi pattern-matching su di esso per rivelare l'istanza Show:

{-# LANGUAGE ScopedTypeVariables #-} 
instance Show1 a => Show (X a) where 
    show (X (v :: a b)) = 
     case show1Dict ShowDict :: ShowDict (a b) of 
      ShowDict -> "X (" ++ show v ++ ")" 

Un'implementazione più completa sarebbe anche inc lude gli altri membri di Show (showsPrec e showList).

La cosa bella di questa soluzione è che possiamo tranquillamente definire Show1 per [], riutilizzando automaticamente il sottostante Show esempio:

instance Show1 [] where 
    show1Dict ShowDict = ShowDict 

anche io preferisco evitare il molto generico Show (a b) esempio dalla risposta di J. Abrahamson, ma il lato negativo di dover mettere la logica nell'istanza Show per X è che finiamo per doverlo implementare manualmente piuttosto che ottenere il comportamento derivato automaticamente per il costruttore.