- Haskell-Cafe - Haskell.org

Open PhD and intern positions at IMDEA
by Niki Vazou 03 Dec '18

03 Dec '18

Hi Haskellers, I recently joined IMDEA and looking for talented Ph.D. students and interns to work with. Projects My current open projects focus on how to establish Liquid Haskell <https://ucsd-progsys.github.io/liquidhaskell-blog/> as a practical and useful theorem prover. Ideas I would like to explore include: - *Integration with Compiler & Compiler Optimizations:* The major goal of verification is to prove that your code satisfies certain correctness properties. But, once your correctness properties are proved, the compiler could use them to optimize the running times. For example properties like associativity, map fusion, and class laws could, and should, be used for provably correct compiler optimizations. The goal of this project is how the Haskell compiler can automatically take full advantage of Liquid Haskell generated proofs. - *Error Reporting:* Error messages are terrible! This is the case in most systems that include type inference, see ghc, and Liquid Haskell is not an exception. Recently <https://nikivazou.github.io/static/oopsla18main-p124-p.pdf>, the idea of using gradual types for error explanation was explored. The goal of this project is to further explore the interaction between gradual types and error reporting, or use further concepts, such as testing to aid error explanation. - *Interactive Proving Environment:* For theorem proving to be usable, proof generation should be interactively directed by the prover. Towards this goal, this project aims to investigate how existing techniques such as tactics and interactive environments from interactive theorem provers like Coq and Isabelle/HOL can be adapted to aid proof generation in Liquid Haskell. At the same time, proof generation can be aided by Haskell’s code generation infrastructures such as the automatic code derivation mechanisms. My passion is functional programing and practical program verification, so I am happy to discuss new research ideas in any of these directions. Requirements If you want to apply for a Ph.D. position you are required to have an undergraduate degree in Computer Science or a closely related area and have strong interest in functional programming. About IMDEA The IMDEA Software Institute <https://software.imdea.org/index.html> is ranked <http://csrankings.org/#/index?plan&europe> among the best european institutes in the areas of Programming Languages and Computer Security. Located in the Montegancedo Science and Technology Park <https://software.imdea.org/contact_and_directions/building.html> it perfectly combines the sunny and vibrant city of Madrid with cutting edge research and competitive salaries. How to apply? To apply send me an email at niki.vazou(a)imdea.org with your CV and submit an online application at IMDEA’s open positions <http://software.imdea.org/open_positions.html>. Best, Niki Vazou

1 0

Can't get Type 3" to work
by Amy de Buitléir 03 Dec '18

03 Dec '18

I'm reading "Thinking with Types" by Sandy Maguire, and there's a bit of code on p. 27 that I don't understand and can't get to work. The "Type 3" seems to have the effect of multiplying by 3. > :set -XDataKinds > :set -XTypeOperators > :kind! (1 + 17) Type 3 (1 + 17) Type 3 :: Nat = 54 But it doesn't work for me. When I try this, I get... $ ghci --version The Glorious Glasgow Haskell Compilation System, version 8.2.2 $ ghci λ> :set -XDataKinds λ> :set -XTypeOperators λ> :kind! (1 + 17) Type 3 <interactive>:1:2: error: Not in scope: type constructor or class '+' <interactive>:1:10: error: Not in scope: type constructor or class 'Type'

3 4

semantics of concurrent program depends on -O level, -f[no-]omit-yields
by Johannes Waldmann 30 Nov '18

30 Nov '18

Dear Cafe, I am surprised by the behaviour of the program below (the interesting property is whether it will output "foo"). Behaviours (plural) actually: it seems to depend on optimisation level, on omit-yields, and on very small changes in the source code: It does print (mostly), when compiled with -O0. It does not, when compiled with -O2. With -O2 -fno-omit-yields, it will print. With -O0 -fno-omit-yields, and when I remove the two newTVar in the beginning, it will mostly not print. How come? These differences already occur with the last two lines replaced by "forever $ return ()", so the STM stuff may be inessential here. But that's the context where I came across the problem. - J.W. import Control.Concurrent.STM import Control.Concurrent ( forkIO ) import Control.Monad ( forever ) import System.IO main = do atomically $ newTVar "bar" atomically $ newTVar False forkIO $ putStrLn "foo" x <- atomically $ newTVar False forever $ atomically $ writeTVar x True

5 16

Haskell-related summer internship in Germany
by Sandra Dylus 30 Nov '18

30 Nov '18

Our department (PL and compiler construction) again offers a summer internship in 2019 sponsored by DAAD Rise Germany [1]. Undergraduate students enrolled at North American, British and Irish universities are eligible to make an application. We'd be very happy to host a motivated student, who is keen to improve our compiler for the functional logic programming language Curry in terms of performance. For more information you may have a look at our project poster [2]. If you have any questions, feel free to mail any of the contact persons. Please also spread the news to your students and classmates. Cheers, Finn and Sandra [1]: https://www.daad.de/rise/en/rise-germany/ <https://www.daad.de/rise/en/rise-germany/> [2]: https://www-ps.informatik.uni-kiel.de/~sad/DAADRise.pdf <https://www-ps.informatik.uni-kiel.de/~sad/DAADRise.pdf>

1 0

Re: [Haskell-cafe] WebAssembly illustrated
by Takenobu Tani 30 Nov '18

30 Nov '18

