This is already an improvement to my current code. But I am not entirely satisfied. I can pick and choose which structures to use in my terms but the context type is still an ordinary data type. Each module which extends the expression language with new structures needs to define a complicated context type.

But the context type does not have to be complicated. There is no rule mandating the single context for any expression. For different sorts of processing, one may define suitable contexts, containing only the needed data. The example from the earlier message had to do something special for a literal that is the left immediate child of Add whose brother has specific value. That example requires a simple context. Here is the complete code, a small simplification of the code in the previous message.

class Lit r where lit :: Integer -> r class Add r where add :: r -> r -> r

instance Lit Integer where lit = fromInteger instance Add Integer where add = (+)

instance Lit String where lit = show instance Add String where add x y = "(" ++ x ++ " + " ++ y ++ ")"

data AddLCtx r = AddL r | NotAddL

instance (Add r, Add s) => Add (AddLCtx s -> r, s) where add (xa, xb) (ya, yb) = ( \c -> add (xa (AddL yb)) (ya NotAddL) , add xb yb )

-- Silly interpreter, version 2.0

instance Lit (AddLCtx Integer -> String, Integer) where lit n = ( \c -> case c of AddL 3 -> "Foo!" _ -> lit n , lit n )

t1 :: (Lit r, Add r) => r t1 = lit 2 `add` lit 3

bar = let (f, x) = t1 :: (AddLCtx Integer -> String, Integer) in f NotAddL -- "(Foo! + 3)"

Later on, we add multiplication.

class Mul r where mul :: r -> r -> r instance Mul Integer where mul = (*) instance Mul String where mul x y = "(" ++ x ++ " * " ++ y ++ ")"

We extend the Ctx interpreter for Mul, assuming AddLCtx meant the immediate left child of the Addition. If a left descendant was meant, the mul rule below should propagate the context rather than override it.

instance (Mul r, Mul s) => Mul (AddLCtx s -> r, s) where mul (xa, xb) (ya, yb) = ( \c -> mul (xa NotAddL) (ya NotAddL) , mul xb yb )

t2 :: (Lit r, Add r, Mul r) => r t2 = (lit 2 `add` lit 3) `mul` (lit 4 `mul` (lit 5 `add` lit 3))

bar' = let (f, x) = t2 :: (AddLCtx Integer -> String, Integer) in f NotAddL -- "((Foo! + 3) * (4 * (Foo! + 3)))"

Let's implement the example in the original message, and do something special at the left immediate child of addition whose brother is so and so and whose parent context is the left child of multiplication. We define the context that suits the problem, tracking if we are the left child of multiplication and if we are the left child of addition that is the left child of multiplication. It is easier done than said.

data AddML r = AddML r | MulL | NotAddML

instance (Add r, Add s) => Add (AddML s -> r, s) where add (xa, xb) (ya, yb) = ( \c -> (case c of MulL -> add (xa (AddML yb)) (ya NotAddML) _ -> add (xa NotAddML) (ya NotAddML)) , add xb yb )

instance (Mul s, Mul r) => Mul (AddML s -> r, s) where mul (xa, xb) (ya, yb) = (\c -> mul (xa MulL) (ya NotAddML), mul xb yb)

The original example:

instance Lit (AddML Integer -> String, Integer) where lit n = ( \c -> case c of AddML 3 -> "FooM!" _ -> lit n , lit n )

bar'' = let (f, x) = t2 :: (AddML Integer -> String, Integer) in f NotAddML -- "((FooM! + 3) * (4 * (5 + 3)))"

The fully safe and explicit Typeable in http://okmij.org/ftp/tagless-final/course/Typ.hs shows example of defining many interpreters with many contexts. It was the tough problem though -- the first example showing how to compare to tagless-final terms for equality.