Tagless final DSL with RValue LValue problems

Question

Typed Tagless Final Interpreters are an interesting alternative to the free monad approach.

But even with a quite simple ToyLang example in tagless final style ambiguous type variables pop up.

ToyLang is an EDSL that should read something like this:

toy :: ToyLang m => m (Maybe Int)
toy = do
    a <- int "a"       -- declare a variable and return a reference
    a .= num 1         -- set a to 1
    a .= a .+ num 1    -- add 1 to a
    ret a              -- returns a

The general goal is, of course, to use the Haskell type system as much as possible in this EDSL, and use polymorphism to instantiate various interpreters.

All would be well if it weren't for the (.+) operation which leads to the notion of lvalue and rvalue: The assignment operator (.=) has a lvalue to its left and either an lvalue or rvalue to its right. The basic idea is taken from two comments in Impredicative Polymorphisms, a Use Case:

{-# LANGUAGE GADTs #-}

data L -- dummies for Expr (see the comments for a better way)
data R

-- An Expr is either a lvalue or a rvalue
data Expr lr where
    Var :: String -> Maybe Int -> Expr L
    Num :: Maybe Int -> Expr R

-- tagless final style
class Monad m => ToyLang m where
    int :: String -> m (Expr L)             -- declare a variable with name
    (.=) :: Expr L -> Expr lr -> m (Expr L) -- assignment
    (.+) :: Expr lr -> Expr lr' -> Expr R   -- addition operation - TROUBLE!
    ret :: Expr lr -> m (Maybe Int)         -- return anything
    end :: m ()                             -- can also just end

A pretty-print 'interpreter' would start like this:

import Control.Monad.Writer.Lazy

-- A ToyLang instance that just dumps the program into a String
instance ToyLang (Writer String) where
    int n = do
        tell $ "var " <> n <> "\n"
        return (Var n Nothing)
    (.=) (Var n _) e = do
        tell $ n <> " = " <> toString e <> "\n"
        return $ Var n (toVal e)
    ...

where the little helper toString has to dig out the values from the summands of the GADT:

toString :: Expr lr -> String
toString (Var n mi) = n
toString (Num i)    = show i

The smart constructor num is simply

num :: Int -> Expr R
num = Num . Just

The (.+) is troublesome for two reasons:

1. (.+) is not in the monad m because otherwise we can't write a .= a + num 1, but for the Writer String instance, for example, the monad is needed in order to tell.

2. The typechecker barks at the ambiguous types created by (.+) :: Expr lr -> Expr lr' -> Expr R. It is clear that it would, without further annotation it can't decide which instance is meant. But annotating a clause like a .= a .+ num 1, if at all possible, would make the DSL very clunky.

One way to make the types work is by moving (.+) into the monad to some extent, and (.=), too:

 class Monad m => ToyLang m where
    ...
    (.=) :: Expr L -> m (Expr lr) -> m (Expr L)
    (.+) :: Expr lr -> m (Expr lr') -> m (Expr R)
    ...

All this is strange, though:

• (.=) and (.+) are asymmetric in where they need the monad m and where they don't.

• Even in the Writer String monad I'm forced to do integer arithmetic in order to create the m (Expr R) return type, although there isn't really any need for the result

• Instantiating ToyLang as a Writer String looks neat, but doesn't really do the job. a .= a .+ num 1 cannot be pretty-printed as such because a .+ num 1 gets evaluated (hence printed) before the .=.

This is somehow all wrong, I feel. Is there a better way to do this?

The source code for this ToyLang example is on github.

References:

• Typed Tagless Final Interpreters by Oleg Kiselyov
• Impredicative polymorphism, a use case by augustss
• Why Free Monads Matter by Gabriel Gonzalez
• Tagless Final Encoding in Haskell by J. P. Royo Sales