Tom Schrijvers wrote:

...

Yeah, subject "Finally Tagless" again, sorry, I'm just not done with it yet.

In Olegs haskell implementation he is using classes mainly to model the syntax and instances to use for evaluators / compilers to allow multiple interpretations.

I wonder if it'd be possible to do the same without classes using data types instead?

Something similar to what Luke Palmer has done here:

http://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-t...

You can just use the dictionary translation of type classes to replace them with data types:

E.g.

class Eval sem where val :: Int -> sem Int add :: sem Int -> sem Int -> sem Int

...

-->

data EvalDict sem = EvalDict { val :: Int -> sem Int, add :: sem Int -> sem Int -> sem Int }

This is the way to program in the final tagless style without using type classes, but there is an important difference to what Luke Palmer did in the blog post cited above. While both approaches allow to encode type classes using data types, they are technically different, and applicable for different programs. In the dictionary approach, the dictionary contains fields of the same types as the members of the class. For example, val has the type Int -> sem Int in both the type class and the data type. This is not the case in the pattern described by Luke. There, the w type is dropped from the types of the methods when converting to a data type. For example, the type of growHorizontal is w -> Bool in the type class, but simply Bool in the data type. The reason for this difference is that Luke uses the fact that w is going to be always existentially bound, so it will not be externally usable anyway. The information contained in the w values can just as well be stored in each of the fields of the data type. The dictionary approach encodes abstract data types: The data type is the interface, each value of the data type is an implementation, and a function which takes the dictionary and is parametric in the type parameters of the dictionary is a program which uses the data type abstractly. For example, a program using the Eval abstract data type from above could look like this: -- using the type class add_two :: Eval sem => sem -> sem add_two x = add x (val 2) -- using the dictionary add_two :: EvalDict sem -> sem -> sem add_two dict x = add dict x (val dict 2) On the other hand, Luke describes an encoding of objects: The data type describes the interface of an object, and each value of that data type is an object, with possibly different implementations of each function in the interface. A program using these objects can invent arbitrary new objects, as long as all fields in the interface are defined. Since abstract data types and objects are fundamentally different, so are these two programming patterns. Tillmann

Martijn van Steenbergen wrote:

Tom Schrijvers wrote:

...

data EvalDict sem = EvalDict { val :: Int -> sem Int, add :: sem Int -> sem Int -> sem Int }

An alternative option is to capture the structure in a GADT:

...

data Eval a where Val :: Int -> Eval Int Add :: Eval Int -> Eval Int -> Eval Int

And then write what were instances before as functions Eval a -> whatever.

But these interpreter functions Eval a -> whatever would have to use pattern matching at runtime to discover the structure of the term, so this approach is no longer tagless. Tillmann

Stephen Tetley wrote:

The finally tagless style is an implementation of the TypeCase pattern (Bruno C. d. S. Oliveira and Jeremy Gibbons):

One part of our work does that, yes.

The authors of the "Finally Tagless" note in the long version of their paper that the GADT TypeCase had some problems with non-exhaustive pattern matching (last paragraph, page 14) - if I'm understanding it correctly, in order to be total, the interpretation function stills needs to introduce pattern matching clauses in some circumstances for values that the GADT actually prevents occurring.

You understand correctly. By using plain HM, augmented with either type classes or functors (to pass a higher-order dictionary around), all the redundant cases can be eliminated in a way that is transparent to the type system. To me, the parametricity in the 'interpreter' buys you more than what GADTs do. This was most definitely unexpected. Jacques

Dear Jacques, you are right, I should have done so and will do my best not to repeat this error. Please accept my sincere apologies to Ken and yourself for my negligence, no offense was meant. Best regards Günther Am 09.03.10 03:37, schrieb Jacques Carette:

Günther Schmidt wrote:

...

In Olegs haskell implementation he is using classes mainly to model the syntax and instances to use for evaluators / compilers to allow multiple interpretations.

When there are 3 authors on a paper (and in the implementation file), it is customary to acknowledge all 3, unless you have personal knowledge that one particular person did the work. In this case, the work was very much joint between Oleg, Ken and I.

Jacques