April 2015 - Haskell-Cafe

Paid internship at Energy startup Moixa Technology
by Chris Wright 28 Apr '15

28 Apr '15

Hi We are looking for a bright sparky developer to join our team in London as a paid intern, with the potential to turn into a full time job. We are based in central London, http://moixatechnology.com/ & www.meetmaslow.com The intern's objective will be creating web interfaces for users of our innovative renewable electricity systems. This opportunity is exciting in many ways. Moixa has won a number of prizes for its innovative products. The enterprise is a cool innovative startup that welcomes open thinking and encourages personal development. London has unarguably the largest UK Haskell community, and developers of most Haskell web frameworks can be met around here. Here is what the intern would have: - good CS background - decent Haskell knowledge: no professional experience, but able to write non-trivial applications - familiarity with web development: knows HTML/CSS and worked with some web frameworks --language mostly unimportant, but hopefully not PHP :) - knowledge of browser-side JavaScript & HTML DOM Contact e-mail: chris(a)moixaenergy.com<mailto:chris@moixaenergy.com> Best Regards Chris Chris Wright CTO - Moixa Technology www.meetmaslow.com 0207 734 1511

1 0

[Job] Intel is hiring: FP/FV oriented folks most welcome..
by Levent Erkok 27 Apr '15

27 Apr '15

The group I work for at Intel has an opening for a recent graduate (BS/MS/PhD) of a US institution. We work within the product team responsible for the Xeon Phi many-core processor which is used to build supercomputers. See: http://en.wikipedia.org/wiki/Xeon_Phi Our team focuses mainly on the floating-point arithmetic verification using an internal STE based model checking tool called Forte, which is based on the reFLect language, which itself is a descendant of ML. (With lazy-evaluation default, and a baked-in BDD based equivalence checking engine, which makes it supercool! Imagine Haskell with a built-in symbolic simulation engine.) We also use Haskell for internal purposes as needed. Our group has extensive freedom in the choice of tools we use. We also work on a variety of non-arithmetic verification problems, including cache coherence, ECC (error-detection/correction) algorithms, instruction length decoders, to name a few. As part of our coherence work we developed an open source explicit state distributed model checker called PReach <https://bitbucket.org/jderick/preach/wiki/Home>. Our group is based in Portland, OR, with one member in Santa Clara, CA. Please let me know if you are, or you know anyone who might be interested in this position. Feel free to forward this request. -Levent.

1 0

ANN: New Haskell.org Committee Members
by Gershom B 27 Apr '15

27 Apr '15

Following the self-nomination period and discussion, the Haskell.org committee has selected new members: * Edward Kmett (reappointment) * Ryan Trinkle * John Wiegley As per the rules of the committee, this discussion was held among the current members of the committee, and the outgoing members of the committee who were not seeking reappointment. Thank you to all candidates who submitted a self-nomination. All of the nominations we received were very strong, and we would encourage all those who nominated themselves to consider self-nominating again in the future. We would also like to thank our two outgoing members, Jason Dagit and Brent Yorgey, for their service. Cheers, Gershom

1 0

Prime ``sieve'' and Haskell demo
by oleg＠okmij.org 27 Apr '15

27 Apr '15

