- Haskell-Cafe - Haskell.org

[ANN] Copilot 3.11 -- hard realtime C runtime verification
by Ivan Perez 07 Sep '22

07 Sep '22

Dear all, We are very happy to announce the release of Copilot 3.11. Copilot is a runtime verification system implemented as a Haskell DSL that generates hard-realtime C99. Among others, Copilot is being used by the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. You can learn more about it at [1]. Copilot 3.11 introduces a new library, copilot-interpreter, that isolates all functions related to simulation of Copilot specifications. The release also contains a number of bug fixes, provides a simplified API, deprecates outdated elements, removes unused code, and introduces support for GHC 9.2. A full list of changes merged is available at [2]. A substantial effort is being made to achieve NASA's Class D software classification, most notably in terms of development process (which you can partly witness in how issues and PRs are being handled on our github repo), test coverage (mostly with quickcheck), and proofs of correctness of the generated code (with what4). Copilot is being used by the Safety-Critical Avionics Systems Branch (D320) of NASA Langley Research Center to conduct experiments related to flight safety of aerial vehicles. We have also built Ogma [3], a tool that allows us to generate full monitoring applications (e.g., NASA's Core Flight System [4] and Robot Operating System [5] applications) from requirements in structured natural language. We invite you all to explore Copilot, to try it, and to extend it. If you like it, please help us draw attention to this work with a star on github or a mention online. Happy Haskelling, The Copilot Team [1] https://github.com/Copilot-Language/copilot [2] https://github.com/Copilot-Language/copilot/milestone/15?closed=1 [3] https://github.com/nasa/ogma [4] https://cfs.gsfc.nasa.gov/ [5] https://www.ros.org/

1 0

any advice for tracking down a failure to compile (it just hangs) with ghc 9.2.4?
by Doug Burke 06 Sep '22

06 Sep '22

