如何在GADT中恢复共享？

Question

在Haskell中的类型安全可观察共享中 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进行吗？

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,这意味着必须有一个Typeable e约束IfThenElse.

Answer 2

我将尝试使用您的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

现在,我们只需要找到一个函数曲线图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找到.