Ertugrul So:ylemez wrote: > How about simply changing `sieve` to `trialDiv`? It's not that I > don't like the given example, because it gives a very small use case > for laziness that is difficult enough to reproduce in an eagerly > evaluated language. Is it really so difficult to reproduce in a strict language? Here is that Haskell example in OCaml let primes = let rec trialDiv (Cons (p,xs)) = Cons (p, lazy (trialDiv @@ filter (fun x -> x mod p <> 0) @@ Lazy.force xs)) in trialDiv @@ iota 2 roughly the same number of lines, and mainly, exactly the same method. Some people prefer to write it as let primes = let rec trialDiv (Cons (p,xs)) = Cons (p, lazy (Lazy.force xs |> filter (fun x -> x mod p <> 0) |> trialDiv)) in iota 2 |> trialDiv The algorithm is the same, it is just as clearly stated. Now it becomes clearer when what is evaluated. OCaml has its own streams (and even a special syntax for them, via a syntactic extension), but it is not difficult to introduce them from scratch type 'a stream = Cons of 'a * 'a stream Lazy.t let rec iota n = Cons (n,lazy (iota (n+1))) let rec filter pred (Cons (p,xs)) = if pred p then Cons (p,lazy (filter pred (Lazy.force xs))) else filter pred (Lazy.force xs) let rec take n (Cons (p,xs)) = if n <= 0 then [] else p :: take (n-1) (Lazy.force xs) That's really all there is to it. I should stress that the typechecker won't lets us forget about lazy and force! The stress on laziness in Haskell is difficult to understand given how easy it is to use laziness in essentially any language if needed. Incidentally, given below is a real sieve of Eratosthenes, written as a *very* concurrent program, where all the concurrency primitives (including Haskell-like mvars) are implemented with delimcc. (The example is an elaboration of the code kindly sent by Christophe Deleuze, July 18, 2012). The full code is part of the delimcc distribution. open Lwc (* Send a stream of integers [m..n] on the channel out *) (* It is a task and hence creates a thunk *) let iota : int mvar -> int -> int -> task = fun out m n () -> for i = m to n do put_mvar out i done (* A task to print the values read from the stream *) let output : int mvar -> task = fun inp () -> while true do let v = take_mvar inp in Printf.printf "%i " v done (* The key step in the Eratosthenes sieve: copy inp to out but replace every n-th element with 0 *) let filter : int -> int mvar -> int mvar -> task = fun n inp out () -> let rec loop i = let v = take_mvar inp in if i <= 1 then (put_mvar out 0; loop n) else (put_mvar out v; loop (i-1)) in loop n (* The main sieving task: move prime numbers from inp to out by composing filters *) let rec sift : int mvar -> int mvar -> task = fun inp out () -> let n = take_mvar inp in if n = 0 then sift inp out () else begin put_mvar out n; let mid = make_mvar () in spawn (filter n inp mid); sift mid out () end (* Start up the task of the sieving job, with n being the upper limit *) let sieve : int -> task = fun n () -> let mi = make_mvar () in let mo = make_mvar () in spawn (iota mi 2 n); spawn (sift mi mo); spawn (output mo)

2 1

Timeout on pure code
by Kostiantyn Rybnikov 27 Apr '15

27 Apr '15

Hi! Our company's main commercial product is a Snap-based web app which we compile with GHC 7.8.4. It works on four app-servers currently load-balanced behind Haproxy. I recently implemented a new piece of functionality, which led to weird behavior which I have no idea how to debug, so I'm asking here for help and ideas! The new functionality is this: on specific url-handler, we need to query n external services concurrently with a timeout, gather and render results. Easy (in Haskell)! The implementation looks, as you might imagine, something like this (sorry for almost-real-haskell, I'm sure I forgot tons of imports and other things, but I hope everything is clear as-is, if not -- I'll be glad to update gist to make things more specific): https://gist.github.com/k-bx/0cf7035aaf1ad6306e76 Now, this works wonderful for some time, and in logs I can see both, successful fetches of external-content, and also lots of timeouts from our external providers. Life is good. But! After several days of work (sometimes a day, sometimes couple days), apps on all 4 servers go crazy. It might take some interval (like 20 minutes) before they're all crazy, so it's not super-synchronous. Now: how crazy, exactly? First of all, this endpoint timeouts. Haproxy requests for a response, and response times out, so they "hang". Secondly, logs are interesting. If you look at the code from gist once again, you can see, that some of CandidateProvider's don't actually require any networking work, so all they do is actually just logging that they're working (I added this as part of debugging actually) and return pure data. So what's weird is that they timeout also! Here's how output of our logs starts to look like after the bug happens: ``` [2015-04-22 09:56:20] provider: CandidateProvider1 [2015-04-22 09:56:20] provider: CandidateProvider2 [2015-04-22 09:56:21] Got timeout while requesting CandidateProvider1 [2015-04-22 09:56:21] Got timeout while requesting CandidateProvider2 [2015-04-22 09:56:22] provider: CandidateProvider1 [2015-04-22 09:56:22] provider: CandidateProvider2 [2015-04-22 09:56:23] Got timeout while requesting CandidateProvider1 [2015-04-22 09:56:23] Got timeout while requesting CandidateProvider2 ... and so on ``` What's also weird is that, even after timeout is logged, the string ""Got responses!" never gets logged also! So hanging happens somewhere in-between. I have to say I'm sorry that I don't have strace output now, I'll have to wait until this situation happens once again, but I'll get later to you with this info. So, how is this possible that almost-pure code gets timed-out? And why does it hang afterwards? CPU and other resource usage is quite low, number of open file-descriptors also (it seems). Thanks for all the suggestions in advance!

