- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] static analysis of a C-like language
by Olaf Klinke 04 Dec '18

04 Dec '18

> Hello Olaf, > > to me that sounds as if you want to do an abstract interpretation with a > forward collecting semantics that employs non-relational abstract > domains for the primitive data types and summarizes the dimensions of > arrays. ... > I would start by writing a simple interpreter for the language to be > analyzed. That way you fix messy details before they bite you, e.g. the > order in which submodules are loaded and initialized. I was hoping not having to write an interpreter (because the language author wrote a translation to C++ already), but if that is the way to go, I'll do it. As I understand it, the Haskell semantics should contain just enough substance so that the errors I am after will cause hiccups in the Haskell compiler? That is indeed a compelling approach. What this does not address is the question about error reporting: How could a translation to Haskell preserve information about scope, source position and masking? Can I leverage the ghc API for that? Regards, Olaf

3 2

10 PhD studentships in Nottingham
by Graham Hutton 04 Dec '18

04 Dec '18

Dear all, The School of Computer Science at the University of Nottingham is seeking applications for 10 fully-funded PhD studentships: https://tinyurl.com/10-phds-2019 Applicants in the area of the Functional Programming Laboratory (https://tinyurl.com/fp-notts) are strongly encouraged! If you are interested in applying, please contact a potential supervisor at least two weeks prior to the 18th January deadline: Thorsten Altenkirch - constructive logic, proof assistants, homotopy type theory, category theory, lambda calculus. Venanzio Capretta - type theory, mathematical logic, corecursive structures, proof assistants, category theory, epistemic logic. Graham Hutton - functional programming, program calculation and transformation, correctness and efficiency, category theory. Henrik Nilsson - functional reactive programming, modelling and simulation, domain-specific languages, probabilistic languages. Best wishes, Graham +-----------------------------------------------------------+ 10 Fully-Funded PhD Studentships School of Computer Science University of Nottingham, UK https://tinyurl.com/10-phds-2019 Applications are invited for up to ten fully-funded PhD studentships in the School of Computer Science at the University of Nottingham, starting on 1 October 2019. The topics for the studentships are open, but should relate to one of the School’s research groups: Agents Lab; Automated Scheduling and Planning; Computer Vision Lab; Data Driven Algorithms, Systems and Design; Functional Programming Lab; Intelligent Modelling and Analysis; Uncertainty in Data and Decision Making; Mixed Reality Lab. The studentships are for a minimum of three years and include a stipend of £14,777 per year and tuition fees. They are open to students of any nationality. Applicants are normally expected to have a first-class MSc or BSc in Computer Science or a related discipline, and must obtain the support of a supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications. Informal enquiries may be addressed to SS-PGR-JC(a)nottingham.ac.uk. To apply, please submit the following items by email to: Christine.Fletcher(a)nottingham.ac.uk: (1) a brief covering letter that describes your reasons for wishing to pursue a PhD, your proposed research area and topic, and the name of the potential supervisor whose support you have already secured; (2) a copy of your CV, including your actual or expected degree classes, and results of all University examinations; (3) an extended example of your technical writing, such as a project report or dissertation; (4) contact details for two academic referees. Closing date for applications: Friday 18 January 2019 +-----------------------------------------------------------+ This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

1 0

ANN: hledger-1.12
by Simon Michael 03 Dec '18

03 Dec '18