I have noticed I can't run one of my tests when building with ghc 9.2.4 (tried via stack and nix) that doesn't happen with ghc 9.2.3 (or older versions). Is there a way to diagnose the problem (so I can look at the ghc bug tracker or try and make the code smaller for testing)? I can see this behavior with the following reproducer (it's a bit heavyweight at the moment!): % git clone https://gitlab.com/dburke/swish temp % cd temp Added to get the timings, but it's not strictly necessary: % sed -i -e "s/-Wall /-Wall -ddump-timings /" swish.cabal Now try to build and run the test. The following build and run the test quickly if using an older GHC (e.g. "--resolver lts" for the stack case or "--argstr compiler ghc923" for the nix case). First with stack % sed -i -e "s/-Wall /-Wall -ddump-timings /" swish.cabal % stack test --resolver nightly-2022-09-05 :test-rdfproof Stack has not been tested with GHC versions above 9.0, and using 9.2.4, this may fail Stack has not been tested with Cabal versions above 3.4, but version 3.6.3.0 was found, this may fail swish> configure (lib + test) Configuring swish-0.10.2.0... swish> build (lib + test) Preprocessing library for swish-0.10.2.0.. Building library for swish-0.10.2.0.. Preprocessing test suite 'test-rdfproof' for swish-0.10.2.0.. Building test suite 'test-rdfproof' for swish-0.10.2.0.. *** initializing unit database: initializing unit database: alloc=7350056 time=8.753 *** initializing unit database: initializing unit database: alloc=3999144 time=16.194 *** Chasing dependencies: *** systool:cpp: systool:cpp: alloc=271104 time=1.991 Chasing dependencies: alloc=10233768 time=8.400 [2 of 2] Compiling Main *** Parser [Main]: Parser [Main]: alloc=24346344 time=33.067 *** Renamer/typechecker [Main]: Renamer/typechecker [Main]: alloc=101896128 time=134.992 *** Desugar [Main]: Desugar [Main]: alloc=24628816 time=24.813 *** Simplifier [Main]: Simplifier [Main]: alloc=667236400 time=775.137 *** Specialise [Main]: Specialise [Main]: alloc=45057312 time=40.543 *** Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [Main]: Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [Main]: alloc=208806472 time=330.396 *** Simplifier [Main]: Simplifier [Main]: alloc=603245992 time=747.067 *** Simplifier [Main]: Simplifier [Main]: alloc=564322584 time=709.583 *** Simplifier [Main]: Simplifier [Main]: alloc=728039528 time=835.525 *** Float inwards [Main]: *** Called arity analysis [Main]: *** Simplifier [Main]: Float inwards [Main]: alloc=23720 time=0.017 Called arity analysis [Main]: alloc=25848 time=0.016 Progress 0/2 Now with nix % nix-shell --argstr compiler ghc924 ... wait an indeterminate amount of time % ghc --version The Glorious Glasgow Haskell Compilation System, version 9.2.4 % cabal test test-rdfproof Warning: The package list for 'hackage.haskell.org' is 19 days old. Run 'cabal update' to get the latest list of available packages. Resolving dependencies... Build profile: -w ghc-9.2.4 -O1 In order, the following will be built (use -v for more details): - swish-0.10.2.0 (lib) (first run) - swish-0.10.2.0 (test:test-rdfproof) (first run) Configuring library for swish-0.10.2.0.. Preprocessing library for swish-0.10.2.0.. Building library for swish-0.10.2.0.. [ 1 of 55] Compiling Data.Interned.URI [ 2 of 55] Compiling Data.Ord.Partial [ 3 of 55] Compiling Data.String.ShowLines [ 4 of 55] Compiling Network.URI.Ord [ 5 of 55] Compiling Swish.GraphClass ... ... a lot more, including some annoying non-exhaustive patterns I don't know how to fix ... but that's for a different post ... [55 of 55] Compiling Swish Configuring test suite 'test-rdfproof' for swish-0.10.2.0.. Preprocessing test suite 'test-rdfproof' for swish-0.10.2.0.. Building test suite 'test-rdfproof' for swish-0.10.2.0.. *** initializing unit database: initializing unit database: alloc=7389248 time=4.436 *** initializing unit database: initializing unit database: alloc=4001312 time=11.992 *** Chasing dependencies: *** systool:cpp: systool:cpp: alloc=319464 time=0.520 Chasing dependencies: alloc=12863280 time=6.581 [1 of 2] Compiling TestHelpers ( tests/TestHelpers.hs, /home/dburke/rdf/temp/dist-newstyle/build/x86_64-linux/ghc-9.2.4/swish-0.10.2.0/t/test-rdfproof/build/test-rdfproof/test-rdfproof-tmp/TestHelpers.o ) *** Parser [TestHelpers]: Parser [TestHelpers]: alloc=5469952 time=2.325 *** Renamer/typechecker [TestHelpers]: Renamer/typechecker [TestHelpers]: alloc=94049744 time=106.001 *** Desugar [TestHelpers]: Desugar [TestHelpers]: alloc=5551840 time=2.974 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=45720248 time=28.537 *** Specialise [TestHelpers]: Specialise [TestHelpers]: alloc=2198344 time=0.717 *** Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [TestHelpers]: Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [TestHelpers]: alloc=6183280 time=3.109 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=27272104 time=16.042 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=20805544 time=12.332 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=6175584 time=2.825 *** Float inwards [TestHelpers]: Float inwards [TestHelpers]: alloc=26272 time=0.012 *** Called arity analysis [TestHelpers]: Called arity analysis [TestHelpers]: alloc=28392 time=0.012 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=14755744 time=7.017 *** Demand analysis [TestHelpers]: Demand analysis [TestHelpers]: alloc=2061096 time=1.296 *** Constructed Product Result analysis [TestHelpers]: Constructed Product Result analysis [TestHelpers]: alloc=466968 time=0.197 *** Worker Wrapper binds [TestHelpers]: Worker Wrapper binds [TestHelpers]: alloc=436552 time=0.201 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=31897488 time=18.652 *** Exitification transformation [TestHelpers]: Exitification transformation [TestHelpers]: alloc=29808 time=0.013 *** Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = True}) [TestHelpers]: Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = True}) [TestHelpers]: alloc=5508568 time=4.009 *** Common sub-expression [TestHelpers]: Common sub-expression [TestHelpers]: alloc=27896 time=0.013 *** Float inwards [TestHelpers]: Float inwards [TestHelpers]: alloc=26272 time=0.021 *** Simplifier [TestHelpers]: Simplifier [TestHelpers]: alloc=24835440 time=15.291 *** Demand analysis [TestHelpers]: Demand analysis [TestHelpers]: alloc=2214560 time=1.044 *** CoreTidy [TestHelpers]: CoreTidy [TestHelpers]: alloc=2814672 time=1.457 *** CorePrep [TestHelpers]: CorePrep [TestHelpers]: alloc=1965920 time=2.636 *** CoreToStg [TestHelpers]: CoreToStg [TestHelpers]: alloc=3134560 time=1.484 *** CodeGen [TestHelpers]: CodeGen [TestHelpers]: alloc=80232584 time=46.410 *** WriteIface [/home/dburke/rdf/temp/dist-newstyle/build/x86_64-linux/ghc-9.2.4/swish-0.10.2.0/t/test-rdfproof/build/test-rdfproof/test-rdfproof-tmp/TestHelpers.hi]: WriteIface [/home/dburke/rdf/temp/dist-newstyle/build/x86_64-linux/ghc-9.2.4/swish-0.10.2.0/t/test-rdfproof/build/test-rdfproof/test-rdfproof-tmp/TestHelpers.hi]: alloc=1780688 time=0.766 *** systool:as: systool:as: alloc=137200 time=0.360 [2 of 2] Compiling Main ( tests/RDFProofTest.hs, /home/dburke/rdf/temp/dist-newstyle/build/x86_64-linux/ghc-9.2.4/swish-0.10.2.0/t/test-rdfproof/build/test-rdfproof/test-rdfproof-tmp/Main.o ) *** Parser [Main]: Parser [Main]: alloc=25235720 time=8.851 *** Renamer/typechecker [Main]: Renamer/typechecker [Main]: alloc=58415520 time=45.291 *** Desugar [Main]: Desugar [Main]: alloc=22098688 time=46.709 *** Simplifier [Main]: Simplifier [Main]: alloc=654052760 time=511.390 *** Specialise [Main]: Specialise [Main]: alloc=44439912 time=34.132 *** Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [Main]: Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) [Main]: alloc=208317448 time=252.154 *** Simplifier [Main]: Simplifier [Main]: alloc=601002912 time=546.343 *** Simplifier [Main]: Simplifier [Main]: alloc=564371608 time=546.970 *** Simplifier [Main]: Simplifier [Main]: alloc=726902400 time=613.423 *** Float inwards [Main]: Float inwards [Main]: alloc=23720 time=0.024 *** Called arity analysis [Main]: Called arity analysis [Main]: alloc=25856 time=0.013 *** Simplifier [Main]: At this point my laptop just sits there making whooshing noises as if it's trying to become an aeroplane, but it never gets to where it's going (to mix up my metaphors). Any help would be appreciated, Doug

