- Haskell-Cafe - Haskell.org

Multiple Research Positions (3 Doctoral, 5 Post-doctoral) on AI Verification
by Ekaterina Komendantskaya 21 Mar '20

21 Mar '20

AI Secure and Explainable by Construction: Multiple Research Positions (3 Doctoral, 5 Post-doctoral) available at Heriot-Watt, Edinburgh and Strathclyde Universities, Scotland, UK. Start date: 1 September 2020; End date: 30 August 2023 Postdoctoral Salary Scale: £31,866 to £40,322 per annum PhD funding: covering PhD fees and stipend for 3.5 years Closing date for Postdoctoral applications: 1 June 2020 We encourage interested applicants to contact us informally ASAP. The project has sufficient flexibility to mitigate the effect of COVID-19, i.e. by accommodating later start date and remote working. The project spans several subjects: type theory, automated and interactive theorem proving, security, AI and machine learning, autonomous systems, natural language processing and generation, legal aspects of AI. It will cover two main application areas: autonomous cars and chatbots, drawing from expertise and infrastructure provided by industrial partners working in these two areas. The project has a significant international span, with 12 partners from Academia and Industry in Europe (France, Germany, Israel, the Netherlands, Norway) and the US. Researchers joining this project will have excellent opportunities to travel to international conferences, organise scientific events, spend time with industrial partners, collaborate with academic leaders in the field, develop their own research profiles as well as gain experience in other AI and CS disciplines. For further information, and instructions how to apply, please visit: http://laiv.uk/index.php/vacancies/ Ekaterina Komendantskaya: http://www.macs.hw.ac.uk/~ek19/ Robert Atkey: https://bentnib.org/ David Aspinall: https://homepages.inf.ed.ac.uk/da/ Burkard Schafer: https://www.law.ed.ac.uk/people/professor-burkhard-schafer Verena Rieser: https://sites.google.com/site/verenateresarieser/

1 0

2 PhD Positions in the Safety and Security of Advanced Systems Group (University of Exeter, UK Deadline 2020-05-01)
by Achim D. Brucker 20 Mar '20

20 Mar '20

Two fully funded PhD scholarships for EU/UK applicants are available in the Security and Trust of Advanced Systems Group [1] (Prof. Achim Brucker [2] and Dr. Diego Marmsoler [3]) at the Department of Computer Science of the University of Exeter, UK [4]. We are looking for enthusiastic and outstanding Computer Science or Mathematics students with a strong background in some of the following topics: - safety or security of (software) systems, - formal modelling or formal reasoning/verification, - program analysis or program verification, - language-based security - semantics of programming languages, - theorem proving, model checking, - cryptographic protocols, - distributed systems (e.g., blockchain), - specification-based testing, and - design and implementation of security architectures. This award provides annual funding to cover UK/EU tuition fees and a tax-free stipend. For students who pay UK/EU tuition fees the award will cover the tuition fees in full, plus at least £15,009 per year tax-free stipend. The studentship will be awarded on the basis of merit for 3.5 years of full-time study. For more details, please consult the official advertisement: http://www.exeter.ac.uk/studying/funding/award/?id=3887 The closing date for applications is midnight on 1 May 2020. Project-specific queries should be directed to the supervisors, Prof Achim Brucker (A.Brucker(a)exeter.ac.uk) or Dr Diego Marmsoler (D.Marmsoler(a)exeter.ac.uk) Best, Achim and Diego [1] http://emps.exeter.ac.uk/computer-science/research/cyber-security/ [2] https://www.brucker.uk/ [3] https://marmsoler.com/ [4] http://emps.exeter.ac.uk/computer-science/ -- Prof. Achim Brucker | https://www.brucker.ch | https://logicalhacking.com/blog *We are hiring:* * Lecturer (Assistant Professor) - Deadline 2020-04-08: https://www.jobs.ac.uk/job/BZH668/lecturer-in-computer-science-education-an… * Two PhD Studentships (EU/UK Tuition Fees) - Deadline 2020-05-01: http://www.exeter.ac.uk/studying/funding/award/?id=3887

1 0

