- Haskell-Cafe - Haskell.org

[ANN] Copilot 4.3
by Ivan Perez 17 Mar '25

17 Mar '25

Hi everyone!! We are really excited to announce Copilot 4.3 [1,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. Compilation to Bluespec, to target FPGAs, is also supported. Copilot is NASA Class D open-source software, and is being used at NASA in drone test flights. Through the NASA tool Ogma [3] (also written in Haskell), Copilot also serves as a runtime monitoring backend for NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the software framework used in the Mars Helicopter). This release introduces several updates, bug fixes and improvements to Copilot: - Specifications now produce information about counterexamples when copilot-theorem is able to prove the property false. - We introduce a new Prop construct in copilot-core that captures the quantifier used in a property. - The What4 backend of Copilot theorem now produces an exception when trying to prove an existential property. The restriction of not being able to handle existentially quantified properties already existed, but due to information loss during the reification process, the quantifier was being lost and all properties to be proved via what4 were being treated as a universally quantified. - Several deprecated functions have been removed. - The installation instructions have been updated. - Compatibility with GHC 9.10 is now explicitly listed in the README. - Several typos have been fixed in comments and documentation. The new implementation is compatible with versions of GHC from 8.6 to 9.10. This release has been made possible thanks to key submissions from Ryan Scott (Galois) and Esther Conrad (NASA), the last of which is also a first-time contributor to the project. We are grateful to them for their timely contributions, especially during the holidays, and for making Copilot better every day. For details on this release, see [1]. https://github.com/Copilot-Language/copilot/releases/tag/v4.3. As always, we're releasing exactly 2 months since the last release. Our next release is scheduled for May 7th, 2025. We want to remind the community that Copilot is now accepting code contributions from external participants again. Please see the discussions and the issues in our github repo [4] to learn how to participate. Current emphasis is on using Copilot for full data processing applications (e.g, system control, arduinos, rovers, drones), improving usability, performance, and stability, increasing test coverage, removing unnecessary dependencies, hiding internal definitions, formatting the code to meet our new coding standards, and simplifying the Copilot interface. Users are encouraged to participate by opening issues, asking questions, extending the implementation, and sending bug fixes. Happy Haskelling! Ivan -- [1] https://github.com/Copilot-Language/copilot/releases/tag/v4.3 [2] https://hackage.haskell.org/package/copilot [3] https://github.com/nasa/ogma [4] https://github.com/Copilot-Language/copilot

1 0

GHC 9.12.2 is now available
by Ben Gamari 14 Mar '25

14 Mar '25

The GHC developers are happy to announce the release of GHC 9.12.2. Binary distributions, source distributions, and documentation are available at [downloads.haskell.org] We hope to have this release available via `ghcup` shortly. This is a small release fixing a critical code generation bug, #25653, affecting some subword division operations. As always, GHC's release status, including planned future releases, can be found on the GHC Wiki [status]. We would like to thank IOG, the Zw3rk stake pool, Well-Typed, Tweag I/O, Serokell, Equinix, SimSpace, the Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors who contribute their code, tickets, and energy to the GHC project. As always, do give this release a try and open a [ticket] if you see anything amiss. [release notes]: https://downloads.haskell.org/ghc/9.12.2/docs/users_guide/9.12.2-notes.html [status]: https://gitlab.haskell.org/ghc/ghc/-/wikis/GHC-status [downloads.haskell.org] https://downloads.haskell.org/ghc/9.12.2 [ticket]: https://gitlab.haskell.org/ghc/ghc/-/issues/new

1 0

Internship opportunity at NASA Ames Research Center -- Deadline Feb 28
by Ivan Perez 27 Feb '25

27 Feb '25

All, We have an opening for an internship opportunity at NASA Ames Research Center working on a Haskell project. The deadline is tomorrow Friday, Feb 28. I've posted the details here: https://www.reddit.com/r/haskell/comments/1ixmlei/haskell_internship_openin… Please have any students who qualify apply ASAP. Thanks, Ivan

1 0

GHC API stability initiative
by Facundo Domínguez 20 Feb '25

20 Feb '25

Dear all, At the end of last year I started collecting feedback from tool maintainers about the costs of dealing with GHC as a library. Eventually the feedback will be used to propose some actions to reduce these costs. Here's the last update on the initiative [1]. [1] https://discourse.haskell.org/t/ghc-api-stability-update-3/11407 This message is to broadcast the invitation for tool maintainers to share their feedback. I can be reached at facundo.dominguez(a)tweag.io, or you can reach me in the discourse thread as well. Best, Facundo

1 0

