July 2021 - Haskell-Cafe

Re: [Haskell-cafe] Check a lack of a constraint?
by Olaf Klinke 14 Jul '21

14 Jul '21

> > Hello cafe, > > Is it possible in Haskell to check a lack of a certain constraint? > > For example, > > ``` > foo :: C => a > foo = undefined > > ``` > > Here `foo` can only be compiled if called with C satisfied. How do I write the > opposite, so that `foo` is only possible to use when C is not satisfied? > > With best regards. Indeed I found myself wanting this, too. Such a feature might reduce the amount of overlapping instances, but of course it bears the danger that others pointed out. For example, suppose you have a type T :: (* -> *) and the library author of T already defined an instance instance C a => C (T a). Now suppose you have a concrete type A which you know can never have a (lawful) C A instance, but you can define an instance C (T A). The latter would be formally overlapping with the former, even if you know that the former will never be implemented. Thus, instead of local non-satisfiability, a token for the proof that an instance can not exist might be more useful (and more safe). This would correspond to case 2 in Sylvain Henry's GHC proposal. I have no idea, however, how such a proof can be presented [*] in a way that can not be circumvented by a third author and lead to unsoundness. As a concrete example, I defined an instance MonadParsec (StateT String Maybe) which makes a wonderfully fast parser that you can swap in for a Megaparsec parser, but it is overlapping because of MonadParsec Maybe => MonadParsec (StateT s Maybe) although it is absurd to try to make Maybe an instance of MonadParsec. Another example: Think about why the mtl library has an instance MonadFoo m => MonadFoo (BarT m) for every pair (Foo,Bar) of transformers. (And there are quadratically many of these!) It is precisely because a catch-all instance like (MonadTrans t, MonadFoo m) => MonadFoo (t m) will be overlapping as long as we can't rule out MonadFoo (t m) by other means. Olaf [*] The logically natural way would be to have a Void constraint, so that we can say: MonadParsec Maybe => Void

1 0

Check a lack of a constraint?
by Lana Black 14 Jul '21

14 Jul '21

Hello cafe, Is it possible in Haskell to check a lack of a certain constraint? For example, ``` foo :: C => a foo = undefined ``` Here `foo` can only be compiled if called with C satisfied. How do I write the opposite, so that `foo` is only possible to use when C is not satisfied? With best regards.

5 9

What can I use for a weighted graph? I thought Data.Graph would work but I see no provision for edge weights?
by Casey Hawthorne 12 Jul '21

12 Jul '21

Hi What can I use for a weighted graph? I thought Data.Graph would work but I see no provision for edge weights?

2 3

Re: [Haskell-cafe] How to do reversible parsing?
by Johannes Waldmann 11 Jul '21

11 Jul '21

Rendell and Ostermann, Invertible syntax descriptions, Haskell Symposium '10 https://doi.org/10.1145/1863523.1863525 https://hackage.haskell.org/package/invertible-syntax For the general background, see, e.g., Grohne and Voigtländer 2017 Formalizing semantic bidirectionalization ... https://doi.org/10.1016/j.jlamp.2016.04.002 And there's a workshop series on Bidirectional Transformations (from 2012 onwards) - J.

3 9

Invitation: Virtual Haskell Cohack, July 10 (Saturday)
by Chris Smith 10 Jul '21

10 Jul '21

Hello everyone, I'd like to formally invite you to the Virtual Haskell Cohack, which will be running monthly beginning Saturday, July 10. Please review times and RSVP at https://www.meetup.com/NY-Haskell/events/279067287/ so that I know how many people are coming. I would need to upgrade my Zoom account if we exceed 100 people, but that would be amazing. Please make that happen! This is an event for the Haskell community to get together and work on collaborative projects. This could mean: - Teaching or learning Haskell - Writing code or docs on your favorite project and introducing it to others - Learning about other people's projects and getting some mentorship to contribute. - Pair programming on programming challenges like Advent of Code or Project Euler. - Just hanging out and geeking out talking category theory or GHC profiling techniques or whatever. The full agenda is listed at the link above, but it also includes lightning talks, which you can propose when you RSVP or just wait and volunteer to give one at the event. If you want to be sure you make it on the list, mention that you'd like to give a talk in your RSVP and you'll get priority on the signup list. Haskell-adjacent technologies are also welcome, so if you'd like to come hack in Elm, Idris, Agda, Coq, Ocaml, or whatever, you are welcome. The only rule we have is to be kind and welcoming to others. Thanks, and hope to see you there.

1 2