Open Position: Lecturer in Computer Science (Exeter, Deadline 2020-04-08)
by Achim D. Brucker 20 Mar '20

20 Mar '20

Open Position: Lecturer in Computer Science (Exeter, Deadline 2020-04-08) As part of the expansion of the Department of Computer Science at the University of Exeter [1], we are recruiting for a Lecturer in Cybersecurity. The lecturer will be part of the newly formed Security and Trust of Advanced Systems Group [2]. We are looking for a candidate with an outstanding research record in any area related to cyber security (information security) such as (but not limited to): - access control - usable security - software/application security - formal methods for security - language-based security/privacy - secure programming - information flow - security protocols - network security - security of distributes systems - human aspects of security - hardware security - security economics - security-by-design - applied cryptography - privacy-enhancing technologies - threat hunting, security analytics - threat modelling - forensics, reverse engineering - trustworthy AI/ML - security/penetration testing You will have a PhD or equivalent in Cybersecurity, Computer Science, Mathematics, Engineering or a related area. Please refer to the job description for full details. We understand **security and safety entangled concepts**: in most modern systems one cannot be achieved without the other. Hence, we encourage also candidates working in related domains such as **safety, dependability, resilience, or reliability** to apply. Please apply by 8th of April 2020! See the full announcement and application details at https://jobs.exeter.ac.uk/hrpr_webrecruitment/wrd/run/ETREC107GF.open?VACAN… We are happy to do online/remote interviews. Feel free to contact me for informal inquiries about the post. Best, Achim [1] https://www.exeter.ac.uk/computer-science/ [2] https://emps.exeter.ac.uk/computer-science/research/cyber-security/ -- Prof. Achim Brucker | https://www.brucker.ch | https://logicalhacking.com/blog *We are hiring:* * Lecturer (Assistant Professor) - Deadline 2020-04-08: https://www.jobs.ac.uk/job/BZH668/lecturer-in-computer-science-education-an… * Two PhD Studentships (EU/UK Tuition Fees) - Deadline 2020-05-01: http://www.exeter.ac.uk/studying/funding/award/?id=3887

1 0

Help with async library and killing child processes
by Michael Hull 20 Mar '20

20 Mar '20

Hi, I am currently learning Haskell, and really enjoying it, thankyou to the community for this well considered language. I have started using the async library, and I can't quite figure out some of the documentation, and I wonder if someone could help. https://hackage.haskell.org/package/async-2.2.2/docs/Control-Concurrent-Asy… Makes the comment that: "This is a useful variant of async <https://hackage.haskell.org/package/async-2.2.2/docs/Control-Concurrent-Asy…> that ensures an Async is never left running unintentionally." However, I can't see how I would use this. To make the example more concrete, I have a function that looks like this: runNodeHwBridgeUdp :: NodeHwInterface -> NodeHwUdpConfig-> IO() runNodeHwBridgeUdp (NodeHwInterface l0up l0down) config = do putStrLn "Starting Node bridge" -- Launch all the subprocesses: t0 <- async $ (runMsgUpReader hwBridgeSharedData l0up) t1 <- async $ (evalStateT (runUDPWriter hwBridgeSharedData) (initialUdpDispatchData timeUs) ) t2 <- async $ (runUDPReader hwBridgeSharedData l0down) putStrLn "Created child processes. Waiting...." (a, is_exception) <- waitAnyCatchCancel [t0, t1, t2] case is_exception of Right _ -> do error "SHOULD NOT GET HERE" Left exception -> do case (fromException exception) of Just (ex :: HwDestroyException) -> do putStrLn $ "BRIDGE ENDING: >>>> GOOD: SHUTDOWN: " ++ show exception Nothing -> do throwIO exception return () This process launches 3 child processes, and then waits on them. I launch this function as an async-process, and it would be really helpful if when I "cancel"ed it, it would also also cancelled the children, but I don't understand how I would structure that... t0 <- withAsync $ (runMsgUpReader hwBridgeSharedData l0up) $ \async -> do ???? t1 <- withAsync $ (evalStateT (runUDPWriter hwBridgeSharedData) (initialUdpDispatchData timeUs) ) $ \async -> do ???? t2 <- async $ (runUDPReader hwBridgeSharedData l0down) $ \async -> do ???? I feel like I must be missing something here. I'd appreciate any input; many thanks for your time, Mike