hledger is a robust, cross-platform plain text accounting tool, for tracking money, time, stocks, cryptocurrencies or any other commodity, using double-entry accounting, private or shared plain text files, revision control, and command-line, curses or web UIs. Find out more at http://hledger.org and http://plaintextaccounting.org. I'm pleased to announce the release of hledger 1.12! Thank you release contributors Alex Chen, Jesse Rosenthal, Samuel May, Mykola Orliuk, Peter Simons, Moritz Kiefer, Dmitry Astapov, Felix Yan, Aiken Cairncross, and Nikhil Jha. After two years of regular quarter-end releases, I am speeding up hledger's release cadence: we now aim to release every 1-3 months, as needed or wanted, with our normal release window being the first few days of each month. Release notes (http://hledger.org/release-notes) ------------------------------------------------- hledger 1.12 * install script: ensure a new-enough version of stack; more informative output * build with GHC 8.6/base-4.12 (Peter Simons) * add required upper bound for statistics (Samuel May) * --anon anonymises more thoroughly (including linked original postings) (Moritz Kiefer) * unbalanced transaction errors now include location info (Mykola Orliuk) * accounts command: --drop also affects the default flat output, without needing an explicit --flat flag * accounts command: the --codes flag has been dropped * accounts command: filtering by non-account-name queries now works * add command: fix transaction rendering regression during data entry and in journal file * balance command: fix wrongful eliding of zero-balance parent accounts in tree mode (Dmitry Astapov) * journal format, bs/bse/cf/is commands: account directives can declare account types (#877) Previously you had to use one of the standard english account names (assets, liabilities..) for top-level accounts, if you wanted them to appear in the right place in the balancesheet, balancesheetequity, cashflow or incomestatement reports. Now you can use your preferred account names, and use account directives to declare which accounting class (Asset, Liability, Equity, Revenue or eXpense) an account (and its subaccounts) belongs to, by writing one of the letters A, L, E, R, X after the account name, after two or more spaces. This syntax may change (see issue). Experimental. Currently we allow unlimited account type declarations anywhere in the account tree. So you could declare a liability account somewhere under assets, and maybe a revenue account under that, and another asset account even further down. In such cases you start to see oddities like accounts appearing in multiple places in a tree-mode report. I have left it this way for now in case it helps with, eg, modelling contra accounts, or combining multiple files each with their own account type declarations. (In that scenario, if we only allowed type declarations on top-level accounts, or only allowed a single account of each type, complications seem likely.) * journal format: periodic transaction rules now require a double space separator. In periodic transaction rules which specify a transaction description or same-line transaction comment, this must be separated from the period expression by two or more spaces, to prevent ambiguous parsing. Eg this will parse correctly as "monthly" thanks to the double space: ~ monthly In 2020 we'll end this monthly transaction. * journal format: exact/complete balance assertions (Samuel May). A stronger kind of balance assertion, written with a double equals sign, asserts an account's complete account balance, not just the balance in one commodity. (But only if it is a single-commodity balance, for now.) Eg: 1/1 (a) A 1 (a) B 1 (a) 0 = A 1 ; commodity A balance assertion, succeeds (a) 0 == A 1 ; complete balance assertion, fails * journal format: account directives now allow whitespace or a comment after the account name * journal format: using ~ for home directory in include directives now works (#896) (Mykola Orliuk) * journal format: prevent misleading parse error messages with cyclic include directives (#853) (Alex Chen) * journal format: transaction modifier multipliers handle total-priced amounts correctly (#928). Multipliers (*N) in transaction modifier rules did not multiply total-priced amounts properly. Now the total prices are also multiplied, keeping the transaction balanced. * journal format: do amount inference/balance assignments/assertions before transaction modifiers (#893, #908) (Jesse Rosenthal) Previously, transaction modifier (auto postings) rules were applied before missing amounts were inferred. This meant amount multipliers could generate too many missing-amount postings, making the transaction unbalanceable (#893). Now, missing amount inference (and balance assignments, and balance assertions, which are interdependent) are done earlier, before transaction modifier rules are applied (#900, #903). Also, we now disallow the combination of balance assignments and transaction modifier rules which both affect the same account, which could otherwise cause confusing balance assertion failures (#912). (Because assignments now generate amounts to satisfy balance assertions before transaction modifier rules are applied (#908).) * journal format: periodic transaction rules are now aware of Y default year directives. (#892) Ie when a default year Y is in effect, they resolve partial or relative dates using Y/1/1 as the reference date, rather than today's date. hledger-ui 1.12 * fix "Any" build error with GHC < 8.4 * error screen: always show error position properly (#904) (Mykola Orliuk) * accounts screen: show correct balances when there's only periodic transactions * drop the --status-toggles flag * periodic transactions and transaction modifiers are always enabled. Rule-based transactions and postings are always generated (--forecast and --auto are always on). Experimental. * escape key resets to flat mode. Flat mode is the default at startup. Probably it should reset to tree mode if --tree was used at startup. * tree mode tweaks: add --tree/-T/-F flags, make flat mode the default, toggle tree mode with T, ensure a visible effect on register screen * hide future txns by default, add --future flag, toggle with F. You may have transactions dated later than today, perhaps piped from print --forecast or recorded in the journal, which you don't want to see except when forecasting. By default, we now hide future transactions, showing "today's balance". This can be toggled with the F key, which is easier than setting a date query. --present and --future flags have been added to set the initial mode. (Experimental. Interactions with date queries have not been explored.) * quick help tweaks; try to show most useful info first * reorganise help dialog, fit content into 80x25 again * styling tweaks; cyan/blue -> white/yellow * less noisy styling in horizontal borders (#838) * register screen: positive amounts: green -> black The green/red scheme helped distinguish the changes column from the black/red balance column, but the default green is hard to read on the pale background in some terminals. Also the changes column is non-bold now. Getting started: ---------------- All install methods are described at http://hledger.org/download . You can download windows binaries, or use a package manager, though in some cases these will install an older hledger version. You can build the latest hledger packages with stack: $ stack install --resolver=lts-12 megaparsec-7.0.4 cassava-megaparsec-2.0.0 config-ini-0.2.3.0 hledger-lib-1.12 hledger-1.12 [hledger-ui-1.12] [hledger-web-1.12] [hledger-api-1.12] or with cabal: $ cabal update && cabal install hledger-1.12 [hledger-ui-1.12] [hledger-web-1.12] [hledger-api-1.12] or with the hledger installer, on systems with bash installed (handy if you don't have a working stack or cabal): $ curl -s https://raw.githubusercontent.com/simonmichael/hledger/master/hledger-insta… > hledger-install.sh $ less hledger-install.sh # satisfy yourself that the script is safe $ bash hledger-install.sh Some commands to try: $ hledger add # record some transactions, with guidance $ hledger print # show recorded transactions $ hledger balance # show totals by account $ hledger -h # show quick help $ hledger # list available commands $ hledger help # list built-in manuals To get oriented, see the tutorials and manuals at http://hledger.org ; say hello and ask questions in the #hledger IRC channel on Freenode, accessible at http://irc.hledger.org . New users and contributors are always welcome! Best, -Simon

1 0

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