Jak mogę odzyskać udostępnianie w GADT?

Question

W Type-Safe Observable Sharing in Haskell Andy Gill pokazuje, jak odzyskać udostępnianie, które istniało na poziomie Haskell, w DSL. Jego rozwiązanie zostało zaimplementowane w data-reify package. Czy to podejście można zmodyfikować tak, aby działało z GADT? Na przykład, biorąc pod uwagę to 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 

chciałbym odzyskać udostępnianie poprzez przekształcenie powyższego AST do

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 

drogą funkcji

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

(I” nie jestem pewien co do typu recoverSharing.)

Uwaga, nie dbam o wprowadzenie nowej bindiny gs poprzez konstrukcję let, ale tylko w odzyskiwaniu udostępniania, które istniało na poziomie Haskella. Dlatego mam recoverSharing return a Map.

Jeśli nie można tego zrobić jako opakowania wielokrotnego użytku, czy można to zrobić przynajmniej dla określonego GADT?

Answer 1

Interesująca łamigłówka! Okazuje się, że możesz użyć funkcji re-data z GADT. To, czego potrzebujesz, to opakowanie, które ukrywa ten typ w egzystencjalnym. Typ można później pobrać za pomocą dopasowania do wzorca na typ danych 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' 

Oto cały kod: https://gist.github.com/3590197

Edit: Lubię użycie Typeable w drugiej odpowiedzi. Więc zrobiłem wersję mojego kodu z Typeable też: https://gist.github.com/3593585. Kod jest znacznie krótszy. Type e -> został zastąpiony przez Typeable e =>, który również ma wadę: nie wiemy już, że możliwe typy są ograniczone do Int i Bool, co oznacza, że ​​musi być ograniczenie Typeable e w IfThenElse.

Answer 2

Spróbuję pokazać, że można to zrobić dla konkretnych GADT, używając swojego GADT jako przykładu.

Będę używał pakietu Data.Reify. Wymaga to zdefiniowania nowej struktury danych, w której pozycje rekurencyjne są zastępowane przez parametr.

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

Należy pamiętać, że usuwam wiele informacji o typie, które były dostępne w oryginalnym GADT. Dla pierwszych trzech konstruktorów jest jasne, jaki jest powiązany typ (Int, Int i Bool). Dla ostatniego zapamiętuję typ używając TypeRep (dostępny w Data.Typeable). Wystąpienie dla MuRef, wymagane przez pakiet reify, pokazano poniżej.

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 

Teraz możemy użyć reifyGraph odzyskać udostępnianie. Jednak wiele informacji o typie zostało utraconych. Spróbujmy go odzyskać.I zmienił swoją definicję AST2 nieznacznie:

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

wykres z pakietu zreifikować wygląda następująco (gdzie e = AstNode):

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

Pozwala tworzyć nowe struktury danych wykresu gdzie możemy przechowywać Ast2 Int i Ast2 Bool osobno (stąd, gdy informacja o typie została odzyskana):

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

Teraz musimy tylko znaleźć funkcję od Graph AstNode (w wyniku reifyGraph) do 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 

Zróbmy przykład:

expr = Add (IntLit 42) expr 

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

Wydruki:

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

Pierwsza linia pokazuje, że reifyGraph poprawnie odzyskała udostępnianie. Druga linia pokazuje nam, że znaleziono tylko typy Ast2 Int (co również jest poprawne).

Ta metoda jest łatwa do dostosowania do innych specyficznych GADT, ale nie widzę, jak można ją w pełni wygenerować.

Kompletny kod można znaleźć pod adresem http://pastebin.com/FwQNMDbs.