6 15

Re: [Haskell-cafe] Adding Content-Addressable Storage to GHC
by Michal J Gajda 19 Mar '20

19 Mar '20

Great idea! We already have syntax for package imports: ``` import "bytestring" Data.ByteString ``` Source plugin could probably pull and build package by CAS: ``` import "CAS_6ffeacff768590" Data.ByteString ``` That would reuse existing syntax without confusion. And without inconvenience of having to import expressions one by one. Or declaring their types. One could even add CAS hashes to Hackage db. Probably the source plugin can add `-package` parameters with GHC_OPTIONS? On the expression side, it seems easy to use Generics to derive hashable for `Exp`, given a *particular compiler version*. Warning is, that one needs to be more careful when the `Exp`ression type changes. -- Cheers Michal

1 0

Adding Content-Addressable Storage to GHC
by Chris Done 18 Mar '20

18 Mar '20

Hi all, Is there any effort or designs ongoing to add CAS (content-addressable storage) to GHC, as in Unison? < https://www.unisonweb.org/docs/tour/> == The idea == The summary of the idea is simply that top-level declarations can be addressed by a hash of their contents. Recursive definitions are transformed into the worker/wrapper to eliminate the self-referencing issue of hashing. == Why I want this == There are lots of advantages to this, but the one that excites me the most is that we can move to running tests, especially property tests, at compile-time. The main downside to running tests at compile-time, as seen done with template-haskell is that you will re-run tests every time the module is recompiled, making your dev cycle slower. However, if your tests are keyed upon CAS hashes, then those hashes are only invalidated when individual declarations actually change. This means the re-running of tests becomes granular at the declaration-level. When a single test completes, either successfully or not, you can cache the result and lookup the result next time, using e.g. the SHA512 of the expression evaluated. Therefore you could change a single function in a library and it would only re-run the tests that are actually affected, rather than running all the tests in the whole module, and rather than the more typical approach which is running ALL tests in a test suite just because one thing changed. If you can couple tests with code then you can avoid the decoupling of code from the tests. == Implementation approaches == There are various ways to implement this with varying degrees of satisfaction: 1. Use TH: reify declarations, inspect the AST, and produce a SHA512. Use ambient values such as the GHC version, instances in scope, extensions, ghc options, etc. With TH, I'm confident that you can only achieve an imperfect hash because I doubt that all information is available to TH. Names that come from external packages could be treated as CAS'd at the scope of the package's installed hash. Ideally, you could have granularity into other packages. But it's not a necessity if you just want caching for your current development package. 2. Use a source plugin. A source plugin is already capable of accessing all GHC context information, so this might lead to more of a perfect hash. 3. Add it to GHC directly. Exposing a `expressionSHA512 :: Exp -> ByteString` could be one imaginary way to access this information. With such a function you could implement caching of fine-grained tests. A related discussion is the deterministic builds: https://gitlab.haskell.org/ghc/ghc/wikis/deterministic-builds Anyone else exploring this? Cheers, Chris

4 3

Re: [Haskell-cafe] Haskell-Cafe Digest, Vol 199, Issue 15
by Michal J Gajda 18 Mar '20

18 Mar '20

