20

在Haskell 中的 Type-Safe Observable Sharing 中， Andy Gill 展示了如何在 DSL 中恢复存在于 Haskell 级别的共享。他的解决方案是在data-reify 包中实现的。可以修改此方法以与 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 转换为

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

通过函数

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

（我不确定 的类型recoverSharing。）

请注意，我不关心通过 let 构造引入新绑定，而只关心恢复存在于 Haskell 级别上的共享。这就是为什么我recoverSharing返回一个Map.

如果它不能作为可重复使用的包完成，至少可以为特定的 GADT 完成吗？

4

2 回答 2

12

有趣的谜题！事实证明，您可以将 data-reify 与 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 =>，这也有一个缺点：我们不再知道可能的类型仅限于Intand Bool，这意味着 . 中必须有一个Typeable e约束IfThenElse。

于 2012-09-01T23:03:22.237 回答
10

我将尝试以您的 GADT 为例，证明这可以针对特定的 GADT 完成。

我将使用Data.Reify包。这需要我定义一个新的数据结构，其中递归位置被一个参数替换。

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

reify 包中的图表如下所示（其中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

现在我们只需要从Graph 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，但我看不出它是如何完全通用的。

The complete code can be found at http://pastebin.com/FwQNMDbs .

于 2012-09-01T23:07:47.607 回答