[ANN] parser-unbiased-choice-monad-embedding - the best parsing library; it is based on arrows (was: Pearl! I just proved theorem about impossibility of monad transformer for parsing with (1) unbiased choice and (2) ambiguity checking before running embedded monadic action (also, I THREAT I will create another parsing lib))
by Askar Safin 10 Jul '21

10 Jul '21

Hi. I announce my parsing library https://hackage.haskell.org/package/parser-unbiased-choice-monad-embedding . I think it is best parsing library, and you should always use it instead of other solutions. I will tell you why. You may check comparison table: https://paste.debian.net/1203863/ (if you don't understand the table, don't worry; come back to the table after reading this mail). My library is solution to problem described in this e-mail thread, so read it for motivation: https://mail.haskell.org/pipermail/haskell-cafe/2021-June/134094.html . Now let me describe my solution in detail. I will distinguish parser errors (i. e. "no parse" or "ambiguous parse") and semantic errors (i. e. "division by zero", "undefined identifier", "type mismatch", etc). So, now I will show you parser with unbiased choice, which allows monad embedding. As a very good introduction to arrows I recommend this: https://ocharles.org.uk/guest-posts/2014-12-21-arrows.html . We start from classic parser with this type: newtype ParserClassic t a = ParserClassic ([t] -> [(a, [t])]) You can make it be instance of Functor, Applicative, Monad and Alternative. This type is similar to ReadS from base ( https://hackage.haskell.org/package/base-4.15.0.0/docs/Text-ParserCombinato… ) and to "type Parser = StateT String []" from example here: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad… . I will not give more information, feel free to find it in internet. Now let's replace "a" with Kleisli arrow "b -> m c". We will get this: newtype Parser1 t m b c = Parser1 ([t] -> [(b -> m c, [t])]) Here is resulting parsing library and example: https://godbolt.org/z/qsrdKefjT (backup: https://paste.debian.net/1203861/ ). We can use this parser in Applicative style. And when we need to lift something to embedded monad, we resort to Arrow style. I didn't test this code much. Parser1 cannot be Monad (I proved this in previous letters). At this point someone may ask: why we need arrows? Can we achieve same effect using Applicative only? Yes, we can. Here is result: https://godbolt.org/z/ocY3csWjs (backup: https://paste.debian.net/1203862/ ), I will call such method "anti-arrow". But we have two problems here: first, I think this method makes parser code uglier. Second, this method is limited, and I will show you why later. Okey, now back to arrows. Still, we have this problems (I'm about our arrow code): - Handling left-recursive grammars is tricky (it is possible, but not as simple as right-recursive ones) - Parsing errors (as opposed to semantic error messages) are not great. I. e. if there is no valid parses, we don't get any additional information, i. e. we don't know which token caused error - We don't track locations, so semantic errors are not great, too (i. e. we want to have location info to embed it into semantic error messages) - I suspect this parsing library will have very bad speed, possibly O(exp(input size)) So, let's combine our ideas with package Earley ( https://hackage.haskell.org/package/Earley ). Earley has type "Prod r e t a". Let's replace "a" with Kleisli arrow "b -> m c". Also let's wrap this Kleisli arrow to "L" from srcloc ( https://hackage.haskell.org/package/srcloc ) to get location info. Also, we wrap "t" to "L", too. Thus we get this type: newtype ArrowProd r e t m b c = ArrowProd (Prod r e (L t) (L (b -> m c))) Here is resulting library with example: https://hackage.haskell.org/package/parser-unbiased-choice-monad-embedding . (I didn't test much.) (I recommend to read docs to Earley first.) (My library is designed to be used with some external lexer, lexer-applicative is recommended.) The example also uses lexer-applicative, because lexer-applicative automatically wraps tokens into "L". So, what we got? We solved original goals, i. e.: - We have combinator parser with unbiased choice. Unfortunately, it is not monadic, but it is Applicative and Arrow - We can embed monad, for example, to handle semantic errors - We can test parsing errors before executing embedded monadic action Additionally we solved 4 remaining problems mentioned above, i. e.: - Handling left-recursive grammars is as simple as right-recursive ones (thanks to Earley's RecursiveDo) - Parsing errors are ok - We track locations and we can embed them into semantic errors - We have relatively good speed thanks to Earley What else? We can test grammar for ambiguity using https://hackage.haskell.org/package/Earley-0.13.0.1/docs/Text-Earley.html#v… (I didn't wrap this function, but this can easily be done). Personally I think that my parsing library is simply best. :) And that one should always use it instead of all others. Why I think this? Because: - We all know that CFG is better than PEG, i. e. unbiased choice is better that biased - I don't want to merely produce AST, I want to process information while I parse, and this processing will uncover some semantic errors - So I want unbiased choice with handling semantic errors - The only existing solution, which can do this is my library (and also "happy") - But "happy" doesn't automatically track locations (as well as I know it tracks lines, but not columns) - So the best parsing solution is my library :) My library has another advantage over happy: by extensive use of Alternative's "many" (and arrow banana brackets) you can write things, which are impossible to write in happy. Consider this artificial example (subset of Pascal): --- var a: integer; b: integer; begin a := b + c; end. --- This is its parser, which uses my library (completely untested): --- arrowRule (proc () -> do { sym TVar -< (); declated <- many (ident <* sym TColon <* sym TInteger <* sym TSemicolon) -< (); sym TBegin -< (); -- Banana brackets (|many (do { x <- ident -< (); lift -< when (x `notElem` declated) $ Left "Undeclated identifier"; sym TAssign -< (); -- My library doesn't have "sepBy", but it can be easily created (|sepBy (do { y <- ident -< (); lift -< when (y `notElem` declated) $ Left "Undeclated identifier"; returnA -< (); })|) [TPlus]; sym TSemicolon -< (); returnA -< (); |); sym TEnd -< (); sym TDot -< (); returnA -< (); }) --- This is impossible to write similar code using "happy" with similar ergonomics, because in happy we would not have access to "declared" inside production for sum. The only way we can access "declared" is using state monad (for example, StateT) and put this "declared" into this state monad. But in my library you don't have to use any StateT! Now let me say why mentioned "anti-arrow" style is not enough. Let's try to rewrite this Pascal example using anti-arrow style: --- antiArrowLift $ do { -- ApplicativeDo sym TVar; declated <- many (ident <* sym TColon <* sym TInteger <* sym TSemicolon); sym TBegin; many $ antiArrowLift $ do { x <- ident; sym TAssign; -- My library doesn't have "sepBy", but it can be easily created sepBy [TPlus] $ antiArrowLift $ do { y <- ident; pure $ when (y `notElem` declated) $ Left "Undeclated identifier"; -- Oops }; sym TSemicolon; pure $ when (x `notElem` declated) $ Left "Undeclated identifier"; -- Oops }; sym TEnd; sym TDot; pure (); } --- Looks good. But there is a huge problem here: look at lines marked as "Oops". They refer to "declared", but they cannot refer to it, because outer "do" is ApplicativeDo. So, yes, merely Applicative is not enough. Does my library have disadvantages? Of course, it has! - It is not monadic - It cannot statically check that grammar is element of LR(1) set (as well as I understand, happy can do this) - My library has relatively good speed asymptotic (same as Earley), but it is still not fastest - My library will freeze on infinitely ambiguous grammars. Attempting to check such grammar for ambiguity using Earley's "upTo" will cause freezing, too. See also: https://github.com/ollef/Earley/issues/54 - My library is based on unbiased choice and CFG (as opposed to biased choice and PEG). I consider this as advantage, but my library will not go if you want to parse language defined by some PEG My library is unfinished. The following things are needed: - We need combinator similar to Alternative's "many", but every item should have access to already parsed part of list. Such combinator should be made to be used by banana brackets - We need combinators similar to parsec's chainl and chainr (my library already supports left and right recursion thanks to Earley, but still such combinators would be useful) - Already mentioned "sepBy" - I didn't wrap all Earley functionality, for example, <?> is left unwrapped I don't have motivation for fix this things, because I decided to switch to Rust as my main language. Final notes - It is quite possible that I actually need attribute grammars or syntax-directed translation. I didn't explore this - I suspect that my parser is arrow transformer (whatever this means) Side note: I really want some pastebin for reproducible shell scripts (possibly dockerfiles), do you know such? Answer me if you have any questions. == Askar Safin http://safinaskar.com https://sr.ht/~safinaskar https://github.com/safinaskar

