- Haskell-Cafe - Haskell.org

Midlands Graduate School - registration now open
by Graham Hutton 18 Mar '25

18 Mar '25

Dear all, Registration is now open for the Midlands Graduate School (MGS) in the Foundations of Computing Science, 7-11 April 2025, Sheffield, UK. Eight fantastic courses on category theory, type theory, coalgebra, semantics and more. Spaces are limited, so please register early to secure your place. Please share in your communities! Best wishes, Graham Hutton ========================================================== 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 REGISTRATION: The registration fee is £300 for academic participants, and £500 for industry participants. The fee includes all lecture courses and example classes, lunch and coffee breaks. The registration deadline is ** Monday 17th 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 1

[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 15 Mar '25

15 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 28 Feb '25

28 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 10 Feb '25

10 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 09 Feb '25

09 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