- Haskell-Cafe - Haskell.org

PhD or Postdoc Position at LMU Munich about Verified Modal Logics
by Andrei Popescu 10 Mar '23

10 Mar '23

We are looking for a PhD student (4 years) or postdoctoral researcher (3 years) to work on the Isabelle formalization of modal model theory. The work will take place within the Chair of Theoretical Computer Science at LMU Munich under Jasmin Blanchette's supervision with the participation of two external experts: Cláudia Nalon (University of Brasília) and Sophie Tourret (Inria Nancy). Modal logics are extensions of classical logics with operators that allow for the qualification of truth. Model theory for modal logics is concerned with the interplay between the language (syntax, i.e., the set of its formulas) and its meaning (semantics, i.e., the structures over which the language is interpreted). There are, however, different ways of characterizing meaning for modal sentences and also several (well-established) results that allow for restriction on the sets of structures being considered. This project concerns the formalization in Isabelle of those results for general Kripke structures for generalized modal operators (i.e., of any arity). The goal is to produce a library that could then be used (and possibly extended) for specific applications, in particular those related to proof theory. The position is categorized as TV-L E13 according to the German salary scale. It includes some teaching obligations. The starting date is flexible. Please contact Jasmin Blanchette (jasmin.blanchette(a)ifi.lmu.de) for more information or if you want to apply. The application deadline is 15 April 2023.

1 0

Alpha Release of Keelung, the New Haskell DSL Designed for Secure and Fast Application Development
by Ting Wang 09 Mar '23

09 Mar '23

Hello developers, I'm Ting with BTQ. We are thrilled to announce the alpha release of Keelung, a new domain-specific language (DSL) designed to make fast, private, and secure application development easy for developers.Both Keelung and its compiler have been implemented in Haskell, enabling you to produce high-level zero-knowledge proofs protected by Haskell's cutting-edge type system while leveraging Haskell's extensive ecosystem and tooling. What's more, Keelung will be 100% open-source, aligning with our values of transparency, collaboration, and community-driven development.Check out our blog post <https://www.btq.com/en/blog/keelung-alpha-release> of Keelung alpha release for more detail. If you're interested in using Keelung to build privacy-preserving applications, please visit our GitHub repository <https://github.com/btq-ag/keelung> and Hackage <https://hackage.haskell.org/package/keelung>. Our documentation <https://btq.gitbook.io/keelung/> also provides detailed information on how to use Keelung, including installation instructions, examples, and tutorials.If you have any questions about Keelung or would like to contribute to the project, please start a thread on our GitHub discussions <https://github.com/btq-ag/keelung/discussions> page or reach out to us via email at desk(a)btq.li. We're always happy to help and would love to hear from you!Thank you and we can't wait to see what you build with it! Ting Wang (Ms.) Product Manager ty.wang(a)btq.li www.btq.com [image: twitter] <https://twitter.com/btq_ag> [image: linkedin] <https://www.linkedin.com/company/btqag/about/>

1 0

[ANN] Copilot 3.14
by Ivan Perez 08 Mar '23

08 Mar '23

(Apologies if you see this through multiple channels.) Hi everyone, I’m very excited to announce Copilot 3.14. Copilot is a stream-based EDSL in Haskell for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms. Copilot has been used at NASA in drone test flights. Through the NASA tool Ogma [1] (also written in Haskell), Copilot also serves as a runtime monitoring backend for the requirements elicitation tool FRET [4], and can target NASA’s Core Flight System and the Robot Operating System (ROS2) applications. This new version provides up-to-date compiler support, simplifies the API, and improves the documentation. For details, see [2]. As always, we’re releasing exactly 2 months since the last release. Our next release is scheduled for May 7th, 2023. We have almost completed the C99 unit tests, and plan to include those in the next version. Copilot is currently undergoing the qualification process necessary for NASA Class D Software. Current emphasis is on increasing test coverage, removing unnecessary dependencies, hiding internal definitions, and formatting the code to meet our new coding standards. Users are encouraged to participate by opening issues and asking questions via our github repo [3] There’s been many more updates on the Copilot front in the last few months. We’ll be able to announce more soon. Stay tuned. Happy Haskelling! Ivan [1] https://github.com/nasa/ogma [2] https://github.com/Copilot-Language/copilot/releases/tag/v3.14 [3] https://github.com/Copilot-Language/copilot [4] https://github.com/NASA-SW-VnV/fret

