haskell - 如何使用 Data.Reify 来具体化数据列表？

Question

我尝试阅读论文( http://www.ittc.ku.edu/csdl/fpg/sites/default/files/Gill-09-TypeSafeReification.pdf )并设法具体化我的符号表达式类型，但我不知道如何具体化它们的列表。这是简化的代码:

{-# OPTIONS_GHC -Wall #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilies #-}
{-# Language FlexibleInstances #-}

import Control.Applicative
import Data.Reify

-- symbolic expression type
data Expr a = EConst a
            | EBin (Expr a) (Expr a)
            deriving Show

-- corresponding node type
data GraphExpr a b = GConst a
                   | GBin b b
                   deriving Show

instance MuRef (Expr a) where
  type DeRef (Expr a) = GraphExpr a
  mapDeRef _ (EConst c)  = pure (GConst c)
  mapDeRef f (EBin u v) = GBin <$> f u <*> f v

-- this works as expected
main :: IO ()
main = reifyGraph (EBin x (EBin x y)) >>= print
  where
    x = EConst "x"
    y = EConst "y"
-- (output: "let [(1,GBin 2 3),(3,GBin 2 4),(4,GConst "y"),(2,GConst "x")] in 1")

-- but what if I want to reify a list of Exprs?
data ExprList a = ExprList [Expr a]
data GraphList a b = GraphList [GraphExpr a b]

instance MuRef (ExprList a) where
  type DeRef (ExprList a) = GraphList a
  --  mapDeRef f (ExprList xs) = ???????

Answer 1

我遇到了完全相同的问题，我找到了使用 data-reify 的解决方案。

要找到解决方案，您必须意识到:1.即使EDSL没有列表，图形类型也可以包含它们2. 可以将不同类型的数据具体化为相同的结果类型。

因此，我们首先向结果类型添加列表构造函数:

data GraphExpr a b = GConst a
                   | GBin b b
                   | Cons b b
                   | Nil
                   deriving Show

然后我们需要第二个 MuRef 实例，它将 Expr a 列表具体化为 GraphExpr。

instance MuRef [Expr a] where
    type DeRef [Expr a] = GraphExpr a
    mapDeRef _ [] = pure Nil
    mapDeRef f (x:xs) = Cons <$> f x <*> f xs

现在，如果我们尝试具体化列表表达式

reified = reifyGraph [EBin x (EBin x y), Ebin y (EBin x y)]
              where x = EConst "x"
                    y = EConst "y"

我们会得到结果

let [(1,Cons 2 6),(6,Cons 7 9),(9,Nil),(7,GBin 5 8),(8,GBin 3 5),(2,GBin 3 4),(4,GBin 3 5),(5,GConst "y"),(3,GConst "x")] in 1

要从该图中提取具体化的节点 ID 列表，我们可以定义一个小函数来遍历 Conses 并将其中的节点 ID 提取到列表中。

walkConses :: Graph (GraphExpr t) -> [Unique]
walkConses (Graph xs root) = go (lookup root xs)
where 
    go (Just (Cons n1 n2)) = n1 : go (lookup n2 xs)
    go (Just Nil) = []

(如果图形很大，在开始步行之前将它们转换为 IntMap 可能是个好主意)

这看起来像一个部分函数，​​但是因为我们知道 DAG 的根将始终是一个 Cons 节点(因为我们具体化了一个列表)，并且因为我们知道所有节点 ID 都在 xs 中，所以这个函数将返回结果列表中所有节点 ID 的列表。

因此，如果我们在结果图上运行 walkConses，我们将得到结果:

[2, 7]

希望这会有所帮助，我也一直在努力解决这个问题一段时间。