March 2024 - Haskell-Cafe

[ANN] Copilot 3.19
by Ivan Perez 08 Mar '24

08 Mar '24

Hi everyone!! We are very excited to announce Copilot 3.19 [2]. 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 is being 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 NASA's Core Flight System, Robot Operating System (ROS2), and FPrime (the software framework used in the Mars Helicopter) applications. This release drastically increases the test coverage of copilot-core. We also remove deprecated functions from copilot-core that had been renamed in prior versions to comply with our style guide. I'd also like to highlight major changes that were released in Copilot 3.18.1, which was not broadly announced: the C backend now produces code that complies with MISRA C, we've introduced testing infrastructure for copilot-libraries and copilot-theorem, fixed an issue with how arrays are generated internally when used as arguments to triggers, fixed several bugs related to testing, introduce compatibility with GHC 9.6, and introduce a new function forAll to void clashes with the language keyword forall, which is needed to be compatible with GHC >= 9.8 in future versions. As always, we're releasing exactly 2 months since the last release. Our next release is scheduled for May 7th, 2024. Current emphasis is on improving the codebase in terms of stability and test coverage, removing unnecessary dependencies, hiding internal definitions, and formatting the code to meet our new coding standards. We also plan to add extensions to the language to be able to updates arrays and structs. Users are encouraged to participate by opening issues and asking questions via our github repo [3]. Happy Haskelling! Ivan [1] https://github.com/nasa/ogma [2] https://github.com/Copilot-Language/copilot/releases/tag/v3.19 [3] https://github.com/Copilot-Language/copilot [4] https://hackage.haskell.org/package/copilot

1 0

[ANN] Agda-2.6.4.3
by Andreas Abel 06 Mar '24

06 Mar '24