Midlands Graduate School 2025 hosted by the University of Sheffield
by Andrei Popescu 18 Feb '25

18 Feb '25

Dear Colleagues, This year's Midlands Graduate School in the Foundations of Computing Science will take place at the University of Sheffield. We have some great lecturers and topics. (Below you can also find information about fees. The registration site will open soon.) Best wishes, Andrei Midlands Graduate School 2025 7-11 April 2025, Sheffield, UK https://tinyurl.com/MGS-2025 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 Eight courses will be given. Participants usually take all the introductory courses and choose additional options from the advanced courses depending on their interests. Invited course - Four Lectures on Proof-Theoretic Semantics, David Pym Introductory courses - Category Theory, Thorsten Altenkirch - The Curry-Howard Correspondence, Anupam Das - Quantum Computing, Venanzio Capretta Advanced courses - Coalgebra, Paul Blain Levy - Linear Logic, Abhishek De and Charles Grellois - Modular Proofs in Isabelle/HOL, Chelsea Edmonds - Refinement Types in Haskell, Brandon Hewer FEES AND REGISTRATION The fees for MGS 25, which also cover catering (including coffee, pastries and lunch) during the day and optionally the conference dinner, are as follows. - Academic participant: £300, plus an optional £30 dinner ticket for Wednesday evening. - Industry participant: £500, plus an optional £30 dinner ticket for Wednesday evening. Registration will be open shortly. 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.

1 1

using the same data structure on a type level and as a value
by Zoran Bošnjak 15 Feb '25

15 Feb '25