2 2

Getting a breakdown of time spend in compile phases
by rowan goemans 04 Sep '22

04 Sep '22

Dear Cafe, I have a Haskell Project where I have a module that quite heavily makes use of constraints and takes ages to compile per module. It also uses some type checker plugins but I'm unsure if they are causing the slowness. So what I would like to see is a breakdown of how much time GHC is spending on compilation of a module. Does something like this exist? Best regards, Rowan Goemans

5 6

[ANN] xmonad and xmonad-contrib 0.17.1 are available
by Tony Zorman 03 Sep '22

03 Sep '22

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ XMONAD AND XMONAD-CONTRIB 0.17.1 ARE AVAILABLE ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ New versions of xmonad and xmonad-contrib have been released. Check out our [download page] for instructions on where to get them. About 10 months after the big release of 0.17.0, we—as promised—picked up the pace a bit and are back with a new minor version; don't let that fool you though, this one still packs a punch! Plus, we now sport a brand-new [logo], courtesy of [Hans Heintze]. As this is a minor release, we tried to keep the breaking changes to a minimum (xmonad core does not have a single one!) However, some were unavoidable for `xmonad-contrib', so be sure to at least glance at the [release notes]! For help getting started—or more info—see [our website] and [talk to us]! If you like what we do, you can support us on [Open Collective] or via [GitHub Sponsors]. Thanks! [GitHub Sponsors] <https://github.com/sponsors/xmonad> [Hans Heintze] <https://github.com/literallyunplayable> [Open Collective] <https://opencollective.com/xmonad> [download page] <https://xmonad.org/download.html> [logo] <https://xmonad.org/images/logo.svg> [our website] <https://xmonad.org/> [release notes] See section 2 [talk to us] <https://xmonad.org/community.html> 1 xmonad 0.17.1 ═══════════════ This release includes 32 non-merge commits by 6 contributors! For a full summary of all the changes, see [xmonad's CHANGES.md] file. [xmonad's CHANGES.md] <https://github.com/xmonad/xmonad/blob/v0.17.1/CHANGES.md> 1.1 Enhancements ──────────────── • Added custom cursor shapes for resizing and moving windows. 1.2 Bug Fixes ───────────── • Change the main loop to try to avoid [GHC bug 21708] on systems running GHC 9.2 up to version 9.2.3. The issue has been fixed in [GHC 9.2.4] and all later releases. • Fixed border color of windows with alpha channel. Now all windows have the same opaque border color. [GHC bug 21708] <https://gitlab.haskell.org/ghc/ghc/-/issues/21708> [GHC 9.2.4] <https://discourse.haskell.org/t/ghc-9-2-4-released/4851> 2 xmonad-contrib 0.17.1 ═══════════════════════ This release includes 212 non-merge commits by 32 contributors! For a full summary of all the changes, see [xmonad-contrib's CHANGES.md] file. [xmonad-contrib's CHANGES.md] <https://github.com/xmonad/xmonad-contrib/blob/v0.17.1/CHANGES.md> 2.1 Breaking Changes ──────────────────── • `XMonad.Config.{Arossato,Dmwit,Droundy,Monad,Prime,Saegesser,Sjanssen}': deprecated all of these modules. The user-specific configuration modules may still be found [on the website]. • `XMonad.Util.NamedScratchpad': scratchpads are now only based on the argument given to `namedScratchpadManageHook'; all other scratchpad arguments are, while still present, ignored. Users passing all of their scratchpads to functions like `namedScratchpadAction' (as is shown in the module's documentation) should /not/ notice any difference in behaviour. • `XMonad.Util.DynamicScratchpads': deprecated the module; use the new dynamic scratchpad functionality of `XMonad.Util.NamedScratchpad' instead. • `XMonad.Hooks.UrgencyHook': deprecated `urgencyConfig'; use `def' from the new `Default' instance of `UrgencyConfig' instead. [on the website] <https://xmonad.org/configurations.html> 2.2 New Modules ─────────────── • `XMonad.Hooks.Modal': a module implementing modal keybindings for XMonad. • `XMonad.Layout.SideBorderDecoration': this module allows for having a configurable border position around windows; i.e., it can move the border to either cardinal direction. • `XMonad.Actions.PerLayoutKeys': a new module for customising keybindings on a per-layout basis. • `XMonad.Actions.RepeatAction': a module for adding a keybinding to repeat the last action, similar to Vim's `.' or Emacs's `dot-mode'. 2.3 Bug Fixes and Minor Changes ─────────────────────────────── • `XMonad.Prompt' and `XMonad.Actions.TreeSelect': added xft-based font fallback support. This may be used by appending other fonts to the given string: `xft:iosevka-11,FontAwesome-9'. Note that this requires `xmonad-contrib' to be compiled with `X11-xft' version 0.3.4 or higher. • `XMonad.Util.Run': added an EDSL—particularly geared towards programs like terminals or Emacs—to spawn processes from XMonad in a compositional way. • `XMonad.Util.Hacks': added `trayerPaddingXmobarEventHook' (plus generic variants for other trays/panels) to communicate trayer resize events to xmobar so that padding space may be reserved on xmobar for the tray. Requires `xmobar' version 0.40 or higher. • `XMonad.Prompt.OrgMode': added the ability to specify alphabetic (`#A', `#B', and `#C') [priorities] at the end of the input note. • `XMonad.Actions.Submap': added `visualSubmap' to visualise the available keys and their actions when inside a submap. • `XMonad.Util.NamedScratchpad': added support for dynamic scratchpads in the form of `dynamicNSPAction' and `toggleDynamicNSP'. • `XMonad.Hooks.WindowSwallowing': fixed windows getting lost when used in conjunction with `smartBorders' and a single window. [priorities] <https://orgmode.org/manual/Priorities.html> -- Tony Zorman | https://tony-zorman.com/

