如何恢復GADT中的共享？

Question

在Type-Safe Observable Sharing in Haskell Andy Gill展示瞭如何在DSL中恢復Haskell級別上存在的共享。他的解決方案在data-reify package中實施。此方法是否可以修改爲與GADT一起使用？例如，鑑於此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 

我想通過將上述AST由函數

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

的方法來恢復共享

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 

（I」 m不知道recoverSharing的類型。）

請注意，我不介意介紹新的bindin gs通過一個let結構，但僅用於恢復Haskell級別上的共享。這就是爲什麼我有recoverSharing返回Map。

如果不能做成可重複使用的軟件包，至少可以做到特定的GADT嗎？

Answer 1

有趣的謎題！事實證明，您可以使用GADT進行數據驗證。你需要的是一個隱藏在存在中的類型的包裝器。該類型稍後可以通過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' 

這裏是整個代碼：https://gist.github.com/3590197

編輯：我喜歡對方的回答使用Typeable。所以我也用Typeable做了我的代碼版本：https://gist.github.com/3593585。代碼顯着縮短。 Type e ->被替換爲Typeable e =>，這也有一個缺點：我們不再知道可能的類型限於Int和Bool，這意味着在IfThenElse中必須有Typeable e約束。

Answer 2

我會試着證明這可以用特定的GADT來完成，以你的GADT爲例。我將使用Data.Reify包。這需要我定義一個新的數據結構，其中recusive位置被一個參數替代。

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

請注意，我刪除了許多原始GADT中可用的類型信息。對於前三個構造函數，很明顯關聯的類型是什麼（Int，Int和Bool）。對於最後一個，我會記住使用TypeRep（可在Data.Typeable）的類型。下面顯示了reify軟件包要求的MuRef的實例。現在

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 

我們可以使用reifyGraph恢復共享。但是，很多類型信息丟失了。讓我們嘗試恢復它。我改變了你的定義AST2略：

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

從物化包中的圖形看起來像這樣（其中E = AstNode）：

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

讓我們做一個新圖形數據結構，其中我們可以分別存儲Ast2 Int和Ast2 Bool（因此，類型信息已被恢復）：

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

現在，我們只需要從圖AstNode（的reifyGraph結果）找到一個函數來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 

讓我們做一個例子：

expr = Add (IntLit 42) expr 

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

打印：

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

第一行顯示我們reifyGraph已正確恢復共享。第二行顯示只有Ast2 Int類型已被找到（這也是正確的）。

這種方法很容易適應其他特定的GADT，但我不明白它如何完全通用。

完整的代碼可以在http://pastebin.com/FwQNMDbs找到。