Come posso recuperare la condivisione in un GADT?

Question

In Type-Safe Observable Sharing in Haskell Andy Gill mostra come ripristinare la condivisione esistente a livello Haskell, in un DSL. La sua soluzione è implementata nel data-reify package. Questo approccio può essere modificato per funzionare con GADT? Ad esempio, dato questo GADT:

data Ast e where 
    IntLit :: Int -> Ast Int 
    Add :: Ast Int -> Ast Int -> Ast Int 
    BoolLit :: Bool -> Ast Bool 
    IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e 

mi piacerebbe recuperare la condivisione trasformando l'AST sopra per

type Name = Unique 

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Ast2 Int -> Ast2 Int -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Ast2 Bool -> Ast2 e -> Ast2 e -> Ast2 e 
    Var :: Name -> Ast2 e 

per la via di una funzione

recoverSharing :: Ast -> (Map Name, Ast2 e1, Ast2 e2) 

(I' Non sono sicuro del tipo di recoverSharing.)

Nota che non mi interessa introdurre il nuovo bindin gs tramite un costrutto let, ma solo nel recupero della condivisione che esisteva a livello di Haskell. Ecco perché ho recoverSharing restituire un Map.

Se non può essere eseguito come pacchetto riutilizzabile, è possibile farlo almeno per GADT specifico?

Answer 1

Interessante puzzle! Si scopre che puoi utilizzare data-reify con GADTs. Quello di cui hai bisogno è un wrapper che nasconda il tipo in un file esistenziale. Il tipo può essere successivamente recuperato dalla corrispondenza del modello sul tipo di dati Type.

data Type a where 
    Bool :: Type Bool 
    Int :: Type Int 

data WrappedAst s where 
    Wrap :: Type e -> Ast2 e s -> WrappedAst s 

instance MuRef (Ast e) where 
    type DeRef (Ast e) = WrappedAst 
    mapDeRef f e = Wrap (getType e) <$> mapDeRef' f e 
    where 
     mapDeRef' :: Applicative f => (forall b. (MuRef b, WrappedAst ~ DeRef b) => b -> f u) -> Ast e -> f (Ast2 e u) 
     mapDeRef' f (IntLit i) = pure $ IntLit2 i 
     mapDeRef' f (Add a b) = Add2 <$> (Var Int <$> f a) <*> (Var Int <$> f b) 
     mapDeRef' f (BoolLit b) = pure $ BoolLit2 b 
     mapDeRef' f (IfThenElse b t e) = IfThenElse2 <$> (Var Bool <$> f b) <*> (Var (getType t) <$> f t) <*> (Var (getType e) <$> f e) 

getVar :: Map Name (WrappedAst Name) -> Type e -> Name -> Maybe (Ast2 e Name) 
getVar m t n = case m ! n of Wrap t' e -> (\Refl -> e) <$> typeEq t t' 

Ecco il codice intero: https://gist.github.com/3590197

Edit: mi piace l'uso del Typeable in altra risposta. Così ho fatto anche una versione del mio codice con Typeable: https://gist.github.com/3593585. Il codice è significativamente più breve. Type e -> è sostituito da Typeable e =>, che ha anche un inconveniente: non sappiamo più che i possibili tipi sono limitati a Int e Bool, il che significa che ci deve essere un vincolo Typeable e in IfThenElse.

Answer 2

Proverò a dimostrare che questo può essere fatto per GADT specifici, utilizzando il GADT come esempio.

Utilizzerò il pacchetto Data.Reify. Ciò mi impone di definire una nuova struttura dati in cui le posizioni recusive sono sostituite da un parametro.

data AstNode s where 
    IntLitN :: Int -> AstNode s 
    AddN :: s -> s -> AstNode s 
    BoolLitN :: Bool -> AstNode s 
    IfThenElseN :: TypeRep -> s -> s -> s -> AstNode s 

Nota che rimuovo un sacco di informazioni tipo che era disponibile nella GADT originale. Per i primi tre costruttori è chiaro quale fosse il tipo associato (Int, Int e Bool). Per l'ultimo, ricorderò il tipo utilizzando TypeRep (disponibile in Data.Typeable). L'istanza per MuRef, richiesta dal pacchetto reify, è mostrata di seguito.

instance Typeable e => MuRef (Ast e) where 
    type DeRef (Ast e)  = AstNode 
    mapDeRef f (IntLit a) = pure $ IntLitN a 
    mapDeRef f (Add a b) = AddN <$> f a <*> f b 
    mapDeRef f (BoolLit a) = pure $ BoolLitN a 
    mapDeRef f (IfThenElse a b c :: Ast e) = 
    IfThenElseN (typeOf (undefined::e)) <$> f a <*> f b <*> f c 

Ora possiamo usare reifyGraph per recuperare la condivisione. Tuttavia, molte informazioni sul tipo sono andate perse. Cerchiamo di recuperarlo.Ho modificato la sua definizione di AST2 leggermente:

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Unique -> Unique -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Unique -> Unique -> Unique -> Ast2 e 

Il grafico dal pacchetto reificare assomiglia a questo (dove e = AstNode):

data Graph e = Graph [(Unique, e Unique)] Unique  

Consente di creare una nuova struttura di dati grafico in cui possiamo memorizzare Ast2 Int e Ast2 Bool separatamente (quindi, se le informazioni sul tipo sono state recuperate):

data Graph2 = Graph2 [(Unique, Ast2 Int)] [(Unique, Ast2 Bool)] Unique 
      deriving Show 

Ora abbiamo solo bisogno di trovare una funzione da Graph AstNode (il risultato di reifyGraph) per Graph2:

recoverTypes :: Graph AstNode -> Graph2 
recoverTypes (Graph xs x) = Graph2 (catMaybes $ map (f toAst2Int) xs) 
            (catMaybes $ map (f toAst2Bool) xs) x where 
    f g (u,an) = do a2 <- g an 
        return (u,a2) 

    toAst2Int (IntLitN a) = Just $ IntLit2 a 
    toAst2Int (AddN a b) = Just $ Add2 a b 
    toAst2Int (IfThenElseN t a b c) | t == typeOf (undefined :: Int) 
         = Just $ IfThenElse2 a b c 
    toAst2Int _   = Nothing 

    toAst2Bool (BoolLitN a) = Just $ BoolLit2 a 
    toAst2Bool (IfThenElseN t a b c) | t == typeOf (undefined :: Bool) 
          = Just $ IfThenElse2 a b c 
    toAst2Bool _   = Nothing 

Consente di fare un esempio:

expr = Add (IntLit 42) expr 

test = do 
    graph <- reifyGraph expr 
    print graph 
    print $ recoverTypes graph 

stampe:

let [(1,AddN 2 1),(2,IntLitN 42)] in 1 
Graph2 [(1,Add2 2 1),(2,IntLit2 42)] [] 1 

La prima riga ci mostra che reifyGraph ha recuperato in modo corretto la condivisione. La seconda riga ci mostra che sono stati trovati solo i tipi Ast2 Int (che è anche corretto).

Questo metodo è facilmente adattabile per altri GADTs specifici, ma non vedo come potrebbe essere realizzato interamente generico.

Il codice completo è disponibile all'indirizzo http://pastebin.com/FwQNMDbs.