5 14

working through "Part I: Dependent Types in Haskell"
by Nicholls, Mark 27 Apr '15

27 Apr '15

Hello, working through https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/de… but a bit stuck...with an error... > {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, StandaloneDeriving #-} > data Nat = Z | S Nat > data Vector a n where > Nil :: Vector a Z > (:-) :: a -> Vector a n -> Vector a (S n) > infixr 5 :- I assume init...is a bit like tail but take n - 1 elements from the front....but... > init' :: Vector a ('S n) -> Vector a n > init' (x1 :- Nil) = Nil > init' (x :- xs) = x :- (init' xs) gives...(I could do with working out what haskell is tryign to tell me). Could not deduce (n1 ~ 'S n0) from the context ('S n ~ 'S n1) bound by a pattern with constructor :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n), in an equation for 'init'' at cafe.lhs:13:10-16 'n1' is a rigid type variable bound by a pattern with constructor :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n), in an equation for 'init'' at cafe.lhs:13:10 Expected type: Vector a n Actual type: Vector a ('S n0) Relevant bindings include xs :: Vector a n1 (bound at cafe.lhs:13:15) In the expression: x :- (init' xs) In an equation for 'init'': init' (x :- xs) = x :- (init' xs) so... the ":-" in "init' (x :- xs)" has type forall a (n :: Nat). a -> Vector a n -> Vector a ('S n) yep that makes sense.... if it knew "n ~ n1" then it knows "n1 ~ 'S n0" so it would know "n ~ 'S n0" but it only knows "'S n ~ 'S n1" hmmmm...surely from the def of Nat, thats "obvious" CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.

2 1

ANN: exference: a different djinn
by lennart spitzner 27 Apr '15

27 Apr '15

Hello folks, Exference[1] is a Haskell tool for generating expressions from a type, e.g. Input: (Show b) => (a -> b) -> [a] -> [String] Output: \ b -> fmap (\ g -> show (b g)) In contrast to Djinn, the well known tool with the same general purpose, Exference supports a larger subset of the haskell type system - most prominently type classes. (Djinn's environment many contain type classes, but using them in queries will not really work.) This comes at a cost, however: Exference makes no promise regarding termination. Where Djinn tells you "there are no solutions", Exference will keep trying, sometimes aborting a non-ending search with "i could not find any solutions". See [2] for a report about the implementation, capabilities and limitations. [1] https://github.com/lspitzner/exference [2] https://github.com/lspitzner/exference/raw/master/exference.pdf Lennart

3 4

Improved Hackage Security document
by Michael Snoyman 27 Apr '15

27 Apr '15

To try and clarify a number of the points brought up in discussion around Hackage security in the past few weeks, Mathieu and I have put some time into trying to organize the information around this a bit. The result is the following page: https://github.com/commercialhaskell/commercialhaskell/blob/master/proposal… Contributions by others are very welcome. If you send a pull request, odds are you'll end up with commit access too.

1 0

[ANN] FLOPS CFP 2016
by oleg＠okmij.org 27 Apr '15

27 Apr '15

FLOPS 2016: 13th International Symposium on Functional and Logic Programming March 3-6, 2016, Kochi, Japan Call For Papers http://www.info.kochi-tech.ac.jp/FLOPS2016/ Writing down detailed computational steps is not the only way of programming. The alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style include functional and logic programming, program transformation and re-writing, and extracting programs from proofs of their correctness. FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. Scope FLOPS solicits original papers in all areas of the declarative programming: * functional, logic, functional-logic programming, re-writing systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers; * foundations, language design, implementation issues (compilation techniques, memory management, run-time systems), applications and case studies. FLOPS promotes cross-fertilization among different styles of declarative programming. Therefore, submissions must be written to be understandable by the wide audience of declarative programmers and researchers. Submission of system descriptions and declarative pearls are especially encouraged. Submissions should fall into one of the following categories: * Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. * System descriptions: they should contain a link to a working system and will be judged on originality, usefulness, and design. * Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy. The proceedings will be published by Springer International Publishing in the Lecture Notes in Computer Science (LNCS) series, as a printed volume as well as online in the digital library SpringerLink. Post-proceedings: The authors of 4-7 best papers will be invited to submit the extended version of their FLOPS paper to a special issue of the journal Science of Computer Programming (SCP). Important dates Monday, September 14, 2015 (any time zone): Submission deadline Monday, November 16, 2015: Author notification March 3-6, 2016: FLOPS Symposium March 7-9, 2016: PPL Workshop Submission Submissions must be written in English and can be up to 15 pages long including references, though pearls are typically shorter. The formatting has to conform to Springer's guidelines. Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to a Web page, or an appendix). Papers should be submitted electronically at https://easychair.org/conferences/?conf=flops2016 Program Committee Andreas Abel Gothenburg University, Sweden Lindsay Errington USA Makoto Hamana Gunma University, Japan Michael Hanus CAU Kiel, Germany Jacob Howe City University London, UK Makoto Kanazawa National Institute of Informatics, Japan Andy King University of Kent, UK (PC Co-Chair) Oleg Kiselyov Tohoku University, Japan (PC Co-Chair) Hsiang-Shang Ko National Institute of Informatics, Japan Julia Lawall Inria-Whisper, France Andres Löh Well-Typed LLP, UK Anil Madhavapeddy Cambridge University, UK Jeff Polakow PivotCloud, USA Marc Pouzet École normale supérieure, France Vítor Santos Costa Universidade do Porto, Portugal Tom Schrijvers KU Leuven, Belgium Zoltan Somogyi Australia Alwen Tiu Nanyang Technological University, Singapore Sam Tobin-Hochstadt Indiana University, USA Hongwei Xi Boston University, USA Neng-Fa Zhou CUNY Brooklyn College and Graduate Center, USA Organizers Andy King University of Kent, UK (PC Co-Chair) Oleg Kiselyov Tohoku University, Japan (PC Co-Chair) Yukiyoshi Kameyama University of Tsukuba, Japan (General Chair) Kiminori Matsuzaki Kochi University of Technology, Japan (Local Chair) flops2016 at logic.cs.tsukuba.ac dot jp

1 0

Munich Haskell Meeting, 2015-04-30 @ 19:30
by Christian Neukirchen 27 Apr '15

27 Apr '15

Dear all, This week, our monthly Munich Haskell Meeting will take place again on Thursday, April 30 at Cafe Puck at 19h30. For details see here: http://www.haskell-munich.de/dates If you plan to join, please add yourself to this dudle so we can reserve enough seats! It is OK to add yourself to the dudle anonymously or pseudonymously. https://dudle.inf.tu-dresden.de/haskell-munich-apr-2015/ Everybody is welcome! cu, -- Christian Neukirchen <chneukirchen(a)gmail.com> http://chneukirchen.org

1 0