- Haskell-Cafe - Haskell.org

F-IDE 2021 - Call for Papers
by Andrei Paskevich 19 Oct '20

19 Oct '20

****************************************************************** F-IDE 2021: 6th Workshop on Formal Integrated Development Environment Affiliated with NASA Formal Methods 2021 May 24-28, 2021 -- held online https://cister-labs.pt/f-ide2021 ****************************************************************** Important Dates * Abstract submission: Mon, Feb 22, 2021 * Full paper submission: Mon, Mar 1, 2021 * Notification: Mon, Apr 19, 2021 * Camera-ready: Mon, May 3, 2021 * Workshop: May 24-28, 2021 Overview High levels of safety, security, and privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language and/or an environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process. Topics The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis, and documentation. It welcomes the presentation of tools, methods, techniques, and experiments. Topics of interest include, but are not limited to, the following: * F-IDE building: design and integration of languages, development of user-friendly front-ends * How to make high-level logical and programming concepts palatable to industrial developers * Integration of object-oriented and modularity features * Integration of static analyzers * Integration of automated proof tools, theorem provers, and testing tools * Documentation tools * Impact of tools on certification * Experience reports on developing F-IDEs * Experience reports on using F-IDEs * Experience reports on formal methods-based assessments in industrial applications Submission Guidelines We accept both long (15 pages) and short (6 pages) paper submissions. The page limit does not include the bibliography. Submitted papers must present original contributions whose main results and conclusions have not been published or submitted elsewhere. Each submission will be reviewed by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the workshop. Submitted papers must be written in English and follow the EPTCS LaTeX format (http://style.eptcs.org) Authors are invited to submit the following types of contributions: * Research papers providing new concepts and results * Experience reports * Position papers and research perspectives * Tool presentations Papers should be submitted via EasyChair at F-IDE 2021's workshop page: https://easychair.org/conferences/?conf=f-ide2021. Preliminary proceedings will be made available in electronic form at the workshop. Post-proceedings will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Program Committee * Andrew Reynolds, University of Iowa, USA * Bernhard Rumpe, RWTH Aachen University, Germany * Carlo A. Furia, Chalmers University of Technology, Sweden * César Muñoz, NASA Langley, USA * Cinzia Bernardeschi, University of Pisa, Italy * Claudio Sacerdoti Coen, University of Bologna, Italy * Enrico Tassi, Inria, France * François Pessaux, ENSTA ParisTech, France * José Creissac Campos, University of Minho, Portugal * Kenneth Lausdahl, Aarhus University, Denmark * Laurent Voisin, Systerel, France * Lucas Wagner, Collins Aerospace, USA * Makarius Wenzel, sketis.net * Markus A. Kuppe, Microsoft Research, USA * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Pierre-Yves Strub, LIX, École Polytechnique, France * Rosemary Monahan, Maynooth University, Ireland * Silvia Lizeth Tapia Tarifa, University of Oslo, Norway * Simão Melo de Sousa, Universidade Beira Interior, Portugal * Stefan Mitsch, Carnegie Mellon University, USA * Stephan Merz, Inria, France * Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay, France * Yannick Moy, AdaCore, France * Yi Zhang, Massachusetts General Hospital, USA PC Chairs * Andrei Paskevich, Université Paris-Saclay, France * José Proença, CISTER/ISEP, Portugal Steering Committee * Catherine Dubois, Samovar, ENSIIE, France * Paolo Masci, US National Institute of Aerospace (NIA), USA * Dominique Méry, LORIA, Université de Lorraine, France

1 0

Need help to get started
by tech＠jimtyrerrobotics.ca 18 Oct '20

18 Oct '20

