An issue with EDSLs in the ``finally tagless'' tradition

newer
Strong duck typing / structural...

older
Beginning of a meta-Haskell [was:...

Brad Larsen

23 Sep 2009 23 Sep '09

9:59 p.m.

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.

Show replies by date

Luke Palmer

23 Sep 23 Sep

11:12 p.m.

On Wed, Sep 23, 2009 at 7:59 PM, Brad Larsen 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

Brad Larsen

24 Sep 24 Sep

midnight

Luke, On Wed, Sep 23, 2009 at 11:12 PM, Luke Palmer wrote:

...

On Wed, Sep 23, 2009 at 7:59 PM, Brad Larsen 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

Brad Larsen

12:24 a.m.

Luke, On Wed, Sep 23, 2009 at 11:12 PM, Luke Palmer wrote:

...

On Wed, Sep 23, 2009 at 7:59 PM, Brad Larsen 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

To elaborate a point I mentioned in my original email, and discussed in ``Unembedding Domain-Specific Languages'' by Atkey, Lindley, and Yallop: EDSLs defined using type classes in this way can be freely combined, and so you can cobble together an EDSL from several smaller EDSLs. For example, we can define an EDSL for boolean expressions: class BooleanExpr exp where true :: exp Bool false :: exp Bool cond :: exp Bool -> exp a -> exp a -> exp a (&&*) :: exp Bool -> exp Bool -> exp Bool (||*) :: exp Bool -> exp Bool -> exp Bool infixr 3 (&&*) infixr 2 (||*) Then, combined with PolyArithExprFixed, we can define an EDSL supporting polymorphic arithmetic and boolean expressions, as well as an evaluator for this language. (I've repeated the PolyArithExprFixed and previous evaluator stuff for reference.) class PolyArithExprFixed exp where pae_constant :: a -> exp a pae_add :: Num a => exp a -> exp a -> exp a class (BooleanExpr exp, PolyArithExprFixed exp) => BoolArithExpr exp -- a well-typed evaluator newtype E a = E { unE :: a } instance BooleanExpr E where true = E True false = E False cond p t f = if unE p then t else f e1 &&* e2 = E (unE e1 && unE e2) e1 ||* e2 = E (unE e1 || unE e2) instance PolyArithExprFixed E where pae_constant = E pae_add e1 e2 = E (unE e1 + unE e2) A simple test case, combining boolean expressions and arithmetic expressions: test1 = cond (true &&* false) (pae_constant 0) (pae_add (pae_constant 22) (pae_constant 20)) -- unE test1 <===> 42 Sincerely, Brad Larsen

Luke Palmer

2:15 a.m.

On Wed, Sep 23, 2009 at 10:24 PM, Brad Larsen wrote:

...

On Wed, Sep 23, 2009 at 11:12 PM, Luke Palmer wrote:

...
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

[...]

A simple test case, combining boolean expressions and arithmetic expressions:

test1 = cond (true &&* false) (pae_constant 0) (pae_add (pae_constant 22) (pae_constant 20)) -- unE test1 <===> 42

Looks great! So, where is the modularity problem? Luke

Brad Larsen

12:30 p.m.

The modularity problem I speak of is that to add a new interpretation of the DSL, I will likely have to modify the EDSL definition to add additional constraints. Ideally, I would like to be able to define the EDSL once, in a module, and be able to write arbitrary interpretations of it in other modules, without having to go back and change the EDSL definition. Regards, Bradford Larsen On Sep 24, 2009 2:15 AM, "Luke Palmer" wrote: On Wed, Sep 23, 2009 at 10:24 PM, Brad Larsen wrote:

...

On Wed, Sep 23, 2009 ...

...

...
I would like to see an example of this unmodularity, making use of the >> polymorphism, so I can ... [...]

...

...
A simple test case, combining boolean expressions and arithmetic expressions: > > test1 = con... Looks great! So, where is the modularity problem?

Luke

wren ng thornton

8:36 p.m.

Brad Larsen wrote:

...

The modularity problem I speak of is that to add a new interpretation of the DSL, I will likely have to modify the EDSL definition to add additional constraints. Ideally, I would like to be able to define the EDSL once, in a module, and be able to write arbitrary interpretations of it in other modules, without having to go back and change the EDSL definition.

The canonical, if theoretically unsatisfying, way to do this is to lift all type variables into the class specification. Thus, instead of class Foo f where foo :: forall a. a -> f a we would instead have class Foo f a where foo :: a -> f a According to the intention of the design, variables thus lifted should remain polymorphic in instances however they can have contexts applied to them: instance (Num a) => Foo F a where foo = ... The reason this is unsatisfying is that there's no way to enforce that instances don't ground these variables, which can interfere with the validity of applying certain laws/transformations. Also, if you need to lift more than one variable in the same class then it can be tricky to do the encoding right. For instance, when converting Monad into this form (e.g. so we can define an instance for Set) it is prudent to separate it into one class for return and another for join/(>>=)/(>>). But it does solve the problem at hand. -- Live well, ~wren

Brad Larsen

25 Sep 25 Sep

12:17 a.m.

Wren, On Thu, Sep 24, 2009 at 8:36 PM, wren ng thornton wrote:

...

Brad Larsen wrote:

...
The modularity problem I speak of is that to add a new interpretation of the DSL, I will likely have to modify the EDSL definition to add additional constraints. Ideally, I would like to be able to define the EDSL once, in a module, and be able to write arbitrary interpretations of it in other modules, without having to go back and change the EDSL definition.

The canonical, if theoretically unsatisfying, way to do this is to lift all type variables into the class specification. Thus, instead of

class Foo f where foo :: forall a. a -> f a

we would instead have

class Foo f a where foo :: a -> f a

According to the intention of the design, variables thus lifted should remain polymorphic in instances however they can have contexts applied to them:

instance (Num a) => Foo F a where foo = ...

The reason this is unsatisfying is that there's no way to enforce that instances don't ground these variables, which can interfere with the validity of applying certain laws/transformations. Also, if you need to lift more than one variable in the same class then it can be tricky to do the encoding right. For instance, when converting Monad into this form (e.g. so we can define an instance for Set) it is prudent to separate it into one class for return and another for join/(>>=)/(>>). But it does solve the problem at hand.

-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I have experimented some in the past day with this canonical technique of lifting type variables into the class specification. This is somewhat successful; however, one problem is that when multiple variables are lifted into the specification, ambiguity creeps in (and over-generality?), in the absence of superclass constraints or functional dependencies. So, for example, Foo seems to work well, but Bar does not: class Foo a where ... class Bar a b where ... One can alleviate the ambiguity of Bar by splitting it into two classes, similarly to splitting up Monad: class PreBar a where ... class (PreBar a) => Bar a b where ... It's not clear to me that such a decomposition is always possible. I'll keep experimenting with modular, tagless EDSLs... Sincerely, Brad

wren ng thornton

11:26 p.m.

Brad Larsen wrote:

...

On Thu, Sep 24, 2009 at 8:36 PM, wren ng thornton wrote:

...
The reason this is unsatisfying is [...] if you need to lift more than one variable in the same class then it can be tricky to do the encoding right. For instance, when converting Monad into this form (e.g. so we can define an instance for Set) it is prudent to separate it into one class for return and another for join/(>>=)/(>>).

As you say :)

...

I have experimented some in the past day with this canonical technique of lifting type variables into the class specification. This is somewhat successful; however, one problem is that when multiple variables are lifted into the specification, ambiguity creeps in (and over-generality?), in the absence of superclass constraints or functional dependencies. [...] One can alleviate the ambiguity of Bar by splitting it into two classes, similarly to splitting up Monad: [...] It's not clear to me that such a decomposition is always possible. I'll keep experimenting with modular, tagless EDSLs...

I don't know that it will always work (though Oleg could say for sure). For simple classes like Monad and similar algebraic concepts, it works quite well; but then the maths are sort of designed that way. The more you move to large families of complexly interconnected methods, the more it seems likely it'll break down or require fundeps/typefamilies to resolve ambiguity cleanly. Depending on exactly what your goal is re multiple interpretation, Ralf Hinze has some nice work on the "lifting lemma" for re-interpreting lambda-calculus syntax under different idioms: http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8//26/slides/ralf.pdf -- Live well, ~wren

Peter Gammie

24 Sep 24 Sep

12:22 a.m.

Brad: On 24/09/2009, at 11:59 AM, excerpts of what Brad Larsen wrote:

...

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.)

