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

[Brad Larsen]

Luke,

On Wed, Sep 23, 2009 at 11:12 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
> On Wed, Sep 23, 2009 at 7:59 PM, Brad Larsen <brad.larsen at gmail.com> wrote:
>> 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.)
>
> I don't know what you expect from pae_add, such that it could "add" a
> couple of a's without knowing anything about them.  Don't think of Num
> as a implementation detail, think of it as information about that a.
> An implementation which adds another typeclass constraint is requiring
> too much information, and either the implementation is undefinable
> (that happens, but it's always for a good reason), or the interface is
> weaker than you wrote.
>
> I don't know what kind of implementation would add another constraint
> on a.  Are you referring maybe to a specialized interpreter for
> Integer math?  Well, if this is truly a polymorphic type that needs a
> constructor class, there could be some non-Integer math in the middle
> somewhere, and your interpreter would be incorrect.
>
> I would like to see an example of this unmodularity, making use of the
> polymorphism, so I can understand what you're asking better.
>
> Luke


The idea with these type classes is that an EDSL can be defined,
separately from any interpretation of its programs.

Instead of evaluating an EDSL program, suppose you want to
pretty-print it, using some pretty-printing type class, along the
lines of this:

    import Text.PrettyPrint

    class PrettyPrintable a where
      pretty :: a -> Doc

    newtype P = P { unP :: Doc }

    instance PolyArithExpr P where
      constant  = P . pretty                                -- bzzt!
Cannot deduce (PrettyPrintable a)
      add e1 e2 = P (pretty e1 <+> text "+" <+> pretty e2)  -- bzzt!
Cannot deduce (PrettyPrintable a)

To write a pretty-printing interpretation for polymorphic arithmetic
expressions, we do not need a Num constraint, but we do need a
PrettyPrintable constraint.  So, we might ``remedy'' the definition of
PolyArithExpr so that we could write the evaluator and pretty-printer:

    class PolyArithExprFixedAgain exp where
      constant_fixed_again :: (Num a, PrettyPrintable a) => a -> exp a
      add_fixed_again      :: (Num a, PrettyPrintable a) => a -> exp a

Similarly, if we wanted to marshall an EDSL program over the network
or to disk, we would have to modify PolyArithExprFixedAgain to add
another constraint.  Such modification would be necessary for other
interesting interpretations, such as compilation to native code.

Perhaps the problem I have encountered is more clear now.  With my
current approach, the EDSL ``language definition'' and interpretations
of EDSL programs are intertwined.  Hence, this is a close relative of
the ``expression problem''.  I want language definition and language
interpretations to be decoupled.


Sincerely,
Brad Larsen