2 3

Help understanding John Hughes' "The Design of a Pretty-printing Library"
by Galaxy Being 10 Jul '21

10 Jul '21

Getting stuck in *Real World Haskell*'s chapter on pretty printing (chap 5), I decided to take a look at one of the suggested sources, i.e., John Hughes' *The Design of a Pretty-printing Library <https://www.researchgate.net/publication/226525714_The_Design_of_a_Pretty-p…>*. Not that I fully got the first three section, still, let me skip ahead to section 4, *Designing a Sequence Type *where we're designing a supposedly generic sequence type, I'm guessing in the same universal, fundamental way that Peano's Axioms give a generic underpinning of the natural numbers. Good. I get it. This is why Haskell is unique. So he says we take the following *signature* as our starting point nil :: Seq a unit :: a -> Seq a cat :: Seq a -> Seq a -> Seq a list :: Seq a -> [a] where nil , unit , and cat give us ways to build sequences, and list is an *observation *[explained before]. The correspondence with the usual list operations is nil = [] unit x = [x] cat = (++) These operations are to satisfy the following laws: xs `cat` ( ys `cat` zs ) = ( xs `cat` ys ) `cat` zs nil `cat` xs = xs xs `cat` nil = xs list nil = [] list ( unit x `cat` xs ) = x : list xs My first question is why must we satisfy these laws? Where did these laws come from? Is this a universal truth thing? I've heard the word *monoid *and *semigroup* tossed around. Is this germane here? Next in *4.1 Term Representation* I'm immediately lost with the concept of *term. *On a hunch, I borrowed a book *Term Rewriting and All That *from Baader and Nipkow which I'm sure goes very deep into the concept of terms, but I'm not there yet. What is meant by *term*? As 4.1 continues, confusing is this passage The most direct way to represent values of [the?] sequence type is just as terms of the algebra [huh?], for example using data Seq a = Nil j Unit a j Seq a `Cat` Seq a But this trivial representation does not exploit the algebraic laws that we know to hold [huh?], and moreover the list observation will be a little tricky to de ne (ideally we would like to implement observations by very simple, non-recursive functions: the real work should be done in the implementations of the Seq operators themselves). Instead, we may choose a restricted subset of terms -- call them simplified forms -- into which every term can be put using the algebraic laws. Then we can represent sequences using a datatype that represents the syntax of simplified forms. In this case, there is an obvious candidate for simplified forms: terms of the form nil and unit x `cat` xs , where xs is also in simplified form. Simplified forms can be represented using the type data Seq a = Nil j a `UnitCat` Seq a with the interpretation Nil = nil x `UnitCat` xs = unit x `cat` xs All of this presupposes much math lore that I'm hereby asking someone on this mailing list to point me towards. I threw in a few [huh?] as specific points, but in general, I'm not there yet. Any explanations appreciated. ⨽ Lawrence Bottorff Grand Marais, MN, USA borgauf(a)gmail.com

