Tagless interpreter, expression problem and zipper

Hello everyone, I am stuck rewriting some code in the tagless style. My problem can be thought of as an interpreter for a very simple language:
data Exp = Lit Integer | Add Exp Exp | Mul Exp Exp deriving (Show)
But some complexity is added by the fact that my interpreter also needs to know the context in which literals appear in an expression. So given the example
t1 :: Exp t1 = (Lit 3 `Add` Lit 4) `Mul` Lit 2
I want to have access to the fact that the literal 3 appears on the left side of an addition. Therefore I created a type:
data Ctx = Empty | AddL Exp Ctx | AddR Exp Ctx | MulL Exp Ctx | MulR Exp Ctx deriving (Show)
This is almost a zipper over the Exp type. I left out a context for literals themselves because it wasn't necessary. Now I can create a simple evaluation function:
eval :: (a -> a -> a) -> (a -> a -> a) -> (Integer -> Ctx -> a) -> Exp -> a eval add mul lit = go Empty where go ctx (Lit n) = lit n ctx go ctx (Add x y) = let x' = go (AddL y ctx) x y' = go (AddR x ctx) y in x' `add` y' go ctx (Mul x y) = let x' = go (MulL y ctx) x y' = go (MulR x ctx) y in x' `mul` y'
This function can evaluate an expression to any type 'a', but it needs some additional functions to accomplish that: add, mul and lit. Notice how the 'lit' function has access to a literal's context. To interpret an Exp as an Integer I use:
evalInt :: Exp -> Integer evalInt = eval (+) (*) const
Or as a String:
evalStr1 :: Exp -> String evalStr1 = eval addStr mulStr (const . show)
addStr x y = "(" ++ x ++ " + " ++ y ++ ")" mulStr x y = "(" ++ x ++ " * " ++ y ++ ")"
Or a silly example which uses the context:
evalStr2 :: Exp -> String evalStr2 = eval addStr mulStr lit where lit _ (AddL (Lit 4) (MulL _ _)) = "Foo!" lit n _ = show n
The silly example replaces a literal with "Foo!" if it appears on the left side of an addition with 4, and the whole addition is the left side of a multiplication, like in (x + 4) * ?. All of this works. But I want to be able to add additional constructors to the Exp language without changing existing code. This looks like the expression problem. Ignoring the zipper-like context I came up with the following: First define the language:
class Lit a where lit :: Integer -> a class Add a where add :: a -> a -> a class Mul a where mul :: a -> a -> a
Integer interpreter:
instance Lit Integer where lit = fromInteger instance Add Integer where add = (+) instance Mul Integer where mul = (*)
String interpreter, using a newtype so I don't need TypeSynonymInstances:
newtype Str = Str {unS :: String} instance Show Str where show = show . unS
instance Lit Str where lit = Str . show instance Add Str where add x y = Str $ addStr (unS x) (unS y) instance Mul Str where mul x y = Str $ mulStr (unS x) (unS y)
Same example expression, now polymorphic:
t1 :: (Lit a, Add a, Mul a) => a t1 = (lit 3 `add` lit 4) `mul` lit 2
This expression can now be interpreted in multiple ways:
t1 :: Integer
14 t1 :: Str "((3 + 4) * 2)"
This solves the expression problem. I can add new structures to my language in other modules without having to change existing code. The necessary parts are mentioned in the type constraint (Lit a, Add a, Mul a). But I lost the power of the context! How do I get it back? Attached are the two approaches, WithTags.hs and Tagless.hs (but without context). Any help would be greatly appreciated!

2011/3/8 Roel van Dijk
Hello everyone,
Hello!
But I lost the power of the context! How do I get it back?
The tagless interpreters splits the interpreter code (in your case, the 'eval' function) into multiple functions on one or more type classes. Now, the key insight is that your interpreter is actually not 'eval' but 'go' =), which has type 'Ctx -> a' (instead of just 'a'). But you don't need to change any code that uses Lit, Add and Mul, they work unmodified. First of all, I'll generalize your context a bit: data Ctx a = Empty | AddL a (Ctx a) | AddR a (Ctx a) | MulL a (Ctx a) | MulR a (Ctx a) deriving (Show) Now we can create a new interpreter: newtype CtxInterpA a = CIA {unCIA :: Ctx a → a} I'm appending A to its name because later on I'll propose another interpreter B. The underlying type 'a' is the same 'a' from your original 'eval' function, so we can't use 'lit' from 'Lit' type class. So we create class CtxLitA a where ctxLitA :: Integer → Ctx a → a Our interpreter's instance for 'Lit' is then simply instance CtxLitA a ⇒ Lit (CtxInterpA a) where lit = CIA∘ctxLitA To get a result from 'CtxInterpA a' we just pass an empty context: fromCtxInterpA :: CtxInterpA a → a fromCtxInterpA x = unCIA x Empty The 'Add' instance, however, is somewhat problematic. We need an 'a' for our 'Ctx a', however the arguments given for 'add' are of type 'CtxInterpA a'. To get an 'a' from 'CtxInterpA a' we need, again, a 'Ctx a'. instance Add a ⇒ Add (CtxInterpA a) where add x y = CIA (λctx → let x' = unCIA x (AddL y' ctx) y' = unCIA y (AddR x' ctx) in x' `add` y') The main problem with this instance with respect to your original 'eval' code is that in 'AddL' and 'AddR' we have y' and x', and not y and x. So y' and x' are mutually recursive. The Mul instance is similar. This may or may not be what you wanted on your original problem. Note, however, that there's a plan B. We can have different definitions of CtxLitA and CtxInterpA, this time using 'Ctx Exp': class CtxLitB a where ctxLitB :: Integer → Ctx Exp → a data CtxInterpB a = CIB {cibMake :: Ctx Exp → a ,cibExp :: Exp} Besides our function that creates 'a's, we also keep note of the corresponding 'Exp' and use it to create the 'Ctx Exp' without mutual recursion: instance CtxLitB a ⇒ Lit (CtxInterpB a) where lit i = CIB (ctxLitB i) (lit i) instance Add a ⇒ Add (CtxInterpB a) where add x y = CIB (λctx → let x' = cibMake x (AddL (cibExp y) ctx) y' = cibMake y (AddR (cibExp x) ctx) in x' `add` y') (add (cibExp x) (cibExp y)) The drawback of this approach should be obvious: we are tagging everything =). So this sort of defeats the tagless interpreter approach. I don't know if this solves your real problem, but it may be a start =). I'm attaching everything. Cheers, -- Felipe.
participants (2)
-
Felipe Almeida Lessa
-
Roel van Dijk