A better fix is to shift the type constraint to the class head, e.g.: class PolyArithExprFixed exp a where pae_constant :: a -> exp a pae_add :: exp a -> exp a -> exp a then: instance PolyArithExprFixed E Integer where ... or if you want to be more general: instance Num n => PolyArithExprFixed E n where ... but note that this instance precludes any other ones for PolyArithExprFixed without allowing overlapping instances and hence some Olegs / Olegging. See, e.g.: http://www.soi.city.ac.uk/~ross/papers/fop.html (the slides link) Ambiguity is IMHO best handled with a judicious application of type (or data) families, but you can get surprisingly far by simply requiring that every class member mention all type variables in the class head. YMMV of course. cheers peter

Brad Larsen

12:45 a.m.

Peter, On Thu, Sep 24, 2009 at 12:22 AM, Peter Gammie wrote: [...]

...

Ambiguity is IMHO best handled with a judicious application of type (or data) families, but you can get surprisingly far by simply requiring that every class member mention all type variables in the class head. YMMV of course.

cheers peter

Can you say more about the use of type/data families? Sincerely, Brad

Peter Gammie

1:10 a.m.

Brad, On 24/09/2009, at 2:45 PM, Brad Larsen wrote:

...

On Thu, Sep 24, 2009 at 12:22 AM, Peter Gammie wrote: [...]

...
Ambiguity is IMHO best handled with a judicious application of type (or data) families, but you can get surprisingly far by simply requiring that every class member mention all type variables in the class head. YMMV of course.

Can you say more about the use of type/data families?

Multi-parameter type classes generally lead to ambiguity - see the classic paper(s) by Simon PJ et al for some good examples. In the context of Arrows, I used type/data families to make the representation type (e.g. Integer) a function of the arrow (e.g. a direct semantics), which makes life a bit easier for using this stuff but is not completely faithful to what I wanted. (Imagine you want to mix Integer and Double in the same expression.) Hope this helps! cheers peter -- http://peteg.org/

5721

Age (days ago)

5723

Last active (days ago)

List overview

Download

11 comments

4 participants

participants (4)

Brad Larsen
Luke Palmer
Peter Gammie
wren ng thornton