- Haskell-Cafe - Haskell.org

VerifyThis 2018: Call for Participation and Travel Grants
by Andrei Paskevich 06 Mar '18

06 Mar '18

******************************************************************************** VerifyThis Verification Competition 2018 CALL FOR PARTICIPATION -- TRAVEL GRANTS Competition to be held at ETAPS 2018 http://verifythis.ethz.ch ******************************************************************************** IMPORTANT DATES Grant application deadline: March 12, 2018 Competition: April 14 and 15, 2018 ABOUT VerifyThis 2018 is a program verification competition taking place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018) on April 14-15, 2018 in Thessaloniki, Greece. It is the 7th event in the VerifyThis competition series. The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness, and elegance. PARTICIPATION: Participation is open for anybody interested. Teams of up to two people are allowed. Registration for ETAPS workshops and physical presence on site is required. We particularly encourage participation of: - student teams (this includes PhD students) - non-developer teams using a tool someone else developed - several teams using the same tool TRAVEL GRANTS: The competition has funds for a limited number of travel grants. A grant covers the incurred travel and accommodation costs up to a certain limit. The expected limit is EUR 350 for those coming from Europe and EUR 600 for those coming from outside Europe. To apply for a travel grant, send an email to verifythis(a)cs.nuim.ie by March 12, 2018. The application should include: - your name - your affiliation - the verification system(s) you plan to use at the competition - the planned composition of your team - a short letter of motivation explaining your involvement with formal verification so far - if you are a student, please state the academic degree you are seeking and have your supervisor send a brief letter of support to verifythis(a)cs.nuim.ie ORGANIZERS * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter Müller, ETH Zürich, Switzerland * Andrei Paskevich, Paris-Sud University, France * Gidon Ernst, National Institute of Informatics Tokyo, Japan CONTACT Email: verifythis(a)cs.nuim.ie Web: http://verifythis.ethz.ch

1 0

missing optimization for (++)
by Ben Franksen 05 Mar '18

05 Mar '18

