我如何恢复GADT中的共享？ [英] How can I recover sharing in a GADT?

问题描述

在 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转换为

$ b来恢复共享
$ b

  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 返回a Map 。

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

有趣的拼图！事实证明，您可以使用GADT进行数据验证。你需要的是一个隐藏在存在中的类型的包装器。该类型稍后可以通过 Type 数据类型上的模式匹配来检索。

  data类型a其中
 Bool :: Type Bool 
 Int :: Type Int 
 
 data WrappedAst s其中
 Wrap :: Type e  - > Ast2 e s  - > WrappedAst s 
 
实例MuRef（Ast e）其中
类型DeRef（Ast e）= WrappedAst 
 mapDeRef f e = Wrap（getType e）< $> mapDeRef'f e 
其中
 mapDeRef':: Applicative f => （全部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） - >类型e  - >名称 - >也许（Ast2 e名称）
 getVar m t n = case m！ n包装包装 - > （\ Refl  - > e）< $> typeEq t t'
  

以下是整个代码： https://gist.github.com/3590197

编辑：我喜欢在另一个答案中使用 Typeable 。所以我也使用了 Typeable 的代码版本： https： //gist.github.com/3593585 。代码显着缩短。 Type e - > 被替换为 Typeable e => ，这也有一个缺点：我们不再知道可能的类型限制为 Int 和 Bool ，这意味着必须有一个在 IfThenElse 中可键入的e 约束。

In Type-Safe Observable Sharing in Haskell Andy Gill shows how to recover sharing that existed on the Haskell level, in a DSL. His solution is implemented in the data-reify package. Can this approach be modified to work with GADTs? For example, given this 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

I'd like to recover sharing by transforming the above AST to

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

by the way of a function

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

(I'm not sure about the type of recoverSharing.)

Note that I don't care about introducing new bindings via a let construct, but only in recovering the sharing that existed on the Haskell level. That's why I have recoverSharing return a Map.

If it can't be done as reusable package, can it at least be done for specific GADT?

解决方案

Interesting puzzle! It turns out you can use data-reify with GADTs. What you need is a wrapper that hides the type in an existential. The type can later be retrieved by pattern matching on the Type data 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'

Here's the whole code: https://gist.github.com/3590197

Edit: I like the use of Typeable in the other answer. So I did a version of my code with Typeable too: https://gist.github.com/3593585. The code is significantly shorter. Type e -> is replaced by Typeable e =>, which also has a downside: we no longer know that the possible types are limited to Int and Bool, which means there has to be a Typeable e constraint in IfThenElse.

这篇关于我如何恢复GADT中的共享？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！