1 0

Re: [Haskell-cafe] selectively allow alternatives in a sum type
by Olaf Klinke 02 Sep '22

02 Sep '22

> Trees that grow is essentially this, but using type families. > > data Foo ksi > = LeftFoo !(XLeftFoo ksi) !A > | RightFoo !(XRightFoo ksi) !B > > type family XLeftFoo ksi :: Type > type family XRightFoo ksi :: Type > > Then you can define > > data Both > type instance XLeftFoo Both = () > type instance XRightFoo Both = () > > or > > data OnlyLeft > type instance XLeftFoo OnlyLeft = () > type instance XRightFoo OnlyLeft = Void > > --- > > Third option is to simply have parametrized data: > > data Foo b > = LeftFoo !A > | RIghtFoo !b > > type FooBoth = Foo B > type FooOnlyLeft = Foo Void > > --- > > Sometimes I prefer a higher-kinded data approach, especially if there is > very little variants needed, and they are "uniform" (e.g. second variant > doesn't have some fields). > Yet, sometimes simple parameterized data is simplest approach > (especially as you get stuff for free by deriving Traversable!). > > On the other hand, if type is big and have many uniform extension points > (even if there are few different combinations), then HKD becomes > boilerplate heavy as well. > The drawback of TTG, is that writing polymorphic code (i.e. which work > for any or some `ksi`s) is not very fun: a lot of equality constraints etc. > > - Oleg So I re-discovered Trees that Grow sans the trick of using type families to name particular combinations of parameters. Hooray Najd, and thanks Oleg for bringing this up. Olaf

5 6

ANN: hledger 1.27
by Simon Michael 01 Sep '22

01 Sep '22

I'm pleased to announce hledger 1.27 ! https://github.com/simonmichael/hledger/releases/1.27 https://hledger.org/install https://hledger.org/release-notes.html#hledger-1-27 Highlights include inferring costs from equity postings, new error checks, and improved error messages. Thank you to release contributors Stephen Morgan, Alex Hirzel, Pranesh Prakash, David D Lowe, Charlotte Van Petegem, Max Thomas, Andrew Lelechenko. What is hledger ? - Fast, reliable, free, multicurrency, double-entry, plain text accounting[1] software that runs on unix, mac, windows, and the web - Built around human-readable, version-controllable plain text files - Inspired by and largely compatible with Ledger CLI[2]; convertible to and from Beancount[3] - Written in Haskell for correctness and longevity. For help getting started, or more info, see https://hledger.org and join our chat via Matrix or IRC: https://hledger.org/support Newcomers, experts, contributors, sponsors, feedback are welcome! Aloha, -Simon [1] https://plaintextaccounting.org [2] https://ledger-cli.org [3] https://beancount.github.io

1 0

STATUS_DLL_NOT_FOUND from HLS 1.7 on Windows 10/11
by J. Garrett Morris 31 Aug '22

31 Aug '22

Dear cafe, A few of my students have encountered a problem running HLS 1.7 on Windows 10/11. Their Haskell installations mostly seem okay---everything installed by `ghcup` (1.8) , and `cabal` (3.6.2) and `ghc` (9.2.2) work as expected. However, when VS Code (via the Haskell plugin) attempts to start the language server, it exits repeatedly with error STATUS_DLL_NOT_FOUND (or its signed integer equivalent). Has anyone encountered a configuration that leads to this problem before? Most of the students are not having this problem (nor am I, on similar software configurations), so I suspect it's a consequence of something else they have installed. Thanks, /g -- Prosperum ac felix scelus virtus vocatur -- Seneca

1 0

Re: [Haskell-cafe] selectively allow alternatives in a sum type
by Olaf Klinke 31 Aug '22

31 Aug '22

> Dear Café, > > Is there prior art/existing packages for the following? Is it maybe functional programming folklore? Is it a sign of bad program design? > Sometimes I feel the need to selectively allow or disallow alternatives > in a sum type. That is, suppose we have a sum type > > data Foo = LeftFoo !A | RightFoo !B > > and at some places in the program we want the type system to enforce > that only the constructor LeftFoo can be used. My solution would be to > make the type higher rank: > > data Foo' f = LeftFoo' !A | RightFoo' !(f B) > type Foo = Foo' Identity > type LeftFoo = Foo' (Const' Void) -- can not construct a RightFoo' > > The advantage over defining LeftFoo as an entirely different type is > that Foo and LeftFoo can share functions operating entirely on the left > option. > > Olaf Henning and Will both suggested accessor type classes. I am fond of my solution because it uses plain algebraic data types, no classes, GADTs or type-level lists. David, can you elaborate how this collides with Coercible? What surprised me is that when writing a function f :: LeftFoo -> r GHC did not warn me (-Wincomplete-patterns) about missing cases when f only uses the LeftFoo' pattern match. Hence the fact that RightFoo' :: Const Void B -> LeftFoo is the empty function must somehow be known to the compiler. Nice! Olaf

