Hi all,
and Oleg et al in particular. 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/ Günther _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> 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/ Günther, 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 } Cheers, Tom _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Günther Schmidt
Hi Günther
The finally tagless style is an implementation of the TypeCase pattern (Bruno C. d. S. Oliveira and Jeremy Gibbons): http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/typecase.pdf TypeCase can be implemented via GADTs or type classes - typed printf in section 4.2 of the paper is shown in both versions. 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. Plain old data types can easily be interpreted by multiple evaluators - the benefit of TypeCase is probably when you want some degree of extensibility, see this message for instance: http://www.haskell.org/pipermail/haskell-cafe/2008-July/045028.html Best wishes Stephen _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Günther Schmidt
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 > _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Günther Schmidt
Stephen Tetley wrote: > The finally tagless style is an implementation of the TypeCase pattern > (Bruno C. d. S. Oliveira and Jeremy Gibbons): > > http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/typecase.pdf The finally tagless style is slightly more general. The TypeCase paper emphasizes that TypeCase is a pattern to define a _closed_ type-indexed function -- the indexed family is fixed but the collection of functions is extensible. This is in contrast to type classes, where the collection of functions is fixed (by the class declaration) but the indexed family is extensible (more type class instances can be defined at any time). The tagless final approach permits the definition of an extensible family of open type-indexed functions. For example, we can define a `data type' of expressions and extend it at any time with more expression forms *and* more processing functions (e.g., a new way to print or compile an expression). With the tagless final approach, we have the extensibility in both dimensions. I'll be talking about this extensibility at some length in two weeks, at the Spring School on Generic and Indexed Programming. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Günther Schmidt
Hi Oleg, On 9 Mar 2010, at 17:52, [hidden email] wrote:
It is true that "Typecase" is aimed at closed type-indexed functions, although in Section 4.2 I note, in passing, that you can achieve extensibility too for the *explicit* representations variation of the typecase pattern (which is the same that is used by tagless final): "The smart datatype solution in this section is fully closed to extension. That is, in order to add another case in the formatting list, such as a constructor Chr that handles characters, we would need to modify the GADT itself. On the other hand, the solution in the previous section using the explicit version of the design pattern allows some form of extensibility. Adding a new case for printf that handles characters corresponds to adding a new function, which could even be in a different module." Fortunately, there is a whole paper devoted to the issue of extensibility for an application of the typecase pattern using *explict* representations: Extensible and Modular Generics for the Masses Bruno C. d. S. Oliveira, Ralf Hinze and Andres Loeh In Henrik Nilsson, editor, Trends in Functional Programming (TFP). And the relation to the expression problem is pointed out there. Perhaps you'd like to have a look at the paper if you haven't seen it already. Bruno _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
On Tue, Mar 9, 2010 at 2:45 PM, Tillmann Rendel
<[hidden email]> 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
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. Of course, this makes it harder to combine multiple models. Martijn. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Günther Schmidt
Hi Oleg,
(cc'ed the haskell-cafe as it may be of interest to other readers) On Tue, 9 Mar 2010 [hidden email] wrote: > > Hi, Bruno! > > Of course I know the EMGM paper and approach -- we discuss it > at great length in the paper we are both editing, don't we? What I had > in mind about tagless final is different from EMGM, without the mediation > by an isomorphism. The isomorphism has no role in extensibility there: it is completely orthogonal to this issue. The isomorphism is used for the generic programming part. If we apply the tecnique directly to the expression problem this is what we get: http://www.haskell.org/pipermail/haskell-cafe/2008-July/045028.html > Whether it is more direct or not is in the eye of > the beholder. > > I guess you probably won't be at the Spring School. No I am not going to be there, unfortunatelly :(. > So, I'm > sending you the code that might hopefully clarify what I meant. The > original code was written in Haskell; I am sending you the OCaml > translation. Somehow I thought you might like it better (and also tell > if it translatable to Scala). I must say that my OCaml is not as good as my Haskell or Scala :). However, if I understand the code correctly I don't see where the difference to the code in the link above is. Regarding whether it is translatable to Scala. The answer for your question is answered here: Modular Visitor Components: A Practical Solution to the Expression Families Problem Bruno C. d. S. Oliveira In Sophia Drossopoulou, editor, LNCS 5653, Proceedings of the 23rd European Conference on Object Oriented Programming (ECOOP). June 2009. Link: http://ropas.snu.ac.kr/%7Ebruno/papers/ModularVisitor.pdf > > I was a little bit surprised that you ended up in Korea. That > was quite a big jump and quite a lot of hassle moving, I imagine. On > the other hand, it makes a lot of sense: governments on that side of > the world seem to have real money, and they are intent in investing > them in science, including basic science. How is your Korean? It is worse than my OCaml :). Bruno > Cheers, > Oleg > > (* Tagless Final using dictionary passing *) > > (* Compare with Haskell's ExpSYM *) > class type ['repr] expSYM = object > method lit : int -> 'repr > method neg : 'repr -> 'repr > method add : 'repr -> 'repr -> 'repr > end;; > > (* Constructor functions *) > let lit n = fun ro -> ro#lit n;; > let neg e = fun ro -> ro#neg (e ro);; > let add e1 e2 = fun ro -> ro#add (e1 ro) (e2 ro);; > > (* Unit is for the sake of value restriction *) > (* The term is exactly the same as that in Intro2.hs *) > let tf1 () = add (lit 8) (neg (add (lit 1) (lit 2)));; > > (* We can write interepreters of expSYM *) > (* and evaluate exp in several ways. The code for the interpreters > is quite like the one we have seen already > *) > class eval = object > method lit n = (n:int) > method neg e = - e > method add e1 e2 = e1 + e2 > end;; > > let eval = new eval;; > > let 5 = tf1 () eval;; > > class view = object > method lit n = string_of_int n > method neg e = "(-" ^ e ^ ")" > method add e1 e2 = "(" ^ e1 ^ " + " ^ e2 ^ ")" > end;; > > let view = new view;; > > let "(8 + (-(1 + 2)))" = tf1 () view;; > > (* We can extend our expression adding a new expression form *) > class type ['repr] mulSYM = object > method mul : 'repr -> 'repr -> 'repr > end;; > > let mul e1 e2 = fun ro -> ro#mul (e1 ro) (e2 ro);; > > > (* Extended sample expressions *) > (* Again, the code is the same as before, modulo the occasional () *) > (* Value restriction is indeed annoying ... *) > let tfm1 () = add (lit 7) (neg (mul (lit 1) (lit 2)));; > > let tfm2 () = mul (lit 7) (tf1 ());; > > class evalM = object > inherit eval > method mul e1 e2 = e1 * e2 > end;; > > let evalM = new evalM;; > > class viewM = object > inherit view > method mul e1 e2 = "(" ^ e1 ^ " * " ^ e2 ^ ")" > end;; > > let viewM = new viewM;; > > (* can use the extended evaluator to evaluate old expressions *) > let 5 = tf1 () evalM;; > > (* Of course we can't use the old evaluator to evaluate extended > expressions > let 5 = tfm1 () eval;; > Error: This expression has type eval but an expression was expected of type > < add : 'a -> 'b -> 'c; lit : int -> 'a; mul : 'a -> 'a -> 'd; > neg : 'd -> 'b; .. > > The first object type has no method mul > *) > > let 5 = tfm1 () evalM;; > > let 35 = tfm2 () evalM;; > > let "(7 + (-(1 * 2)))" = tfm1 () viewM;; > > let "(7 * (8 + (-(1 + 2))))" = tfm2 () viewM;; > > (* The expressions are first-class: we can put them into the same list *) > > let tl1 () = [lit 1; tf1 ()];; > > (* and add the extended objects afterwards *) > > let tl2 () = tfm1 () :: tfm2 () :: tl1 ();; > > let [5; 35; 1; 5] = List.map (fun x -> x evalM) (tl2 ());; > > let ["(7 + (-(1 * 2)))"; "(7 * (8 + (-(1 + 2))))"; "1"; "(8 + (-(1 + 2)))"] > = List.map (fun x -> x viewM) (tl2 ());; > > Printf.printf "\nAll done\n";; > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Martijn van Steenbergen-2
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
Tom Schrijvers wrote:
> 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). I agree that dictionaries can be seen as objects. This is an interesting point of view. At first glance, dictionaries seem to be not that interesting objects, becaus the observation functions never return new objects, but only plain values instead. However, we can use the object-like nature of dictionaries to produce new dictionaries in creative ways. For example, we could produce a dictionary by performing the operations in two dictionaries in parallel: evalProduct eval1 eval2 = EvalDict valProduct addProduct where valProduct x = (val eval1 x, val eval2 x) addProduct (a, b) (c, d) = (add eval1 a c, add eval2 b d) Of course, the same can be done with typeclass using a newtype. In [1], we argue that this kind of code enables us to implement semantics of EDSLs as components, which can be composed etc. Since we used Scala, we had modelled dictionaries as objects. But with this point of view about dictionaries as objects, its the exact same story in Haskell, of course. [1] Hofer et al. Polymorphic embedding of DSLs. GPCE 2008. > 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? Well, we could encode numbers as objects using church numerals, similar to how Cook uses characteristic functions for sets: data Number = Number (iter :: forall a . (a -> a) -> a -> a) The val constructor: valNumber :: Int -> Number valNumber x = Number (\f -> iterate f !! x) Addition: add :: Number -> Number -> Number add (Number iter1) (Number iter2) = Number (\f -> iter1 f . iter2 f) > 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. We could use the Number objects to implement sem Int as follows. (Luckily, sem was always applied to Int in this reduced example, so we do not have to introduce non-parametric type-level functions): newtype Const a b = Const a evalAsObject :: EvalDict (Const NumberObject) evalAsObject = EvalDict valAsObject addAsObject where valAsObject x = Const (valNumber x) addAsObject (Const a) (Const b) = Const (add a b) We can often (always?) provide a sufficiently rich interface to our objects to support the same operations as with an abstract data type. I am not sure what laziness does to the picture in Cook's essay. Could a thunk be seen as an object with force as the only observing function? That would mean that in Haskell, even algebraic data types behave like objects because we are not handling them directly, but rather their thunks. From this point of view, Haskell is purely object-oriented. Tillmann _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |