- Haskell-Cafe - Haskell.org

Workshop on Logic Programming: Trends, Extensions, Applications, 28-29 May 2020
by Ekaterina Komendantskaya 19 May '20

19 May '20

We invite participants to the on-line workshop on * Trends, Extensions, Applications and Semantics of Logic Programming* Logic programming is a framework for expressing programs, propositions and relations as Horn clause theories, and for automatic inference in these theories. Horn clause theories are famous for their well-understood declarative semantics, in which models of logic programs are given inductively or coinductively. At the same time, Horn clauses give rise to efficient inference procedures, usually involving resolution. Logic programming found applications in type inference, verification, and AI. While logic programming was originally conceived for describing simple propositional facts, it was extended to account for much more complex theories. This includes first-order theories, higher-order theories, inductive and coinductive data, and stochastic/probabilistic theories. The aim of this workshop is to bring together researchers that work on extensions of logic programming and inference methods, and to foster an exchange of methods and applications that have emerged in different communities. Keynote talk: *Dale Miller*. Structural Proof-Theory and Logic Programming <https://www.coalg.org/tease-lp/2020/dale-miller-structural-proof-theory-and…> Invited tutorial: *Uli Sattler*.* Description Logics and Ontology Languages - an introduction and overview* In light of COVID-19, we organise TEASE-LP as a virtual workshop and online-only event. To achieve broad participation, we use three different mediums: Discussion Forum, Pre-recorded lightning talks, Live sessions with invited and contributed live talks. Further details can be found here: https://www.coalg.org/tease-lp/workshop-schedule/. Registration is free, but we require all participants to register at https://teaselp.flarum.cloud/ For any further queries, please contact the organisers: Henning Basold <henning(a)basold.eu> Katya Komendantskaya <ek19(a)hw.ac.uk>

1 0

tuple and pattern synonym
by Kazu Yamamoto 18 May '20

18 May '20

Hi, I have a question about PatternSynonyms. Suppose we have: data Foo = Foo Int Int I would like to define a pattern as follows: pattern P :: (Int,Int) -> Foo pattern P (x,y) = Foo x y But this results in "parse error on input ‘(’". Are there any ways to use tuple in the left side hand of patterns? This is important to maintain backward compatibility for the "network" library. If there is no way, I will define Foo as: data Foo = Foo (Int,Int) -- awkward and define P as: pattern P :: (Int,Int) -> Foo pattern P xy = Foo xy Regards, --Kazu

3 4

