- Haskell-Cafe - Haskell.org

[Lambda Days + TFP + TFPIE 2021] call for participation
by Peter Achten 22 Jan '21

22 Jan '21

------------------------------------------------------------------------------- C A L L F O R P A R T I C I P A T I O N 8th Lambda Days + 10th International Workshop on Trends in Functional Programming in Education + 22nd Symposium on Trends in Functional Programming 16 - 19 February 2021 https://www.lambdadays.org/lambdadays2021 ------------------------------------------------------------------------------- The programmes for Lambda Days, TFPIE, and TFP are online: - Lambda Days overall program at: https://www.lambdadays.org/lambdadays2021 - TFPIE specific program at: https://wiki.tfpie.science.ru.nl/TFPIE2021 - TFP specific program at: http://tfp2021.org/ (all times are in Central European Time Zone: 12.00:18.00 (CEST)) Lambda Days is a place where academia meets industry, where research and practical application collide. Once again Lambda Days joins forces with Trends in Functional Programming (TFP) and Trends in Functional Programming in Education (TFPiE) so that for four days you can be at the centre of the functional programming world. The program has a lot of interesting talks, possibilities for interaction, and a host of keynote presentations: Lambda Days keynote speakers: ----------------------------- Perdita Stevens, Pat Hannahan, Simon Peyton Jones, Andy Gordon, Philip Wadler. Trends in Functional Programming in Education keynote speakers: --------------------------------------------------------------- Francesco Cesarini, Simon Thompson, and Bartosz Milewski. Trends in Functional Programming keynote speaker: ------------------------------------------------- Zhenjiang Hu. Thanks to a generous sponsor, TFP has a limited number of free tickets for PhD, Msc, Bsc students with an interest in functional programming. To apply, send a mail to the program chair of TFP, Viktória Zsók (zsv(a)elte.hu) with your name, university, 2-3 lines of motivation, and a valid student card photo to get the registration code. Tickets will be delivered in the order of application.

1 0

Munich Virtual Haskell Meeting, 2021-01-25 @ 19:30
by Leah Neukirchen 22 Jan '21

22 Jan '21

Dear all, Next week, our monthly Munich Haskell Meeting will take place again on Monday, January 25 on Google Meet. For details see here: **Due to meetup limitations in Bavaria, this meeting will take place online!** For details see here: http://muenchen.haskell.bayern/dates.html A Google Meet link to join the room is provided on the page. Everybody is welcome, especially the Haskellers from Bavaria that do not usually come to our Munich meetings due to travel distance! cu, -- Leah Neukirchen <leah(a)vuxu.org> https://leahneukirchen.org/

1 0

stack: duplicate modules in library
by Chris Reade 22 Jan '21

22 Jan '21

I have come across a problem with haskell stack putting duplicate modules in a library. On "stack build" I get "Cabal-simple_mPHDZzAJ_3.0.1.0_ghc-8.8.4: Duplicate modules in library:..” This may have originally been caused when I changed capitalisation of a filename, but changing back did not resolve the problem. My question is how do I get rid of the library so I can rebuild? I tried "stack purge” and also removing ~/.stack with no luck (the latter causes a new ghc download on stack build, but with the same message afterwards) I know the source modules are fine because they all load in "stack ghci” Is there some other directory that stack/cabal uses for binary cache that I can safely delete? Chris

2 1

Bind the GAP barely legible?
by Viktor Dukhovni 20 Jan '21

20 Jan '21

I tried to read "Bind the GAP": https://bindthegap.news/issues.html but the colours, fonts, and layout are so disorienting that I'm afraid it is just too much work to make much sense of it. Am I just too old-fashioned in my expectations, or do others alos find that the festive artwork completely overwhelms the content in this publication? If there's anyone on this list who's involved in producing the publication, please consider drastically dialing back the decorations. -- Viktor.

10 10

Time to vote on possible haskell-language-server logos
by Alan & Kim Zimmerman 19 Jan '21

19 Jan '21

As we announced in December last year, we are looking for a logo for the haskell language server. We now have a selection of candidates, and the voting is open [1] You can vote for as many options as you like. We are closing the poll on 26 Jan (a week from now). Make your preference known, you will hopefully be seeing it a *lot*. Alan [1] https://github.com/haskell/haskell-language-server/issues/694#issuecomment-…

1 0

2nd Call for Participation: BOB 2021 (February 26, online)
by Stefan Wehr 11 Jan '21

11 Jan '21

================================================================================ BOB 2021 Conference “What happens if we simply use what’s best?” February 26, 2021, online (UTC+0100) http://bobkonf.de/2021/ Program: http://bobkonf.de/2021/program.html Registration: http://bobkonf.de/2021/registration.html ================================================================================ BOB conference is a place for developers, architects and decision-makers to explore technologies beyond the mainstream in software development, and to find the best tools available to software developers today. Our goal is for all participants of BOB to return home with new insights that enable them to improve their own software development experience. The program features 14 talks and 8 tutorials on current topics: http://bobkonf.de/2021/program.html The subject range includes functional programming, logic programming, revision control, formal methods, mindfulness, event sourcing, front-end development, and more. Jeremy Gibbons will give the keynote talk. BOB 2021 will take place online. We are working towards fostering lively exchange of exciting ideas and enable meaningful social interactions. Registration is open online: http://bobkonf.de/2021/registration.html Registration is €30 for a regular ticket, €15 for a student ticket. (If you need financial aid, let us know.) We intend to make this the most diverse, colorful, fun BOB ever!