Dear haskellers, I would like to reuse some (complex) data structures at a type level and as a regular value. The intention is to have the original specification on the type level (something like web API in Servant). But the idea is also to be able to convert the same structure to the value (of the same shape) and print it for example. There is no need to go from values back to types. I am not sure if Generic could help me do the conversion or do I need Typeable or even something else. I would like to avoid template haskell if possible, but please do advice if TH is the way to go in such cases. In my case, the data type structure is suppose to be the same, with the only difference being the 2 "primitives", which is: number is (Nat or Integer, depending on the usecase) and text is (Symbol or String). My attempt was something like this. import GHC.Generics -- not sure if this is required, but deriving works OK import GHC.TypeLits data Usecase = TypeLevel | ValueLevel -- Generic Int is 'Nat' or 'Integer'. type family GInt (u :: Usecase) where GInt 'TypeLevel = Nat GInt 'ValueLevel = Integer -- Generic Text is 'Symbol' or 'Text'. type family GText (u :: Usecase) where GText 'TypeLevel = Symbol GText 'ValueLevel = String -- Positive/zero or negative value. data PlusMinus = Plus | Minus deriving (Generic, Show) -- Now we can define generic plus/minus number. data PMInt (u :: Usecase) = PMInt PlusMinus (GInt u) deriving (Generic) deriving instance Show (PMInt 'ValueLevel) -- And we also define some more complex structure. data GNumber (u :: Usecase) = GNumInt (PMInt u) | GNumDiv (GNumber u) (GNumber u) | GNumPow (PMInt u) (PMInt u) deriving (Generic) deriving instance Show (GNumber 'ValueLevel) data GTest (u :: Usecase) = GTest [GInt u] [GText u] deriving (Generic) deriving instance Show (GTest 'ValueLevel) -- This does not work, but the idea is to define some type aliases -- In real application, this will be a huge list of structure descriptions (as types) type Example1 = 'PMInt 'Plus 3 -- GHC does not like '3' here?? type Example2 = 'PMInt 'Minus 4 type Example3 = 'GNumInt Example1 type Example4 = 'GNumDiv Example3 Example3 type Example5 = 'GTest '[ 1, 2, 3 ] '[ "Test1", "Test2"] -- 'convert' implementation ?? -- ... and be able to convert types to values, something like this val1 :: PMInt 'ValueLevel val1 = convert @Example1 -- ... or print it directly f :: IO () f = print ( convert @Example1, convert @Example2, convert @Example3 , convert @Example4, convert @Example5) Appreciate your suggestions. regards, Zoran

1 0

Re: [Haskell-cafe] Course-of-value recursion by defining a sequence as a self-referential infinite list
by Douglas McIlroy 10 Feb '25

10 Feb '25

> catalanNumbers :: Num a => [a] > catalanNumbers = > let xs = 1 : PowerSeries.mul xs xs > in xs This example of a generating function come to life as a program deserves to be better known. Bill Burge presented it 50 years ago in "Recursive Programming Techniques", Addison-Wesley, 1975. I revisited it in "Power series, power serious", JFP 9 (1999) 323-335, where, with overloadied arithmetic, it became ts = 1 : ts^2 The technique is laid bare in ten one-liners at https://www.cs.dartmouth.edu/~doug/powser.html. Doug

4 5

A Conversation With Sandy Maguire - Melbourne Haskell Users' Group - 28-03-2024
by John Walker 09 Feb '25

09 Feb '25

Hi All, Our interview with Sandy Maguire at Melbourne Haskell Users' Group, (now Melbourne Compose Group) is now on [YouTube](https://youtu.be/dnHIsr6gGnE). Sandy is well known in the Haskell and broader FP community, particularly as the author of: - [Thinking With Types](https://leanpub.com/thinking-with-types) - [Algebra Driven Design](https://leanpub.com/algebra-driven-design) - [Certainty By Construction](https://leanpub.com/certainty-by-construction) John

2 1

Re: [Haskell-cafe] Course-of-value recursion by defining a sequence as a self-referential infinite list
by Douglas McIlroy 08 Feb '25

08 Feb '25

>> Karczmarczuk’s solution via the Haskell prelude: >> >> part = 1 : b 1 >> where b n = (1 : b (n + 1)) + (replicate n 0 ++ b n) >> > This is broken code, no?, just 2 reasons I can spot why: > - function 'b n' calls 'b n' unconditionally (infite loop) > - What is the reutrn type of 'b'? It seems like it returns list, but the > return value is in the form 'a + b' , where (+) is instance of num so > I don't think prelude contains any ad-hoc definition of (+) that > returns list Not broken, just insufficiently documented. "part "is supposed to produce an infinite stream whose nth element is the number of distinct representations of n as a sum of positive integers. The "infinite loop" is deliberate, quite like ones = 1 : ones which generates an infinite sequence of 1s. It is not stated, but the (+) is understood to have been overloaded to handle lists of Nums in the natural way Doug

1 0

[ANN] NASA's Ogma 1.6.0
by Ivan Perez 04 Feb '25

04 Feb '25

Hi everyone! I'm thrilled to announce the release of Ogma 1.6.0! NASA's Ogma is a mission assurance tool that facilitates integrating runtime monitors or runtime verification applications into other systems. Use cases supported by Ogma include producing Robot Operating System (ROS 2) packages [3], NASA Core Flight System (cFS) applications [4], and components for FPrime [1] (the software framework used for the Mars Helicopter). Ogma is also one of the solutions recommended for monitoring in Space ROS applications [2]. Ogma is fully written in Haskell, and leverages existing Haskell work, like the Copilot language [5] (also funded by NASA) and BNFC [6]. For more details, including videos of monitors being generated and flown in simulators, see: https://github.com/nasa/ogma * What's changed This major release includes the following improments: - Update Ogma to be able to extract data from XML files, including standard formats used in MBSE tools. - Provide a new diagram command capable of generating state machine implementations from diagrams. - Make the ROS and F' backend able to use any JSON- or XML files as input, makes the ROS, F', standalone backends capable of using literal Copilot expressions in requirements and state transitions. - Extend Ogma to be able to use external tools to translate requirements, including LLMs. - Make the F' backend able to use templates. - Allow users to provide custom definitions for XML and JSON formats unknown to the tool. - Fixes several other smaller maintenance issues. - Upgrades the README to include instructions for external contributors. This constitutes the single largest release of Ogma in number of new features added, since its first release. For details about the release, see: https://github.com/nasa/ogma/releases/tag/v1.6.0 * Releases Ogma is released as a collection of packages in Hackage. The entry point is https://hackage.haskell.org/package/ogma-cli. * Code The github repo is located at: https://github.com/nasa/ogma. * What's coming The next release is planned for Mar 21st, 2025. We are currently working on a GUI for Ogma that facilitates collecting all mission data relative to the design, diagrams, requirements and deployments, and help users refine designs and requirements, verify them for correctness, generate monitors and full applications, follow live missions, and produce reports. We also want to announce that both Ogma and Copilot can now accept contributions from external users, and we are also keen to see students use them for their school projects, their final projects and theses, and other research. If you are interested in collaborating, please reach out to ivan.perezdominguez(a)nasa.gov. We hope that you are as excited as we are and that our work demonstrates that, with the right support, Haskell can reach farther than we ever thought possible. Happy Haskelling! Ivan [1] https://github.com/nasa/fprime [2] https://space.ros.org/ [3] https://www.ros.org/ [4] https://github.com/nasa/cFS [5] https://github.com/Copilot-Language/copilot [6] https://github.com/BNFC/bnfc

1 0