how to reify a list of data using Data.Reify?

Question

I tried to read the paper (http://www.ittc.ku.edu/csdl/fpg/sites/default/files/Gill-09-TypeSafeReification.pdf) and managed to reify my symbolic expression type, but I can't figure out how to reify a list of them. Here's the simplified code:

{-# 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

I had the exact same problem, and I found a solution using data-reify.

The things you have to realise to arrive at a solution is that: 1. Even though the EDSL doesnt have lists, the graph type could contain them 2. It is possible to reify different types of data to the same result type.

So we start by adding list constructors to our result type:

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

Then we need a second instance of MuRef, that reifies lists of Expr a to GraphExpr.

instance MuRef [Expr a] where
    type DeRef [Expr a] = GraphExpr a
    mapDeRef _ [] = pure Nil
    mapDeRef f (x:xs) = Cons <$> f x <*> f xs

Now with this in place, if we try to reify a list expression

reified = reifyGraph [EBin x (EBin x y), Ebin y (EBin x y)]
              where x = EConst "x"
                    y = EConst "y"

We'll get the result

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

To extract the list of reified node-ids from this graph we can define a little function to walk the Conses and to extract the node-ids from them into a list.

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) = []

(If the graphs are huge, it might be a good idea to convert them to an IntMap before starting the walk)

This looks like a partial function, but since we know that the root of the DAG will always be a Cons-node (since we reify a list), and since we know that all node-ids are in xs this function will return a list of all node-ids in the result list.

So if we run walkConses on our resulting graph we'll get the result:

[2, 7]

Hope this helps, I've been wrestling with this problem for a while too.