3 2

IFL'21 Third call for papers
by Pieter Koopman 09 Jul '21

09 Jul '21

================================================================================ IFL 2021 33rd Symposium on Implementation and Application of Functional Languages venue: online 1 - 3 September 2021 https://ifl21.cs.ru.nl <https://ifl21-publicity-dot-yamm-track.appspot.com/Redirect?ukey=1NdKhGOLpm…> ================================================================================ News - Paper submission details. - Registration information added Scope The goal of the IFL symposia is to bring together researchers actively engaged in the implementation and application of functional and function-based programming languages. IFL 2021 will be a venue for researchers to present and discuss new ideas and concepts, work in progress, and publication-ripe results related to the implementation and application of functional languages and function-based programming. Industrial track and topics of interest This year's edition of IFL explicitly solicits original work concerning *applications* of functional programming in industry and academia. These contributions will be reviewed by experts with an industrial background. Topics of interest to IFL include, but are not limited to: * language concepts * type systems, type checking, type inferencing * compilation techniques * staged compilation * run-time function specialisation * run-time code generation * partial evaluation * (abstract) interpretation * meta-programming * generic programming * automatic program generation * array processing * concurrent/parallel programming * concurrent/parallel program execution * embedded systems * web applications * (embedded) domain-specific languages * security * novel memory management techniques * run-time profiling performance measurements * debugging and tracing * testing and proofing * virtual/abstract machine architectures * validation, verification of functional programs * tools and programming techniques * applications of functional programming in the industry, including ** functional programming techniques for large applications ** successes of the application functional programming ** challenges for functional programming encountered ** any topic related to the application of functional programming that is interesting for the IFL community Post-symposium peer-review Following IFL tradition, IFL 2021 will use a post-symposium review process to produce the formal proceedings. Before the symposium authors submit draft papers. These draft papers will be screened by the program chairs to make sure that they are within the scope of IFL. The draft papers will be made available to all participants at the symposium. Each draft paper is presented by one of the authors at the symposium. After the symposium every presenter is invited to submit a full paper, incorporating feedback from discussions at the symposium. Work submitted to IFL may not be simultaneously submitted to other venues; submissions must adhere to ACM SIGPLAN's republication policy. The program committee will evaluate these submissions according to their correctness, novelty, originality, relevance, significance, and clarity, and will thereby determine whether the paper is accepted or rejected for the formal proceedings. We plan to publish these proceedings in the International Conference Proceedings Series of the ACM Digital Library, as in previous years. Moreover, the proceedings will also be made publicly available as open access. Important dates Submission deadline of draft papers: 17 August 2021 Notification of acceptance for presentation: 19 August 2021 Registration deadline: 30 August 2021 IFL Symposium: 1-3 September 2021 Submission of papers for proceedings: 6 December 2021 Notification of acceptance: 3 February 2022 Camera-ready version: 15 March 2022 Submission details All contributions must be written in English. Papers must use the ACM two columns conference format, which can be found at: http://www.acm.org/publications/proceedings-template <https://ifl21-publicity-dot-yamm-track.appspot.com/Redirect?ukey=1NdKhGOLpm…> . (For LaTeX users, start your document with \documentclass[format=sigconf]{acmart}.) Note that this format has a rather long but limited list of packages that can be used. Please make sure that your document adheres to this list. The submission Web page for IFL21 is https://easychair.org/conferences/?conf=ifl21 <https://ifl21-publicity-dot-yamm-track.appspot.com/Redirect?ukey=1NdKhGOLpm…> . Peter Landin Prize The Peter Landin Prize is awarded to the best paper presented at the symposium every year. The honoured article is selected by the program committee based on the submissions received for the formal review process. The prize carries a cash award equivalent to 150 Euros. Organisation IFL 2021 Chairs: Pieter Koopman and Peter Achten, Radboud University, The Netherlands IFL Publicity chair: Pieter Koopman, Radboud University, The Netherlands PC: Peter Achten (co-chair) - Radboud University, Netherlands Thomas van Binsbergen - University of Amsterdam, Netherlands Edwin Brady - University of St. Andrews, Scotland Laura Castro - University of A Coruña, Spain Youyou Cong - Tokyo Institute of Technology, Japan Olaf Chitil - University of Kent, England Andy Gill - University of Kansas, USA Clemens Grelck - University of Amsterdam, Netherlands John Hughes - Chalmers University, Sweden Pieter Koopman (co-chair) - Radboud University, Netherlands Cynthia Kop - Radboud University, Netherlands Jay McCarthey - University of Massachussetts Lowell, USA Neil Mitchell - Facebook, England Jan De Muijnck-Hughes - Glasgow University, Scotland Keiko Nakata - SAP Innovation Center Potsdam, Germany Jurriën Stutterheim - Standard Chartered, Singapore Simon Thompson - University of Kent, England Melinda Tóth - Eötvos Loránd University, Hungary Phil Trinder - Glasgow University, Scotland Meng Wang - University of Bristol, England Viktória Zsók - Eötvos Loránd University, Hungary Virtual symposium Because of the Covid-19 pandemic, this year IFL 2021 will be an online event, consisting of paper presentations, discussions and virtual social gatherings. Registered participants can take part from anywhere in the world. Registration Please use the below link to register for IFL 2021: https://docs.google.com/forms/d/e/1FAIpQLSdMFjo-GumKjk4i7szs7n4DhWqKt96t8of… <https://ifl21-publicity-dot-yamm-track.appspot.com/Redirect?ukey=1NdKhGOLpm…> Thanks to the sponsors and the support of the Radboud university registration is free of charge. [image: beacon]