Re: [Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
by Olaf Klinke 18 May '20

18 May '20

> You're misplacing your quantifiers. > > (a -> Void) -> Void) > > is not isomorphic to > > forall r. (a -> r) -> r > > but *is* isomorphic to > > (a -> (forall r. r)) -> (forall r. r) > ...which is because you could _define_ Void to be (forall r. r): {-# LANGUAGE Rank2Types #-} newtype Void = Void {absurd :: forall r. r} In practice, Void used to be implemented as data Void = Void Void before it became just data Void by means of EmptyDataDecls extension. The latter has the advantage that there is no constructor named 'Void'. In reality of course, Void does have an element, bottom, which it shares with all other types. Hence the 'absurd' function that returns the bottom in type r when given the bottom in type Void. But as you know the correspondence between types and theorems in intuitionistic logic explicitly regards only total values. Excersise: Prove that intuitionistically, it is absurd to deny the law of excluded middle: Not (Not (Either a (Not a))) There is a whole world to be discovered beneath the total values. Think about the type () as truth values and what universal quantification could be. Olaf

7 10

Re: [Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
by Olaf Klinke 17 May '20

17 May '20

> 2. Double negation enables a translation of classical logic in > intuitionistic logic, here embedded in Haskell: > Below I'll give a variant of Li-yao's logic language in Haskell98. Again, the open set model may help to visualize CPS translation: Consider all open sets A on the real line which are fixed points of double negation. All intervals are of this kind, but poking holes in them destroys this property: ---(====)(====)--- A ===)----------(=== Not A ---(==========)--- Not (Not A) Denote the collection of open sets invariant under double negation by X. As the example above demonstrates, X is not closed under set union. But set intersection preserves membership of X. So we have a funny logic that has (&&) but no (||). The CPS trick is now to define a new (||) by means of double negation: ---(====)--------- A ---------(====)--- B ---(====)(====)--- set union of A and B ---(==========)--- A || B, double negation of set union. In fact X is the largest Boolean algebra contained in the Heyting algebra of open sets. In terms of Haskell, we define a new Either: Either' a b = ((Either a b) -> Void) -> Void Looks familiar? Indeed, in this thread we already proved Either' a (Not a). This says that Not A is the Boolean complement of A in X. Using (,) and Either' for (&&) and (||) you can realize all proofs of classical propositional logic in Haskell without GADTs. Olaf

2 1

Re: [Haskell-cafe] Decorating exceptions with backtrace information
by Carter Schonwald 15 May '20

15 May '20

On Fri, May 8, 2020 at 9:32 AM Carter Schonwald <carter.schonwald(a)gmail.com> wrote: > ben, could you please email the libraries list with this too? This seems > like a core libraries / base change rather than a ghc-the-compiler change > > On Thu, May 7, 2020 at 6:57 PM Michael Sloan <mgsloan(a)gmail.com> wrote: > >> Thanks so much for making a proposal for this, Ben!! It's great to see >> progress here. >> >> I'm also glad that there is now a proposal process. I made a fairly >> similar proposal almost exactly 5 years ago to the libraries list - >> https://mail.haskell.org/pipermail/libraries/2015-April/025471.html - >> but without the subtlety of particular backtrace representations. Skimming >> the ensuing thread may still be informative. >> >> In particular, there is one thing I would like to highlight from that old >> proposal. I think it'd be good to have a standard way to represent a chain >> of exceptions, and build this into `catch` and `finally`. Python and Java >> both have a mechanism for this, and both refer to it as a "cause" >> exception. When an exception is thrown during exception handling, the >> exception being handled is preserved as its "cause". I find this mechanism >> to be incredibly useful in Java, it has made the underlying issue much >> clearer in many cases, and in other cases at least provides helpful >> context. I have no doubt such a mechanism would have saved me many hours >> of debugging exceptions in Haskell systems I've worked on in the past. >> >> I considered commenting about that directly on the proposal, but I figure >> this is a better place to suggest expanding the scope of the change :) . >> Totally understandable if you want to keep this proposal focused on >> stacktraces, but I think it'd be good to consider this as a potential >> future improvement. >> >> -Michael >> >> On Thu, May 7, 2020 at 3:55 PM Ben Gamari <ben(a)well-typed.com> wrote: >> >>> >>> Hi everyone, >>> >>> After a nice discussion on IRC about the unfortunate state of error >>> reporting in Haskell, I felt compelled to write down some long-lingering >>> thoughts regarding backtraces on exceptions. The result is GHC proposal >>> #330 [1]. I think the approach is viable and perhaps even >>> straightforward. I have the sketch of an implementation here [2]. >>> >>> Please have a look at the proposal and leave your comments. If there is >>> consensus it is possible that we could have this done for 8.12. >>> >>> Cheers, >>> >>> - Ben >>> >>> >>> [1] https://github.com/ghc-proposals/ghc-proposals/pull/330 >>> [2] https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3236 >>> _______________________________________________ >>> ghc-devs mailing list >>> ghc-devs(a)haskell.org >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs(a)haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >

7 15

CFP: GPCE 2020 − 19th International Conference on Generative Programming: Concepts & Experiences
by Erwan BOUSSE 13 May '20

13 May '20

----------------------------------------------------------------------- GPCE 2020: 19th International Conference on Generative Programming: Concepts & Experiences November 16-17, 2020 Chicago, IL (USA) (a part of the SPLASH series of conferences) https://conf.researchr.org/home/gpce-2020 ----------------------------------------------------------------------- --------------------------- CALL FOR PAPERS --------------------------- The ACM SIGPLAN International Conference on Generative Programming: Concepts & Experiences is a programming languages conference focusing on techniques and tools for code generation, language implementation, and product-line development. GPCE seeks conceptual, theoretical, empirical, and technical contributions to its topics of interest, which include but are not limited to: program transformation, staging, macro systems, preprocessors, program synthesis, and code-recommendation systems, domain-specific languages, language embedding, language design, and language workbenches, feature-oriented programming, domain engineering, and feature interactions, applications and properties of code generation, language implementation, and product-line development. Authors are welcome to check with the PC chair whether their planned papers are in scope. --------------------------- IMPORTANT DATES --------------------------- - Abstract submission: July 20, 2020 (Monday), AoE - Paper submission: July 27, 2020 (Monday), AoE - Author notification: September 9, 2020 (Wednesday) - Conference: November 16-17, 2020 --------------------------- PAPER SELECTION --------------------------- The GPCE program committee will evaluate each submission according to the following selection criteria: - Novelty. Papers must present new ideas or evidence and place them appropriately within the context established by previous research in the field. - Significance. The results in the paper must have the potential to add to the state of the art or practice in significant ways. - Evidence. The paper must present evidence supporting its claims. Examples of evidence include formalizations and proofs, implemented systems, experimental results, statistical analyses, and case studies. - Clarity. The paper must present its contributions and results clearly. --------------------------- PAPER CATEGORIES --------------------------- GPCE solicits three kinds of submissions: - Full Papers reporting original and unpublished results of research that contribute to scientific knowledge in any GPCE topic listed above. Full paper submissions must not exceed 12 pages excluding bibliography. - Short Papers presenting unconventional ideas or visions about any GPCE topic listed above. Short papers do not always require complete results as in the case of a full paper. In this way, authors can introduce new ideas to the community and get early feedback. Please note that short papers are not intended to be position statements. Short papers are included in the proceedings and will be presented at the conference. Short paper submissions must not exceed 6 pages excluding bibliography. Short papers must have the text “(Short Paper)” appended to their title, though any papers of 6 or fewer pages that are not tool demonstration papers will be considered as short papers. - Tool Demonstrations presenting tools for any GPCE topic listed above. Tools must be available for use and must not be purely commercial. Submissions must provide a tool description not exceeding 6 pages excluding bibliography and a separate demonstration outline including screenshots also not exceeding 6 pages. Tool demonstrations must have the keywords “Tool Demo” or “Tool Demonstration” appended in their title. If the submission is accepted, the tool description will be published in the proceedings. The demonstration outline will only be used by the program committee for evaluating the submission. --------------------------- PAPER SUBMISSION --------------------------- All submissions must use the ACM SIGPLAN Conference Format “acmart” (http://sigplan.org/Resources/Author/#acmart-format) Please be sure to use the latest LaTeX templates and class files. the SIGPLAN sub-format, and 10 point font. Consult the sample-sigplan.tex template and use the document-class \documentclass[sigplan,anonymous,review]{acmart}. Please do not make any changes to this format! To increase fairness in reviewing, a double-blind review process has become standard across SIGPLAN conferences. GPCE will follow a very lightweight model, where author identities are revealed to reviewers after submitting their initial reviews. Hence, the purpose is not to conceal author identities at all cost, but merely to provide reviewers with an unbiased first look at a submission. Author names and institutions should be omitted from submitted papers, and references to the authors’ own related work should be in the third person. No other changes are necessary, and authors will not be penalized if reviewers are able to infer their identities in implicit ways. Papers must be submitted using HotCRP: https://gpce2020.hotcrp.com/ The official publication date is the date the proceedings are made available in the ACM Digital Library. Papers must describe work not currently submitted for publication elsewhere as described by the SIGPLAN Republication Policy (http://www.sigplan.org/Resources/Policies/Republication/) --------------------------- ORGANIZATION --------------------------- - Steering Committee Chair: Ulrik Pagh Schultz (Denmark) - General Chair: Martin Erwig (USA) - Program Chair: Jeff Gray (USA) - Publicity Chair: Erwan Bousse (France) For additional information, clarification, or answers to questions please contact the program chair at gray(a)cs.ua.edu --------------------------- PROGRAM COMMITTEE --------------------------- - Juliana Alves Pereira (Brazil) - Ira Baxter (USA) - Don Batory (USA) - Sandrine Blazy (France) - Sheng Chen (USA) - Shigeru Chiba (Japan) - Thomas Degueule (France) - Robert Glück (Denmark) - Aniruddha Gokhale (USA) - Elisa Gonzalez Boix (Belgium) - Julia Lawall (France) - Geoffrey Mainland (USA) - Marjan Mernik (Slovenia) - Bruno Oliveira (Hong Kong) - Alex Potanin (New Zealand) - Suman Roychoudhury (India) - Christoph Seidl (Denmark) - Michel Steuwer (UK) - Eli Tilevich (USA) - Naoyasu Ubayashi (Japan) - Tijs van der Storm (Netherlands) - Vadim Zaytsev (Netherlands)

1 0

Way to prevent a value from being garbage collected too early
by YueCompl 13 May '20

13 May '20

Folks, I need a little help, I remember I had read some where that, there's a function to fake a use of a value, so it won't be garbage collected too early, as GHC has an optimization to forget a value as early as possible. But I can't remember the function name or even the keyword to google it out, hint me please! Best regards, Compl

5 5

Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
by Ruben Astudillo 13 May '20

13 May '20

Hello cafe I've been doing some basic logic exercises on Haskell the last few days. Along the way I learned about intuitionistic logic and double negation. On STLC types are propositions and terms of those types are proofs of those propositions. The standard way to negate a proposition/type ~A~ in Haskell is via the type type Not a = a -> Void So far so good. On classical logic we have an equivalence between a proposition and it's double negation. On intuitionistic logic I only have a single implication that ~forall a. a -> Not (Not a)~, this is easy to see as we have the proof/term proof :: forall a. a -> Not (Not a) proof a = \cont -> cont a But we don't have the implication between ~forall a. Not (Not a) -> a~, there is no way to obtain an ~a~ from the void continuations. Worse than that, to even use such continuation I would need to have an ~a~ already. On blogposts I've seen the claim that the types ~Void~ and ~forall a. a~ are almost the same. I can see the second one only has bottom as a term. H98 versions of Void also had that term. The curious fact is that people treat them as if they were the same without questioning. But they are not the same, we can see this as there is an implication ~(forall r. (a -> r) -> r) -> a~ given by the proof proof1 :: forall a. (forall r. (a -> r) -> r) -> a proof1 cont = cont id That leads me to believe that given that ~(forall r. (a -> r) -> r)~ and ~(a -> Void) -> Void)~ are not obviously the same, the relationship between ~Void~ and ~forall a. a~ is not as people say. So cafe, how can I reconcile these facts? -- -- Rubén -- pgp: 4EE9 28F7 932E F4AD

2 1

ML Family Workshop 2020: Deadline extension
by Leo White 13 May '20

13 May '20

Due to the COVID-19 pandemic, ML 2020 will take place online. The submission deadline has been extended to the end of the month to accommodate for the change in situation. ============================================================= We are happy to invite submissions to the ML Family Workshop 2020, to be held during the ICFP conference week on Thursday, August 27th. The ML family workshop warmly welcomes submission touching on the programming languages traditionally seen as part of the "ML family" (Standard ML, OCaml, F#, CakeML, SML#, Manticore, MetaOCaml, etc.). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. We also encourage presentations from related languages (such as Haskell, Scala, Rust, Nemerle, Links, Koka, F*, Eff, ATS, etc), to exchange experience of further developing ML ideas. Due to the COVID-19 pandemic, the workshop will take place online. See our detailed CFP online on the ICFP website: https://icfp20.sigplan.org/home/mlfamilyworkshop-2020 Important dates --------------- - Friday 29th May (any time zone): Abstract submission deadline - Friday 17th July: Author notification - Thursday 27th August: ML Family Workshop Program committee ----------------- - Youyou Cong (Tokyo Institute of Technology) - Ivan Gotovchits (Carnegie Mellon University) - Gowtham Kaki (Purdue University) - Neel Krishnaswami (University of Cambridge) - Daan Leijen (Microsoft Research) - Koko Muroya (Kyoto University) - Atsushi Ohori (Tohoku University) - Jonathan Protzenko (Microsoft Research) - Gabriel Radanne (INRIA) - Claudio Russo (Dfinity) - Leo White (Jane Street) (Chair) - Jeremy Yallop (University of Cambridge) Submission details ------------------ See the online CFP for the details on the expected submission format. Submissions must be uploaded to the workshop submission website https://ml2020.hotcrp.com/ before the submission deadline.

1 0

Re: [Haskell-cafe] When did it become so hard to install Haskell on Windows?
by Gershom B 12 May '20

12 May '20

On May 11, 2020 at 10:52:36 AM, Michal J Gajda (mgajda(a)mimuw.edu.pl) wrote: > 3. To enter relevant command line in admin PowerShell so that Chocolatey installs GHC. > 4. Ditto for Mingw (3 attempts, since I think default Mingw package lacks full build environment.) > 4. Ditto for every dependency of my Haskell package. (Is there a way to get standardized library dependencies across the platforms? Drop me a line if it is at all possible without Nix.) I’m confused. When you used chocolatey, why did you not run “choco install haskell-dev” as suggested on https://www.haskell.org/platform/#windows (and i imagine everywhere else)? This should have installed ghc, msys2 and cabal for you at once. Further what do you mean "Ditto for every dependency of my Haskell package” — do you mean haskell dependencies or c dependencies? If the latter, how is this different than any other OS? Also, why were you installing c dependencies with chocolatey, if that’s indeed what you were doing? With msys2 the way to do things is install them with pacman. Perhaps what is needed is just better and more centralized documentation? -g

2 1