hello, I'm an industrial robot tech and the code I write seems to be composed of 99% side-effects ;-) That's the big dumb ones bolted to the floor that make cars and stuff. Decades of imperative sequence coding seem to have fossilized something in my brain. Trying to teach myself Haskell and going nowhere very slowly. Spent the last 8 weeks slowly plodding through "Real World Haskell" and "Learn you a Haskell" with the intention of re-writing a bash script in Haskell. I've normally learned programming by writing something I need instead of tutorials with which I seem to have an attention deficit problem. I use Linux for work and have written a bash script that uses bc and heredocs to write an .adoc file and then calls asciidoctor-pdf to generate an invoice. It's about 90 lines so I am not a scripting pro either. So typing './invoice Wk38' rolls a file called Wk38-of-2020-Invoice.pdf to send to clients. It was while writing this script that I stumbled upon pandoc and then Haskell. And that's where the trouble started. Tha abstraction and macro-approach of Haskell could provide a whole bag of tools for maintaining code (text files) on lines of multiple robots. About the existing script: I write plain text files on my phone that look like this: 14 Sep 0745 1600 Foo y 15 Sep 0815 1500 Foo y 16 Sep 0745 1400 Foo y 17 Sep 0745 1430 Foo y 18 Sep 0745 1400 Foo y and this one is called Wk38 and the fields are: |Date|Time In|Time Out|Proj|Lunch. Then I email it to myself and run the script. So I would be very grateful if someone could write some code for me and put my bootstraps in my fumbling hands: Get the name of the Wkxx file from the command line when running a Haskell standalone executable. fileName <- getArgs Load the lines of the file into a list of list of String[[]]. (or a better way?) lines <- fmap Text.lines (Text.readFile fileName) Recurse through each line of the list(s) and: *: Construct a date::String from the first two fields. (just a string, does not need a real "Date") *: Calc dailyElapsedTime::Double from difference between fields 4 and 3. *: Subtract 0.5hr lunch from dailyElapsedTime if field 6 == "y" *: Add dailyElapsedTime to accumlatedWeekTime::Double. *: Charge = If accumlatedWeekTime < 40hrs then multiply by rate1 *: elseif accumlatedWeekTime > 40hrs then multiply by rate2 *: Append |Date|Time In|Time Out|Charge|Project| to adoc file. If I could load it into ghci and step through it the lights may come on. Thanks very much Noodles

4 3

Re: [Haskell-cafe] ANN: stack-2.5.1
by waldmann 17 Oct '20

17 Oct '20

> Doesn't compile for me GHC 8.10.2 when building using cabal [...] for stack-2.5.0.1, this worked: cabal install --constraint 'base16-bytestring==0.1.1.7' --constraint 'optparse-applicative==0.15.1.0' https://github.com/commercialhaskell/stack/issues/5298#issuecomment-7023387… NB : seems to me there's a whole recent-social-history-of-haskell essay waiting to be written around that question (build 'stack' with 'cabal'). - J.W.

1 0

ANN: stack-2.5.1
by Emanuel Borsboom 15 Oct '20

15 Oct '20

See https://haskellstack.org/ for installation and upgrade instructions. **Changes since v2.3.3** Major changes: * Add the `snapshot-location-base` yaml configuration option, which allows to override the default location of snapshot configuration files. This option affects how snapshot synonyms (LTS/Nightly) are expanded to URLs by the `pantry` library. * `docker-network` configuration key added to override docker `--net` arg Behavior changes: * File watching now takes into account specified targets, old behavior could be restored using the new flag `--watch-all` [#5310](https://github.com/commercialhaskell/stack/issues/5310) Other enhancements: * `stack ls dependencies json` now includes fields `sha256` and `size` for dependencies of `type` `archive` in `location`. [#5280](https://github.com/commercialhaskell/stack/issues/5280) * Build failures now show a hint to scroll up to the corresponding section [#5279](https://github.com/commercialhaskell/stack/issues/5279) * Customisable output styles (see `stack --help` and the `--stack-colors` option, and `stack ls stack-colors --help`) now include `info`, `debug`, `other-level`, `secondary` and `highlight`, used with verbose output. Bug fixes: * Fix `stack test --coverage` when using Cabal 3 * `stack new` now generates PascalCase'd module name correctly. [#5376](https://github.com/commercialhaskell/stack/issues/5376) * Connection issues to Casa server no longer cause builds to failure. Casa acts only as an optimizing cache layer, not a critical piece of infrastructure. * Fix modified time busting caches by always calculating sha256 digest during the build process. [#5125](https://github.com/commercialhaskell/stack/issues/5125) **Thanks to all our contributors for this release:** * Andrea Condoluci * Andreas Herrmann * Andres Schmois * Ariel D. Moya Sequeira * Brandon Chinn * Cheah Jer Fei * DerpyCrabs * Emanuel Borsboom * Felix Yan * Jannik Theiß * Jens Petersen * Junji Hashimoto * Kirill Zaborsky * Michael Snoyman * Mihai Maruseac * Mike Pilgrem * Niklas Hambüchen * Ondřej Slámečka * Piper McCorkle * Thomas Lopatic * tomjaguarpaw