Hi Sven, Thank you for teaching me. > Also, are you slides free to use? Could you please share the source? Of course you can use it freely :) I also commit the source. (But it is PowerPoint.) Cheers, Takenobu On Fri, Nov 30, 2018 at 9:10 PM Sven Sauleau <sven(a)sauleau.com> wrote: > Hi, > > Interesting document, thanks for sharing! > > I opened a clarification issue: [1]. > > Also, are you slides free to use? Could you please share the source? > [1]: https://github.com/takenobu-hs/WebAssembly-illustrated/issues/1 > > Thanks! > Sven > > On 30/11/2018 12:45, Takenobu Tani wrote: > > Hi cafe, > > I share this even in this place. > > WebAssembly illustrated > https://takenobu-hs.github.io/downloads/WebAssembly_illustrated.pdf > > > P.S. > Haskell has backends such as asterius [1] and dhc [2]. > > [1]: https://github.com/tweag/asterius > [2]: https://github.com/dfinity/dhc > > Cheers, > Takenobu > > > > _______________________________________________ > 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

WebAssembly illustrated
by Takenobu Tani 30 Nov '18

30 Nov '18

Hi cafe, I share this even in this place. WebAssembly illustrated https://takenobu-hs.github.io/downloads/WebAssembly_illustrated.pdf P.S. Haskell has backends such as asterius [1] and dhc [2]. [1]: https://github.com/tweag/asterius [2]: https://github.com/dfinity/dhc Cheers, Takenobu

1 0

GHC 8.6.2 zombie processes?
by Viktor Dukhovni 30 Nov '18

30 Nov '18

It seems that GHC 8.6.2 does not reap defunct child processes in a timely manner when compiling many modules (e.g. "base" when stack is building a new sandbox). This is especially visible when using LLVM 6.0 whose optimizer is particularly CPU-intensive (read mind-numbingly slow) on my X86_84 FreeBSD system: The process: $ ps -wwwwwww -o pid,etime,args -p 98525 PID ELAPSED COMMAND 98525 55:47 /home/viktor/.local/lib/ghc-8.6.2.20181122/bin/ghc -B/home/viktor/.local/lib/ghc-8.6.2.20181122 --make -fbuilding-cabal-package -O -static -dynamic-too -dynosuf dyn_o -dynhisuf dyn_hi -outputdir .stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -odir .stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -hidir .stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -stubdir .stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -i -i.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -i. -i.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build/autogen -i.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build/global-autogen -I.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build/autogen -I.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build/global-autogen -I.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build -I/usr/local/Cellar/postgresql/10.0/include -I/usr/local/include -I/usr/local/opt/icu4c/include -optP-include -optP.stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/build/autogen/cabal_macros.h -this-unit-id Cabal-2.4.1.0-IaB5GUEm19R82R9cEdbB1D -hide-all-packages -Wmissing-home-modules -no-user-package-db -package-db /usr/home/viktor/.stack/snapshots/x86_64-freebsd/nightly-2018-11-28/8.6.2.20181122/pkgdb -package-db .stack-work/dist/x86_64-freebsd/Cabal-2.4.0.1/package.conf.inplace -package-id array-0.5.3.0 -package-id base-4.12.0.0 -package-id binary-0.8.6.0 -package-id bytestring-0.10.8.2 -package-id containers-0.6.0.1 -package-id deepseq-1.4.4.0 -package-id directory-1.3.3.0 -package-id filepath-1.4.2.1 -package-id mtl-2.2.2 -package-id parsec-3.1.13.0 -package-id pretty-1.1.3.6 -package-id process-1.6.3.0 -package-id text-1.2.3.1 -package-id time-1.8.0.2 -package-id transformers-0.5.5.0 -package-id unix-2.7.2.2 -XHaskell2010 Distribution.Backpack Distribution.Backpack.Configure Distribution.Backpack.ComponentsGraph Distribution.Backpack.ConfiguredComponent Distribution.Backpack.DescribeUnitId Distribution.Backpack.FullUnitId Distribution.Backpack.LinkedComponent Distribution.Backpack.ModSubst Distribution.Backpack.ModuleShape generated multiple hundreds of "zombies": $ ps $(pgrep -P 98525) | egrep -c defunct 460 I guess the build taking an hour is far more an issue than a few hundred zombies, but this message is about the zombies. Is this a feature or a bug? -- Viktor.

1 0

Is there some way to hack the type system without recompiling GHC?
by ducis 29 Nov '18

29 Nov '18

We know that the type system is now a second language where you spec formal requirements and let the compiler solve it, kinda like logic programming. But sometimes I knew something is correct or at least willing to take the risk of runtime errors, but the typechecker is not (yet) able to figure it out. In this case is it possible to somehow insert (regular haskell) code into the typechecker and force the compiler to think some values are of some types, rather than waiting for or inventing some formally correct solution, which may be fundamentally very difficult?

4 3

Tidal (musical pattern library) refactor - feedback appreciated
by Alex McLean 28 Nov '18

28 Nov '18

https://slab.org/tidal-1-0-0-refactor/ -- blog: http://slab.org/

1 1

XText vs DSL in Haskell in mission critical software
by Puck 28 Nov '18

28 Nov '18

Hello all, how can I convince my bosses to use existing functional languages for specifying the future embedded softwares from the company instead of using Xtext or other things that firm under the name "model driven development". The softwares are mission critical. A local cooperation is already building an research institute with the goal of "model driven development". Why they do not use plain Haskell, LiquidHaskell and Coq? Neither can I imagine, that Haskell or Coq is so hard to learn, neither can I imagine that they want the developers to dive through handwritten Java extensions for their tool, that can only be analyzed with Java-tools and cannot be proven. Is XText, for example, really so good? Is a Haskell-DSL as a counterpart, not very much fewer dependent on other things, and very much easier to maintain? Thanks for suggestions and arguments Puck

2 1