- Haskell-Cafe - Haskell.org

ANN: Copilot 3.10
by Ivan Perez 26 Jul '22

26 Jul '22

Dear all, We are very happy to announce the release of Copilot 3.10. Copilot is a runtime verification system implemented as a Haskell DSL that generates hard-realtime C99. You can learn more about it at [1]. This new version of Copilot contains a small but important change in how structs are handled in C functions invoked by the monitors when property violations are detected. This change is API-breaking, so users of Copilot may need to adapt their systems accordingly. The release also contains a number of bug fixes, provides a simplified API, deprecates outdated elements, removes unused code, and relaxes version constraints for dependencies. 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] applications) from requirements in structured natural language. We'd like to take this opportunity to welcome Will Pogge to the team with his first commit, and thank the Galois team for their contributions. We also want to thank everyone who uses and helps promote Copilot; we are seeing increased attention, and gave three talks in the last two months at JPL, USC, and VCU, with two more taking place this month. 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/14?closed=1 [3] https://github.com/nasa/ogma [4] https://cfs.gsfc.nasa.gov/

4 7

Munich Haskell Meeting, 2022-07-28 @ 19:30
by Leah Neukirchen 25 Jul '22

25 Jul '22

Dear all, This week, our monthly Munich Haskell Meeting will take place again on Thursday, July 28 at Hirschgarten (Biergarten, self-service area) at 19h30. For details see here: http://muenchen.haskell.bayern/dates.html Please sign up here if you are coming so we'll look out for you. https://dudle.inf.tu-dresden.de/haskell-munich-jul-2022/ Everybody is welcome! cu, -- Leah Neukirchen <leah(a)vuxu.org> https://leahneukirchen.org/

1 0

Re: [Haskell-cafe] [ANNOUNCE] GHC 9.4.1-rc1 is now available
by Ben Gamari 24 Jul '22

24 Jul '22

George Colpitts <george.colpitts(a)gmail.com> writes: > +Kazu Yamamoto <kazu(a)iij.ad.jp> > > Hi Ben > > My 2 machines also have: > > $ spctl --status > assessments enabled > Hmm, interesting. Then I am truly perplexed. > Speculations: > > /usr/local/lib/ghc-9.4.0.20220721/bin/../lib/x86_64-osx-ghc-9.4.0.20220721/libHSterminfo-0.4.1.5-ghc9.4.0.20220721.dylib > is created after xattr -rc . was run so it doesn't have the necessary > attributes. Is it possible that ghc developers and/or the test machines > have this file on another of the paths in the error message and that is why > it works for them? > I'm not sure where this would be but at this point anything is possible. What happens if you try to install to do something like (in the extracted binary distribution), $ ./configure --prefix=`pwd`/tmp $ make install # this will fail $ xattr -rc . $ make install # perhaps this will finish successfully? # tmp/bin/ghc --version # GHC should be usable > I hope I didn't offend you by asking if the fix had been tested; I assume > it had been but I thought it was important to rule that out. > Not to worry; it's a very reasonable question to ask given the circumstances. > More than happy to test. I really appreciate all the work you and others > have put into GHC ! > Ultimately I think we may just need to bite the bullet and start properly notarising/codesigning releases (resolving #17418). At this point we have spent more time trying to avoid the notarisation requirement than it would likely take to satisfy it. Unfortunately, this will require that I find an Apple device somewhere which may take a few weeks. I'm afraid I am on holiday next week but I would quite grateful if we could arrange for a chat after I return such that we can debug this in realtime. Cheers, - Ben

1 0

Re: [Haskell-cafe] [ANNOUNCE] GHC 9.4.1-rc1 is now available
by Ben Gamari 23 Jul '22

23 Jul '22