I found that in base [1] we have (++) [] ys = ys (++) (x:xs) ys = x : xs ++ ys I had expected there to be a clause (++) xs [] = xs at the top, which would avoid the list traversal in this common case. Is this somehow magically taken care of by the {-# RULES "++" [~1] forall xs ys. xs ++ ys = augment (\c n -> foldr c n xs) ys #-} ? No, inlining @augment g xs = g (:) xs@ gives me (\c n -> foldr c n xs) (:) ys = foldr (:) ys xs which still traverses xs even if ys=[]. Any thoughts? [1] http://hackage.haskell.org/package/base-4.10.1.0/docs/src/GHC.Base.html#%2B… Cheers Ben

9 11

Haskell memory model
by Li-yao Xia 05 Mar '18

05 Mar '18

Hello café, What guarantees are there about shared memory concurrency in Haskell? In particular, I'm wondering how to correctly and efficiently synchronize mutable operations from the vector package, using stm or atomic-primops. - Are reads/writes on vectors sequentially consistent? As a concrete example, can the following program (a common test for relaxed memory models) print anything? import qualified Data.Vector.Mutable as MV import Control.Concurrent main :: IO () main = do v <- MV.replicate 2 0 t <- newEmptyMVar forkIO $ do MV.write v 0 1 x <- MV.read v 1 putMVar t x forkIO $ do MV.write v 1 1 x <- MV.read v 0 putMVar t x a <- takeMVar t b <- takeMVar t if a == 0 && b == 0 then putStrLn "Relaxed!" else return () - Do atomic operations (via stm or atomic-primops) imply some constraints between vector operations? As another concrete example, can the snippet linked below ever throw an exception? One thread writes to a vector, and another reads from it, and they communicate via stm to guess whether the read value is safe to evaluate (in one test case the first thread overwrites a defined value with undefined, and in the other case it overwrites undefined with a defined value). http://lpaste.net/362596 Regards, Li-yao

2 2

Re: [Haskell-cafe] missing optimization for (++)
by Markus Läll 04 Mar '18

04 Mar '18

Hi Viktor What I think the OP is asking for is a case where the original list would be returned immediately if the second is empty -- keeping the original spine. Since that case is missing then the list is pattern-matched and then reconstructed. Whether this actually happens after compilation is the real question. On Mar 4, 2018 21:24, "Viktor Dukhovni" <ietf-dane(a)dukhovni.org> wrote: > On Mar 4, 2018, at 4:32 AM, Ben Franksen <ben.franksen(a)online.de> wrote: > > I found that in base [1] we have > > (++) [] ys = ys > (++) (x:xs) ys = x : xs ++ ys > > I had expected there to be a clause > > (++) xs [] = xs > > at the top, which would avoid the list traversal in this common case. > > [...] > > which still traverses xs even if ys=[]. > > Any thoughts? Haskell is lazy, the traversal of x happens only when the combined list is actually traversed, and only for as many elements as requested, so the construction of the concatenated list carries little additional cost. And as pointed out, needlessly forcing the first element of y can have unintended consequences. For example: GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Prelude> let x = [1..] Prelude> let y = [1..] Prelude> let z = x ++ y Prelude> take 20 z [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20] -- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

1 0

cabal: Couldn't parse the output of 'setup register --gen-pkg-config':NoParse
by Henk-Jan van Tuyl 03 Mar '18

03 Mar '18

L.S., I am trying to get wxHaskell compiled with GHC 8.4.0.20180224 and cabal-install 2.1.0.0; compilation fails with the message: wxcore-0.93.0.0-1L9rVktyK3zIYrrLxBiCr9 failed during the final install step. The exception was: dieVerbatim: user error (cabal: Couldn't parse the output of 'setup register --gen-pkg-config':NoParse "license" 5 ) I am using Windows 8.1. Can anybody tell me what to do about this? Regards, Henk-Jan van Tuyl -- Message from Stanford University: Folding@home What if you could share your unused computer power to help find a cure? In just 5 minutes you can join the world's biggest networked computer and get us closer sooner. Watch the video. http://foldingathome.stanford.edu/ -- http://members.chello.nl/hjgtuyl/tourdemonad.html Haskell programming --

1 0

ANN: network-2.6.3.4
by evan＠evan-borden.com 01 Mar '18

01 Mar '18

Announcing network-2.6.3.4 * Don't touch IPv6Only when running on OpenBSD [#227](https://github.com/haskell/network/pull/227) * Do not closeFd within sendFd [#271](https://github.com/haskell/network/pull/271) * Updating examples and docs. A big thanks to the network contributors. http://hackage.haskell.org/package/network-2.6.3.4

1 0

Software engineer job situated in a PL research group
by Ryan Newton 28 Feb '18

28 Feb '18

Hi all, This posting is for a potentially long term position with the department. In the short term the work will be largely about sandboxing, containerization, and other low level systems stuff, but *all* the high-level software in the group is written in Haskell: https://iujobs.peopleadmin.com/postings/44056 The OOPSLA17 paper, "Monadic Composition for Deterministic, Parallel Batch Processing <https://2017.splashcon.org/event/splash-2017-oopsla-detflow-a-monad-for-det…>", should give an idea of what this initial project is about. The engineer would be co-located with a large Programming Languages group (6 faculty and a couple dozen Ph.D. students). University benefits are good and our college town combines culture and beautiful surroundings with convenience and affordability. Best regards, -Ryan

1 0

[ANNOUNCE] GHC 8.4.1-rc1 available
by Ben Gamari 28 Feb '18

28 Feb '18

The GHC development team is pleased to announce the first (and likely final) release candidate of GHC 8.4.1. The usual release artifacts are available from https://downloads.haskell.org/~ghc/8.4.1-rc1 This release will likely be the last release before the final 8.4.1 release, which, if things go well, will be released one week from today. Due to user demand we now offer a binary distribution for 64-bit Fedora 27, which links against ncurses6. This is in contrast to the Debian 8 distribution, which links against ncurses5. Users of newer distributions (Fedora 27, Debian Sid) should use this new Fedora 27 distribution. Also due to user demand we have reintroduced compatibility with GCC 4.4, which earlier alphas had dropped due to #14244. Note that this release candidate is still affected by #14705, although this will certainly be resolved before the final release is made. === Notes on release scheduling === The 8.4.1 release marks the first release where GHC will be adhering to its new, higher-cadence release schedule [1]. Under this new scheme, major releases will be made in 6-month intervals with interstitial minor releases as necessary. In order to minimize the likelihood of schedule slippage and to ensure adequate testing, each major release will be preceded by a number of regular alpha releases. We will begin issuing these releases roughly three months before the final date of the major release and will issue roughly one every two weeks during this period. This high release cadence will allow us to quickly get fixes into users' hands and more quickly identify potential issues. As always, do let us know if you encounter any trouble in the course of testing. Thanks for your help! Cheers, - Ben [1] https://ghc.haskell.org/trac/ghc/blog/2017-release-schedule

3 5

Optimization demonstration
by Dušan Kolář 28 Feb '18

28 Feb '18

Dear Café, I'm trying to do very small, but impressive example about optimizations possible during Haskell compilation. So far, I can demonstrate that the following two programs (if compiled) perform computation in the same time: 1) main = putStrLn $ show $ sum $ map (*(2::Int)) [(1::Int)..(100000000::Int)] 2) main = putStrLn $! show $! sumup 1 0 sumup :: Int -> Int -> Int sumup n total = if n<=(100000000::Int) then sumup (n+1) $! total+(2*n) else total Nevertheless, I expect a question on comparison with C: 3) #include <stdio.h> int main(void) { long sum, i; sum = 0; for (i=1; i <= 100000000L; ++i) { sum += 2*i; } printf("%ld\n",sum); return 0; } Unfortunately, in this case the C is much more faster (it prints the result immediately), at least on my machine. Is it due to a fact that C compiler does a brutal optimization leading to compile-time evaluation, while ghc is not able to do that? I'm using -O2 -dynamic --make ghc compiler flags. For gcc for C compilation just -O2, running Arch Linux. Is there any option, how to force compile time evaluation? The reason, why I think it works this way is the fact, that when running out of long type values in C a code is generated that computes the values regularly (providing misleading value as a result) taking its time. Best regards, Dušan

6 8

Re: [Haskell-cafe] Optimization demonstration
by Dušan Kolář 28 Feb '18

28 Feb '18

Many thanks all for replies, yes, that's what I assumed/wrote. C compiler does compile- time evaluation, while ghc does another transformation. And, well, yes, declaring upper bound in loop in extra file breaks the optimization for C compiler and, thus, both evaluation times for C and Haskell binaries are the same thus. Thank you once, again, Dušan P.S. If anyone can point me to resource, where examples on demonstration of Haskell optimization are, I'll be very glad. D. On úterý 27. února 2018 23:06:38 CET Richard O'Keefe wrote: > In order to optimise array indexing and to automatically vectorise > your code, high performance compilers for imperative languages > like C and Fortran analyse counted loops like you wouldn't believe. > You can find out what the C compiler does with your code by using > the -S command line option. gcc 7.2 optimised the whole loop away. > > Split your C program into two files. > One contains > long bound = 100000000L, incr = 1L; > The other is a version of your existing code with > extern long bound, incr; > ... > for (i = 1L; i <= bound; i += incr) { ... } > ... > gcc 7.2 isn't quite smart enough to optimise this away. Yet. > > The polyhedral optimisations going on are described in the > open literature and are valuable for imperative array- > crunching code. You are not likely to see them in GHC any > time soon, just as you're not likely to see deforestation > in gcc any time soon. > > On 28 February 2018 at 04:06, Dušan Kolář <kolar(a)fit.vut.cz> wrote: > > Dear Café, > > > > > > > > I'm trying to do very small, but impressive example about optimizations > > possible during Haskell compilation. So far, I can demonstrate that the > > following two programs (if compiled) perform computation in the same time: > > > > > > > > 1) > > > > > > > > main = > > > > putStrLn $ show $ sum $ map (*(2::Int)) [(1::Int)..(100000000::Int)] > > > > > > > > > > > > 2) > > > > > > > > main = > > > > putStrLn $! show $! sumup 1 0 > > > > > > > > sumup :: Int -> Int -> Int > > > > sumup n total = > > > > if n<=(100000000::Int) then sumup (n+1) $! total+(2*n) > > > > else total > > > > > > > > > > > > Nevertheless, I expect a question on comparison with C: > > > > > > > > 3) > > > > > > > > #include <stdio.h> > > > > > > > > int main(void) { > > > > long sum, i; > > > > sum = 0; > > > > for (i=1; i <= 100000000L; ++i) { > > > > sum += 2*i; > > > > } > > > > printf("%ld\n",sum); > > > > return 0; > > > > } > >

1 0