Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Interpreting an abstract syntax graph efficiently

Take a minimal language (apparently called Hutton's Razor):

{-# OPTIONS_GHC -fno-warn-missing-methods #-}

data Expr =
    Lit Int
  | Add Expr Expr
  deriving (Eq, Show)

instance Num Expr where
  fromInteger = Lit . fromInteger
  (+)         = Add

tree 0 = 1
tree n =
  let shared = tree (n - 1)
  in  shared + shared

If we just run tree 30 in GHCi, the type will default to Integer and we'll get an immediate answer as recursive computations of tree are shared. But if we run tree 30 :: Expr, we get an enormous syntax tree as the sharing provided by Haskell's let doesn't transfer to expressions in the embedded language.

The data-reify library can be used to observe any implicit sharing that might be present in an expression. We can add some machinery to enable that:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeFamilies #-}

import Control.Applicative
import Data.Reify

data ExprF e =
    LitF Int
  | AddF e e
  deriving (Eq, Show, Functor)

instance MuRef Expr where
  type DeRef Expr = ExprF
  mapDeRef f (Add e0 e1) = Add <$> f e0 <*> f e1
  mapDeRef _ (Lit d)     = pure (LitF d)

And applying the reifyGraph function to an expression like tree 30 :: Expr now returns a graph where sharing is explicit. Here's a more digestible example:

> reifyGraph (tree 2 :: Expr)
let [(1,AddF 2 2),(2,AddF 3 3),(3,LitF 1)] in 1

So now I'm interested in interpreting an abstract syntax graph rather than an abstract syntax tree.

A naive evalGraph function eliminates sharing by interpreting it as if it were a tree:

evalGraph (Graph env r) = go r where
  go j = case lookup j env of
    Just (AddF a b) -> go a + go b
    Just (LitF d)   -> d
    Nothing         -> 0

as can be verified by trying

> evalGraph <$> reifyGraph (tree 50 :: Expr)

Not being all that experienced in this sort of thing, I have found it surprisingly difficult to come up with an simple and efficient implementation of evalGraph.

Oliveira and Löh provide an example in which a graph like this is used to build an expression in a proxy language where sharing is explicit (which can then just be evaluated in that setting), but it seems like that's an unnecessarily heavyweight approach to take if I just want to consume the graph immediately.

What is the best approach to evaluate this type of graph while preserving its sharing?

Edit:

Memoization à la Data.StableMemo handles everything perfectly right from the get-go, but given some syntax in a DAG structure (for whatever reason), I think that the topological sort + memoization is the right way to go here.

Here's a quick/hacky graph-based evaluator:

import Data.Graph
import Data.Maybe
import System.IO.Unsafe

graphEval :: Expr -> Int
graphEval expr = consume reified where
  reified = unsafePerformIO (toGraph <$> reifyGraph expr)
  toGraph (Reify.Graph env _) = graphFromEdges . map toNode $ env
  toNode (j, AddF a b) = (AddF a b, j, [a, b])
  toNode (j, LitF d)   = (LitF d, j, [])

consume :: Eq a => (Graph, Vertex -> (ExprF a, a, b), c) -> Int
consume (g, vmap, _) = go (reverse . topSort $ g) [] where
  go [] acc = snd $ head acc
  go (v:vs) acc =
    let nacc = evalNode (vmap v) acc : acc
    in  go vs nacc

evalNode :: Eq a => (ExprF a, b, c) -> [(a, Int)] -> (b, Int)
evalNode (LitF d, k, _)   _ = (k, d)
evalNode (AddF a b, k, _) l =
  let v = fromJust ((+) <$> lookup a l <*> lookup b l)
  in  (k, v)
like image 544
jtobin Avatar asked May 30 '14 06:05

jtobin


People also ask

What is abstract interpretation?

•Abstract interpretation was invented partially to find a firm semantic foundation for data flow analysis •Precise relationship between concrete domain (program executions) and abstract domain (data flow facts) •Generic correctness proof •Caveat: Data flow typically uses meet, abstract interpretation typically uses join 22

How to construct and interpret graphs?

How to Construct and Interpret Graphs 1 Drawing a Graph. To see how a graph is constructed from numerical data, we will consider a hypothetical example. ... 2 The Slope of a Curve. In this section, we will see how to compute the slope of a curve. ... 3 A Graph Showing a Negative Relationship. ... 4 Shifting a Curve. ... 5 Rotating a Curve. ...

What is abstraction?

Abstraction is Imprecise 4 Abstraction function α maps each concrete set to the best abstract value α Concrete values: sets of integers Abstract values Stephen Chong, Harvard University Composing α and γ

What is the abstraction function α4?

4 Abstraction function α maps each concrete set to the best abstract value α Concrete values: sets of integers Abstract values Stephen Chong, Harvard University Composing α and γ 5


2 Answers

You need not give up on the tree approach yet. Sharing does indeed occur, the problem is just that function calls are not memoized even over shared subexpressions.

You can solve this quite easily by using identity based memoization in your eval function.

eval = go
 where go = memo eval'
       eval' (Lit i) = i
       eval' (Add e1 e2) = go e1 + go e2

I tested this using the stable-memo package and it seems to work well.

like image 120
firefrorefiddle Avatar answered Nov 06 '22 18:11

firefrorefiddle


Assuming your graph is a DAG, the problem is quite simple:

  1. Order nodes topologically
  2. Evaluate in order, looking up values as you go.

It would work like this for your example:

Reverse the nodes to:

[(3,LitF 1),(2,AddF 3 3),(1,AddF 2 2)]

Then evaluate them in order, looking up the previous values:

[1,2,4]
like image 44
nulvinge Avatar answered Nov 06 '22 16:11

nulvinge