- Haskell-Cafe - Haskell.org

GHC Steering Committee Call for Nominations
by Adam Gundry 28 Jan '24

28 Jan '24

Dear Haskellers, The GHC Steering Committee is seeking nominations for new members. The committee scrutinizes, debates and eventually decides to accept or reject proposals to change the language or major features supported by GHC. Our processes are described in the GitHub repository where proposals are submitted (https://github.com/ghc-proposals/ghc-proposals) In particular, please have a look at the committee bylaws (https://github.com/ghc-proposals/ghc-proposals/blob/master/committee.rst) We are looking for members who have the ability to: - understand GHC proposals (e.g. for new language extensions), - find holes and missing corner cases in the specifications, - foresee the interaction with other language or compiler features, - comment constructively and improve proposals through engagement with others, - judge the cost/benefit ratio of changes, and - come to a justifiable conclusion. Ideally, committee members should: - have substantial experience of writing or teaching Haskell; - have a track record of active contributions to the Haskell community; or - have expertise in language design and implementation, in either Haskell or related languages. It is our aim that this committee be diverse; by representing different viewpoints, we will make decisions that benefit larger segments of our community. Even if you are uncertain whether your background qualifies you for the role, you are warmly encouraged to apply. The committee's work requires a small, but non-trivial amount of time, especially when you are assigned a proposal for shepherding. We estimate the workload to be around 2 hours per week, and our process works best if members usually respond to technical emails within 1-2 weeks (within days is even better). Please keep that in mind if your email inbox is already overflowing. To nominate yourself, please send an email to me (as the committee secretary) at adam(a)well-typed.com by February 16th 2024, briefly summarising your background and relevant experience. I will distribute the nominations among the committee, and we will keep the nominations and our deliberations private. Self-nominations are the norm. You can nominate someone else, but please obtain their explicit consent to do so. (We don't want to choose someone who turns out to be unable to serve.) On behalf of the committee, Adam Gundry -- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

1 0

`queue` package take-over request
by Mitchell Rosen 23 Jan '24

23 Jan '24

Hi all, I'd like to take over the `queue` package, last updated 14 years ago, and marked "deprecated" on Hackage. I intend to replace it with a simple, clean implementation of Okasaki's "real time" (meaning O(1) worst-case operations) queue, which you can find implemented here: https://github.com/awkward-squad/queues I had originally named the package `queues` (with an s), but figured it would be better to repurpose the singular `queue` with something useful, if possible. Thanks! Mitchell

4 7

heads-up: tls v2.0.0
by Kazu Yamamoto 20 Jan '24

20 Jan '24

Hello guys, I'm planning to release the "tls" package v2.0.0 probably within one month. It removes TLS 1.0/1.1 and provides only TLS 1.2/1.3 with safe cipher suites according to recent RFCs and internet-drafts. This version does not change the default usage. But if you are using custom parameters, you might have to modify your code. This breaking change is *intentional* to notice users that they are using vulnerable versions and/or parameters. The attached is the current change log. --Kazu ## Version 2.0.0 * `tls` now only supports TLS 1.2 and TLS 1.3 with safe cipher suites. * Security: BREAKING CHANGE: TLS 1.0 and TLS 1.1 are removed. * Security: BREAKING CHANGE: all CBC cipher suite are removed. * Security: BREAKING CHANGE: RC4 and 3DES are removed. * Security: BREAKING CHANGE: DSS(digital signature standard) is removed. * Security: BREAKING CHANGE: TLS 1.2 servers require EMS(extended master secret) by default. * BREAKING CHANGE: the package is now complied with `Strict` and `StrictData`. * BREAKING CHANGE: Many data structures are re-defined with `PatternSynonyms` for extensibility. * BREAKING CHANGE: the structure of `SessionManager` is changed to support session tickets. * API: `handshake` can receive an alert of client authentication failure for TLS 1.3 [#463](https://github.com/haskell-tls/hs-tls/pull/463) * API: `bye` can receive NewSessionTicket for TLS 1.3 * Channel binding: `getFinished` and `getPeerFinished` are deprecated. Use `getTLSUnique` instead. * Channel binding: `getTLSExporter` and `getTLSServerEndPoint` are provided. [#462](https://github.com/haskell-tls/hs-tls/pull/462) * Refactoring: the monolithic `handshake` is divided to follow the diagram of TLS 1.2 and 1.3 for readability. * Refactoring: test cases are refactored for maintenability and readablity. `hspec` is used instead of `tasty`. * Code format: `fourmolu` is used as an official formatter.

5 18

Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
by Olaf Klinke 20 Jan '24

20 Jan '24

> For functions types, there is only one equivalence class, because > there > is only one way to pattern-match a function. Observe that two > elements > can be distinguished by a set of patterns if and only if there is one > element in the pattern set that already distinguishes them. Do > pattern > synonyms refine the equivalence relation induced by ordinary > constructors? No. What I said is only true in the absence of view patterns. With view patterns, a pattern match is no longer guaranteed to terminate, since the viewing function could diverge on the value being matched. Consider -- diverges on infinite lists end :: [a] -> [a] end xs = case tl xs of [] -> [] (_:xs') -> end xs' pattern Finite <- (end -> []) isFinite :: [a] -> Bool isFinite xs = case xs of Finite -> True _ -> False Notice that isFinite is no longer a clopen but an open: It either returns True or diverges. Moreover, view patterns introduce fine- grained clopens on function spaces, like pattern Q <- (($ 4) -> 3) We must conclude that in the presence of the ViewPatterns extension, the equivalenve relation induced by pattern matching is: "x~y whenever there is no function v and no pattern P such that (v x) and (v y) can be distinguished by P." It should not be hard to prove that deciding coverage by view patterns such as Finite would solve the halting problem. Olaf

1 0

Parallel Haskell on an M2 Mac
by Dennis Raddle 20 Jan '24

20 Jan '24

I don't know a lot about parallel Haskell, so I'm wondering in general terms how that would work with my M2 Mac. I have a search task that's easily run in parallel. For example, I might map a function over a list, and each item's evaluation can run in parallel. On the M2 MacBook I have, there are 4 efficiency cores with 1 thread each, and 8 performance cores with 2 threads each. Is it fairly easy to use parallel Haskell to spread the task over these 20 possible threads? By any chance could I limit it to using the performance cores if that helps the speed? Thanks, Dennis

3 3

Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
by Olaf Klinke 19 Jan '24

19 Jan '24

> > Should we open a feature request at Haddock? > > I think that would be a good idea. A cursory search suggests there's > no feature request already Done: https://github.com/haskell/haddock/issues/1625 I would also like to humbly suggest that the GHC devs consider my proof that pattern synonym completeness checks are decidable, thus improving the situation that caused this thread. I have a proof-of-concept implementation with a type signature like covers :: PatternMatch t => [Pattern t] -> Bool where type Pattern t = t -> Bool and PatternMatch is a type class much like Generic which derives instances for all Generic Rep types (except V1) plus function spaces and fixed points. What is left to do is to convert the GHC-internal pattern representation into (t -> Bool). Is that feasible? As I elaborated, that task ist quite mechanistic and could likely be done in Template Haskell. Olaf

1 0

ZuriHac 2014 takes place 8-10 June, registration now open
by Jasper Van der Jeugt 19 Jan '24

19 Jan '24

Hi Friends of Haskell, It is our pleasure to announce that ZuriHac 2024 will take place Saturday 8 June - Monday 10 June 2024 as a physical event at the Rapperswil-Jona campus of the OST Eastern Switzerland University of Applied Sciences. The focus of ZuriHac is being a community event and hackathon, but we will also have some exciting keynotes from Ningning Xie, Alex McLean, Ivan Perez and Mary Sheeran. In addition to that, there will be some more hands-on content: Well-Typed will host a workshop, Jesper Cockx will host an Agda track and Manuel Bärenz will host an FRP Track. We also welcome beginners or people unfamiliar to Haskell who are curious to learn more. Eliane Schmidli will teach a beginners workshop, and there will be many mentors from the Haskell Community happy to answer all your questions. Two days prior to ZuriHac, the Haskell Foundation and OST will organize a co-located 2-day Haskell Infrastructure Workshop. More details about that will be announced soon. You can find more information about the event and register at <https://zurihac.info>. The event is free for participants. This is only possible with the help of our generous supporters, who are currently: - The Haskell Foundation - Jane Street - OST Eastern Switzerland University of Applied Sciences - Tweag - Well-Typed In case you would like to support ZuriHac, please get in touch with us. We hope to see you there! The Zurich Friends of Haskell

1 0

Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
by Olaf Klinke 19 Jan '24

19 Jan '24

> My point is that which patterns are expected to be complete is an API > design choice, subject to API stability decisions, and not just a > matter > of deductive reasoning. Now I understand: Even though completeness is (provably) provable, the COMPLETE pragma can signal the library user which sets of patterns the library author intended to cover the (opaque) type, much like the MINIMAL pragma for type classes. Otherwise the library user could only know this by compiling a code snippet with -Wincomplete-uni-patterns. To further draw the parallel between MINIMAL and COMPLETE, is COMPLETE picked up by Haddock? Seems not: The Data.Sequence.Internal module contains {-# COMPLETE (:<|), Empty #-} {-# COMPLETE (:|>), Empty #-} yet the "bundled patterns" section in https://hackage.haskell.org/package/containers-0.7/docs/Data-Sequence.html#… does not show it. If COMPLETE is indeed never picked up by Haddock, I'd say this pragma is currently fairly useless for conveying contracts. Should we open a feature request at Haddock? Olaf

2 1

Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
by Olaf Klinke 18 Jan '24

18 Jan '24

> > Hence I believe that completeness checks in presence of patterns is > > equivalent to determine whether a disjunction of logic formulae, > > which > > are possibly self-referential, is a tautology. That may well be > > semi- > > decidable at best. > > That seems plausible, but I think that interface stability is a more > serious concern. It isn't enough to know that *as-implemented* at a > given time some particular set of patterns is complete. > > The implementation of a set of patterns (or the underlying type) can > change in a manner that changes complete <-> incomplete in either > direction. Such changes are non-breaking, provided there was no > "contract" (COMPLETE pragma) that the patterns are *intended* to be > complete. > You are right: It is possible that the types of the bidirectional patterns do not change, but the completeness changes. In your example given I would argue the contract is broken, because the new patterns are for a different type Foo. Instead -- before: Good, Bad are complete data Foo = A | B pattern Good :: Foo pattern Good = A pattern Bad :: Foo pattern Bad = B -- after: Good, Bad are incomplete -- Foo, Good as before pattern Bad = A Here neither the definition of Foo nor the types of Good or Bad have changed, but completeness has. Here is why I think that completeness checks even with pattern synonyms should work and we would not need COMPLETE pragmas. The algorithm for a set of patterns of type T is: 1. Construct a Stone [1] space X from the given type T. (Often X = T) 2. Translate each pattern to a clopen of that Stone space 3. Use Stone duality to translate coverage into a Zeroth-order logic problem, which is decidable. Let us define an equivalence relation on the elements of a type. Say x~y whenever there is no pattern that can distinguish x and y by pattern match. Notice that any pattern partitions the set of equivalence classes into two disjoint subsets, think of isJust or isNothing. In general, given a pattern Pat for type T, write isPat :: T -> Bool isPat x = case x of Pat -> True _ -> False For functions types, there is only one equivalence class, because there is only one way to pattern-match a function. Observe that two elements can be distinguished by a set of patterns if and only if there is one element in the pattern set that already distinguishes them. Do pattern synonyms refine the equivalence relation induced by ordinary constructors? No. Consider type Clopen x = x -> Bool data C = L C | R C cl :: Clopen C cl = isL . shift where isL :: Clopen C -- a pattern isL (L c) = True isL (R c) = False shift :: C -> C shift (L c) = c shift (R c) = c Can one define a single pattern synonym pattern CL :: C -> C such that CL matches c if any only if cl c == True? Note that cl is the disjunction of two ordinary patterns, namely L (L _) R (L _) CL morally should be the pattern (_(L _)) but that is not valid pattern syntax. Indeed with synonyms we can define the CL pattern: {-# LANGUAGE PatternSynonyms, ViewPatterns #-} swap :: C -> C swap (L (R c)) = R (L c) swap (R (L c)) = L (R c) swap c = c pattern CL c <- (swap -> L c) isCL :: Clopen C isCL c = case c of CL _ -> True _ -> False Now, at least as long as a type X has only a finite number of constructors (integers with numeric literals being an exception), the type Clopen X defines a Stone space, a compact zero-dimensional Hausdorff space. By Stone duality these are dually equivalent to Boolean algebras. The duality translates the problem of coverage by clopens to the problem of proving that the disjunction of some elements in the algebra is the top element 'True'. Since Zeroth-order logic is decidable, completness checks even in the presence of pattern synonyms should be, too. For the countably infinite type C above, one can use the Select monad [2] to decide whether any number of clopens covers the space, pattern or not. For numeric literal patterns we can safely say that any set of patterns is not covering unless a wildcard pattern is among them. Olaf [1] https://en.wikipedia.org/wiki/Stone_space [2] https://hackage.haskell.org/package/transformers-0.6.1.1/docs/Control-Monad… see also https://hackage.haskell.org/package/infinite-search

2 1

Re: [Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns
by Olaf Klinke 16 Jan '24

16 Jan '24

> > I think the completeness checker works fine in all > > pattern-synonym-free cases, i.e. when you're using only real > > constructors. One can envision a simple recursive divide-and-conquer algorithm, see below. > I don't actually understand why completeness > > annotations are needed for pattern synonyms. > > I remember reading somewhere, but I can't find it now, that GHC's > coverage checker does not look inside pattern synonym definitions at > all, and this is by design: namely to ensure abstraction boundaries. > Looking inside the definition would mean that type checking behaviour > (in a way -- if you count coverage checks as "type checking") of user > code is influenced by invisible implementation details of the > "constructors" they're using. Compare that to 'type' versus 'newtype' on the type level: A type is just an alias, a synonym. The type checker has access to all information on the right hand side of the equality. With extensions like TypeSynonymInstances, A type alias is interchangeable with the aliased type. If what you report is true, they should not have called pattern synonyms a "synonym". > > My own thoughts on this: if GHC would look inside pattern synonym > definitions, then it would be hard to ensure that GHC thinks that > certain things are _not_ complete even if technically they are. For > example, if you have a data type with, say, 3 constructors, but you > hide > some of those (don't export them) and use pattern synonyms to make it > look like 4 constructors, then you might want GHC's coverage checker > to > consider that a data type with 4 constructors, not one with 3. > COMPLETE > pragmas add "positive" information -- "this set is complete, in > addition > to whatever other complete sets GHC might already know" -- and there > is > no way to _subtract_ complete sets from GHC's knowledge base. > > This is mostly me theorising, but perhaps it helps. > > - other Tom > I don't think the number of constructors/patterns is the issue. Likely the problem lies in the fact that while ordinary constructors make up disjoint subsets of the type, with patterns you can define overlapping sets, which makes completeness checks much more complicated. Hence I believe that completeness checks in presence of patterns is equivalent to determine whether a disjunction of logic formulae, which are possibly self-referential, is a tautology. That may well be semi- decidable at best. Olaf

3 2