1 0

Package takeover request for fgl
by Troels Henriksen 30 Aug '22

30 Aug '22

I am requesting to take over the package fgl: https://hackage.haskell.org/package/fgl It is currently broken in GHC 9.4, which is fixed by this pull request: https://github.com/haskell/fgl/pull/104 The maintainer Ivan Miljenovic has not been active on GitHub since January. I wrote Ivan on August 12th offering to help out with maintenance, but have received no response yet. The package is part of the 'haskell' organisation on GitHub. I don't know whether that is supposed to signify some kind of "community maintenance" (it appears Ivan is not the original author of fgl), but I would eventually need Hackage upload rights as well.

2 1

selectively allow alternatives in a sum type
by Olaf Klinke 30 Aug '22

30 Aug '22

Dear Café, Is there prior art/existing packages for the following? Is it maybefunctional programming folklore? Is it a sign of bad program design? Sometimes I feel the need to selectively allow or disallow alternatives in a sum type. That is, suppose we have a sum type data Foo = LeftFoo !A | RightFoo !B and at some places in the program we want the type system to enforce that only the constructor LeftFoo can be used. My solution would be to use a strict version of Data.Functor.Const and make the type higher rank: newtype Const' a b = Const' !a -- Const' Void b ~ Void -- Const' () b ~ () data Foo' f = LeftFoo' !A | RightFoo' !(f B) type Foo = Foo' Identity type LeftFoo = Foo' (Const' Void) -- can not construct a RightFoo' The advantage over defining LeftFoo as an entirely different type is that Foo and LeftFoo can share functions operating entirely on the left option. Olaf

6 6