[Haskell-cafe] An issue with EDSLs in the ``finally tagless'' tradition

[Brad Larsen]

I seem to have run into an instance of the expression problem [1], or
something very similar, when experimenting with ``finally tagless''
EDSLs, and don't see a good way to work around it.

I have been experimenting with embedded DSLs, using the techniques
described in a couple recent papers [2,3].  The idea is this:
implement an embedded DSL using type classes, rather than ADTs or
GADTs.  This allows one to define analyses, queries, and manipulations
of EDSL programs independently, as class instances.  Furthermore, by
using type classes rather than data types, there is no interpretive
overhead in the analyses, queries, and manipulations on the EDSL
programs.  Finally, using type classes permits greater modularity, as
an EDSL can be defined as the combination of several simpler EDSLs
[3].

Suppose we have a type class for simple integer arithmetic expressions:

> class IntArithExpr exp where
>   integer :: Integer     -> exp Integer
>   add     :: exp Integer -> exp Integer -> exp Integer

We can write an evaluator for these expressions like this:

> newtype E a = E { eval :: a }
>
> instance IntArithExpr E where
>   integer   = E
>   add e1 e2 = E (eval e1 + eval e2)
>
> -- eval $ add (integer 20) (integer 22) <==> 42

The trouble comes in when defining a more general arithmetic
expression type class.  Suppose we want polymorphic arithmetic
expressions:

> class PolyArithExpr exp where
>   constant :: a     -> exp a
>   addP     :: exp a -> exp a -> exp a

We then try to define an evaluator:

> -- instance PolyArithExpr E where
> --   constant   = E
> --   addP e1 e2 = E (eval e1 + eval e2)  -- bzzt!

The instance definition for `addP' is not type correct:
    Could not deduce (Num a) from the context ()
      arising from a use of `+' at /home/blarsen/mail.lhs:42:20-36

One way to remedy this is to change the class definition of
PolyArithExpr so that `addP' has a Num constraint on `a':

> class PolyArithExprFixed exp where
>   pae_constant :: a -> exp a
>   pae_add      :: Num a => exp a -> exp a -> exp a

which allows us to define an evaluator:

> instance PolyArithExprFixed E where
>   pae_constant = E
>   pae_add e1 e2 = E (eval e1 + eval e2)

I find this ``fix'' lacking, however: to define a new interpretation
of the EDSL, we may be forced to change the DSL definition.  This is
non-modular, and seems like an instance of the expression
problem. (There may be a multiparameter type class solution for this.)

How can one define the polymorphic arithmetic EDSL without cluttering
up the class definitions with interpretation-specific constraints, and
still write the desired interpretations?


Sincerely,
Bradford Larsen



References:

  [1] Philip Wadler.  The Expression Problem.  November 12, 1998.
      http://www.daimi.au.dk/~madst/tool/papers/expression.txt.

  [2] Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.  Finally
      Tagless, Partially Evaluated: Tagless Staged Interpreters for
      Simpler Typed Languages.  APLAS 2007.

  [3] Robert Atkey, Sam Lindley, and Jeremy Yallop.  Unembedding
      Domain-Specific Languages.  ICFP Haskell Symposium 2009.