Great idea! We already have syntax for package imports: ``` import "bytestring" Data.ByteString ``` Source plugin could probably pull and build package by CAS: ``` import "CAS_6ffeacff768590" Data.ByteString ``` That would reuse existing syntax without confusion. And without inconvenience of having to import expressions one by one. Or declaring their types. One could even add CAS hashes to Hackage db. Wonder if source plugin can add `-package` parameters? On Wed, Mar 18, 2020, 13:01 <haskell-cafe-request(a)haskell.org> wrote: > Send Haskell-Cafe mailing list submissions to > haskell-cafe(a)haskell.org > > To subscribe or unsubscribe via the World Wide Web, visit > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > or, via email, send a message with subject or body 'help' to > haskell-cafe-request(a)haskell.org > > You can reach the person managing the list at > haskell-cafe-owner(a)haskell.org > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Haskell-Cafe digest..." > Today's Topics: > > 1. Re: Help with async library and killing child processes (YueCompl) > 2. Adding Content-Addressable Storage to GHC (Chris Done) > > > > ---------- Forwarded message ---------- > From: YueCompl <compl.yue(a)icloud.com> > To: Branimir Maksimovic <branimir.maksimovic(a)gmail.com> > Cc: haskell-cafe(a)haskell.org > Bcc: > Date: Wed, 18 Mar 2020 18:42:56 +0800 > Subject: Re: [Haskell-cafe] Help with async library and killing child > processes > Um, event processing applications by procedural programmers (part data > analyst personnels for some) is a thing in my org, so I'm baking an DSL > doing it. > > On 2020-03-18, at 18:18, Branimir Maksimovic < > branimir.maksimovic(a)gmail.com> wrote: > > That's just library, not built into language. You can do it with forkIO as > I do it per specifics > > of application. > > Greets, > Branimir. > On 3/18/20 11:06 AM, YueCompl wrote: > > No, not to cancel a thread, but the business task on that thread's way > ahead. That's what Go's Context is designed for. > > > - About Go context from: https://blog.golang.org/context > > At Google, we require that Go programmers pass a Context parameter as the > first argument to every function on the call path between incoming and > outgoing requests. This allows Go code developed by many different teams to > interoperate well. It provides simple control over timeouts and cancelation > and ensures that critical values like security credentials transit Go > programs properly. > Server frameworks that want to build on Context should provide > implementations of Context to bridge between their packages and those that > expect a Context parameter. Their client libraries would then accept a > Context from the calling code. By establishing a common interface for > request-scoped data and cancelation, Context makes it easier for package > developers to share code for creating scalable services. > > I (and seems Windows api too) strongly agree that cancelling a thread is > problematic: > > > https://docs.microsoft.com/en-us/windows/win32/api/processthreadsapi/nf-pro… > > TerminateThread is a dangerous function that should only be used in the > most extreme cases. You should call TerminateThread only if you know > exactly what the target thread is doing, and you control all of the code > that the target thread could possibly be running at the time of the > termination. For example, TerminateThread can result in the following > problems: > > - If the target thread owns a critical section, the critical section > will not be released. > - If the target thread is allocating memory from the heap, the heap > lock will not be released. > - If the target thread is executing certain kernel32 calls when it is > terminated, the kernel32 state for the thread's process could be > inconsistent. > - If the target thread is manipulating the global state of a shared > DLL, the state of the DLL could be destroyed, affecting other users of the > DLL. > > > On 2020-03-18, at 17:16, Branimir Maksimovic < > branimir.maksimovic(a)gmail.com> wrote: > > I'm pretty sure you can't cancel goroutine. Actually I have > > very bad experience with thread cancelation. Therefore flags > > passed via channels/mvars or shared flags are used to stop > > threads. > > Greets, > Branimir. > On 3/18/20 10:10 AM, YueCompl wrote: > > Idiomatic resource leakage prevention in short. > > An app wants to be as responsive to its users as practically feasible, it > would try multiple paths to load-balanced resources, and use the first > response that come back, then cancel other paths. Cancellation can help > reducing vain computation in such architectures, sometimes largely enough. > > On 2020-03-18, at 16:58, Branimir Maksimovic < > branimir.maksimovic(a)gmail.com> wrote: > > What's wrong with forkIO? > > Greets, > Branimir. > On 3/18/20 9:37 AM, YueCompl via Haskell-Cafe wrote: > > If not for tight loops or other CPU intensive tasks, you may be interested > in Edh, which introduces Go's goroutine to GHC runtime. But Edh threads add > much higher overhead on top of GHC threads, so there's a price to pay for > simplicity of end programmer's job. > > It's briefly described at > https://github.com/e-wrks/edh/tree/master/Tour#program--threading-model . > This is very new and I'm right now actively working on it for PoC of an STM > powered in-memory graph database implementation. > > Best regards, > Compl > > On 2020-03-18, at 11:15, Niklas Hambüchen <mail(a)nh2.me> wrote: > > I've you're new to async, also check out my recent rework of the docs that > talk about this topic specifically: > > https://github.com/simonmar/async/pull/105/files > > (To be available in the next release of async.) > _______________________________________________ > 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. > > > > _______________________________________________ > 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. > > _______________________________________________ > 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. > > > > > > > > ---------- Forwarded message ---------- > From: Chris Done <haskell-cafe(a)chrisdone.com> > To: haskell-cafe(a)haskell.org > Cc: > Bcc: > Date: Wed, 18 Mar 2020 11:21:29 +0000 > Subject: [Haskell-cafe] Adding Content-Addressable Storage to GHC > Hi all, > > Is there any effort or designs ongoing to add CAS (content-addressable > storage) to GHC, as in Unison? < > https://www.unisonweb.org/docs/tour/> > > == The idea == > > The summary of the idea is simply that top-level declarations can be > addressed by a hash of their contents. Recursive definitions are > transformed into the worker/wrapper to eliminate the self-referencing issue > of hashing. > > == Why I want this == > > There are lots of advantages to this, but the one that excites me the most > is that we can move to running tests, especially property tests, at > compile-time. > > The main downside to running tests at compile-time, as seen done with > template-haskell is that you will re-run tests every time the module is > recompiled, making your dev cycle slower. However, if your tests are keyed > upon CAS hashes, then those hashes are only invalidated when individual > declarations actually change. This means the re-running of tests becomes > granular at the declaration-level. When a single test completes, either > successfully or not, you can cache the result and lookup the result next > time, using e.g. the SHA512 of the expression evaluated. > > Therefore you could change a single function in a library and it would > only re-run the tests that are actually affected, rather than running all > the tests in the whole module, and rather than the more typical approach > which is running ALL tests in a test suite just because one thing changed. > > If you can couple tests with code then you can avoid the decoupling of > code from the tests. > > == Implementation approaches == > > There are various ways to implement this with varying degrees of > satisfaction: > > 1. Use TH: reify declarations, inspect the AST, and produce a SHA512. Use > ambient values such as the GHC version, instances in scope, extensions, ghc > options, etc. With TH, I'm confident that you can only achieve an imperfect > hash because I doubt that all information is available to TH. > > Names that come from external packages could be treated as CAS'd at the > scope of the package's installed hash. Ideally, you could have granularity > into other packages. But it's not a necessity if you just want caching for > your current development package. > > 2. Use a source plugin. A source plugin is already capable of accessing > all GHC context information, so this might lead to more of a perfect hash. > > 3. Add it to GHC directly. Exposing a `expressionSHA512 :: Exp -> > ByteString` could be one imaginary way to access this information. With > such a function you could implement caching of fine-grained tests. > > A related discussion is the deterministic builds: > https://gitlab.haskell.org/ghc/ghc/wikis/deterministic-builds > > Anyone else exploring this? > > Cheers, > > Chris > > > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe >

1 0

[HiW'20] Call for Talks
by Ben Gamari 16 Mar '20

16 Mar '20

Hello everyone, Haskell Implementors Workshop is calling for talk proposals. Co-located with ICFP, HiW is an ideal place to describe a Haskell library, a Haskell extension, compiler, works-in-progress, demo a new Haskell-related tool, or even propose future lines of Haskell development. The deadline for submissions is July 2nd 2020. Call for Talks ============== The 12th Haskell Implementors’ Workshop is to be held alongside ICFP 2020 this year in New Jersey. It is a forum for people involved in the design and development of Haskell implementations, tools, libraries, and supporting infrastructure, to share their work and discuss future directions and collaborations with others. Talks and/or demos are proposed by submitting an abstract, and selected by a small program committee. There will be no published proceedings. The workshop will be informal and interactive, with open spaces in the timetable and room for ad-hoc discussion, demos and lightning talks. Scope and Target Audience ------------------------- It is important to distinguish the Haskell Implementors’ Workshop from the Haskell Symposium which is also co-located with ICFP 2020. The Haskell Symposium is for the publication of Haskell-related research. In contrast, the Haskell Implementors’ Workshop will have no proceedings – although we will aim to make talk videos, slides and presented data available with the consent of the speakers. The Implementors’ Workshop is an ideal place to describe a Haskell extension, describe works-in-progress, demo a new Haskell-related tool, or even propose future lines of Haskell development. Members of the wider Haskell community encouraged to attend the workshop – we need your feedback to keep the Haskell ecosystem thriving. Students working with Haskell are specially encouraged to share their work. The scope covers any of the following topics. There may be some topics that people feel we’ve missed, so by all means submit a proposal even if it doesn’t fit exactly into one of these buckets: - Compilation techniques - Language features and extensions - Type system implementation - Concurrency and parallelism: language design and implementation - Performance, optimization and benchmarking - Virtual machines and run-time systems - Libraries and tools for development or deployment Talks ----- We invite proposals from potential speakers for talks and demonstrations. We are aiming for 20-minute talks with 5 minutes for questions and changeovers. We want to hear from people writing compilers, tools, or libraries, people with cool ideas for directions in which we should take the platform, proposals for new features to be implemented, and half-baked crazy ideas. Please submit a talk title and abstract of no more than 300 words. Submissions can be made via HotCRP at https://icfp-hiw20.hotcrp.com/ until July 2nd (anywhere on earth). We will also have lightning talks session. These have been very well received in recent years, and we aim to increase the time available to them. Lightning talks be ~7mins and are scheduled on the day of the workshop. Suggested topics for lightning talks are to present a single idea, a work-in-progress project, a problem to intrigue and perplex Haskell implementors, or simply to ask for feedback and collaborators. Logistics --------- We recognize the on-going threat that COVID-19 poses to our participants' safety. While August is nearly half a year away, we must account for the possibility that the virus continues to pose a significant threat into the summer. For this reason, we are investigating options that would allow remote presentations this year. In light of this, we urge potential presenters not to be discouraged from submitting and encourage participants to keep time open in their calendars, regardless of the on-going COVID situation. Rest assured that the conference organizers are working to ensure that the Implementors Workshop can be held safely and productively, regardless of how the COVID-19 situation evolves. Program Committee ----------------- - Andrey Mokhov (Newcastle University) - Ben Gamari (Well-Typed LLP) - Christian Baaij (QBayLogic) - George Karachalias (Tweag I/O) - Klara Marntirosian (KU Leuven) - Matthew Pickering (Univeristy of Bristol) - Ryan Scott (Indiana University Bloomington) Best wishes, Ben

1 0

Re: [Haskell-cafe] Data.Map - visiting tree nodes withi a given key range ?
by Olaf Klinke 16 Mar '20

16 Mar '20

You can roll your own indexKeyRange using the Data.Map.Internal module which exposes the (currently used) Map implementation. Also note that if the list of values in range is to be consumed immediately, you might want to go for a fold-based function: foldlWithRange :: (a -> k -> b -> a) -> (a,a) -> b -> Map k a -> b Olaf

2 5

Data.Map - visiting tree nodes within a given key range ?
by Compl Yue 15 Mar '20

15 Mar '20

Hello, I have a question regarding 'Data.Map' api, filed an issue https://github.com/haskell/containers/issues/708 And may be I can ask here at the same time? I'm not sure why|Data.Map|doesn't have a key range based visiting API, I figured out I can do it this way: |indexKeyRange :: IndexKey -> IndexKey -> Map IndexKey Object -> [(IndexKey, Object)] indexKeyRange !minKey !maxKey = toList . takeWhileAntitone (<= maxKey) . dropWhileAntitone (< minKey) | But wouldn't it save the computation needed to re-balance the intermediate tree generated ? Or that re-balancing can be optimized out actually ? I am creating an in-memory graph database, using|Data.Map.Strict.Map|as business object indices with specified object attributes. The typical scenario will be querying a small number of entries by key range, out of possibly all business objects of a certain class globally, so the implementation above would work, but not reasonable by far as it seems. I think a lazy list returned by mere node visiting (i.e. no new node creation) would satisfy my needs, or I missed something ? Thanks, Compl

2 1