[Haskell] Haskell-related PhD Scholarships in Hong Kong
The University of Hong Kong has a special early-recruitment program for graduate studies starting next year (September 2015). Anyone interested in coming to Hong Kong and doing a PhD in the area of Programming Languages and Functional Programming is very welcome to apply! A strong Haskell background is definitely a plus, but experience with other Functional Languages and/or Theorem Provers (Scala, ML, OCaml, Agda, Idris, Coq, Isabelle …) is equally valued. There are a number of projects available on the areas of compiler implementation, programming language design, dependent types, property-based testing (think Quickcheck) and various other FP-related topics. For more details please contact me (br...@cs.hku.hk). General information about HKU’s early recruitment program can be found here: http://www.cs.hku.hk/programme/mphil-phd/admission_2015.jsp Some information about my research can be found here: http://i.cs.hku.hk/~bruno/ Best Regards, Bruno Oliveira ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] WGP Call for Participation
== CALL FOR PARTICIPATION WGP 2010 6th ACM SIGPLAN Workshop on Generic Programming Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Collocated with the International Conference on Functional Programming (ICFP 2010) == Goals of the workshop - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. Program --- * 09.00-10.00: Session 1 Chair: Marcin Zalewski * Welcome + PC chair report Bruno C. d. S. Oliveira and Marcin Zalewski * Outrageous but Meaningful Coincidences (Dependent type-safe syntax and evaluation) Conor McBride * 10.00-10.30: Tea/coffee * 10.30-12.30: Session 2 Chair: Shin-Cheng Mu * Scrap Your Zippers: A Generic Zipper for Heterogeneous Types Michael D. Adams * Generic Storage in Haskell Sebastiaan Visser and Andres Loeh * Generic Selections of Subexpressions Martijn van Steenbergen, José Pedro Magalhães and Johan Jeuring * 12.30-14.00: Lunch * 14.00-16.00: Session 3 Chair: Bruno C. d. S. Oliveira * Generic Multiset Programming for Language-Integrated Querying Fritz Henglein and Ken Friis Larsen * Algorithms for Traversal-Based Generic Programming Bryan Chadwick and Karl Lieberherr * Ad-hoc Polymorphism and Dynamic Typing in a Statically Typed Functional Language Thomas van Noort, Peter Achten and Rinus Plasmeijer * 16.00-16.30: Tea/coffee * 16.30-18.00: Session 4 Chair: Conor McBride * Reason Isomorphically! Ralf Hinze and Daniel James * Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning Shin-Cheng Mu, Yu-Han Lyu and Akimasa Morihata Workshop homepage: http://osl.iu.edu/wgp2010/ Registration link: https://regmaster3.com/2010conf/ICFP10/register.php Local arrangements: http://www.icfpconference.org/icfp2010/local.html ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell-cafe] WGP Call for Participation
== CALL FOR PARTICIPATION WGP 2010 6th ACM SIGPLAN Workshop on Generic Programming Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Collocated with the International Conference on Functional Programming (ICFP 2010) == Goals of the workshop - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. Program --- * 09.00-10.00: Session 1 Chair: Marcin Zalewski * Welcome + PC chair report Bruno C. d. S. Oliveira and Marcin Zalewski * Outrageous but Meaningful Coincidences (Dependent type-safe syntax and evaluation) Conor McBride * 10.00-10.30: Tea/coffee * 10.30-12.30: Session 2 Chair: Shin-Cheng Mu * Scrap Your Zippers: A Generic Zipper for Heterogeneous Types Michael D. Adams * Generic Storage in Haskell Sebastiaan Visser and Andres Loeh * Generic Selections of Subexpressions Martijn van Steenbergen, José Pedro Magalhães and Johan Jeuring * 12.30-14.00: Lunch * 14.00-16.00: Session 3 Chair: Bruno C. d. S. Oliveira * Generic Multiset Programming for Language-Integrated Querying Fritz Henglein and Ken Friis Larsen * Algorithms for Traversal-Based Generic Programming Bryan Chadwick and Karl Lieberherr * Ad-hoc Polymorphism and Dynamic Typing in a Statically Typed Functional Language Thomas van Noort, Peter Achten and Rinus Plasmeijer * 16.00-16.30: Tea/coffee * 16.30-18.00: Session 4 Chair: Conor McBride * Reason Isomorphically! Ralf Hinze and Daniel James * Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning Shin-Cheng Mu, Yu-Han Lyu and Akimasa Morihata Workshop homepage: http://osl.iu.edu/wgp2010/ Registration link: https://regmaster3.com/2010conf/ICFP10/register.php Local arrangements: http://www.icfpconference.org/icfp2010/local.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Difficulties with tagless - create primitives or compose them
Hi Gunther, The finally tagless approach can be viewed as one instance of the typecase pattern, which myself and others have investigated the past: http://ropas.snu.ac.kr/~bruno/papers/Typecase.pdf Your problem is related to a problem that is found when designing generic programming libraries. Namely the existence of what we call ad-hoc cases. These are cases that most of the times have a default, but sometimes we would like to override that default. This is essentially the source of your confusion. What is the best thing todo: shall I provide a default by using composition by creating a definition for mul outside the class; or shall I create a primitive. There is a trade-off between the two. Fortunatelly it is possible to avoid such trade-off. This is one of the things that is described in the EMGM paper, which uses the same variation of the typecase pattern that is used in the finally tagless approach: http://ropas.snu.ac.kr/~bruno/papers/ExtensibleGM.pdf Now, for your particular example, this amounts to the following: type Arr exp a b = exp a - exp b class EDSL exp where lam :: (exp a - exp b) - exp (Arr exp a b) app :: exp (Arr exp a b) - exp a - exp b int :: Int - exp Int-- Integer literal add :: exp Int - exp Int - exp Int sub :: exp Int - exp Int - exp Int class EDSL exp = EDSLMul exp where mul :: exp Int - exp Int - exp Int mul e1 e2 = -- a default definition in terms of the primitives in EDSL By creating a subclass and defining mul as a default method you get the advantages of the primitive approach ( you can define your own interpretations) with the advantages of the compositional approach (you can modularly add as many as you want without having to touch EDSL). There is a little extra work that you need to do though, because now you'll need to say: instance EDSLMul MyInterpretation to get an instance for mul at a particular interpretation. You can actually avoid this, if you use overlapping instances: instance EDSLMul a then, only when you you really want to override an interpretation, you will need an instance. More generally this approach tells you how you can modularize your EDSLs. Or, put another way, if offers a solution for the expression problem: http://www.daimi.au.dk/~madst/tool/papers/expression.txt Hope this helps! Cheers, Bruno Oliveira On Jun 13, 2010, at 10:58 AM, Günther Schmidt wrote: Hi list, there is one thing about the Finally tagless EDSL approach that really confuses me: (Well more than one actually but this one more so) When to decide to introduce a term as a primitive in the syntax class and when to define it from primitives already defined. For example this one here: type Arr exp a b = exp a - exp b class EDSL exp where lam :: (exp a - exp b) - exp (Arr exp a b) app :: exp (Arr exp a b) - exp a - exp b int :: Int - exp Int-- Integer literal add :: exp Int - exp Int - exp Int sub :: exp Int - exp Int - exp Int mul :: exp Int - exp Int - exp Int Let's take mul here, defined as a primitive, in other words defined in the EDSL class. Technically, with lam, app and add already defined, I could have defined mul outside the EDSL class, just built from the 3 primitive operators. Of course doing so then does not give me the possibility to choose alternative evaluation strategies for mul itself, only for lam, app and add. So what is a good measure for deciding when to define a term primitive or not? Günther ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell] Workshop on Generic Programming (WGP) 2010 Final Call for papers!
Dear all, This a final reminder that the deadline for WGP submissions is in one week! See the call for papers below: == CALL FOR PAPERS WGP 2010 6th ACM SIGPLAN Workshop on Generic Programming Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Collocated with the International Conference on Functional Programming (ICFP 2010) == Goals of the workshop - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. We welcome contributions on all aspects, theoretical as well as practical, of * polytypic programming, * programming with dependent types, * programming with type classes, * programming with (C++) concepts, * generic programming, * programming with modules, * meta-programming, * adaptive object-oriented programming, * component-based programming, * strategic programming, * aspect-oriented programming, * family polymorphism, * object-oriented generic programming, * and so on. Organizers -- Co-Chair Bruno C. d. S. Oliveira, Seoul National University Co-Chair Marcin Zalewski, Indiana University Programme Committee --- Alley Stoughton, Kansas State University Andrei Alexandrescu, Facebook Bruno C. d. S. Oliveira (Co-Chair), Seoul National University Doug Gregor, Apple Gilad Bracha, I am a Computational Theologist Emeritus Magne Haveraaen, Universitetet i Bergen Marcin Zalewski (Co-Chair), Indiana University Neil Mitchell, Standard Chartered Ralf Lämmel, University of Koblenz-Landau Shin-Cheng Mu, Academia Sinica Thorsten Altenkirch, University of Nottingham Ulf Norell, Chalmers University Important Information - We plan to have formal proceedings, published by the ACM. Submission details Deadline for submission: Sunday2010-06-13 Notification of acceptance: Monday2010-07-12 Final submission due: Tuesday 2010-07-27 Workshop:Sunday2010-09-26 Authors should submit papers, in postscript or PDF format, formatted for A4 paper, to the WGP09 EasyChair instance by 13th of June 2010. The length should be restricted to 12 pages in standard (two-column, 9pt) ACM format. Accepted papers are published by the ACM and will additionally appear in the ACM digital library. History of the Workshop on Generic Programming -- This year: * Baltimore, Maryland, US 2010 (affiliated with ICFP10) Earlier Workshops on Generic Programming have been held in * Edinburgh, UK 2009 (affiliated with ICFP09) * Victoria, BC, Canada 2008 (affiliated with ICFP), * Portland 2006 (affiliated with ICFP), * Ponte de Lima 2000 (affiliated with MPC), * Marstrand 1998 (affiliated with MPC). Furthermore, there were a few informal workshops * Utrecht 2005 (informal workshop), * Dagstuhl 2002 (IFIP WG2.1 Working Conference), * Nottingham 2001 (informal workshop), There were also (closely related) DGP workshops in Oxford (June 3-4 2004), and a Spring School on DGP in Nottingham (April 24-27 2006, which had a half-day workshop attached). Additional information: The WGP steering committee consists of J Gibbons, R Hinze, P Jansson, J Jarvi, J Jeuring, B Oliveira, S Schupp and M Zalewski___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] WGP 2010 Second Call for Papers (Apologies for multiple copies)
== CALL FOR PAPERS WGP 2010 6th ACM SIGPLAN Workshop on Generic Programming Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Collocated with the International Conference on Functional Programming (ICFP 2010) == Goals of the workshop - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. We welcome contributions on all aspects, theoretical as well as practical, of * polytypic programming, * programming with dependent types, * programming with type classes, * programming with (C++) concepts, * generic programming, * programming with modules, * meta-programming, * adaptive object-oriented programming, * component-based programming, * strategic programming, * aspect-oriented programming, * family polymorphism, * object-oriented generic programming, * and so on. Organizers -- Co-Chair Bruno C. d. S. Oliveira, Seoul National University Co-Chair Marcin Zalewski, Indiana University Programme Committee --- Alley Stoughton, Kansas State University Andrei Alexandrescu, Facebook Bruno C. d. S. Oliveira (Co-Chair), Seoul National University Doug Gregor, Apple Gilad Bracha, I am a Computational Theologist Emeritus Magne Haveraaen, Universitetet i Bergen Marcin Zalewski (Co-Chair), Indiana University Neil Mitchell, Standard Chartered Ralf Lämmel, University of Koblenz-Landau Shin-Cheng Mu, Academia Sinica Thorsten Altenkirch, University of Nottingham Ulf Norell, Chalmers University Important Information - We plan to have formal proceedings, published by the ACM. Submission details Deadline for submission: Sunday2010-06-13 Notification of acceptance: Monday2010-07-12 Final submission due: Tuesday 2010-07-27 Workshop:Sunday2010-09-26 Authors should submit papers, in postscript or PDF format, formatted for A4 paper, to the WGP09 EasyChair instance by 13th of June 2010. The length should be restricted to 12 pages in standard (two-column, 9pt) ACM format. Accepted papers are published by the ACM and will additionally appear in the ACM digital library. History of the Workshop on Generic Programming -- This year: * Baltimore, Maryland, US 2010 (affiliated with ICFP10) Earlier Workshops on Generic Programming have been held in * Edinburgh, UK 2009 (affiliated with ICFP09) * Victoria, BC, Canada 2008 (affiliated with ICFP), * Portland 2006 (affiliated with ICFP), * Ponte de Lima 2000 (affiliated with MPC), * Marstrand 1998 (affiliated with MPC). Furthermore, there were a few informal workshops * Utrecht 2005 (informal workshop), * Dagstuhl 2002 (IFIP WG2.1 Working Conference), * Nottingham 2001 (informal workshop), There were also (closely related) DGP workshops in Oxford (June 3-4 2004), and a Spring School on DGP in Nottingham (April 24-27 2006, which had a half-day workshop attached). Additional information: The WGP steering committee consists of J Gibbons, R Hinze, P Jansson, J Jarvi, J Jeuring, B Oliveira, S Schupp and M Zalewski ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell-cafe] WGP 2010 Second Call for Papers (Apologies for multiple copies)
== CALL FOR PAPERS WGP 2010 6th ACM SIGPLAN Workshop on Generic Programming Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Collocated with the International Conference on Functional Programming (ICFP 2010) == Goals of the workshop - Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. We welcome contributions on all aspects, theoretical as well as practical, of * polytypic programming, * programming with dependent types, * programming with type classes, * programming with (C++) concepts, * generic programming, * programming with modules, * meta-programming, * adaptive object-oriented programming, * component-based programming, * strategic programming, * aspect-oriented programming, * family polymorphism, * object-oriented generic programming, * and so on. Organizers -- Co-Chair Bruno C. d. S. Oliveira, Seoul National University Co-Chair Marcin Zalewski, Indiana University Programme Committee --- Alley Stoughton, Kansas State University Andrei Alexandrescu, Facebook Bruno C. d. S. Oliveira (Co-Chair), Seoul National University Doug Gregor, Apple Gilad Bracha, I am a Computational Theologist Emeritus Magne Haveraaen, Universitetet i Bergen Marcin Zalewski (Co-Chair), Indiana University Neil Mitchell, Standard Chartered Ralf Lämmel, University of Koblenz-Landau Shin-Cheng Mu, Academia Sinica Thorsten Altenkirch, University of Nottingham Ulf Norell, Chalmers University Important Information - We plan to have formal proceedings, published by the ACM. Submission details Deadline for submission: Sunday2010-06-13 Notification of acceptance: Monday2010-07-12 Final submission due: Tuesday 2010-07-27 Workshop:Sunday2010-09-26 Authors should submit papers, in postscript or PDF format, formatted for A4 paper, to the WGP09 EasyChair instance by 13th of June 2010. The length should be restricted to 12 pages in standard (two-column, 9pt) ACM format. Accepted papers are published by the ACM and will additionally appear in the ACM digital library. History of the Workshop on Generic Programming -- This year: * Baltimore, Maryland, US 2010 (affiliated with ICFP10) Earlier Workshops on Generic Programming have been held in * Edinburgh, UK 2009 (affiliated with ICFP09) * Victoria, BC, Canada 2008 (affiliated with ICFP), * Portland 2006 (affiliated with ICFP), * Ponte de Lima 2000 (affiliated with MPC), * Marstrand 1998 (affiliated with MPC). Furthermore, there were a few informal workshops * Utrecht 2005 (informal workshop), * Dagstuhl 2002 (IFIP WG2.1 Working Conference), * Nottingham 2001 (informal workshop), There were also (closely related) DGP workshops in Oxford (June 3-4 2004), and a Spring School on DGP in Nottingham (April 24-27 2006, which had a half-day workshop attached). Additional information: The WGP steering committee consists of J Gibbons, R Hinze, P Jansson, J Jarvi, J Jeuring, B Oliveira, S Schupp and M Zalewski ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: more thoughts on Finally tagless
Hi Oleg, (cc'ed the haskell-cafe as it may be of interest to other readers) On Tue, 9 Mar 2010 o...@okmij.org 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: more thoughts on Finally tagless
Hi Oleg, On 9 Mar 2010, at 17:52, o...@okmij.org wrote: 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. 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). Link: http://ropas.snu.ac.kr/%7Ebruno/papers/ExtensibleGM.pdf 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell] WGP 2010 Call for Papers
6th ACM SIGPLAN Workshop on Generic Programming, 2010 Baltimore, Maryland, US Sunday, September 26th, 2010 http://osl.iu.edu/wgp2010 Goals of the workshop Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area. We welcome contributions on all aspects, theoretical as well as practical, of * polytypic programming, * programming with dependent types, * programming with type classes, * programming with (C++) concepts, * generic programming, * programming with modules, * meta-programming, * adaptive object-oriented programming, * component-based programming, * strategic programming, * aspect-oriented programming, * family polymorphism, * object-oriented generic programming, * and so on. Organisers: Co-Chair Bruno C. d. S. Oliveira, Seoul National University Co-Chair Marcin Zalewski, Indiana University Programme Committee: Alley Stoughton, Kansas State University Andrei Alexandrescu, Facebook Bruno C. d. S. Oliveira (Co-Chair), Seoul National University Doug Gregor, Apple Gilad Bracha, I am a Computational Theologist Emeritus Magne Haveraaen, Universitetet i Bergen Marcin Zalewski (Co-Chair), Indiana University Neil Mitchell, Standard Chartered Ralf Lämmel, University of Koblenz-Landau Shin-Cheng Mu, Academia Sinica Thorsten Altenkirch, University of Nottingham Ulf Norell, Chalmers University We plan to have formal proceedings, published by the ACM. Submission details Deadline for submission: Sunday2010-06-13 Notification of acceptance: Monday2010-07-12 Final submission due: Tuesday 2010-07-27 Workshop:Sunday2010-09-26 Authors should submit papers, in postscript or PDF format, formatted for A4 paper, to the WGP09 EasyChair instance by 13th of June 2010. The length should be restricted to 12 pages in standard (two-column, 9pt) ACM format. Accepted papers are published by the ACM and will additionally appear in the ACM digital library. History of the Workshop on Generic Programming This year: * Baltimore, Maryland, US 2010 (affiliated with ICFP10) Earlier Workshops on Generic Programming have been held in * Edinburgh, UK 2009 (affiliated with ICFP09) * Victoria, BC, Canada 2008 (affiliated with ICFP), * Portland 2006 (affiliated with ICFP), * Ponte de Lima 2000 (affiliated with MPC), * Marstrand 1998 (affiliated with MPC). Furthermore, there were a few informal workshops * Utrecht 2005 (informal workshop), * Dagstuhl 2002 (IFIP WG2.1 Working Conference), * Nottingham 2001 (informal workshop), There were also (closely related) DGP workshops in Oxford (June 3-4 2004), and a Spring School on DGP in Nottingham (April 24-27 2006, which had a half-day workshop attached). Additional information: The WGP steering committee consists of J Gibbons, R Hinze, P Jansson, J Jarvi, J Jeuring, B Oliveira, S Schupp and M Zalewski ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] GPCE'10 First Call for Papers
Hi all, Haskell is a great language for developing generative programming tools and developing highly expressible and reusable components (think of all the cool uses of type classes, type families or GADTs). The GPCE conference is interested to hear about cutting-edge techniques of generative and component-based software. You can show what Haskell can do in this area by submitting a research paper or a tool demonstration to GPCE! CALL FOR PAPERS Ninth International Conference on Generative Programming and Component Engineering (GPCE 2010) October 10-13, 2010 Eindhoven, The Netherlands (co-located with SLE 2010) http://www.gpce.org IMPORTANT DATES * Submission of abstracts: May 17, 2010 * Submission of papers: May 24, 2010 * Author notification: Jul 5, 2010 SCOPE Generative and component approaches are revolutionizing software development similar to how automation and components revolutionized manufacturing. Generative Programming (concerning programs that synthesize other programs), Component Engineering (concerning modularity in application design), and Domain-Specific Languages (DSLs) (concerning compact domain-specific notations for expressing programs) are key technologies for automating program development. The International Conference on Generative Programming and Component Engineering is a venue for researchers and practitioners interested in techniques that, through deploying components and program generation, increase programmer productivity, improve software quality, and shorten the time-to-market of software products. In addition to exploring cutting-edge techniques of generative and component-based software, our goal is to foster further cross-fertilization between the software engineering and the programming languages research communities. SUBMISSIONS Research papers: 10 pages in SIGPLAN proceedings style (sigplanconf.cls) reporting original research results that contribute to scientific knowledge in the areas listed below (the PC chair can advise on appropriateness). Tool demonstrations: Tool demonstrations should present tools that implement novel generative and component-based software engineering techniques, and are available for use. Any of the GPCE'10 topics of interest are appropriate areas for research demonstrations. Purely commercial tool demonstrations will not be accepted. Submissions should contain a tool description of 4 pages in SIGPLAN proceedings style (sigplanconf.cls) and a demonstration outline of up to 2 pages text plus 2 pages screen shots. The four page description will, if the demonstration is accepted, be published in the proceedings. The 2+2 page demonstration outline will only be used by the PC for evaluating the submission. TOPICS GPCE seeks contributions in software engineering and in programming languages related (but not limited) to: * Generative programming o Reuse, meta-programming, partial evaluation, multi-stage and multi-level languages, step-wise refinement, generic programming o Semantics, type systems, symbolic computation, linking and explicit substitution, in-lining and macros, templates, program transformation o Runtime code generation, compilation, active libraries, synthesis from specifications, development methods, generation of non-code artifacts, formal methods, reflection * Generative techniques for o Product-line architectures o Distributed, real-time and embedded systems o Model-driven development and architecture o Resource bounded/safety critical systems. * Component-based software engineering o Reuse, distributed platforms and middleware, distributed systems, evolution, patterns, development methods, deployment and configuration techniques, formal methods * Integration of generative and component-based approaches * Domain engineering and domain analysis o Domain-specific languages including visual and UML-based DSLs * Separation of concerns o Aspect-oriented and feature-oriented programming, o Intentional programming and multi-dimensional separation of concerns * Industrial applications of the above Submissions must adhere to SIGPLAN's republication policy. Please contact the program chair if you have any questions about how this policy applies to your paper (cha...@gpce.org). ORGANIZATION General Chair:Eelco Visser (Delft University of Technology, The Netherlands) Program Chair:Jaakko J‰rvi (Texas AM University, USA) Publicity Chair: Giorgios Economopoulos (University of Southampton, UK) Program Committee * Sven Apel (University of Passau, Germany) * Don Batory (University of Texas, USA) * Martin Bravenboer (LogicBlox,
Re: [Haskell] Should the following program be accepted by ghc?
Hello, Maybe a more slightly more honest type for decomp would be:) : decomp :: Injective f = f a :=: f b - a :=: b Cheers, Bruno On Wed, 16 Jan 2008, Derek Elkins wrote: On Wed, 2008-01-16 at 09:18 +, J.N. Oliveira wrote: On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote: Hello, I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error: data a :=: b where Eq :: a :=: a decomp :: f a :=: f b - a :=: b decomp Eq = Eq However, I find this odd because if you interpret f as a function and :=: as equality, then this is saying that if f a = f b then a = b This is saying that f is injective. So perhaps the standard interpretation leads implicitly to this class of functions. Just like data constructors, type constructors are injective. f a doesn't simplify and so essentially you have structural equality of the type terms thus f a = f b is -equivalent- to a = b. Obviously type functions change this, just like normal value functions do at the value level. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell-cafe] GADTs: the plot thickens?
Hello Conor, The following seems to work: On 31 Jan 2007, at 11:46, Conor McBride wrote: Hi folks A puzzle for you (and for me too). I just tried to translate an old Epigram favourite (which predates Epigram by some time) into GADT- speak. It went wrong. I had a feeling it might. I wonder how to fix it: I imagine it's possible to fix it, but that some cunning may be necessary. Here it is: Type-level Nat data Z = Z data S x = S x Lets also have naturals reflected at the value level: data Nat :: * - * where Zero :: Nat Z Succ :: Nat n - Nat (S n) Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n data Fin :: * - * where Fz :: Fin (S n) Fs :: Fin n - Fin (S n) The thinning function: thin i is the order-preserving embedding from Fin n to Fin (S n) which never returns i. Now we modify thin to take an extra Nat n (not needed, but just to show the duality with thickening): thin :: Nat n - Fin (S n) - Fin n - Fin (S n) thin n Fz i = Fs i thin (Succ n) (Fs i) (Fz)= Fz thin (Succ n) (Fs i) (Fs j) = Fs (thin n i j) The thing to note here is that only: thin (Succ n) (Fs i) (Fz)= Fz is well typed; if you had the case: thin Zero (Fs i) (Fz)= Fz you get: Conor.lhs:28:21: Inaccessible case alternative: Can't match types `S n' and `Z' In the pattern: Fz In the definition of `thin': thin Zero (Fs i) (Fz) = Fz Failed, modules loaded: none. Its partial inverse, thickening has the spec thicken i i = Nothing thicken i (thin i j) = Just j Now lets go for the thickening function: thicken :: Nat n - Fin (S n) - Fin (S n) - Maybe (Fin n) thicken nFz Fz = Nothing thicken nFz (Fs j) = Just j thicken Zero (Fs i) Fz = Nothing thicken (Succ _) (Fs i) Fz = Just Fz thicken (Succ n) (Fs i) (Fs j) = fmap Fs (thicken n i j) Note that this version of thicken is more precise than the version you had -- your third case splits into two different cases now. The problem is that when you had: thicken (Fs i) Fz = ... you need to account for two possibilities: the first possibility is (Fz :: Fin (S Zero)), to which you want to return Nothing and (Fz :: Fin (S (S n))) for which you can safely return Just Fz. Let me know if that helps. Cheers, Bruno ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs: the plot thickens?
Hello Pablo, What I meant was simply that the function thin does not need the extra Nat n argument to compile; Conor's original version was already compiling: thin :: Fin (S n) - Fin n - Fin (S n) thin Fz i = Fs i thin (Fs i) Fz = Fz thin (Fs i) (Fs j) = Fs (thin i j) The reason why I modified thin was to show the similarity with thicken (since thicken is the partial inverse of thin). When you have the new version of thin: thin :: Nat n - Fin (S n) - Fin n - Fin (S n) thin n Fz i = Fs i thin (Succ n) (Fs i) (Fz)= Fz thin (Succ n) (Fs i) (Fs j) = Fs (thin n i j) it becomes easier to see how to define the inverse, for example we can see that there is not a case for: thin Zero (Fs i) (Fz)= Fz-- type-error which hints for the following case in thicken: thicken Zero (Fs i) Fz = Nothing So, although having the new version of thin helps you with the definition of thicken, we do not need it to have a working thin function. That's all I meant. Cheers, Bruno On 31 Jan 2007, at 12:57, Pablo Nogueira wrote: Bruno, Now we modify thin to take an extra Nat n (not needed, but just to show the duality with thickening): I'm puzzled by the not needed bit. Isn't the introduction of Fin's indices reflected as values in the GADT , and the fact that the GADT makes that reflection, what makes it work? P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what is a difference between existential quantification and polymorhic field?
Hello Bullat, now i'm reading Haskell' proposals and found that these two things considered as different: http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification http://hackage.haskell.org/trac/haskell-prime/wiki/PolymorphicComponents can you please explain me what is the difference between data Ex = forall a. Num a = Ex a and data Po = Po (forall a. Num a = a) With existencial types you know what what the type of the thing you are packing is: t = Ex (3 :: Int) and you forget about it once it is packed. However, with polymophic components the following is a type error t = Po ( 3 :: Int) because you are required to provide a polymorphic value (forall a . Num a = a) and you have given it a value Int. However, the following is valid: t1 = Po 3 since (3 :: forall a . Num a = a). So, perhaps an easy way to think about existencials is that they are almost like: data Ex a = Ex a except that the type "a" is lost as soon as you construct such a value. Where does this make a difference? Try the following two definitions: addPo :: Po - Po - Po addPo (Po x) (Po y) = Po (x + y) addEx :: Ex - Ex - Ex addEx (Ex x) (Ex y) = Ex (x + y) The first one works, the second one doesn't. The reason that the first works is because "x" and "y" are polymorphic and thus they can be unified. This is more/less equivallent to: addPo' :: (forall a . Num a = a) - (forall a . Num a = a) - (forall a . Num a = a) addPo' x y = x + y The second does *not* work because when you created the values for the existencials you assumed some concrete types. So, "x" could be an Integer and "y" could be a Float and therefore, you should not be allowed to perform this operation. also, ghc66 adds impredicative polymorphism. how it differs from unqualified existentials? I have not tried ghc66, but I think one of the things you should be able to do and that is perhaps helpful for understanding existencial is: myList :: [forall a . Num a = a] myList = [3 :: Int, 4 :: Float, 6 :: Integer] which in previous versions of GHC would need to be written as: myList :: [Ex] myList = [Ex (3 ::Int), Ex (4 :: Float), Ex (6 :: Integer)] Hope this helps. Cheers, Bruno Oliveira ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what is a difference between existential quantification and polymorhic field?
Hello Bullat, also, ghc66 adds impredicative polymorphism. how it differs from unqualified existentials? I have not tried ghc66, but I think one of the things you should be able to do and that is perhaps helpful for understanding existencial is: myList :: [forall a . Num a = a] myList = [3 :: Int, 4 :: Float, 6 :: Integer] which in previous versions of GHC would need to be written as: myList :: [Ex] myList = [Ex (3 ::Int), Ex (4 :: Float), Ex (6 :: Integer)] I took a look at the documentation and I think I told you the wrong thing here. I think this should be equivallent to: myList :: [Po] myList = [Po 3, Po 4, Po 6] which, in this case wouldn't be too useful (would it?). Having structures with polymorphic components is more useful when you have functions. The example they give is: f :: Maybe (forall a. [a] - [a]) - Maybe ([Int], [Char]) f (Just g) = Just (g [3], g hello) f Nothing = Nothing However, the following (which would be the right way to express my example) would be handy to have as well: myList :: [exists a . Num a = a] myList = [3 :: Int, 4 :: Float, 6 :: Integer] but I don't think this is available in GHC 6.6. Can anyone confirm this? Cheers, Bruno Oliveira ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
Hello, Consider the following: data SimpExist a = SimpExist (forall x . x - a) f :: SimpExist Bool f = SimpExist (const True) g = SimpExist id What is the type of g? In a similar example, GHC tells me it is of type SimpExist c. Yet, I can't unify it with any other SimpExist c'. Have you tried to type check this example (the g)? It does not type check in my GHC. There are not many functions with the type forall x . x - a when a is also polymorphic --- it is the type of unsafeCoerce. It seems to me that this is something like exists x . SimpExist x, and is similar to: data ExistWrap = forall a . ExistWrap (forall x . x - a) Sure, you should read a forall on the left side of a constructor as exists. Look at section 7.4.1.4.1 of: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html The design decision here was to avoid introducing a new exist construct. I believe that the justification for this option is that in Logic a forall in a contravariant position has the same effect as an existential. Cheers, Bruno ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Optimization problem
Hello, I think it is possible to do it in O(n) (if you change the representation of the output stream). Note that the solution is quite similar toTwan van Laarhoven, and it should be trivial use Map instead of Rel. Here is my take on it: The type of the output stream: type Rel a b = a - [b] Here are cons and nil: cons :: Eq a = (a,b) - Rel a b - Rel a b cons (x,y) l z | x == z= y : l x | otherwise = l z nil :: Rel a b nil _ = [] and a lookUp function: lookUp :: Rel a b - a - [b] lookUp = id Finally the splitStreams algorithm: splitStreams :: Eq a = [(a,b)] - Rel a b splitStreams = foldr cons nil Here is a test with finite lists: fin = splitStreams [(3,'x'),(1,'y'),(3,'z'),(2,'w')] and here are the console tests: *General7 lookUp fin 1 y *General7 lookUp fin 2 w *General7 lookUp fin 3 xz Now with infinite lists: inf = splitStreams (map (\x - (0, x)) [1..]) and here a case where it terminates with infinite lists: *General7 take 10 (lookUp inf 0) [1,2,3,4,5,6,7,8,9,10] Cheers, Bruno Oliveira ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Optimization problem
Hello Magnus, You are right. Silly me. I was thinking of Rel as a kind of Hashtable. In this case, I think it should be possible to have O(n), since "cons" would only need constant time. Cheers, Bruno On Thu, 14 Sep 2006 13:11:05 -0400 (EDT), Magnus Jonsson wrote: Thanks Bruno. However I think this is still O(n*m). As far as I understand your code it is a longwinded way to say "[b | (a,b) - input, b == myChannelOfInterest]". This is fine if you are only interested in one channel, and for that case I agree it's O(n), but if you are interested in many different channels, it will take O(n*m). Here's why I think your code is equivalent to using a filter/list-comprehension: cons :: Eq a = (a,b) - Rel a b - Rel a b cons (x,y) l z | x == z= y : l x | otherwise = l z z is the channel that the user is interested in. x is the channel of the current message in the list. y is the message content. l is a function for searching the rest of the list. For each element of the list you create a function that compares the requested channel to a (in (a,b)). If it's the same, you return that element followed by a continued search down the list. If you don't find it, you forward the request to the next function down the list. That's exactly the same as what the filter function does. It is possible I made a mistake somewhere and if I did, let me know. / Magnus On Thu, 14 Sep 2006, Bruno Oliveira wrote: Hello, I think it is possible to do it in O(n) (if you change the representation of the output stream). Note that the solution is quite similar toTwan van Laarhoven, and it should be trivial use "Map" instead of "Rel". Here is my take on it: The type of the output stream: type Rel a b = a - [b] Here are cons and nil: nil :: Rel a b nil _ = [] and a lookUp function: lookUp :: Rel a b - a - [b] lookUp = id Finally the splitStreams algorithm: splitStreams :: Eq a = [(a,b)] - Rel a b splitStreams = foldr cons nil Here is a test with finite lists: fin = splitStreams [(3,'x'),(1,'y'),(3,'z'),(2,'w')] and here are the console tests: *General7 lookUp fin 1 "y" *General7 lookUp fin 2 "w" *General7 lookUp fin 3 "xz" Now with infinite lists: inf = splitStreams (map (\x - (0, x)) [1..]) and here a case where it terminates with infinite lists: *General7 take 10 (lookUp inf 0) [1,2,3,4,5,6,7,8,9,10] Cheers, Bruno Oliveira ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rank 2 polymorphism in pattern matching?
Hello, See this message: http://article.gmane.org/gmane.comp.lang.haskell.general/13145/ Your (initial) program should work in GHC 6.2. I actually find this feature useful, but Simon apparently changed this when moving to GHC 6.4 and nobody complained... Apparently not many people use this feature. Cheers, Bruno On Sat, 08 Apr 2006 18:31:03 +, C Rodrigues wrote: This counterintuitive typechecking result came up when I wrote a wrapper around runST. Is there some limitation of HM with respect to type checking pattern matching? data X a b = X (a - a) run :: forall a. (forall b. X a b) - a - a -- This definition doesn't pass the typechecker run (X f) = f -- But this definition works run x = (\(X f) - f) x ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell] Pattern Matching with rank-2 types
Hello, The following function is a valid function in ghc6.2.2: func :: (forall a . [a]) - [b] func [] = [] However, in ghc6.4.1 it does not work anymore: Iterators4.lhs:56:6: Couldn't match `forall a. [a]' against `[a]' When checking the pattern: [] In the definition of `func': func [] = [] Is this supposed to happen? Cheers, Bruno ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] State Monad
Hello, Can somebody point me out the exact CVS location of the State Monad implementation that ships with GHC? I am a bit lost in the CVS directory structure ... Related to this, I saw the following thread: http://www.mail-archive.com/haskell@haskell.org/msg17702.html Which seems to hint that there are 2 alternative implementations for the State Monad: one lazy version and one more strict version. Is this correct? What I am really trying to find out is if the version that ships with GHC is the strict version. At least I am inclined to think that, since a program that I expected to terminate is not terminating ... Finally, if there are indeed two versions, can somebody write (or point me out) the two different implementations. Thanks, Bruno ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Parsing bug in GHC 6.4.1 ?
Hello, The following class definition: class Foo o where (:+) :: o - o - o and even the following function definition: bar f (x,y) = x :+ y are accepted by GHC. However, when I try to create one instance of Foo: instance Foo Int where x :+ y = x + y I get the following error message: Parsing.lhs:7:5: Pattern bindings (except simple variables) not allowed in instance declarations x :+ y = x + y The same error still occurs if I change the infix operator to be (:+:). However, if I define: class Foo3 o where (+) :: o - o - o instance Foo3 Int where x + y = x + y Everything works as expected. The only explanation that I have is that this is a (parsing) bug in GHC... This is probably related to the fact that (:+) :: Int - Int - Int f :+ g = f + g is an invalid definition (it complains that :+ is not a data constructor). I have not tried this code in other Haskell compiler (like Hugs) or even previous versions of GHC. I would be interested to know how do those behave. Cheers, Bruno ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
RE: [Haskell] A question about fundeps - GADT interaction
Hello Tomasz,
Unfortunatelly I have only seen your message after Simon answered to it.
I am sorry for the late answer!
| If there is another way to do this right now (conveniently, Oleg! ;-),
I
| would be more than happy to hear about it.
|
| If this worked, it would be a cool trick and a nice example for GADT
| use. Let me know if it was proposed before.
Well, it is true that GADTs and type classes functional depencies do not
work well, but there is no problem if you only use type classes.
The first alternative would be using a multiple parameter type classes with
functional dependencies. This would be something that Oleg would be likely
to propose you. But I think you do not want this :)
A second alternative would be to simulate your GADT with a type class and
your constructors with the functions of that type class:
class Term g where
lit :: F f Int int = Int - g f int
suc :: F f Int int = g f int - g f int
isZero :: (F f Int int, F f Bool bool) =
g f int - g f bool
iff :: (F f Bool bool, F f a a') =
g f bool - g f a' - g f a' - g f a'
As a remark, this is a church encoding of the GADT.
Your examples:
ex1 :: Term g = g Untyped ()
ex1 =
iff (isZero (suc (lit 0)))
(lit 1)
(lit 2)
| the same as ex1, but Typed
ex1' :: Term g = g Typed Int
ex1' =
iff (isZero (suc (lit 0)))
(lit 1)
(lit 2)
| a term that has type bug, but will be accepted as Untyped
ex2 :: Term g = g Untyped ()
ex2 =
iff (isZero (suc (lit 0)))
(lit 1)
(isZero (lit 2))
Now you can encode functions on the GADT as instances of this type class:
newtype Untype g b a = Untype {untype :: g Untyped ()}
instance Term g = Term (Untype g) where
lit x = Untype (lit x)
suc t = Untype (suc (untype t))
isZero t = Untype (isZero (untype t))
iff c t e = Untype (iff (untype c) (untype t) (untype e))
This should suffice for encoding your untype.
Although this might look like a bit puzzling at first glance, the translation
of the GADT code into the type class version (and vice versa) is quite
straighforward and mechanical.
The advantages of this encoding in relation to GADTs are that:
1) It does not have the GADTs - fundeps problem;
2) It does not require any heavy machinary from the compiler
(if it would not be for your F class, it would be Haskell 98).
The main disadvantage is that in some functions that you can define
with GADT might not be easily definable with this encoding. I must
say that, from my experience, that functions of this kind do not occur
often.
Until GHC fixes the problem of the interaction between fundeps and
GADTs, you might want to consider using this. All code you develop
with this encoding can be very easily translated to GADT form once the
problem is solved.
If you want further references to this technique check this:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg10047.html
The original thread by Conor is:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg10033.html
The discussion that derived from this thread is quite interesting.
Cheers,
Bruno
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell-cafe] Can this be improved?
Hello,
On Tue, 27 Dec 2005 16:39:34 +, Chris Kuklewicz wrote:
Happy Holidays,
I was wondering if it this small snippet of code could be altered to
require fewer OPTIONS -fallow-... switches.
Here is a partial solution using only -fglasgow-exts:
module MyShow where
class MyShow t where
swim :: String - t
instance MyShow String where
swim = id
instance (Show a, MyShow t) = MyShow (a - t) where
swim s x = swim (s ++ show x)
test foo = foo and 7 are
main = do putStrLn $ swim Hello World # [17,18,19] !
putStrLn $ test (swim I also think [4,5,6]) cool .
The problem of this solution is that, because we are using show in the
definition of swim for (a - t), the strings are beeing printed with extra
\.
*MyShow main
Hello World #[17,18,19]!
I also think [4,5,6] and 7 are cool.
You can, ofcourse, add a new instance for (String - t) but that will
cost you -fallow-incoherent-instances and -fallow-overlapping-instances.
instance MyShow t = MyShow (String - t) where
swim s x = swim (s ++ x)
Could this be improved by TypeEq machinery? Is there a Haskell 98 way
to make myShow work this way?
The problem of the previous solution is that you do not want, in the general
case,
use the default instance of Show for Strings. An alternative is to just
introduce
a newtype S (isomorphic to String) that allows you to handle Strings
differently:
module MyShow where
class MyShow t where
swim :: S - t
newtype S = S {unS :: String}
instance MyShow S where
swim = id
instance Show S where
show = unS
instance (Show a, MyShow t) = MyShow (a - t) where
swim s x = swim (S $ unS s ++ show x)
putSLn = putStrLn . unS
test foo = foo (S and ) 7 (S are )
main = do putSLn $ swim (S Hello) (S ) (S World #) [17,18,19] (S !)
putSLn $ test (swim (S I also think ) [4,5,6]) (S cool)
(S .)
By using the newtype S instead of Haskell String, you obtain an Haskell 98
solution. I am not sure if this is good enough for you but it seems a good
compromise.
Hope it helps!
Cheers,
Bruno
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Regular Expressions without GADTs
Hello Conor, I personally think GADTs are a great idea, don't get me wrong. I am not arguing that we should all start programming using on a Church encoding. Neither I am arguing that this encoding can replace GADTs in all cases. Nevertheless, I believe that knowing about this encoding, in the first place, can be extremely valuable for programmers. Let's not forget that neither GADTs or multiple parameter type classes are Haskell 98! In fact, as far as I understood from the Haskell Workshop, we are a long way from those extensions becoming standard. My point is that if you are developing software, then you want to use something standard (this is, running on Hugs, Nhc, Ghc, Ehc, ...). This encoding tries to avoid extensions (not saying that it does for all cases). In the end, that is what most design patterns are: workarounds on missing language features. In this case missing features of Haskell 98 (but not GHC Haskell). Best Regards, Bruno Oliveira ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Regular Expressions without GADTs
Hello,
You can also write this code in Haskell 98. Jeremy Gibbons and I have
recently written a paper entitled TypeCase: A design pattern for
type-indexed functions where we explore the use of some techniques from
lightweight approaches to generic programming (Ralf Hinze and James
Cheney's work) for other purposes.
If you are interested you can take a look at:
http://web.comlab.ox.ac.uk/oucl/work/bruno.oliveira/typecase.pdf
Basically, we can use type classes and GADTs as two alternatives approaches
to implement type-based case analysis. A well-known example of this is
printf. With printf we want to construct a format string that determines the
type of printf. Something similar happens here, we want to build a parser based
on the type of the regular expression.
There is nothing ingenious with this solution --- I basically translated
Oleg's and Conor's code. In the paper we discuss in details different
trade-offs between different implementations (e.g. GADT vs type classes).
For instance, here is something you cannot do (easily) with the GADT
approach:
myParser :: MonadPlus m = Parse m tok Int
myParser = Parse (\_ - return (1::Int))
test = asList (parse myParser ole)
Basically, with the code that follows you can define your own customized
Regular expressions that you can use with your parser. (Sorry for the
stupid example, but just to give you the idea).
Ultimately you can reason on your programs (of this kind!) using GADTs or
multiple-parameter
type classes with functional dependencies and them translate them into
Haskell 98.
Here is the code:
module RegExps where
import Monad
newtype Zero = Zero Zero -- Zero type in Haskell 98
class RegExp g where
zero :: g tok Zero
one:: g tok ()
check :: (tok - Bool) - g tok tok
plus :: g tok a - g tok b - g tok (Either a b)
mult :: g tok a - g tok b - g tok (a,b)
push :: tok - g tok r - g tok r
star :: g tok a - g tok [a]
newtype Parse m tok t = Parse {parse :: [tok] - m t}
instance MonadPlus m = RegExp (Parse m) where
zero= Parse (\_ - mzero)
one = Parse (\l -
case l of
[] - return ()
_ - mzero)
check p = Parse (\l -
case l of
[t] - if (p t) then return t else mzero
_ - mzero)
plus r1 r2 = Parse (\l - (liftM Left $ parse r1 l) `mplus`
(liftM Right $ parse r2 l))
push tok r = Parse (\l - parse r (tok:l))
mult r1 r2 = Parse (\l -
case l of
[] - liftM2 (,) (parse r1 l) (parse r2 l)
(t:ts) - parse (mult (push t r1) r2) ts `mplus`
liftM2 (,) (parse r1 ([] `asTypeOf` ts)) (parse r2
(t:ts)))
star r = Parse (\l -
case l of
[] - return []
ts - parse (mult r (star r)) ts = (\(x,xs) - return
$ x : xs))
Problem with the monomorphism restriction
p1 :: RegExp g = g Char ([Char], [Char])
p1 = mult (star (check (== 'a'))) (star (check (== 'b')))
p1 = (Mult (Star (Check (== 'a'))) (Star (Check (== 'b'
asMayBe :: Maybe a - Maybe a
asMayBe = id
asList :: [a] - [a]
asList = id
testp = asMayBe $
parse (star (mult (star (check (== 'a'))) (star (check (==
'b')
abaabaaa
*RX testp
Just [(a,b),(aa,b),(aaa,)]
-- see alternative parses
testp1 = take 3 $ asList $
parse (star (mult (star (check (== 'a'))) (star (check (==
'b')
abaabaaa
-- Parsing the list of integers
ieven = even :: Int-Bool
iodd = odd :: Int-Bool
p2 :: RegExp g = g Int (Either (Int, (Int, [Int])) (Int, [Int]))
p2 = plus (mult (check iodd) (mult (check iodd) (star (check ieven
(mult (check ieven) (star (check iodd)))
-- the parser is ambiguous. We can see the alternatives
test2 = take 3 $ asList $ parse (star p2) [1::Int,1,2,3,3,4]
Connor's code for empty.
{-
newtype Empty tok t = Empty {empty :: Maybe t}
instance RegExp Empty where
zero= Empty mzero
one = Empty (return ())
check _ = Empty mzero
plus r1 r2 = Empty ((return Left `ap` empty r1) `mplus`
(return Right `ap` empty r2))
mult r1 r2 = Empty (return (,) `ap` empty r1 `ap` empty r2)
star _ = Empty (return [])
-}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simulating OO programming with type classes; writing a factory fu nction
Hi Alistair! Just a quick reply (I didn't had time to look at Ralf's technique). Looking at your code, it seems to me that you are missing the notion of a supertype (perhaps, that's the intended thing with BaseClass?). I would use an existencial type to capture this notion: === data Base = forall c . Method c = Base c instance BaseClass Base instance Method Base where method1 (Base x) i = Base (method1 x i) method2 (Base x) = method2 x the modifications on the code would be: class BaseClass c = Method c where -- method1 returns a supertype Base method1 :: c - Int - Base method2 :: c - Int instance Method c = Method (SubBase2 c) where -- method1 does not fail any more method1 x i = Base (SubBase2 (SubBase1 5)) method2 x = 2 makeSubType s = if s == SubBase1 then Base (SubBase1 3) else Base (SubBase2 (SubBase1 4)) Perhaps a better name for Base would be SuperMethod (since it is really trying to capture the fact that is the super type for Method). Hope it helps Cheers, Bruno ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Correct interpretation of the curry-howard isomorphism
Hi! Thanks Connor, I enjoyed your answer, it was very illustrative. but then, it would be too easy to write this in haskell: coerce :: a - b coerce x = undefined As an obvious consequence, Haskell type system would be unsound. So, I assumed that this would be a wrong interpretation. This is the part of your email which frightens me the most. Of course Haskell's type system is unsound! What factors lead you to this kind of assumption? Clearly a misconception of mine. Is it a good excuse that people told me that (or I misunderstood them) :) ? The type system does not become a logic until you populate some of the types (hopefully only those corresponding to true propositions) with the terms which describe the construction of proofs. You can't pretend that Haskell is sound just by hoping that Curry and Howard (when properly interpreted) won't be able to see the broken bits. It's nonetheless an interesting question which bits you need to throw away to get a sound language. You'll have to get rid of y :: (p - p) - p unJust :: Maybe wmd - wmd and hence the programming language features which enable them to be constructed, in particular, pattern matching with incomplete coverings, and general recursion. Yes, I thought about those implications, that's why I also thought (incorrectly) that it would be too limiting and therefore probably wrongly interpreted. It is also, not too hard to see, as you said, that general recursion would validate that interpretation (even without using any other primitives or functions): coerce :: a - b coerce = coerce or even coerce :: a - b coerce x = let y = y in y Then, even if we ignored the primitives, Haskell would still be unsound! Moreover, we could then say that most of the functional languages (which have a similar type system) are unsound. Right ? Is it Charity an exception on this? There's an interesting paper `Elementary Strong Functional Programming' by David Turner, in which he proposes such a language. He suggests that, at least for paedagogical purposes, a functional language which gave up completeness for consistency might be no bad thing. I'm inclined to agree with him. I will take a look on it. So I won't make any foolish and portentous pronouncements about dependent types being the only way to save us from damnation. I'll merely observe that we often use the unsound parts of programming languages as the best approximations available to the programs we really mean: we don't intend recursion to loop infinitely, we just have no means to explain in the program why it doesn't; we don't intend to apply unJust to Nothing, we just have no means to explain in the program why this can't happen. Dependent types support a higher level of articulacy about what is really going on, reducing, but not removing entirely the need to work outside the consistent fragment of the language. They do not save us from Satan but from Wittgenstein. Whereon you know something, thereon speak! Dependent types definitely seem an advance to me. I saw recently a presentation of a very impressive tool (epigram - I wonder if you have heard about it :P). I'll be definitely take a better look on it as soon as I finish some work with more priority. Best Regards, Bruno ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