1 0

Call for Talks: Haskell Implementors' Workshop 2023
by Ryan Scott 08 Mar '23

08 Mar '23

ACM SIGPLAN Haskell Implementors' Workshop https://icfp23.sigplan.org/home/hiw-2023 Seattle, Washington, United States, September 4, 2023 Co-located with ICFP 2023 https://icfp23.sigplan.org/ Important dates --------------- Deadline: July 4, 2023 (AoE) Notification: August 4, 2023 Workshop: September 4, 2023 The 15th Haskell Implementors' Workshop is to be held alongside ICFP 2023 this year in Seattle. It is a forum for people involved in the design and development of Haskell implementations, tools, libraries, and supporting infrastructure to share their work and to discuss future directions and collaborations with others. Talks and/or demos are proposed by submitting an abstract, and selected by a small program committee. There will be no published proceedings. The workshop will be informal and interactive, with open spaces in the timetable and room for ad-hoc discussion, demos, and short lightning talks. Scope and target audience ------------------------- It is important to distinguish the Haskell Implementors' Workshop from the Haskell Symposium which is also co-located with ICFP 2023. The Haskell Symposium is for the publication of Haskell-related research. In contrast, the Haskell Implementors' Workshop will have no proceedings -- although we will aim to make talk videos, slides, and presented data available with the consent of the speakers. The Implementors' Workshop is an ideal place to describe a Haskell extension, describe works-in-progress, demo a new Haskell-related tool, or even propose future lines of Haskell development. Members of the wider Haskell community are encouraged to attend the workshop -- we need your feedback to keep the Haskell ecosystem thriving. Students working with Haskell are especially encouraged to share their work. The scope covers any of the following topics. There may be some topics that people feel we've missed, so by all means submit a proposal even if it doesn't fit exactly into one of these buckets: * Compilation techniques * Language features and extensions * Type system implementation * Concurrency and parallelism: language design and implementation * Performance, optimisation and benchmarking * Virtual machines and run-time systems * Libraries and tools for development or deployment Talks ----- We invite proposals from potential speakers for talks and demonstrations. We are aiming for 20-minute talks with 5 minutes for questions and changeovers. We want to hear from people writing compilers, tools, or libraries, people with cool ideas for directions in which we should take the platform, proposals for new features to be implemented, and half-baked crazy ideas. Please submit a talk title and abstract of no more than 300 words. Submissions can be made via HotCRP at https://icfphiw23.hotcrp.com until July 4 (anywhere on earth). We will also have a lightning talks session. These have been very well received in recent years, and we aim to increase the time available to them. Lightning talks should be ~7mins and are scheduled on the day of the workshop. Suggested topics for lightning talks are to present a single idea, a work-in-progress project, a problem to intrigue and perplex Haskell implementors, or simply to ask for feedback and collaborators. Program Committee ----------------- * Gergő Érdi (Standard Chartered Bank) * Sebastian Graf (Karlsruhe Institute of Technology) * Wen Kokke (University of Strathclyde) * Ryan Scott (Galois, Inc.) * Rebecca Skinner (Mercury) * Li-yao Xia (University of Edinburgh) Contact ------- * Ryan Scott <ryan.gl.scott at gmail.com>

1 0

Takeover request: unix-compat
by Mitchell Rosen 07 Mar '23

07 Mar '23

Hi all, I'd like to take over maintenance responsibility for the `unix-compat` package. Unfortunately, I've been unable to get in touch with the maintainer. I intend to make a release compatible with `unix-2.8`, and will be around to make subsequent bounds bumps and whatnot. You can find me on GitHub: https://github.com/mitchellwrosen Or Hackage: https://hackage.haskell.org/user/mitchellwrosen Thanks, Mitchell

4 6

[ANN] dunai-0.10.1 and bearriver-0.14.1
by Ivan Perez 07 Mar '23