2 1

Re: [Haskell-cafe] Overlapping instances: are functions and typeclass methods treated differently?
by Daniel Díaz 13 Oct '20

13 Oct '20

On Thu, Oct 8, 2020 at 2:12 PM Henning Thielemann < lemming(a)henning-thielemann.de> wrote: > > On Thu, 8 Oct 2020, Daniel Díaz wrote: > > > But now consider this instance: > > > > > newtype Wrapper a = Wrapper (Maybe a) > > > instance Show a => Show (Wrapper a) where > > > show (Wrapper x) = show x > > > > This compiles just fine, despite—to my mind—suffering from the exact > same problem that the "foo" function had. > > Why does it work? > > There is an instance Show (Maybe a) in Prelude, but no instance Show > (Wrapper a), so no overlapping. Sorry, I wasn't very clear there. The problem is not with the "Show (Wrapper a)" instance itself, but with its implementation of "show". It depends (just as the function "foo" did) on "Show (Maybe a)", for which there are overlapping instances. And yet "foo" compiles without problem, while the typeclass method doesn't.

3 2

showing execution steps
by Luc Duponcheel 04 Oct '20

04 Oct '20

Hi, Is there a way to let ghci (or executable code generated by ghc) show all intermediate rewrite results when an expression is evaluated to its final result? Luc -- __~O -\ <, (*)/ (*) reality goes far beyond imagination

3 2

ghc-9 needs type declaration where ghc-8 didn't (with RankNTypes)
by Johannes Waldmann 02 Oct '20

02 Oct '20

Dear Cafe, and thanks, Georgi, for answering my previous question here's another difference I noticed (based on real code, but reduced to a minimal test case) GHCi, version 9.0.0.20200925: https://www.haskell.org/ghc/ :? for help Prelude> :set -XRankNTypes Prelude> let f :: (forall a . a -> ()) -> () ; f = g ; g x = undefined <interactive>:2:43: error: • Couldn't match type ‘p0’ with ‘forall a. a -> ()’ Expected: (forall a. a -> ()) -> () Actual: p0 -> () Cannot instantiate unification variable ‘p0’ with a type involving polytypes: forall a. a -> () • In the expression: g In an equation for ‘f’: f = g The declaration is accepted by ghc-8. For ghc-9, I have to give a type signature for g (copy that of f), or replace `f = g` with `f x = g x`. - J.W.

4 4

Novel error triggered building aeson on Mac
by Vanessa McHale 01 Oct '20

01 Oct '20

