20

Andy Gillは、 Haskellレベルで存在していた共有を DSL で復元する方法を示しています。彼のソリューションは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

面白いパズル！GADT で data-reify を使用できることがわかりました。必要なのは、存在の型を隠すラッパーです。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 =>に限定されていることがわかりません。これは、 に制約が必要であることを意味します。IntBoolTypeable eIfThenElse

于 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 で利用可能だった多くの型情報を削除していることに注意してください。最初の 3 つのコンストラクターについては、関連付けられた型 (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が正しく共有を回復したことを示しています。2 行目は、Ast2 Int型のみが見つかったことを示しています (これも正しいです)。

この方法は、他の特定の GADT に簡単に適用できますが、完全に一般的なものにする方法がわかりません。

完全なコードはhttp://pastebin.com/FwQNMDbsにあります。

于 2012-09-01T23:07:47.607 に答える