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

本当にMuRefで行うことはできません。 GraphListsにはGraphListsが含まれていません。あなたは順番に各Exprを明示して、GraphListにそれらを潰すための一度限りのコンビネータを書くことができます：

ExprListの内容についてtraverse reifyGraphを使うだけです。

また、後者はどちらも新しいタイプである必要があります。

Answer 2

私はまったく同じ問題を抱えていましたが、私はdata-reifyを使って解決策を見つけました。

あなたが解に到達するために実現しなければならない事があることである：EDSL doesntのは、リストを持っているにもかかわらず、グラフの種類は彼らに 2が含まれている可能性が 1.同じに異なるタイプのデータを具体化することが可能です結果の型。

は、だから我々は、我々の結果の型にリストコンストラクタを追加することで起動します。

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

はその後、我々はGraphExprにexprのリストを具体化するMuRefの2番目のインスタンスを、必要とします。代わりにこれで今

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" 

を具体化しようとした場合、我々は物象化ノードIDのリストを抽出するには、結果

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 

を取得しますこのグラフから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] 

希望これは私もしばらくの間、この問題と格闘してきた、役立ちます。