07 Mar '23

Dear all, I'm happy to announce the release of Dunai 0.10.1 and Bearriver 0.14.1! Dunai is a reactive programming library structured around a notion of Monadic Stream Functions. Dunai can be used to implement other reactive and FRP frameworks on top, including Classic FRP and Arrowized FRP variants. Dunai comes with: - bearriver: API-compatible implementation of Yampa. (The Bear River is a tributary to the Yampa river.) - dunai-test: QuickCheck-based temporal testing library that can be connected with the testing system haskell-titan. See https://github.com/ivanperez-keera/dunai#features for details on Dunai's features. This new release introduces a breaking change in Monadic Stream Functions' instance of VectorSpaces. Most code using that instance should work without changes but, in some cases, the use of 'constantly' is now necessary. (This case is described in the discussion thread of issue #298.) * Summary of Version 0.10.1: - Implement dot in MSF's instance of VectorSpace (#298). - Enable FlexibleContexts in VectorSpace instance module (#344). As always, dunai, dunai-test and bearriver are released in sync. For details, see: - https://github.com/ivanperez-keera/dunai/releases/tag/v0.10.1 * Releases You can explore the current versions at: - https://hackage.haskell.org/package/dunai - https://hackage.haskell.org/package/dunai-test - https://hackage.haskell.org/package/bearriver * Code The github repo is located at: https://github.com/ivanperez-keera/dunai * What's coming This release comes exactly 2 months after the last release. The next release is planned for Apr 21, 2023. There are several issues open that you can contribute to: https://github.com/ivanperez-keera/dunai/issues Following our roadmap, the pending changes remain as follows: - Full conformance to style guide. - Benchmarks: Facilitate making sound, evidence-based decisions about suggested improvements to the implementation, by completing a series of benchmarks. * Donations Our project is now seeking donations to help continue developing dunai, create new open source libraries, new material, and give talks. Special thanks go to @johannes-riecken for sponsoring my work on the dunai project with a regular contribution. Github will match the first 5K donated, so if you donate $1/month, github will donate the same amount. No donation is too small. Any contribution will absolutely help. See https://github.com/sponsors/ivanperez-keera for details. If you can help, please come forward. All the best, Ivan

1 0

Take-over request for: snappy
by Andrey Prokopenko 06 Mar '23

06 Mar '23

Hello, - Few months ago Andrew Martin opened PR in `snappy`: https://github.com/bos/snappy/pull/10 <https://github.com/bos/snappy/pull/10> - The package is either direct or transient dependency for `tensorflow`, `kafka-client` and few more packages. - While forks maintenance is a well-known practice it creates burden on maintainers. - Moreover, I cannot easily fix cabal build for tensorflow for different GHC versions. Note for Bryan: I haven’t forked `snappy` so there will be no name clashes during the transfer. I would like to become a maintainer for `snappy` package and keep it up-to-date at least for a next few years. I have already followed that procedure a few years ago for `blaze-textual` package. (Recently I discovered a flaw in my maintenance setup and fixed it.) So my intent is to resolve recent PRs and to keep supporting for newer compiler versions and build tools. Please consider this message as a step 2 in take-over procedure: https://wiki.haskell.org/Taking_over_a_package <https://wiki.haskell.org/Taking_over_a_package> Kind Regards, Andrey Prokopenko

1 0

[ANNOUNCE] GHC 9.6.1-rc1 is now available
by Ben Gamari 03 Mar '23

03 Mar '23

The GHC team is very pleased to announce the availability of the first (and likely final) release candidate of GHC 9.6.1. As usual, binaries and source distributions are available at [downloads.haskell.org](https://downloads.haskell.org/ghc/9.6.1-rc1/). Beginning with GHC 9.6.1, GHC can be built as a cross-compiler to WebAssembly and JavaScript. This is an important step towards robust support for compiling Haskell to the Web, but there are a few caveats to be aware of in the 9.6 series: - Both the Javascript and WebAssembly backends are still at an early stage of development and are present in this release as a technology preview - Using GHC as a cross-compiler is not as easy as we would like it to be; in particular, there are challenges related to Template Haskell - GHC is not yet run-time retargetable; a given GHC binary targets exactly one platform, and both WebAssembly and JavaScript are considered platforms for this purpose. Cross-compilers must be built from source by their users We hope to lift all of these limitations in future releases. Additionally, 9.6.1 will include: - Significant latency improvements in the non-moving garbage collector - Efficient runtime support for delimited continuations - Improvements in compiler error messages - Numerous improvements in the compiler's memory usage See the [release notes][] for a comprehensive accounting of changes in this release. As always, one can find a migration guide to aid in transitioning from older releases on the [GHC Wiki][migration-guide]. We have also recently started extending our release process to cover a wider set of Linux distributions. In particular, we now offer Rocky 8 and Ubuntu 20.04 binary distributions which cover RedHat-derivative and distributions using older `glibc` releases (namely 2.27), respectively. Please do give this release a try and open a [ticket][] if you see anything amiss. If all goes well we expect the final release should be available by late next week. Happy Haskelling, ~ Ben [ticket]: https://gitlab.haskell.org/ghc/ghc/issues/ [migration-guide]: https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.6 [release notes]: https://downloads.haskell.org/ghc/9.6.1-rc1/docs/users_guide/9.6.1-notes.ht…

1 0

dynamic web form generation for algebraic data types
by Olaf Klinke 03 Mar '23

03 Mar '23

Dear Cafe, has anyone ever attempted (and maybe succeeded) in building dynamic forms using one of the Haskell web frameworks (Yesod,Servant,...)? By "dynamic" form I mean a form that changes the number of fields based on selections the user makes in other fields of the form. For example, say one has an algebraic data type data T = Number Int | Check Bool T A form for such a type would initially consist of radio buttons or a drop-down list with options "Number" and "Check" that lets the user select the constructor. When "Number" is selected, an <input type="number"> field is shown. When "Check" is selected, an <input type="checkbox"> is displayed next to another form of this kind. In the end, one would use the GHC.Generics machinery to generate forms for a wide range of algebraic data types. I've seen this in the Clean language's iTask library [1] and it's very convenient. Of course this would involve a lot of JavaScript like document.createElement() as well as book-keeping how to re-asseble the fields into a T value upon submission. At least the latter is already handled by libraries such as yesod-form. Olaf [1] https://cloogle.org/src/#itasks/iTasks/UI/Editor/Generic [2] https://github.com/haskell-servant/servant-swagger/issues/80

5 8

Re: [Haskell-cafe] dynamic web form generation for algebraic data types
by Gustavo Bicalho 03 Mar '23

03 Mar '23

>From briefly reading the wiki page https://wiki.haskell.org/Tangible_Value, it looks like it relies on Applicative functors for combining values. So maybe the missing piece for sum-types was Selective functors https://hackage.haskell.org/package/selective? Gustavo Bicalho > ---------- Forwarded message ---------- > From: Olaf Klinke <olf(a)aatal-apotheke.de> > To: Ivan Perez <ivanperezdominguez(a)gmail.com> > Cc: "Haskell Café" <haskell-cafe(a)haskell.org> > Bcc: > Date: Thu, 02 Mar 2023 17:40:18 +0100 > Subject: Re: [Haskell-cafe] dynamic web form generation for algebraic data types > On Thu, 2023-03-02 at 07:34 -0800, Ivan Perez wrote: > > All of this reminds me of Conal Elliott's Tangible Values. > > > > http://conal.net/papers/Eros/ > > > > (Not for web but the idea still applies.) > > > > Ivan > > Yes, the concept has been re-invented multiple times, as is the case > with most good ideas. TVs are general enough to bolt a web interface on > top, I guess. > > Seems that Conal, too, has not solved the sum type problem. > The tangible value GADT > https://hackage.haskell.org/package/TV-0.5.0/docs/Interface-TV-Input.html > has a Pair constructor but not for Sum. I wonder whether there is a > deeper categorical reason for this. > > So I should re-phrase my question: > Has anyone extended tangible values to Generic types and given them a > modern html interface? > > Olaf

1 0