George Colpitts <george.colpitts(a)gmail.com> writes: > Hi Ben > > /ust/bin/xattr exists on my machine. Running "xattr -rc ." manually does > not fix the bug as noted at the start of 21506. It was sufficient in the > past but no longer fixes this error. As noted farther down in 21506 > > the workaround given in #17418 </ghc/ghc/-/issues/17418> no longer works. > It did not work in 9.2.2 either. The current workaround is similar to what > Kazu explained in > https://twitter.com/kazu_yamamoto/status/1500643489985761282 > > sudo xattr -rc . > > sudo spctl --global-disable > > ./configure > > sudo make install > > sudo spctl --global-enable > > It seems there are files created during sudo make install that have an > issue as xattr -rc . was never run on them. Perhaps this is related to > using Hadrian. Is it possible that the fix that was made was never tested? > I tested the change both manually and via CI on the hardware that I have access to; in both cases installing the binary distribution resulted in a functional compiler. However, given how the effects of SIP are essentially undocumented, it is very hard to know what variables may be at play here. Running spctl --status on the machine on which I tested claims: > spctl --status objc[48908]: Class SPExecutionPolicy is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class AppWrapper is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class AppWrapperPolicyResult is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class AppWrapperPolicy is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class SPLog is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class MIS is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class SPExecutionHistoryItem is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class SPExecutionPolicyItem is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class SPDeveloperPolicy is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. objc[48908]: Class GKScanResult is implemented in both /System/Library/PrivateFrameworks/SystemPolicy.framework/Versions/A/SystemPolicy and /usr/sbin/spctl. One of the two will be used. Which one is undefined. assessments enabled Which to me suggests that SIP (which, I imagine, is responsible for #21506) is enabled. However, the lack of comprehensive documentation here makes it very hard to say with certainty what might differ between your machine and mine. Without more information I don't know how to proceed here. Perhaps someone (Moritz or Simon, perhaps) with more familiarity with macOS has some insight? Thanks for your help in testing, George! Cheers, - Ben

1 0

Re: [Haskell-cafe] [ANNOUNCE] GHC 9.4.1-rc1 is now available
by Ben Gamari 23 Jul '22

23 Jul '22

George Colpitts <george.colpitts(a)gmail.com> writes: > Hi Ben, > > I expected https://gitlab.haskell.org/ghc/ghc/-/issues/21506 (ghc-9.4.1-alpha1 > does not install on macos: ghc-pkg-9.4.0-20220501 cannot be opened because > the developer cannot be verified) to be fixed in rc1 but it is not. Are my > expectations wrong? What is the ETA for fixing it? > Thanks for letting us know, George. The fix that we have [1] is present in 9.4.1-rc1. If that commit doesn't resolve the issue then there is something that we don't understand. Does `/usr/bin/xattr` exist? Running `xattr -rc` manually on the binary distribution allow you to run the compiler? Cheers, - Ben [1] https://gitlab.haskell.org/ghc/ghc/-/commit/641972d65b476aac11424bde6c3bcfd…

1 0

An org backend to Haddock
by Yuchen Pei 21 Jul '22

21 Jul '22

Hello, I decided to write an Org backend to Haddock[1], so that haskell library documentation can be generated in org mode markup. Compared to the existing backends (html, latex and hoogle), the org format allows utilising features like the infinite levels of heading hierarchy, flexible folding / unfolding, cross-package linking, jumping to any declaration with org-goto and the endless potentials of emacs customisation. It seems to me most information and haskell language features one can find on displayed on hackage are supported by the org backend and included in the output org files, though there are still some rough edges and unsupported language features (like infix declarations and linear types) which I aim to fix. Some example output can be found at [2] (I will need to rename the "assets" part of the url as it is not accurate), including base[4], ghc-prim[5] and ghc-lib-parser[6] (I use it for reference of the GHC API as it is easier to build than GHC). For more information, check out the README file[3]. Given this is not the official version of haddock and my changes are in haddock-api, I'm calling it haddorg-api, for lack of a better name / approach. I'll be happy to contribute my changes upstream if a different license covering my contribution (AGPLv3+) is accepted. Let me know what you think. [1] https://g.ypei.me/haddock.git/tree/haddock-api [2] https://ypei.org/assets/haddorg-output/ [3] https://g.ypei.me/haddock.git/tree/haddock-api/README.org [4] https://ypei.org/assets/haddorg-output/base-4.16.1.0.org.gz [5] https://ypei.org/assets/haddorg-output/ghc-prim-0.8.0.org.gz [6] https://ypei.org/assets/haddorg-output/ghc-lib-parser-9.2.2.20220307.org.gz Best, Yuchen -- PGP Key: 47F9 D050 1E11 8879 9040 4941 2126 7E93 EF86 DFD0 <https://ypei.org/assets/ypei-pubkey.txt>

