[Haskell-cafe] more thoughts on "Finally tagless"

[Tom Schrijvers]

On Tue, Mar 9, 2010 at 2:45 PM, Tillmann Rendel
<rendel at mathematik.uni-marburg.de> wrote:
> 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-typeclass/
>>
>> 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,

Thanks for your insight of objects vs. abstract data types.
William Cook's Onward! essay is relevant here. He characterizes the difference
between objects and abstract data types nicely: the latter allow
binary methods that
pattern match (to exploit the combined knowledge of the internals of
two different values)
whereas objects only know their own implementation.

Dictionaries by themselves are objects in Cook's sense: they are just
a record of functions that cannot be
inspected. We can have an infinite number of them (while we can only
have one type class instance
per sem type).  However, the (sem a) values are not objects, and
varying the dictionaries while keeping the sem type the same does not
seem very useful for implementing different semantics.

For a type class function like add :: sem Int -> sem Int -> sem Int, binary
pattern matching seems essential for meaningful implementations, and
hence objects don't make much sense. Would you agree?

Cheers,

Tom