Agda 2.6.4.3 has been released to replace the deprecated 2.6.4.2. Changes over Agda 2.6.4.2 are two fixes: - [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with` - [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances # GHC supported versions Agda 2.6.4.3 has been tested with GHC 9.8.1, GHC 9.6.4, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4.3 can be installed using cabal-install or stack: 1. Getting the release candidate $ cabal get https://hackage.haskell.org/package/Agda-2.6.4.3/Agda-2.6.4.3.tar.gz $ cd Agda-2.6.4.3 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.3, v2.0 or the `master` branch of the standard library with Agda 2.6.4.3. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.4.2 https://hackage.haskell.org/package/Agda-2.6.4.3/changelog Enjoy Agda! Report problems and regressions to: https://github.com/agda/agda/issues Andreas, on behalf of the Agda Developers

1 0

PLMW@PLDI 2024: Call for Scholarship Applications
by Yao Li 05 Mar '24

05 Mar '24

The application for attending the Programming Language Mentoring Workshop (PLMW) @PLDI 2024 is open. The deadline is March 25th AOE for full consideration but we'll continue on a rolling basis after that as long as we have funding. The application link is here https://forms.gle/2haU1bMM7UKxU39y8. Please encourage undergraduates, MS students, and junior PhD students that you think could benefit from the workshop to apply. Below is more information about PLMW@PLDI 2024. PLMW aims to broaden the exposure of late-stage undergraduate students and early-stage graduate students to research and career opportunities in programming languages. The workshop includes mentoring sessions that cover effective habits for navigating research careers, technical sessions that cover core subfields of programming languages research, and social sessions that create opportunities for students to interact with researchers in the field. Applications from underrepresented groups in computing are especially welcome. PLMW @ PLDI 2024 will be co-located with the conference on Programming Language Design and Implementation. It will be held on June 24-25, 2024, Copenhagen, Denmark. The workshop program will cover important topics such as: • Career paths after graduate school • Interplay between PL and other areas of research in Computer Science • Useful research skills such as giving good talks and writing papers • Overview of key PL research areas both in academia and industry Find out more about the workshop at https://pldi24.sigplan.org/track/PLMW-PLDI-2024 Anitha Gollamudi. Assistant Professor, Miner School of Computer Science, Univ. of Massachusetts, Lowell. https://sites.uml.edu/anitha-gollamudi/

1 0

2024 Haskell Ecosystem Workshop, June 6-7, co-located with Zurihac
by Jose Calderon 05 Mar '24

05 Mar '24

Hello, In this two-day event, held on the lakeside campus of OST in lovely Rapperswil, Switzerland, you can learn what you need to know in order to get started working on these tools. We’ve asked the presenters to identify ‘good first issues’ for those wanting to get their feet wet on contributing. Because the workshop is immediately prior to Zurihac 2024, you will have the opportunity to tackle one of these issues while the core developers are easily available! The following speakers have been confirmed, with more to follow: Michael Peyton Jones: Haskell Language Server Julian Ospald: GHCUp Richard Eisenberg: GHC Alan Zimmerman: ghc-exactprint Hécate: Haddock and Documentation There will also be experts on ecosystem-wide issues (e.g. Security), in order to facilitate conversations about how to address cross-cutting issues in our tooling ecosystem. We will update the list of confirmed speakers as we receive confirmation. Registration is via eventbrite: https://www.eventbrite.com/e/2024-haskell-ecosystem-workshop-tickets-851066… More details on the Haskell Foundation website: https://haskell.foundation/events/2024-haskell-ecosystem-workshop.html I hope to see you there! -Jose

1 0

Midlands Graduate School (MGS)
by Graham Hutton 04 Mar '24

04 Mar '24

Dear all, There are just a few days left now to register for this years Midlands Graduate School (MGS) in Leicester. Seven fantastic courses on category theory, proof theory, type theory, session types, and more. 8-12 April 2024, Leicester, UK. Registration closes Friday 8th March. Best wishes, Graham Hutton ========================================================== Midlands Graduate School 2024 8-12 April 2024, Leicester, UK https://www.cs.le.ac.uk/events/mgs2024/ BACKGROUND: The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the mathematical foundations of computing. The MGS has been running since 1999, and is aimed at PhD students in their first or second year of study, but the school is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world! COURSES: Seven courses will be given. Participants usually take all the introductory courses and choose additional options from the advanced courses depending on their interests. Guest lecture - Formalisation of Mathematics, Kevin Buzzard Introductory courses - Category Theory, Thorsten Altenkirch - Proof Theory, Abhishek De and Iris van der Giessen - Type Theory with Agda, Todd Ambridge Advanced courses - Session Types, Sonia Marin - Synthetic Homotopy Theory with HoTT/UF, Ulrik Buchholtz - Graph Rewriting, Reiko Heckel - Categorical Realisability, Tom de Jong REGISTRATION: Registration is £295 for students, and £550 for academic, industry and independent participants. The fee includes all lecture courses and example classes, lunch and coffee breaks, and the conference dinner. The registration deadline is ** Friday 8th March **. Spaces are limited, so please register early to secure your place. SPONSORSHIP: We offer a range of sponsorship opportunities for industry (bronze, silver, gold and platinum), each with specific benefits. Please see the website for further details. ========================================================== — Professor Graham Hutton School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~pszgmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

1 0

Re: [Haskell-cafe] Is it possible to type a function to accept only literal values?
by Olaf Klinke 01 Mar '24

01 Mar '24

> Recently I was experimenting with a GCC intrinsic functions for x86 > SMID instructions to write a fast CSV parser Could you please elaborate on what you are planning to vectorize? Profiling shows that for usually number-heavy formats such as CSV or JSON, decoding the data fields outweighs the work necessary to decode the structure of the data format. Thus I assume you would want a streaming parser to decode input into a structure of yet unparsed blobs (cassava does this), then traverse the structure in parallel to finish parsing. I can imagine this poses difficulties to the standard model of parse error reporting, though, which often relies on sequential processing. Pretty much every streaming framework has incorporated cassava, and some streaming frameworks have abstractions for parsing. What is missing? (Not related to the OP:) Is streaming and parallel processing incompatible with formats such as XML or JSON, where well-formedness is typically determined by the very last byte in the input? (The last closing parenthesis or tag.) Olaf

2 1