1 1

Postdoc Vacancy at St Andrews
by Christopher Brown 20 Jul '22

20 Jul '22

The Programming Languages Group at the University of St Andrews seeks a post-doctoral research fellow for a fixed 12-month position. Details of the position can be found here: https://www.vacancies.st-andrews.ac.uk/Vacancies/W/4238/0/352367/889/resear… Vacancy Description School of Computer Science Salary: £34,304 per annum Start date: 1 October 2022 or as soon as possible thereafter Fixed-term: 12 months Applications are sought for a committed Post-doctoral Research Fellow to work with Dr Chris Brown conducting research for a EPSRC funded project entitled Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems. The primary duties will be to implementing refactorings for target languages such as C; proving general soundness of the refactorings using e.g. dependent types; developing new programming abstractions (skeletons) for abstracting common energy-reducing programming patterns; running experiments; writing proofs of correctness. The successful applicant will have (or be near to completion of) a PhD in Programming Languages with expertise in formal semantics of programming languages, compilers, program transformation, lightweight formal methods (including, e.g. dependent types) and/or knowledge of parallelism and non-functional properties, including energy. The post is available on a fixed-term basis for 12 months starting 1st October or as soon as possible thereafter. Further details of the project can be found by contacting Dr Christopher Brown (cmb21(a)st-andrews.ac.uk<mailto:cmb21@st-andrews.ac.uk>). Applications are particularly welcome from women, people from the Black, Asian and Minority Ethnic (BAME) community, and other protected characteristics who are under-represented in research posts at the University. Equality, diversity and inclusion are at the heart of the St Andrews experience. We strive to create a fair and inclusive culture demonstrated through our commitment to diversity awards (Athena Swan, Carer Positive, LGBT Charter, Race Charters and Stonewall). We celebrate diversity by promoting profiles of BAME, LGBTIQ+ staff and supporting networks including the Staff BAME Network; Staff with Disabilities Network; Staff LGBTIQ+ Network; and the Staff Parents & Carers Network. Full details available online: https://www.st-andrews.ac.uk/hr/edi/ Closing Date: 29 July 2022 Interview Date: 23 August 2022 Please quote ref:AR2699GB School of Computer Science Salary: £34,304 per annum Start date: 1 October 2022 or as soon as possible thereafter Fixed-term: 12 months

1 0

Re: [Haskell-cafe] An org backend to Haddock
by Yuchen Pei 19 Jul '22

19 Jul '22

On Tue 2022-07-19 21:58:26 +0800, Ihor Radchenko wrote: > Yuchen Pei <id(a)ypei.org> writes: > >> Given this is not the official version of haddock and my changes are in >> haddock-api, I'm calling it haddorg-api, for lack of a better name / >> approach. I'll be happy to contribute my changes upstream if a >> different license covering my contribution (AGPLv3+) is accepted. >> >> Let me know what you think. > > I am pretty sure that you are asking the Haskell people for upstreaming > ;) Yes - I sent the email to both haskell-cafe and emacs-orgmode, but upstream here means haddock / haddock-api indeed, thanks for clarifying. > > From Org side, it is always welcome when other Free software projects > are making use of Org. > > Also, I looked into > https://g.ypei.me/haddock.git/tree/haddock-api/src/Haddock/Backends/Org/Typ… > > Beware of possible edge cases with "*/~|" in formatting. I am not > sure if text containing such symbols is possible as an input for your > library, but if it is, things may get formatted wrongly. > > For example, text containing "|" anywhere inside a table field must have > "|" escaped using \vert entity. The markup can be escaped using > zero-width space. True. I have not addressed these edge cases in my code, except a quick hack to prepend a space whenever any line a src block / result block has a leading star. Tables on the other hand are extremely rare in Haskell package documentation strings, and having a | in them is even rarer. I do wonder what is the best way to handle cross-package links. Currently I'm using CUSTOM_ID in the format of package-name-x.y.z.Module.Name.IdentifierName, as well as Module.Name.IdentifierName. But this is a "one big org file" approach, and can make navigation slow when say the org file reaches 15+MB in size. Ideally one should be able to navigate the a hackage worth of documentations easily, with working cross-package links and low latency org-goto to jump to any identifier or module, but I don't see how to achieve that. To be further investigated. > > Best, > Ihor Best, Yuchen -- PGP Key: 47F9 D050 1E11 8879 9040 4941 2126 7E93 EF86 DFD0 <https://ypei.org/assets/ypei-pubkey.txt>

