How to use literal haskell functions in DSL?

Question

I'd like to use literal haskell functions in a dsl as follows:

program :: forall m . DSL m => m ()
program = do
  stm $ Stm (Var "a")
  -- this way:
  f <- fun $ \(a :: Expr a) (b :: Expr b) -> do
    -- function body is of the same monad `m` as the one in top level
    stm $ Stm (Var "b")
  stm $ Stm $ Apply f (Var "c")
  pure ()

.. and turn the above into code ([Stm]).

To make the functions work there is a helper class Fun (code below) that saturates the function with fresh variables until it reaches function body, then returns both the list of arguments and body itself so that they could be made into function syntax[1]. There is a recursive case to generate arguments[2] and a base case to evaluate body to [Stm].[3]

The worrisome instance is the base case[4], which currently requires {-# INCOHERENT #-}, because ghc can't choose a Fun instance because function's body in the program is ambiguous (while it should just be whatever m is at top level code).

So the question is:

• is there a way to force the body to always use the same m as in top level and not require incoherent instances?

---

A stub AST, the MTL-style DSL "effect" and a sample instance of the class:

-- | An AST
data Expr a
  = Var String
  | Apply String (Expr a)
  | Function String [String] [Stm]

data Stm = Stm (Expr ())

-- | The "effect"
class Monad m => DSL m where
  freshName :: m String -- generate fresh variable name
  stm :: Stm -> m () -- emit statement
  toAST :: m a -> m [Stm] -- turn code `m a` into [Stm] (without emitting it)
  fun :: Fun f m => f -> m String -- emit function f, return its name

-- | Helper class to convert literal haskell functions to the dsl
class Fun f m where
  mkFun :: DSL m => f -> [String] -> m ([String], [Stm])

instance Fun f m => Fun (Expr a -> f) m where
  mkFun f acc = do
    name <- freshName -- [2]
    mkFun (f $ Var name) (name : acc)

instance {-# INCOHERENT #-} (m0 ~ m) => Fun (m0 a) m where -- [4]
  mkFun m args = do
    fname <- freshName
    body <- toAST m -- [3]
    return (args, body)

-- | A sample implementation
instance DSL (StateT Int (Writer [Stm])) where
  freshName = do
    n <- get
    put $ n + 1
    return $ "var" <> show n
  stm stm' = tell [stm']
  toAST m = do
    state0 <- get
    let ((_, state1), w) = run m state0
    put state1
    return w
  fun f = do
    (args, body) <- mkFun f []
    name <- freshName
    stm $ Stm $ Function name args body -- [1]
    return name

run :: StateT Int (Writer [Stm]) a -> Int -> ((a, Int), [Stm])
run m s = runWriter $ runStateT m s

Answer 1

I guess one way is to mark the base case of the recursion yourself.

newtype Cook m a = Cook (m a)
deriving instance DSL m => DSL (Cook m)

instance Fun f m => Fun (Expr a -> f) m
instance m0 ~ m => Fun (Cook m0 a) (Cook m)

type SampleImplRaw = StateT Int (Writer [Stm])
type SampleImpl = Cook SampleImplRaw

instance DSL SampleImpl

I haven't typed this into the compiler, so I'm not sure, but it may be that you get into a funny situation where you want a DSL m instance, and have a DSL (Cook m) instance in scope, but the compiler can't figure out how to get from A to B. In such a case it should be possible to coerce the offending term to use the Cook m instance.

Another way might be to try making the base case have a different kind. Something like this:

instance Fun f m => Fun (Expr a -> f) m
instance (m ~ m', p ~ p', p ~ '()) => Fun (m p a) (m' p')

data SampleImplRaw (x :: ()) a = {- whatever you would have written before for new data declarations -}
type SampleImpl = SampleImplRaw '()
newtype Const1 (x :: ()) m a = Const1 (m a) deriving (EVERYTHING) -- still need a cook for mere monad transformer stacks

I guess probably if your plan is mostly to use transformer stacks, the first one will be less roundabout; if your plan is mostly to define new data types, the second will have a cleaner user experience.