Hi all, I recently ran into the following interesting bug (reproducible on Mac; I used ghcup to install GHC and cabal-install): cabal unpack aeson-1.2.1.0 cabal build -w ghc-8.0.2 (yields this error log) Configuring library for aeson-1.2.1.0.. Preprocessing library for aeson-1.2.1.0.. Building library for aeson-1.2.1.0.. [ 1 of 23] Compiling Data.Attoparsec.Time.Internal ( attoparsec-iso8601/Data/Attoparsec/Time/Internal.hs, dist/build/Data/Attoparsec/Time/Internal.o ) [ 2 of 23] Compiling Data.Attoparsec.Time ( attoparsec-iso8601/Data/Attoparsec/Time.hs, dist/build/Data/Attoparsec/Time.o ) [ 3 of 23] Compiling Data.Aeson.Types.Internal ( Data/Aeson/Types/Internal.hs, dist/build/Data/Aeson/Types/Internal.o ) [ 4 of 23] Compiling Data.Aeson.Types.Generic ( Data/Aeson/Types/Generic.hs, dist/build/Data/Aeson/Types/Generic.o ) [ 5 of 23] Compiling Data.Aeson.Parser.UnescapePure ( pure/Data/Aeson/Parser/UnescapePure.hs, dist/build/Data/Aeson/Parser/UnescapePure.o ) [ 6 of 23] Compiling Data.Aeson.Parser.Unescape ( Data/Aeson/Parser/Unescape.hs, dist/build/Data/Aeson/Parser/Unescape.o ) [ 7 of 23] Compiling Data.Aeson.Parser.Time ( Data/Aeson/Parser/Time.hs, dist/build/Data/Aeson/Parser/Time.o ) [ 8 of 23] Compiling Data.Aeson.Parser.Internal ( Data/Aeson/Parser/Internal.hs, dist/build/Data/Aeson/Parser/Internal.o ) <command line>: can't load .so/.DLL for: /Users/vmchale/.cabal/store/ghc-8.0.2/lib/libHStm-lcl-cmpt-0.1.1.5-83154f89-ghc8.0.2.dylib (dlopen(/Users/vmchale/.cabal/store/ghc-8.0.2/lib/libHStm-lcl-cmpt-0.1.1.5-83154f89-ghc8.0.2.dylib, 5): REBASE_OPCODE_SET_SEGMENT_AND_OFFSET_ULEB has segment 2 which is not a writable segment (__LINKEDIT) in /Users/vmchale/.cabal/store/ghc-8.0.2/lib/libHStm-lcl-cmpt-0.1.1.5-83154f89-ghc8.0.2.dylib) Seems to be new; I guess the past libraries didn’t trigger it? I can’t tell if it’s a cabal-install bug, GHC bug, mac novelty… Cheers, Vanessa McHale

1 0

ghc-9 strictness annotations change?
by Johannes Waldmann 01 Oct '20

01 Oct '20

Dear Cafe, did something change w.r.t. placement of the bang? GHCi, version 9.0.0.20200925: https://www.haskell.org/ghc/ :? for help Prelude> data T = T { foo :: ! Int } <interactive>:1:21: error: Operator applied to too few arguments: ! Prelude> data T = T { foo :: !Int } Prelude> - J.W.

2 1

Re: [Haskell-cafe] I think I discovered my first Monoid instance
by David Banas 30 Sep '20

30 Sep '20

> > But we're talking about xor for the Word64 type, so it is slightly more > complicated to prove that it has a unit. Here's a proof in Agda: -- Agda proof that zero is the unit (i.e. - left and right identity) -- for the XOR operation. import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_) -- Binary data. data Bin : Set where ⟨⟩ : Bin _O : Bin → Bin _I : Bin → Bin _xor_ : Bin → Bin → Bin ⟨⟩ xor y = y (x O) xor ⟨⟩ = x O (x O) xor (y O) = (x xor y) O (x O) xor (y I) = (x xor y) I (x I) xor ⟨⟩ = x I (x I) xor (y O) = (x xor y) I (x I) xor (y I) = (x xor y) O lemma : ∀ (b : Bin) ------------ → b xor ⟨⟩ ≡ b lemma ⟨⟩ = refl lemma (b O) = refl lemma (b I) = refl _ : ( ⟨⟩ I O O I O I I O ) xor ( ⟨⟩ O I I I O O O O ) ---------------------- ≡ ( ⟨⟩ I I I O O I I O ) _ = refl -- Left & right identity proofs. postulate binO : (⟨⟩ O) ≡ ⟨⟩ -- Just accomodating a syntactical nuisance. xor-idₗ : ∀ (b : Bin) ---------------- → (⟨⟩ O) xor b ≡ b xor-idₗ ⟨⟩ rewrite binO = refl xor-idₗ (b O) = refl xor-idₗ (b I) = refl xor-idᵣ : ∀ (b : Bin) ---------------- → b xor (⟨⟩ O) ≡ b xor-idᵣ ⟨⟩ rewrite binO = refl xor-idᵣ (b O) rewrite lemma b = refl xor-idᵣ (b I) rewrite lemma b = refl -db

1 0