1 0

2nd CFP - IFL22 - The 34th Symposium on Implementation and Application of Functional Languages
by Pieter Koopman 15 Jul '22

15 Jul '22

*CALL FOR PAPERS: * The 34th Symposium on Implementation and Application of Functional Languages (IFL 2022) *Submission and registration are open.* See https://ifl22.github.io/. Copenhagen, August 31st-September 2nd, 2022 *Important dates * Draft paper submission: August 7th, 2022 Draft paper notification: August 9th, 2022 Early registration deadline: August 12th, 2022 Late registration deadline: September 2nd, 2022 Symposium: August 31st-September 2nd, 2022 (3 days) *Scope * The goal of the IFL symposia is to bring together researchers actively engaged in the implementation and application of functional and function-based programming languages. IFL 2022 will be a venue for researchers to present and discuss new ideas and concepts, work in progress, and publication-ripe results related to the implementation and application of functional languages and function-based programming. Topics of interest to IFL include, but are not limited to: * language concepts * type systems, type checking, type inferencing * compilation techniques * staged compilation * run-time function specialization * run-time code generation * partial evaluation * abstract interpretation * metaprogramming * generic programming * automatic program generation * array processing * concurrent/parallel programming * concurrent/parallel program execution * embedded systems * web applications * embedded domain specific languages * security * novel memory management techniques * run-time profiling performance measurements * debugging and tracing * virtual/abstract machine architectures * validation, verification of functional programs * tools and programming techniques * industrial applications *Submissions and peer-review * Following IFL tradition, IFL 2022 will use a post-symposium review process to produce the formal proceedings. Before the symposium authors submit draft papers. These draft papers will be screened by the program chair to make sure that they are within the scope of IFL. The draft papers will be made available to all participants at the symposium. Each draft paper is presented by one of the authors at the symposium. Notice that it is a requirement that accepted draft papers are presented physically at the symposium. After the symposium, a formal review process will take place, conducted by the program committee. Reviewing is single blind. There will be at least 3 reviews per paper. The reviewers have 6 weeks to write their reviews. For the camera-ready version the authors can make minor revisions which are accepted without further reviewing. Contributions submitted for the draft paper deadline must be between two and twelve pages long. For submission details, please consult the IFL 2022 website at https://ifl22.github.io/. *Where * IFL 2022 will be held physically in Copenhagen, Denmark, arranged by DIKU at the University of Copenhagen. See the IFL 2022 website at https://ifl22.github.io/ for more information. [image: beacon]

1 0

What is the exponential version of dependently-typed Vector and Tensor?
by Johannes Riecken 15 Jul '22

15 Jul '22

I noticed that the definitions of Vector and Tensor have a parallel structure. Vector is an ornamentation of the Peano natural numbers, and Tensor is the parallel construction with multiplication and the multiplicative identity, except that the factors are stored in a list instead of directly multiplying, so that the dependent typing can ensure that the number of elements in the tensor is indeed equal to the product of these factors. (To make it more parallel, the Nat in Vector could be replaced with a list of ones.) ```haskell {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} import GHC.TypeLits import Data.Kind import Numeric.Natural import Data.Proxy data Vector (n :: Nat) a where Nil :: Vector 0 a Cons :: a -> Vector n a -> Vector (n + 1) a data Tensor :: forall n. Vector n Nat -> Type -> Type where Scalar :: a -> Tensor Nil a Dimension :: Vector n (Tensor d a) -> Tensor (Cons n d) a ``` That made me wonder what the exponential version with functions would look like and if that is a useful concept, too, or one that also exists in maths? As going from Vector to Tensor isn't completely mechanical, I had trouble figuring out myself how to go from Tensor to the next higher data structure. Cheers, Johannes

1 0