1 0

Re: [Haskell-cafe] A quick question about distribution of finite maps.
by Olaf Klinke 10 Jan '21

10 Jan '21

> Hello! > > Finite maps from `"containers" Data.Map` look like they may form a > Cartesian closed category. So it makes sense to ask if the rule _α ⇸ > (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds in such > categories does hold for finite maps. Note that, a map being a > functor, this also may be seen as _f (g α) ≡ g (f α)_, which would > work if maps were `Distributive` [1]. > > It looks to me as though the following definition might work: > > distribute = unionsWith union . mapWithKey (fmap . singleton) > > — And it works on simple examples. _(I checked the law `distribute ∘ > distribute ≡ id` — it appears to be the only law required.)_ > > Is this definition correct? Is it already known and defined > elsewhere? > > [1]: > https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distribu… Hi Ignat, TL;DR: No and no. The documentation says that every distributive functor is of the form (->) x for some x, and (Map a) is not like this. If Maps were a category, what is the identity morphism? Let's put the Ord constraint on the keys aside, Tom Smeding has already commented on that. Next, a Map is always finite, hence let's pretend that we are working inside the category of finite types and functions. Then the problems of missing identity and missing Ord go away. Once that all types are finite, we can assume an enumerator. That is, each type x has an operation enumerate :: [x] which we will use to construct the inverse of flip Map.lookup :: Map a b -> a -> Maybe b thereby showing that a Map is nothing but a memoized version of a Kleisli map (a -> Maybe b). Convince yourself that Map concatenation has the same semantics as Kleisli composition (<=<). Given a Kleisli map k between finite types, we build a Map as follows. \k -> Map.fromList (enumerate >>= (\a -> maybe [] (pure.(,) a) (k a))) With that knowledge, we can answer your question by deciding: Is the Kleisli category of the Maybe monad on finite types Cartesian closed? Short answer: It is not even Cartesian. There is an adjunction between the categories (->) and (Kleisli m) for every monad m, where * The left adjoint functor takes types x to x, functions f to return.f * The right adjoint functor takes types x to m x, Kleisli maps f to (=<<) f Right adjoint functors preserve all existing limits, which includes products. Therefore, if (Kleisli m) has binary products, then m must preserve them. So if P x y was the product of x and y in Kleisli m, then m (P x y) would be isomorphic to (m x,m y). This seems not to hold for m = Maybe: I can not imagine a type constructor P where Maybe (P x y) ~ (Maybe x,Maybe y). In particular, P can not be (,). The only sensible Kleisli projections from (x,y) would be fst' = return.fst and snd' = return.snd. Now think of two Kleisli maps f :: Bool -> Maybe x, g :: Bool -> Maybe y. Assume that f True = Just x for some x and g True = Nothing. In order to satisfy g True = (snd' <=< (f&&&g))True, the unique pair arrow (f&&&g) would need to map True to Nothing, but then f True = (fst' <=< (f&&&g)) True can not hold. We conclude that (Kleisli Maybe) does not even have categorical products, so asking for Cartesian closure does not make sense. You might ask for a weaker property: For every type x, ((,) x) is a functor on (Kleisli Maybe). Indeed, the following works because ((,) x) is a polynomial functor. fmapKleisli :: Functor m => (a -> m b) -> (x,a) -> m (x,b) fmapKleisli f (x,a) = fmap ((,) x) (f a) Thus you may ask whether this functor has a right adjoint in the Kleisli category of Maybe. This would be a type constructor g with a natural isomorphism (x,a) -> Maybe b ~ a -> Maybe (g b). The first thing that comes to mind is to try g b = x -> Maybe b and indeed djinn can provide two functions going back and forth that have the right type, but they do not establish an isomorphism. I doubt there is such a right adjoint g, but can not prove it at the moment. The idea is that a function (x,a) -> Maybe b may decide for Nothing depending on both x and a, and therefore the image function under the isomorphism must map every a to Just (g b) and delay the Nothing-decision to the g b. But for the reverse isomorphism you can have functions that do not always return Just (g b) and there is no preimage for these. Regards, Olaf

5 16

A quick question about distribution of finite maps.
by Ignat Insarov 10 Jan '21

10 Jan '21

Hello! Finite maps from `"containers" Data.Map` look like they may form a Cartesian closed category. So it makes sense to ask if the rule _α ⇸ (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds in such categories does hold for finite maps. Note that, a map being a functor, this also may be seen as _f (g α) ≡ g (f α)_, which would work if maps were `Distributive` [1]. It looks to me as though the following definition might work: distribute = unionsWith union . mapWithKey (fmap . singleton) — And it works on simple examples. _(I checked the law `distribute ∘ distribute ≡ id` — it appears to be the only law required.)_ Is this definition correct? Is it already known and defined elsewhere? [1]: https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distribu…

4 7

GHC / macports / Big Sur
by Sean Matthews 09 Jan '21

09 Jan '21

It may be that someone has already asked this question, but I am having a problem (= it does not work) installing GHC using macports. Pure vanilla Mac/macports, with a few standard installed packages, but deliberately as few manual interventions as possible. Does the group have any advice? Thanks, Sean Matthews PS this is what macports says: r.packages.macports.org/stack ---> Attempting to fetch stack-2.5.1_0.darwin_20.x86_64.tbz2 from https://cph.dk.packages.macports.org/stack ---> Building stack Error: Failed to build stack: command execution failed Error: See /opt/local/var/macports/logs/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_stack/stack/main.log for details. Error: Follow https://guide.macports.org/#project.tickets to report a bug. Error: Processing of port ghc failed ---> Some of the ports you installed have notes: pinentry-mac has the following notes: If you previously didn't have pinentry or gpg-agent installed and pinentry-mac has been installed as a dependency of gpg-agent, you don't need to do anything to use pinentry-mac. If you want to switch to the GTK2, ncurses or Qt4 based pinentry program, please install pinentry with the correct use flags and follow the instructions below substituting the pinentry-mac program path with /opt/local/bin/pinentry. If you previously had pinentry and gpg-agent installed and would like to switch to pinentry-mac, you will have to set it as your pinentry program in $HOME/.gnupg/gpg-agent.conf. Add the following line to the mentioned file: pinentry-program /Applications/MacPorts/pinentry-mac.app/Contents/MacOS/pinentry-mac Be sure to comment previous "pinentry-program" lines, for example: pinentry-program SAMPLE becomes #pinentry-program SAMPLE Afterwards, run killall -HUP gpg-agent or simply log out and back in again. -- Sean Matthews seanmatthews1(a)gmail.com / +49 163 803 1396

2 1

F-IDE 2021 - 2nd Call for Papers
by Andrei Paskevich 08 Jan '21

08 Jan '21

****************************************************************** F-IDE 2021: 6th Workshop on Formal Integrated Development Environment Affiliated with NASA Formal Methods 2021 May 24-25, 2021 -- held online https://cister-labs.pt/f-ide2021 ****************************************************************** Keynotes * Prof. Jan Friso Groote, Eindhoven Univ. of Technology, the Netherlands * Benoît Rognier, Edukera, France Important Dates * Abstract submission: Mon, Feb 22, 2021 * Full paper submission: Mon, Mar 1, 2021 * Notification: Mon, Apr 19, 2021 * Camera-ready: Mon, May 3, 2021 * Workshop: May 24-25, 2021 Overview High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language and/or an environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. Topics The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques, and experiments. Topics of interest include, but are not limited to, the following: * F-IDE building: design and integration of languages, development of user-friendly front-ends * How to make high-level logical and programming concepts palatable to industrial developers * Integration of object-oriented and modularity features * Integration of static analyzers * Integration of automated proof tools, theorem provers, and testing tools * Documentation tools * Impact of tools on certification * Experience reports on developing F-IDEs * Experience reports on using F-IDEs * Experience reports on formal methods-based assessments in industrial applications Submission Guidelines We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers must be written in English and follow the EPTCS LaTeX format (http://style.eptcs.org) Authors are invited to submit the following types of contributions: * Research papers providing new concepts and results * Experience reports * Position papers and research perspectives * Tool presentations Papers should be submitted via EasyChair at F-IDE 2021's workshop page: https://easychair.org/conferences/?conf=f-ide2021. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Program Committee * Andrew Reynolds, University of Iowa, USA * Damien Doligez, Inria, France * Bernhard Rumpe, RWTH Aachen University, Germany * Carlo A. Furia, Chalmers University of Technology, Sweden * César Muñoz, NASA Langley, USA * Cinzia Bernardeschi, University of Pisa, Italy * Claudio Sacerdoti Coen, University of Bologna, Italy * Enrico Tassi, Inria, France * François Pessaux, ENSTA ParisTech, France * José Creissac Campos, University of Minho, Portugal * Kenneth Lausdahl, Aarhus University, Denmark * Laurent Voisin, Systerel, France * Lucas Wagner, Collins Aerospace, USA * Makarius Wenzel, sketis.net * Markus A. Kuppe, Microsoft Research, USA * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Pierre-Yves Strub, LIX, École Polytechnique, France * Rosemary Monahan, Maynooth University, Ireland * Silvia Lizeth Tapia Tarifa, University of Oslo, Norway * Simão Melo de Sousa, Universidade Beira Interior, Portugal * Stefan Mitsch, Carnegie Mellon University, USA * Stephan Merz, Inria, France * Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay, France * Yannick Moy, AdaCore, France * Yi Zhang, Massachusetts General Hospital, USA PC Chairs * Andrei Paskevich, Université Paris-Saclay, France * José Proença, CISTER/ISEP, Portugal Steering Committee * Catherine Dubois, Samovar, ENSIIE, France * Paolo Masci, US National Institute of Aerospace (NIA), USA * Dominique Méry, LORIA, Université de Lorraine, France

1 0