1 0

Re: [Haskell-cafe] Where have the discussions moved to?
by Anthony Clayden 09 Jul '21

09 Jul '21

Yes I miss the free-and-easy atmosphere of the cafe. As of 9/10 years ago, we thought we'd nearly figured out how to fix the bogusness with FunDeps. And there were several ideas for better records. But no, GHC's FunDeps are just as bad as 2006; records have got a bit of lipstick. My take is that GHC has got so loaded with features, it's almost impossible to engineer in any 'tweaks'. So there has to be a bloated bureaucratic proposals process to make sure nothing gets broken. No free-wheeling what-if kind of discussion. Reddit I find almost impossible to follow. The Discourse site seems to be too much cut-and-dried. If you want to peek at what code people are cutting, StackOverflow gets some surprising material. But yeah. Haskell is different these days. In a way I don't like. It doesn't feel like 'popularity and community has expanded'. AntC

1 0

Re: [Haskell-cafe] Prolog-style list syntax?
by Anthony Clayden 09 Jul '21

09 Jul '21

Ok thank you for the feedback, I get the message not to re-purpose currently valid syntax. For that reason, this won't fly: I see no technical issues in allowing > something like `[ x, y || ys]` `||` is already an operator in the Prelude. > [x, y ,: ys ] -- ? not currently valid We could make list syntax work harder > [x, y ,:+ ys ] Means desugar the commas by applying constructor `:+` instead of `:`. That could be in general any constructor starting `:`. Or indeed could be a pattern synonym starting `:`, which is a 'smart constructor' to build the list maintaining some invariant.

3 4