- Haskell-Cafe - Haskell.org

can this be done with stack?
by Dennis Raddle 03 Jun '17

03 Jun '17

Using stack, but I have a need to build lots of executables. **lots** and new ones all the time .. my application is music playback. I used to have a single executable for playing music, and used it for all compositions. I later found that I needed to do a lot of configuration specific to each composition, and that the most natural language for specifying all the data and functions specific to a composition was Haskell. That means I have a source file for every composition, in the same directory where I store that composition (as a Sibelius file). But a couple things. (1) they aren't in the stack tree, (2) I don't want to add every one of these to a cabal file. What is the best way to approach this goal? D

2 5

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 03 Jun '17

03 Jun '17

> On Fri Jun 2 10:26:16 UTC 2017, J. Garrett Morris wrote: > This conversation has become deeply mysterious to me. Hi Garrett, thank you for the opportunity to debate the ideas in Instance Chains, and correct any misunderstandings I might have gained. The interaction of Overlapping Instances with other Haskell features has been vexing for a long time. There have been many approaches. I find this continuing situation particularly frustrating, because it seems to me there was an answer in 2002 [1], whose effectiveness was confirmed by the HList work 2004 [2]. I've been banging this drum for a long time [4]. > I understand that you're revisiting arguments on the structuring of conditionals ... No. Until your comment yesterday re Dijkstra (thank you for the tip), I was continuing ideas in the Sulzmann and Stuckey Constraint Handling Rules approach [1]. Although your papers/Dissertation cite some of S&S's work, you seem unaware of type disequality guards. I think that's a significant oversight. > ... that were tried and discarded in the 70s; I can see why Dijkstra's ideas might be discarded for term-level calculation: * the impossibility of determining whether guards are mutually exclusive (that's a specie of the halting problem) * the deliberate non-determinacy But that first objection is not applicable for instances/guards, because they have a very simple semantic structure: pattern-match on the instance head, then type (dis-)unifiability test. The second is a definite plus-feature for instance selection. (Reflecting how GHC works today.) So I'm fully up with the programme of the great programmer. > what I don't understand is why you need > to repeatedly mischaracterize my work to do so. If I'm mischaracterising, I apologise. I note, though, you haven't demurred at my observation that instance chains need backtracking. I find backtracking far more unacceptable than indeterminacy. > For one example, I have no idea why you make the following claim: >> Nevertheless, I can only write one Instance Chain >> per class. So I can't (say in another module) >> introduce a new datatype with instances. > The instance chains paper is quite explicit in ruling out this > interpretation; when introducing the notion of chains, we wrote: > In ilab, a class can be populated by multiple, non-overlapping > instance chains, where each chain may contain multiple clauses > (separated by the keyword else). Then I apologise. The two chief examples in that paper (gcd and the Swierstra encoding) both show a final `else ... fails` branch with a catch-all instance head. Section 3.2 comments "..., closing the Gcd class." For the Swierstra encoding in particular, the algorithm requires the class to be total (it must be closed), so that the recursive descent test/validation for go-left/go-right can be determinate. > For another, you give a fanciful description of the problems that > might arise in implementing instance chains, including: I reject "fanciful". So I'm going to give citations. >> There's a persistent problem for the compiler >> testing for type equality: >> the usage sites must have the types grounded. >> It's often more successful to prove disequality. That's straight out of the HList paper [2], Section 9 "By chance or by design?". "We should point out however groundness issues. If TypeEq is to return HTrue, the types must be ground; TypeEq can return HFalse even for unground types, provided they are instantiated enough to determine that they are not equal." > and also: >> I suspect that for the compiler, >> Instance Chains will be as problematic >> for type inference as with Closed Type Families: >> CTFs have a lot of searching under the covers >> to 'look ahead' for equations that can safely match. That's from Richard, particularly this comment [3]. The whole blog post is relevant here, I think. > Luckily, both instance chains and closed type families have > formalizations that can be checked to evaluate these claims. Yes, Overlapping Instances has suffered for too long from under-/non-formalised semantics. What I'll be doing for Instance Guards is giving a translation into Haskell2010 + MPTCs __without__ overlaps. (I will need to assume, though, a type-level type equality test/total function. You've already commented that's easliy produced.) A serious weakness of Instance Chains, it seems to me, is it can't be translated to existing Haskell. > In neither case do we find either equality limited to ground types > or anything that should be construed as 'look ahead'. I think the situation has changed with the introduction of Type Families. They weren't applicable in 2010. So not relevant to the Instance Chains paper. "Look ahead" is exactly what Richard is describing in the bulk of that blog post. That is, looking down the sequence of instance equations, to see if any would match and be confluent. This significantly helps progress in inference. If Instance Chains aren't going to be doing that, that's another weakness. > Perhaps you're trying to refer to the use of > infinitary unification in checking apartness (but not in > checking equality) for closed type families? No, infinitary unification is a whole 'nother bag of spanners. I am still goggling at your joint paper with Richard. > Here again, not only is there no use of or need > for infinitary unification with instance chains, ... Good! > but I discussed this difference and its consequences > in my 2015 paper. OK. I've not yet got through that paper. What I do see in the 2010 paper (perhaps this has changed subsequently) is using typeclass membership to determine whether a type is a member of the __same__ class. This seems to be essential to the Swierstra encoding such as: > else f :<: (g :+: h) if f :<: g > else f :<: (g :+: h) if f :<: h Gloss: "f is related to (g :+: h), if f is related to g". And likewise for f related to h. So: * this needs look inside the ( :+: ) to see if f is related to g or to h, or to both (fail) or to neither (fail). And now you tell me there might be other instance chains for `:<:`, so the compiler has to work through them. * it breaks down the 'phase distinctions' in instance selection. I feel very queazy about a recursion like that at the class level. We can express Russell's paradox: > else f :<: g fails if f :<: g Haskell very strictly doesn't support instance contexts driving selection of instances. That is confusing for newbies, but it's for very good decidability reasons. > Finally, you make various claims about what is and is not a solution > to the expression problem which have no apparent relationship to any of > the existing work on the expression problem or its encodings. > ... Again, this is all laid out, with examples, in my 2015 paper. I was being brief. (And this post has gone on plenty long enough, too.) I'll come back and debate that point when I've worked through your 2015 paper. What's strongly motivating me with Haskell is getting the type system to cater for extensible/anonymous records. (I'm a Relational Theorist by trade.) Closed instances (be they Chains or Type Families, or the proposed Closed Classes) are just not going to hack it. Adam G for the Overloaded Records Fields work has eschewed Type Families in favour of FunDeps. That's because it needs to create instances 'on the fly'. Now he hasn't needed overlaps yet (ORF is at an early stage), but anonymous/extensible records will. Just like HList. AntC [1] Sulzmann & Stuckey 2002 "A Theory of Overloading", esp section 8.2 "Overlapping Definitions" [2] Kiselyov et al 2004 "Strongly Typed Heterogeneous Collections" [3] https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-f… [4] https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage

3 2

Haskell Weekly
by Taylor Fausak 02 Jun '17

02 Jun '17

Hello haskell-cafe! I am the Haskell Weekly editor. In the past, some people have expressed interest in receiving my newsletter on this mailing list. Is that something I should set up? If you're curious about Haskell Weekly, please check out the latest issue, which was published today: <https://haskellweekly.news/issues/57.html> I've also included issue 57 as plain text here. If you like what you see, head over to <https://haskelweekly.news> and subscribe! --- # Haskell Weekly ## Issue 57 Welcome to another issue of Haskell Weekly! Haskell is a purely functional programming language that focuses on robustness, concision, and correctness. This is a weekly summary of what’s going on in its community. - Realizing Hackett, a metaprogrammable Haskell <https://lexi-lambda.github.io/blog/2017/05/27/realizing-hackett-a-metaprogr…> > Almost five months ago, I wrote a blog post about my new programming language, Hackett, a fanciful sketch of a programming language from a far-off land with Haskell's type system and Racket's macros. [...] Hackett is not only real, it's working, and you can try it out yourself! - Imperative Haskell <http://vaibhavsagar.com/blog/2017/05/29/imperative-haskell/> > Why don't we do this all the time, when Haskell is at least a serviceable imperative language? Because writing imperative programs is hard! They don't compose as well, have less useful type signatures, and are harder to reason about. Getting away from those things is why we have Haskell to begin with! - A Haskell cross compiler for Android <https://medium.com/@zw3rk/a-haskell-cross-compiler-for-android-8e297cb74e8a> > Finally launching and running the application on the device, we are greeted with "Hello from Haskell". While the utility of this application is certainly questionable it illustrates the essential steps required to build, link and run an Android application calling a native Haskell function. - Smart data with conduits <https://mmhaskell.com/blog/2017/5/29/smart-data-with-conduits> > If you're a programmer now, there's one reality you'd best be getting used to. People expect you to know how to deal with big data. The kind of data that will take a while to process. The kind that will crash your program if you try to bring it all into memory at the same time. - Wire is hiring a Software Backend Developer (Operations) in Berlin, Germany (ad) <https://wire.softgarden.io/job/1022464?l=en> > Wire is an open source, end-to-end encrypted messenger for personal and business use. For our development center in Berlin we are hiring two Backend Haskell Developers. As Software Developer Backend Operations you will maintain our infrastructure, ensuring that it runs 24/7. Check out our jobs at wire.com/jobs and our open source code on github.com/wireapp. - What we talk about when we talk about types <https://joyofhaskell.com/posts/2017-05-31-is-vs-has.html> > These dialogues somewhat pedantically dissect what we mean when we say a type is an instance of a type class or a type has an instance of a type class and why. Through the course of conversation, we touch on the nature of types, type constructors, and type classes, which led to us talking about math, set theory and category theory, and what they have to do with types and type classes. - The partial options monoid <https://medium.com/@jonathangfischoff/the-partial-options-monoid-pattern-31…> > Parsing options is not the hardest problem. However, if you do not create a pattern the rest of your team can follow, your program can become a tangled mess of random file reads, environment variable lookups and unpredictable defaulting. The Monoid class is a rock solid abstraction for combining options. - Playing with lens-aeson <https://www.snoyman.com/blog/2017/05/playing-with-lens-aeson> > That works, but it's far from inspiring. We're declaring a Color data type simply for the purpose of writing a type class instance. But it feels pretty heavyweight to have to declare a data type and make a type class instance for just one use site. ### Packages of the week Several interesting packages were announced this week. Instead of picking one to feature, all four are this week's packages of the week! - double-pendulum-simulation <https://github.com/lotz84/double-pendulum-simulation> Simulates and renders a double pendulum system. - legion <https://github.com/aviaviavi/legion> Implements a simple block chain server that synchronizes nodes over the network. - prettyprinter <https://github.com/quchen/prettyprinter> Aims to end the Wadler/Leijen zoo dilemma by being a modern, well-documented pretty printer. - sitepipe <https://github.com/ChrisPenner/SitePipe> Generates static sites with plain values and less magic.

5 6

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 02 Jun '17

02 Jun '17

> On Fri Jun 2 02:32:39 UTC 2017, Richard Eisenberg wrote: > > > On May 31, 2017, at 12:31 AM, Anthony Clayden wrote: > > >> You could always view > >> > >>> instance TypeError ... => C Int Bool > >> > >> as sugar for > >> > >>> instance C Int Bool fails > > > > Yes I understand that. > > But no I don't want any instance. > > (Sugar on rotten fruit doesn't hide the smell.) > > I hereby pronounce > > > instance TypeError ... => C Int Bool > > as "not an instance". ... Hmm. I'd be interested how you're going to stop the compiler matching some usage site to it. > In other words, I'm not sure what > you're getting at here other than concrete syntax. > How does not having an instance differ > than the TypeError solution? Good question. I've been struggling to explain it. Re-reading the Instance Chains paper has clarified the issue for me. And looking at Garrett's later 'Variations on Variants' paper. (Clarified, because that's a non-solution.) It's the Expression Problem: Once I have a catch-all instance (even if it has an impossible-to-fulfill constraint) the compiler is committed to selecting that instance. I can't introduce a new data type and new instance for it, because it'll overlap the catch-all instance. IIUC, Instance Chain's 'fail' is more powerful, it triggers back-tracking to look for another instance that doesn't fail. But we don't want to introduce backtracking into Haskell search for instances. Nevertheless, I can only write one Instance Chain per class. So I can't (say in another module) introduce a new datatype with instances. Sometimes closed/chained instances are the right solution. (That's the case for HList, for example. But even there I'm not convinced. I might want as well as HNil, HCons, a constructor with explicit type-labelling.) But sometimes closed instances are not right. I would say that where closed instances are needed, you can still achieve that with a 'catch-all' stand-alone instance, suitably guarded, of course. So I disagree with Garrett: not only do Instance Chains fail to solve the expression problem, they actually exacerbate it. (Same for Closed Type Families, or Closed Class Instances.) > > OK. Perhaps you're seeing something I can't. > > To adapt your example from a parallel message, suppose: > > <snip> > > What you're getting at here is that there may be > interesting interplay between instance guards and > OverlappingInstances. Indeed. This would have to be worked > out (or left as an open question) in the proposal. > > Regardless, I think that hashing out this level of detail > here is the wrong place. ... OK, fair enough. > Put it in the proposal! That way, the ensuing > debate involves more of the community and > persists better. > Oh! that I had "Deserts of vast eternity" to write the thing. As it is, it's easier to tackle as bite-size pieces on the forum. AntC

3 2

Call for participation: Trends in Functional Programming, 19-21 june 2017 AND Trends in Functional Programming in Education, 22 june 2017, University of Kent, Canterbury
by Peter Achten 02 Jun '17

02 Jun '17

----------------------------- C A L L F O R P A R T I C I P A T I O N ----------------------------- ======== TFP 2017 =========== 18th Symposium on Trends in Functional Programming 19-21 June, 2017 University of Kent, Canterbury https://www.cs.kent.ac.uk/events/tfp17/index.html ========= TFPIE 2017 ======== Co-located with TFP, and included in the registration fee, is Workshop on Trends in Functional Programming in Education 22 June 2017 University of Kent, Canterbury https://www.cs.kent.ac.uk/people/staff/sjt/TFPIE2017/ The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions (see below). Authors of draft papers will be invited to submit revised papers based on the feedback receive at the symposium. A post-symposium refereeing process will then select a subset of these articles for formal publication. TFP 2017 will be the main event of a pair of functional programming events. TFP 2017 will be accompanied by the International Workshop on Trends in Functional Programming in Education (TFPIE), which will take place on 22 June. The TFP symposium is the heir of the successful series of Scottish Functional Programming Workshops. Previous TFP symposia were held in * Edinburgh (Scotland) in 2003; * Munich (Germany) in 2004; * Tallinn (Estonia) in 2005; * Nottingham (UK) in 2006; * New York (USA) in 2007; * Nijmegen (The Netherlands) in 2008; * Komarno (Slovakia) in 2009; * Oklahoma (USA) in 2010; * Madrid (Spain) in 2011; * St. Andrews (UK) in 2012; * Provo (Utah, USA) in 2013; * Soesterberg (The Netherlands) in 2014; * Inria Sophia-Antipolis (France) in 2015; * and Maryland (USA) in 2016. For further general information about TFP please see the TFP homepage. (http://www.tifp.org/) == SCOPE == The symposium recognizes that new trends may arise through various routes. As part of the Symposium's focus on trends we therefore identify the following five article categories. High-quality articles are solicited in any of these categories: Research Articles: leading-edge, previously unpublished research work Position Articles: on what new trends should or should not be Project Articles: descriptions of recently started new projects Evaluation Articles: what lessons can be drawn from a finished project Overview Articles: summarizing work with respect to a trendy subject Articles must be original and not simultaneously submitted for publication to any other forum. They may consider any aspect of functional programming: theoretical, implementation-oriented, or experience-oriented. Applications of functional programming techniques to other languages are also within the scope of the symposium. Topics suitable for the symposium include, but are not limited to: Functional programming and multicore/manycore computing Functional programming in the cloud High performance functional computing Extra-functional (behavioural) properties of functional programs Dependently typed functional programming Validation and verification of functional programs Debugging and profiling for functional languages Functional programming in different application areas: security, mobility, telecommunications applications, embedded systems, global computing, grids, etc. Interoperability with imperative programming languages Novel memory management techniques Program analysis and transformation techniques Empirical performance studies Abstract/virtual machines and compilers for functional languages (Embedded) domain specific languages New implementation strategies Any new emerging trend in the functional programming area If you are in doubt on whether your article is within the scope of TFP, please contact the TFP 2017 program chairs, Scott Owens and Meng Wang. == BEST PAPER AWARDS == To reward excellent contributions, TFP awards a prize for the best paper accepted for the formal proceedings. TFP traditionally pays special attention to research students, acknowledging that students are almost by definition part of new subject trends. A student paper is one for which the authors state that the paper is mainly the work of students, the students are listed as first authors, and a student would present the paper. A prize for the best student paper is awarded each year. In both cases, it is the PC of TFP that awards the prize. In case the best paper happens to be a student paper, that paper will then receive both prizes. == PAPER SUBMISSIONS == Acceptance of articles for presentation at the symposium is based on a lightweight peer review process of extended abstracts (4 to 10 pages in length) or full papers (20 pages). The submission must clearly indicate which category it belongs to: research, position, project, evaluation, or overview paper. It should also indicate which authors are research students, and whether the main author(s) are students. A draft paper for which ALL authors are students will receive additional feedback by one of the PC members shortly after the symposium has taken place. We use EasyChair for the refereeing process. Papers must be submitted at: https://easychair.org/conferences/?conf=tfp17 Papers must be written in English, and written using the LNCS style. For more information about formatting please consult the Springer LNCS web site: http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 == INVITED SPEAKERS == Conor McBride University of Strathclyde (UK) Cătălin Hriţcu INRIA Paris (FR) Heather Miller Northeastern University (USA) and EPFL (CH) == IMPORTANT DATES == Submission of draft papers: 5 May, 2017 Notification: 12 May, 2017 Registration: 11 June, 2017 TFP Symposium: 19-21 June, 2017 Student papers feedback: 29 June, 2017 Submission for formal review: 2 August, 2017 Notification of acceptance: 3 November, 2017 Camera ready paper: 2 December, 2017 == PROGRAM COMMITTEE == Co-Chairs Meng Wang University of Kent (UK) Scott Owens University of Kent (UK) PC Jeremy Yallop University of Cambridge (UK) Nicolas Wu University of Bristol (UK) Laura Castro University of A Coruña (ES) Gabriel Scherer Northeastern University (US) Edwin Brady University of St Andrews (UK) Janis Voigtländer Radboud University Nijmegen (NL) Peter Achten Radboud University Nijmegen (NL) Tom Schrijvers KU Leuven (BE) Matthew Fluet Rochester Institute of Technology (US) Mauro Jaskelioff CIFASIS/Universidad Nacional de Rosario (AG) Patricia Johann Appalachian State University (US) Bruno Oliveira The University of Hong Kong (HK) Rita Loogen Philipps-Universität Marburg (GE) David Van Horn University of Marylan (US) Soichiro Hidaka Hosei University (JP) Michał Pałka Chalmers University of Technology (SE) Sandrine Blazy University of Rennes 1 - IRISA (FR)

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 02 Jun '17

02 Jun '17

> On Tue May 30 19:43:30 UTC 2017, Richard Eisenberg wrote: > > On May 24, 2017, at 3:13 AM, Anthony Clayden wrote: > ... Some functions are defined by an ordered set of equations. > Some (that is, class methods) are defined by > an unordered set of equations, perhaps distributed across modules. > Both models are useful. Sure. Let a 100 schools of thought contend. >>> ... [equality constraints and equality guards are] >>> different, but I think the equality guard is useless >> I agree adds nothing over repeating the typevar. And I've already agreed the potential for confusion with (~) constraints. So noted. I'll include it in the proposal, where a wider audience can bikeshed. >> I see two main uses/benefits: >> 1. avoids the need for non-linear patterns in the head > > Agreed that it would do this. But why is that important? > I was in part thinking of your wondering-out-loud earlier in the Partially applied thread https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127078.html If we want to part-apply a type Fun which has a non-linear lhs, how does that go with your case-equation style? Adapting that earlier example: > type family F a b where > F a a = () -- added an equation > F Int b = b > F a Bool = a would really mean > type F a b = case a of > _ -> case b of -- ?? _ match-all > a -> () -- ?? re-using typevar a > Int -> b > _ -> case b of > Bool -> a > _ -> F a b > > 2. visually points up the 'non-apartness' vs an, um. > > "apartness guard" > > > > (When I was figuring out Andy A-M's 2013 example, > > I rewrote the non-linear patterns with ~ guards, > > so I could figure out the apartness guards > > esp for the semi-apart instances. > > I posted the later workings to your blog > > Somehow, this is more convincing. But I'm still not > convinced on this point. Happily, you don't need to > convince me -- put in the proposal what you like and then > we can debate a concrete design. > > >> [except as a type-level "let", I suppose].) > > They would work as "let", I think: > > > instance Either a a | a ~ SomethingBigAndUgly where ... > > Note that the `a` is not introduced in the guard. Ah, OK. I get you. Equally that could be > instance Either a b | a ~ b, a ~ SomethingBigAndUgly where .. > > > Ok thanks, yes [TypeError] helps. > > Nevertheless it seems disergonomic > > to write an instance for a type-equal case, > > even with a helpful error message; > > when what you want is: no such instance. > > You could always view > > > instance TypeError ... => C Int Bool > > as sugar for > > > instance C Int Bool fails Yes I understand that. But no I don't want any instance. (Sugar on rotten fruit doesn't hide the smell.) There are (or at least used to be) all sorts of side-effects from there in effect being an instance that matched. > > What I can see will be awkward is backwards > > compatibility: can a class/type family with guards > > coexist with CTFs and with classes using overlap? > > Sure. There would be no problem with this. The new idea is > just that: new. I don't see it as getting rid of anything > we already have. Perhaps some day we could think about > removing OverlappingInstances, but we certainly don't have > to do that at the same time as introducing instance > guards. (I do like that name, too.) > OK. Perhaps you're seeing something I can't. To adapt your example from a parallel message, suppose: > module A > > class {-# INSTANCEGUARDS #-} C a where ... > instance C (Maybe a) | a /~ Int where ... > instance C (Maybe Int) where ... > > module B > -- knows nothing of InstanceGuards > import A > > instance {-# OVERLAPPABLE #-} C (Maybe Bool) where ... I want to reject that `(Maybe Bool)` instance. Even though it would legitimately be OVERLAPPABLE by (Maybe a) (that is, without the `a /~ Int` guard). Furthermore I might want a class to be InstanceGuarded, even though the instances I declare don't themselves need guards. (That is, I'm wanting to avoid 'future' overlaps in modules that import the class.) > > > > I'll have a crack at the proposal. > > Great. Thanks! (Likely I'll need some help with the protocols.) AntC

2 1

Vim syntax file typo
by Matthew Fernandez 02 Jun '17

02 Jun '17

Hello Haskell Cafe, The attached patch fixes what looks to be a typo in a comment in the Haskell Vim syntax file. Pretty trivial, but I'm mailing it to this list as it's listed as the maintainer of the file and I believe that's the Vim policy. Please let me know if there's somewhere more appropriate I should send this or if you'd prefer me to just submit it as a pull request on the Vim Github. Thanks, Matt

1 1

Re: [Haskell-cafe] Type-level GCD [Instance Chains]
by Anthony Clayden 01 Jun '17

01 Jun '17

> On Thu Jun 1 12:44:32 UTC 2017, Anthony Clayden wrote: >> For example, consider the simple chain: >> >> class C t u where f :: t -> u >> instance C Int Int where >> f = M >> else C t u where >> f = N Ah, silly me. There's a neater way to achieve that. > I think Instance Guards both have less lexical clutter, > and help the compiler see what's coherent: > instance C Int Int where f = M > instance C t u | (t, u) /~ (Int, Int) where f = N AntC

1 0

Re: [Haskell-cafe] Type-level GCD [Instance Chains]
by Anthony Clayden 01 Jun '17

01 Jun '17

> On Thu Jun 1 09:51:25 UTC 2017, J. Garrett Morris wrote: >> On Thu, Jun 1, 2017 at 3:23 AM, Anthony Clayden wrote: >> No, my concern is readability. > Well, presumably from the readability perspective, > the point is that instance chains allow you to express > Euclid's algorithm directly, following the > mathematical presentation, ... What I see in the mathematical presentation, is that each equation is stand-alone, with a guard. I guess we'll just agree to differ on the readability of the Haskell. (What if Euclid had taken up lazy functional programming ..?) >> I must admit I hadn't though of stand-alone instances >> as being like rows in truth tables. >> They're like separate lines of equations, >> each guarded by a condition. > I sense a Dijkstra-like argument that we should avoid writing > "else" or "otherwise", ... If I'm in the company of Dijkstra and Euclid, that's good enough for me. > ... we generally hope for programs to have meanings Yes we do. > and thus for instance resolution to be coherent. I agree the current (under-/non-)specified rules for overlap don't help us reason much about coherence. (But see my post on the cafe last month wrt "Well-behaved instances".) > For example, consider the simple chain: > > class C t u where f :: t -> u > instance C Int Int where > f = M > else C t u where > f = N This is an example where overlap is well-behaved. (Assuming those are the only instances.) > Now, it is simple to define type equality t == u There's a persistent problem for the compiler testing for type equality: the usage sites must have the types grounded. It's often more successful to prove disequality. > using functional dependencies, and so (...) > in the instance chains framework these could be written > as separate instances. This is a case of well-behaved overlap, so they'd work as separate instances anyway. > We might hope to get away with just one extra instance: > instance C Int Int where f = M > instance C t u if t == Int fails where f = N > instance C t u if u == Int fails where f = N > But note that the latter instances will seem incoherent to the compiler, That first most specific instance exhibits 3 type equalities: (t ~ Int. u ~ Int, t ~ u) So there's various ways to slice up the space. I think Instance Guards both have less lexical clutter, and help the compiler see what's coherent: > instance C Int Int where f = M > instance C t t | t /~ Int where f = N > instance C t u | t /~ u where f = N > [4-instance example elided] > ... we have taken one "intuitive" case and split it into > three apparently distinct branches ... I guess what's intuitive will depend on the application. It's difficult to make much claim in the abstract. > ... ---or made things easier for the compiler--- > since we now have four axiom clauses for class C > instead of two, and 6 coherence checks instead of none. The compiler author will love having precise rules for when instances are apart. And being able to check that when compiling the instance (not delay it to the usage site). And needing to validate only each pair of instances; not worry about overlaps of overlaps. I suspect that for the compiler, Instance Chains will be as problematic for type inference as with Closed Type Families: CTFs have a lot of searching under the covers to 'look ahead' for equations that can safely match. AntC

1 0

Re: [Haskell-cafe] Type-level GCD [Instance Chains]
by Anthony Clayden 01 Jun '17

01 Jun '17

> On Wed May 31 14:19:55 UTC 2017, J. Garrett Morris wrote: > [Apologies for breaking threading...] Thanks Garrett, my email client does horribler things to threading. Since the O.P. was about the aesthetics/readibility of code, I'm surprised you elided all the code. (I suppose de gustibus non disputandum.) >> On Wed May 31, Anthony Clayden wrote: >> Leaving aside the question of backtracking >> on instance non-match, >> would anybody write a type-level GCD like this? >Your question seems to be "would you use > the standard recursive statement of > Euclid's algorithm to demonstrate Euclid's algorithm?" > This certainly seemed to be a reasonable idea in 2010. I think the code I posted was using Euclid's algorithm. I agree it's difficult to cast one's mind back to what was reasonable Haskell in 2010, but I didn't use Type Families. > If your concern is efficiency, .. No, my concern is readability. >> (And Subt needs a nasty kludge in case you're trying to >> subtract the larger: it returns Z.) > What you call a nasty kludge, I call a standard operation > on commutative monoids. [https://en.wikipedia.org/wiki/Monus] Well, OK sometimes the kludge is justified ;-). Not for GCD, methinks. Because the equation guards specifically avoid the need. >> I think these days (esp with TypeFamilies/Assoc types), > You seem to be discovering that closed instance chains > can be implemented by writing out truth tables. I must admit I hadn't though of stand-alone instances as being like rows in truth tables. They're like separate lines of equations, each guarded by a condition. (In math, typically the condition is trailing with comma sep.) OK I'll mirror that style below. > I discussed this transformation at length, > and suggested that doing might make your code > harder to write and to read, ... Ok, let's see. Here's the math (adapted from wikipedia): gcd(m, n) = m , if m == n gcd(m, n) = gcd(m - n, n) , if m > n gcd(m, n) = gcd(m, n - m) , if m < n Here's some Haskell (this works in Hugs, just to make sure I'm getting the right vintage) > data Z; data S n > > data LT; data EQ; data GT > data If t > > class Gcd m n p | m n -> p where > -- methods for Gcd go here > > instance (GcdCase m n p (If d), Diff m n d) > => Gcd m n p where -- single 'catch all' instance > -- method definitions > > -- GcdCase instances mirror the Euclid equations > > class GcdCase m n p d | m n d -> p > instance (HTypeCast m p) > => GcdCase m n p (If (EQ, d')) > instance (Gcd d' n p) > => GcdCase m n p (If (GT, d')) > instance (Gcd m d' p) > => GcdCase m n p (If (LT, d')) > > class Diff m n d | m n -> d > instance Diff Z Z (EQ, Z) > instance Diff (S m') Z (GT, S m') > instance Diff Z (S n') (LT, S n') > instance (Diff m' n' d) => Diff (S m') (S n') d > > -- HTypeCast omitted, use standard HList > ... in my Haskell 2015 paper "Variations on Variants". OK, will study. I see that's focussing on Wadler's "expression problem", as does the Instance Chains paper. It's the Swiestra example there I want to get on to. > Of course, you'll have an easier time of it > if you limit yourself to only considering > type-level definitions, and not > the corresponding method definitions. > But doing so rather misses the point > of instance chains. I've used classes throughout the above. So could easily add methods. The idiom (following HList 2004) is some classes are type-level only. So I see no harm making those Type Families in 2017. (Whether they should be Closed TFs vs stand-alone instances is a separate debate.) AntC

2 1