News aggregator

Mark Jason Dominus: Controlling the KDE screen locking works now

Planet Haskell - Thu, 07/28/2016 - 1:10pm

Yesterday I wrote about how I was trying to control the KDE screenlocker's timeout from a shell script and all the fun stuff I learned along the way. Then after I published the article I discovered that my solution didn't work. But today I fixed it and it does work.

What didn't work

I had written this script:

timeout=${1:-3600} perl -i -lpe 's/^Enabled=.*/Enabled=False/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /MainApplication reparseConfiguration sleep $timeout perl -i -lpe 's/^Enabled=.*/Enabled=True/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /MainApplication reparseConfiguration

The strategy was: use perl to rewrite the screen locker's configuration file, and then use qdbus to send a D-Bus message to the screen locker to order it to load the updated configuration.

This didn't work. The System Settings app would see the changed configuration, and report what I expected, but the screen saver itself was still behaving according to the old configuration. Maybe the qdbus command was wrong or maybe the whole theory was bad.

More strace

For want of anything else to do (when all you have is a hammer…), I went back to using strace to see what else I could dig up, and tried

strace -ff -o /tmp/ss/s /usr/bin/systemsettings

which tells strace to write separate files for each process or thread. I had a fantasy that by splitting the trace for each process into a separate file, I might solve the mysterious problem of the missing string data. This didn't come true, unfortunately.

I then ran tail -f on each of the output files, and used systemsettings to update the screen locker configuration, looking to see which the of the trace files changed. I didn't get too much out of this. A great deal of the trace was concerned with X protocol traffic between the application and the display server. But I did notice this portion, which I found extremely suggestive, even with the filenames missing:

3106 open(0x2bb57a8, O_RDWR|O_CREAT|O_CLOEXEC, 0666) = 18 3106 fcntl(18, F_SETFD, FD_CLOEXEC) = 0 3106 chmod(0x2bb57a8, 0600) = 0 3106 fstat(18, {...}) = 0 3106 write(18, 0x2bb5838, 178) = 178 3106 fstat(18, {...}) = 0 3106 close(18) = 0 3106 rename(0x2bb5578, 0x2bb4e48) = 0 3106 unlink(0x2b82848) = 0

You may recall that my theory was that when I click the “Apply” button in System Settings, it writes out a new version of $HOME/.kde/share/config/kscreensaverrc and then orders the screen locker to reload the configuration. Even with no filenames, this part of the trace looked to me like the replacement of the configuration file: a new file is created, then written, then closed, and then the rename replaces the old file with the new one. If I had been thinking about it a little harder, I might have thought to check if the return value of the write call, 178 bytes, matched the length of the file. (It does.) The unlink at the end is deleting the semaphore file that System Settings created to prevent a second process from trying to update the same file at the same time.

Supposing that this was the trace of the configuration update, the next section should be the secret sauce that tells the screen locker to look at the new configuration file. It looked like this:

3106 sendmsg(5, 0x7ffcf37e53b0, MSG_NOSIGNAL) = 168 3106 poll([?] 0x7ffcf37e5490, 1, 25000) = 1 3106 recvmsg(5, 0x7ffcf37e5390, MSG_CMSG_CLOEXEC) = 90 3106 recvmsg(5, 0x7ffcf37e5390, MSG_CMSG_CLOEXEC) = -1 EAGAIN (Resource temporarily unavailable) 3106 sendmsg(5, 0x7ffcf37e5770, MSG_NOSIGNAL) = 278 3106 sendmsg(5, 0x7ffcf37e5740, MSG_NOSIGNAL) = 128

There is very little to go on here, but none of it is inconsistent with the theory that this is the secret sauce, or even with the more advanced theory that it is the secret suace and that the secret sauce is a D-Bus request. But without seeing the contents of the messages, I seemed to be at a dead end.


Browsing random pages about the KDE screen locker, I learned that the lock screen configuration component could be run separately from the rest of System Settings. You use

kcmshell4 --list

to get a list of available components, and then

kcmshell4 screensaver

to run the screensaver component. I started running strace on this command instead of on the entire System Settings app, with the idea that if nothing else, the trace would be smaller and perhaps simpler, and for some reason the missing strings appeared. That suggestive block of code above turned out to be updating the configuration file, just as I had suspected:

open("/home/mjd/.kde/share/config/", O_RDWR|O_CREAT|O_CLOEXEC, 0666) = 19 fcntl(19, F_SETFD, FD_CLOEXEC) = 0 chmod("/home/mjd/.kde/share/config/", 0600) = 0 fstat(19, {st_mode=S_IFREG|0600, st_size=0, ...}) = 0 write(19, "[ScreenSaver]\nActionBottomLeft=0\nActionBottomRight=0\nActionTopLeft=0\nActionTopRight=2\nEnabled=true\nLegacySaverEnabled=false\nPlasmaEnabled=false\nSaver=krandom.desktop\nTimeout=60\n", 177) = 177 fstat(19, {st_mode=S_IFREG|0600, st_size=177, ...}) = 0 close(19) = 0 rename("/home/mjd/.kde/share/config/", "/home/mjd/.kde/share/config/kscreensaverrc") = 0 unlink("/home/mjd/.kde/share/config/kscreensaverrc.lock") = 0

And the following secret sauce was revealed as:

sendmsg(7, {msg_name(0)=NULL, msg_iov(2)=[{"l\1\0\1\30\0\0\0\v\0\0\0\177\0\0\0\1\1o\0\25\0\0\0/org/freedesktop/DBus\0\0\0\6\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\2\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\3\1s\0\f\0\0\0GetNameOwner\0\0\0\0\10\1g\0\1s\0\0", 144}, {"\23\0\0\0org.kde.screensaver\0", 24}], msg_controllen=0, msg_flags=0}, MSG_NOSIGNAL) = 168 sendmsg(7, {msg_name(0)=NULL, msg_iov(2)=[{"l\1\1\1\206\0\0\0\f\0\0\0\177\0\0\0\1\1o\0\25\0\0\0/org/freedesktop/DBus\0\0\0\6\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\2\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\3\1s\0\10\0\0\0AddMatch\0\0\0\0\0\0\0\0\10\1g\0\1s\0\0", 144}, {"\201\0\0\0type='signal',sender='org.freedesktop.DBus',interface='org.freedesktop.DBus',member='NameOwnerChanged',arg0='org.kde.screensaver'\0", 134}], msg_controllen=0, msg_flags=0}, MSG_NOSIGNAL) = 278 sendmsg(7, {msg_name(0)=NULL, msg_iov(2)=[{"l\1\0\1\0\0\0\0\r\0\0\0j\0\0\0\1\1o\0\f\0\0\0/ScreenSaver\0\0\0\0\6\1s\0\23\0\0\0org.kde.screensaver\0\0\0\0\0\2\1s\0\23\0\0\0org.kde.screensaver\0\0\0\0\0\3\1s\0\t\0\0\0configure\0\0\0\0\0\0\0", 128}, {"", 0}], msg_controllen=0, msg_flags=0}, MSG_NOSIGNAL) = 128 sendmsg(7, {msg_name(0)=NULL, msg_iov(2)=[{"l\1\1\1\206\0\0\0\16\0\0\0\177\0\0\0\1\1o\0\25\0\0\0/org/freedesktop/DBus\0\0\0\6\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\2\1s\0\24\0\0\0org.freedesktop.DBus\0\0\0\0\3\1s\0\v\0\0\0RemoveMatch\0\0\0\0\0\10\1g\0\1s\0\0", 144}, {"\201\0\0\0type='signal',sender='org.freedesktop.DBus',interface='org.freedesktop.DBus',member='NameOwnerChanged',arg0='org.kde.screensaver'\0", 134}]

(I had to tell give strace the -s 256 flag to tell it not to truncate the string data to 32 characters.)

Binary gibberish

A lot of this is illegible, but it is clear, from the frequent mentions of DBus, and from the names of D-Bus objects and methods, that this is is D-Bus requests, as theorized. Much of it is binary gibberish that we can only read if we understand the D-Bus line protocol, but the object and method names are visible. For example, consider this long string:


With qdbus I could confirm that there was a service named org.freedesktop.DBus with an object named / that supported a NameOwnerChanged method which expected three QString arguments. Presumably the first of these was org.kde.screensaver and the others are hiding in other the 134 characters that strace didn't expand. So I may not understand the whole thing, but I could see that I was on the right track.

That third line was the key:

sendmsg(7, {msg_name(0)=NULL, msg_iov(2)=[{"… /ScreenSaver … org.kde.screensaver … org.kde.screensaver … configure …", 128}, {"", 0}], msg_controllen=0, msg_flags=0}, MSG_NOSIGNAL) = 128

Huh, it seems to be asking the screensaver to configure itself. Just like I thought it should. But there was no configure method, so what does that configure refer to, and how can I do the same thing?

But org.kde.screensaver was not quite the same path I had been using to talk to the screen locker—I had been using org.freedesktop.ScreenSaver, so I had qdbus list the methods at this new path, and there was a configure method.

When I tested

qdbus org.kde.screensaver /ScreenSaver configure

I found that this made the screen locker take note of the updated configuration. So, problem solved!

(As far as I can tell, org.kde.screensaver and org.freedesktop.ScreenSaver are completely identical. They each have a configure method, but I had overlooked it—several times in a row—earlier when I had gone over the method catalog for org.freedesktop.ScreenSaver.)

The working script is almost identical to what I had yesterday:

timeout=${1:-3600} perl -i -lpe 's/^Enabled=.*/Enabled=False/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /ScreenSaver configure sleep $timeout perl -i -lpe 's/^Enabled=.*/Enabled=True/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /ScreenSaver configure

That's not a bad way to fail, as failures go: I had a correct idea about what was going on, my plan about how to solve my problem would have worked, but I was tripped up by a trivium; I was calling MainApplication.reparseConfiguration when I should have been calling ScreenSaver.configure.

What if I hadn't been able to get strace to disgorge the internals of the D-Bus messages? I think I would have gotten the answer anyway. One way to have gotten there would have been to notice the configure method documented in the method catalog printed out by qdbus. I certainly looked at these catalogs enough times, and they are not very large. I don't know why I never noticed it on my own. But I might also have had the idea of spying on the network traffic through the D-Bus socket, which is under /tmp somewhere.

I was also starting to tinker with dbus-send, which is like qdbus but more powerful, and can post signals, which I think qdbus can't do, and with gdbus, another D-Bus introspector. I would have kept getting more familiar with these tools and this would have led somewhere useful.

Or had I taken just a little longer to solve this, I would have followed up on Sumana Harihareswara’s suggestion to look at Bustle, which is a utility that logs and traces D-Bus requests. It would certainly have solved my problem, because it makes perfectly clear that clicking that apply button invoked the configure method:

I still wish I knew why strace hadn't been able to print out those strings through.

Categories: Offsite Blogs

Mark Jason Dominus: Controlling KDE screen locking from a shell script

Planet Haskell - Wed, 07/27/2016 - 4:59pm

Lately I've started watching stuff on Netflix. Every time I do this, the screen locker kicks in sixty seconds in, and I have to unlock it, pause the video, and adjust the system settings to turn off the automatic screen locker. I can live with this.

But when the show is over, I often forget to re-enable the automatic screen locker, and that I can't live with. So I wanted to write a shell script:

#!/bin/sh auto-screen-locker disable sleep 3600 auto-screen-locker enable

Then I'll run the script in the background before I start watching, or at least after the first time I unlock the screen, and if I forget to re-enable the automatic locker, the script will do it for me.

The question is: how to write auto-screen-locker?


My first idea was: maybe there is actually an auto-screen-locker command, or a system-settings command, or something like that, which was being run by the System Settings app when I adjusted the screen locker from System Settings, and all I needed to do was to find out what that command was and to run it myself.

So I tried running System Settings under strace -f and then looking at the trace to see if it was execing anything suggestive.

It wasn't, and the trace was 93,000 lines long and frighting. Halfway through, it stopped recording filenames and started recording their string addresses instead, which meant I could see a lot of calls to execve but not what was being execed. I got sidetracked trying to understand why this had happened, and I never did figure it out—something to do with a call to clone, which is like fork, but different in a way I might understand once I read the man page.

The first thing the cloned process did was to call set_robust_list, which I had never heard of, and when I looked for its man page I found to my surprise that there was one. It begins:

NAME get_robust_list, set_robust_list - get/set list of robust futexes

And then I felt like an ass because, of course, everyone knows all about the robust futex list, duh, how silly of me to have forgotten ha ha just kidding WTF is a futex? Are the robust kind better than regular wimpy futexes?

It turns out that Ingo Molnár wrote a lovely explanation of robust futexes which are actually very interesting. In all seriousness, do check it out.

I seem to have digressed. This whole section can be summarized in one sentence:

strace was no help and took me a long way down a wacky rabbit hole.

Sorry, Julia!

Stack Exchange

The next thing I tried was Google search for kde screen locker. The second or third link I followed was to this StackExchange question, “What is the screen locking mechanism under KDE? It wasn't exactly what I was looking for but it was suggestive and pointed me in the right direction. The crucial point in the answer was a mention of

qdbus org.freedesktop.ScreenSaver /ScreenSaver Lock

When I saw this, it was like a new section of my brain coming on line. So many things that had been obscure suddenly became clear. Things I had wondered for years. Things like “What are these horrible

Object::connect: No such signal org::freedesktop::UPower::DeviceAdded(QDBusObjectPath)

messages that KDE apps are always spewing into my terminal?” But now the light was on.

KDE is built atop a toolkit called Qt, and Qt provides an interprocess communication mechanism called “D-Bus”. The qdbus command, which I had not seen before, is apparently for sending queries and commands on the D-Bus. The arguments identify the recipient and the message you are sending. If you know the secret name of the correct demon, and you send it the correct secret command, it will do your bidding. ( The mystery message above probably has something to do with the app using an invalid secret name as a D-Bus address.)

Often these sorts of address hierarchies work well in theory and then fail utterly because there is no way to learn the secret names. The X Window System has always had a feature called “resources” by which almost every aspect of every application can be individually customized. If you are running xweasel and want just the frame of just the error panel of just the output window to be teal blue, you can do that… if you can find out the secret names of the xweasel program, its output window, its error panel, and its frame. Then you combine these into a secret X resource name, incant a certain command to load the new resource setting into the X server, and the next time you run xweasel the one frame, and only the one frame, will be blue.

In theory these secret names are documented somewhere, maybe. In practice, they are not documented anywhere. you can only extract them from the source, and not only from the source of xweasel itself but from the source of the entire widget toolkit that xweasel is linked with. Good luck, sucker.

D-Bus has a directory

However! The authors of Qt did not forget to include a directory mechanism in D-Bus. If you run


you get a list of all the addressable services, which you can grep for suggestive items, including org.freedesktop.ScreenSaver. Then if you run

qdbus org.freedesktop.ScreenSaver

you get a list of all the objects provided by the org.freedesktop.ScreenSaver service; there are only seven. So you pick a likely-seeming one, say /ScreenSaver, and run

qdbus org.freedesktop.ScreenSaver /ScreenSaver

and get a list of all the methods that can be called on this object, and their argument types and return value types. And you see for example

method void org.freedesktop.ScreenSaver.Lock()

and say “I wonder if that will lock the screen when I invoke it?” And then you try it:

qdbus org.freedesktop.ScreenSaver /ScreenSaver Lock

and it does.

That was the most important thing I learned today, that I can go wandering around in the qdbus hierarchy looking for treasure. I don't yet know exactly what I'll find, but I bet there's a lot of good stuff.

When I was first learning Unix I used to wander around in the filesystem looking at all the files, and I learned a lot that way also.

  • “Hey, look at all the stuff in /etc! Huh, I wonder what's in /etc/passwd?”

  • “Hey, /etc/protocols has a catalog of protocol numbers. I wonder what that's for?”

  • “Hey, there are a bunch of files in /usr/spool/mail named after users and the one with my name has my mail in it!”

  • “Hey, the manuals are all under /usr/man. I could grep them!”

Later I learned (by browsing in /usr/man/man7) that there was a hier(7) man page that listed points of interest, including some I had overlooked.

The right secret names

Everything after this point was pure fun of the “what happens if I turn this knob” variety. I tinkered around with the /ScreenSaver methods a bit (there are twenty) but none of them seemed to be quite what I wanted. There is a

method uint Inhibit(QString application_name, QString reason_for_inhibit)

method which someone should be calling, because that's evidently what you call if you are a program playing a video and you want to inhibit the screen locker. But the unknown someone was delinquent and it wasn't what I needed for this problem.

Then I moved on to the /MainApplication object and found

method void org.kde.KApplication.reparseConfiguration()

which wasn't quite what I was looking for either, but it might do: I could perhaps modify the configuration and then invoke this method. I dimly remembered that KDE keeps configuration files under $HOME/.kde, so I ls -la-ed that and quickly found share/config/kscreensaverrc, which looked plausible from the outside, and more plausible when I saw what was in it:

Enabled=True Timeout=60

among other things. I hand-edited the file to change the 60 to 243, ran

qdbus org.freedesktop.ScreenSaver /MainApplication reparseConfiguration

and then opened up the System Settings app. Sure enough, the System Settings app now reported that the lock timeout setting was “4 minutes”. And changing Enabled=True to Enabled=False and back made the System Settings app report that the locker was enabled or disabled.

The answer

So the script I wanted turned out to be:

timeout=${1:-3600} perl -i -lpe 's/^Enabled=.*/Enabled=False/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /MainApplication reparseConfiguration sleep $timeout perl -i -lpe 's/^Enabled=.*/Enabled=True/' $HOME/.kde/share/config/kscreensaverrc qdbus org.freedesktop.ScreenSaver /MainApplication reparseConfiguration

Problem solved, but as so often happens, the journey was more important than the destination.

I am greatly looking forward to exploring the D-Bus hierarchy and sending all sorts of inappropriate messages to the wrong objects.

Just before he gets his ass kicked by Saruman, that insufferable know-it-all Gandalf says “He who breaks a thing to find out what it is has left the path of wisdom.” If I had been Saruman, I would have kicked his ass at that point too.


Right after I posted this, I started watching Netflix. The screen locker cut in after sixty seconds. “Aha!” I said. “I'll run my new script!”

I did, and went back to watching. Sixty seconds later, the screen locker cut in again. My script doesn't work! The System Settings app says the locker has been disabled, but it's mistaken. Probably it's only reporting the contents of the configuration file that I edited, and the secret sauce is still missing. The System Settings app does something to update the state of the locker when I click that “Apply” button, and I thought that my qdbus command was doing the same thing, but it seems that it isn't.

I'll figure this out, but maybe not today. Good night all!

[ Addendum 20160728: I figured it out the next day ]

[ Addendum 20160729: It has come to my attention that there is actually a program called xweasel. ]

Categories: Offsite Blogs

Managed Languages & Runtimes Week '16 - Call forParticipation

General haskell list - Wed, 07/27/2016 - 9:57am
Managed Languages & Runtimes Week '16 PPPJ '16 / JTRES '16 / VMM '16 August 29 - September 2, 2016 Lugano, Switzerland ------------------------------------------------------------------------------- Managed Languages & Runtimes Week '16 is a premier forum for presenting and discussing innovations and breakthroughs in the area of programming languages and runtime systems, which form the basis of many modern computing systems, from small scale (embedded and real-time systems) to large-scale (cloud-computing and big-data platforms). Managed Languages & Runtimes Week '16 features three international academic and industry venues for the first time: - PPPJ '16 - 13th International Conference on Principles and Practices of Programming on the Java Platform: virtual machines, languages, and tools - A forum for researchers, practitioners, and educators to present and discuss novel results on all aspects of managed languages and their runtime systems, including virtual ma
Categories: Incoming News

Fully Abstract Compilation via Universal Embedding

Lambda the Ultimate - Wed, 07/27/2016 - 9:57am

Fully Abstract Compilation via Universal Embedding by Max S. New, William J. Bowman, and Amal Ahmed:

A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context.

We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation—specifically, closure conversion of simply typed λ-calculus with recursive types—uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a deep embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.

Potentially a promising step forward to secure multilanguage runtimes. We've previously discussed security vulnerabilities caused by full abstraction failures here and here. The paper also provides a comprehensive review of associated literature, like various means of protection, back translations, embeddings, etc.

Categories: Offsite Discussion

The team: Updates for July

Planet Haskell - Tue, 07/26/2016 - 6:00pm

Since July we've made a number of updates, mostly content. Here's a rundown:

  • Intero was added to the site under /intero.
  • We've added Intero to the get-started page.
  • We've added the /tutorial/ hierarchy, with a sample tutorial.
  • The /packages page has been renamed to /libraries. The idea being this might be more obvious to newcomers from other languages.
  • Added a library description for conduit.

The complete diff can be found here.

Categories: Offsite Blogs

Forcing the kind in data

haskell-cafe - Tue, 07/26/2016 - 11:36am
Hi, if I have: data Foobar a b = Foobar it has kind: * -> * -> * How can I force the kind to: (* -> *) -> * -> * ? Thank you! _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: Only members subscribed via the mailman list are allowed to post.
Categories: Offsite Discussion

ETAPS 2017 1st call for papers

General haskell list - Tue, 07/26/2016 - 9:04am
****************************************************************** JOINT CALL FOR PAPERS 20th European Joint Conferences on Theory And Practice of Software ETAPS 2017 Uppsala, Sweden, 22-29 April 2017 ******************************************************************
Categories: Incoming News

Use GHC API in standalone executable?

haskell-cafe - Mon, 07/25/2016 - 10:03pm
I guess this depends on what you want to do. I've seen various level of GHC API usage in standalone applications, but it just depends on how much of the compiler pipeline you want to use. Their are ways to override the paths or provide stubs for programs ghc expects to be there. I've packaged API calls into shared libraries myself before, in that case I was mostly accessing the compiler frontend. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: Only members subscribed via the mailman list are allowed to post.
Categories: Offsite Discussion

Is there any way in GHC plugin to refer exposed butdefined in a hidden module?

haskell-cafe - Mon, 07/25/2016 - 4:24pm
Hi Cafe, I'm currently writing a simple GHC Typechecker plugin to augment typelevel naturals with a presburger arithmetic solver [^1]. I want to use type-class constraints to give premisses to the solver, for example, `Empty a` constraint means "a is false (empty type)". So I have to get TyCon information in TcPluginM monad and I wrote as follows: ```haskell do md <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning") classTyCon <$> (tcLookupClass =<< lookupOrig md (mkTcOcc "Empty")) ``` But this code doesn't work as expected. For example, the code ```haskell {-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-} import Data.Type.Equality import GHC.TypeLits (type (+), type (<=), type (<=?)) import Proof.Propositional (Empty(..)) predSucc :: Empty (n :~: 0) => proxy n -> (n + 1 <=? n + n) :~: 'True predSucc _ = Witness ``` resulted in the following compile-time error: ``` Can't find interface-file declaration for ty
Categories: Offsite Discussion

linking dlls with relative paths on Windows

haskell-cafe - Mon, 07/25/2016 - 1:52pm
Hi Peter, I forgot to respond to this, if you haven't received an answer to this yet then feel free to open a ticket on the ghc trac and I will take a look as soon as I have working Internet again. I don't know what the status is of this for now, the linked to stackoverfow article should work though. Also 7.10.3 has some issues when loading dependent dlls in the same folder as the main one being loaded when not on the search path. 8.0.1 should be fine. Kind regards, Tamar _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: Only members subscribed via the mailman list are allowed to post.
Categories: Offsite Discussion

Munich Haskell Meeting,2016-07-27 < at > 19:30 Augustiner Bierhalle

haskell-cafe - Mon, 07/25/2016 - 1:22pm
Dear all, This week, our monthly Munich Haskell Meeting will take place again on Wednesday, July 27 at Augustiner Bierhalle (Neuhauser Str.) at 19h30. For details see here: 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. Everybody is welcome! cu,
Categories: Offsite Discussion

Neil Mitchell: Maintainer required for Derive

Planet Haskell - Mon, 07/25/2016 - 8:45am

Summary: I'm looking for a maintainer to take over Derive. Interested?

The Derive tool is a library and set of definitions for generating fragments of code in a formulaic way from a data type. It has a mechanism for guessing the pattern from a single example, plus a more manual way of writing out generators. It supports 35 generators out of the box, and is depended upon by 75 libraries.

The tool hasn't seen much love for some time, and I no longer use it myself. It requires somewhat regular maintenance to upgrade to new versions of GHC and haskell-src-exts. There are lots of directions the tool could be taken, more derivations, integration with the GHC Generic derivation system etc. There's a few generic pieces that could be broken off (translation between Template Haskell and haskell-src-exts, the guessing mechanism).

Anyone who is interested should comment on the GitHub ticket. In the absence of any volunteers I may continue to do the regular upgrade work, or may instead have it taken out of Stackage and stop upgrading it.

Categories: Offsite Blogs

Dimitri Sabadie: luminance-0.6.0 sample

Planet Haskell - Mon, 07/25/2016 - 3:40am

It’s been two weeks luminance is at version 0.6.0. I’m very busy currently but I decided to put some effort into making a very minimalistic yet usable sample. The sample uses luminance and luminance-gl (the OpenGL 3.3 backend being the single one available for now).

You’ll find it here. The code is heavily commented and you can of course clone the repository and and run the executable with cargo.

I’ll post a more detailed blog post about the application I’m building with luminance right now later on.

Keep the vibe! :)

Categories: Offsite Blogs

good choice for random number generator ?

haskell-cafe - Mon, 07/25/2016 - 12:48am
There's quite a few. Many are very old. I would have like to use vector-random and got this : Data/Vector/Random/Mersenne.hs:33:18: Could not find module ‘Data.Vector.Fusion.Stream’ It is a member of the hidden package ‘vector-< at >vecto_1COyUuV1LrA1IjYnWfJnbs’. Perhaps you need to add ‘vector’ to the build-depends in your .cabal file. Use -v to see a list of the files searched for. Data/Vector/Random/Mersenne.hs:35:18: Could not find module ‘Data.Vector.Fusion.Stream.Size’ It is a member of the hidden package ‘vector-< at >vecto_1COyUuV1LrA1IjYnWfJnbs’. Perhaps you need to add ‘vector’ to the build-depends in your .cabal file. Use -v to see a list of the files searched for. I wouldn't be opposed to fixing it, but I'm wondering at this point there isn't a better package to use instead. I'm looking for both integer and floating point random numbers, uniform and gaussian. gsl-random looks promising as does mwc-random. any other suggestio
Categories: Offsite Discussion

Ken T Takusagawa: [leijaltq] Typeof as a type

Planet Haskell - Sun, 07/24/2016 - 9:03pm

Wherever one can specify a type, let it be possible to use "TYPE_OF(EXPRESSION)" instead.  For example, it can be used in type signatures and declarations of type synonyms.  Here is an example with syntax similar to Haskell:

A library has functions

f1 :: Int -> Foo;
f1 i = ...
f2 :: Foo -> Int;
f2 f = ...

The user's code importing the library might do something like

type MyFoo = TYPE_OF(f1 undefined);
intermediate :: MyFoo;
intermediate = f1 42;

consume_intermediate :: Int;
consume_intermediate = f2 intermediate;

If a new version of the library were to rename Foo into Bar, the user's code would still work unmodified.  (It is irrelevant whether the library exports Foo, later Bar, though not exporting the type would force the user to use TYPE_OF or avoid explicit type signatures, which seems silly.)

This feature could be useful during development if the names of things are not yet decided (bike shedding), but we do know how we want to use them.

The compiler will have to flag errors of circular references of TYPE_OF.

Categories: Offsite Blogs

How do I debug this RTS segfault?

haskell-cafe - Sun, 07/24/2016 - 6:50pm
Hello, I have run into this RTS bug recently. In short, when executing multiple consequtive forks, after 500-600 or so the process is terminated by SIGSEGV. I know this kind of thing is totally artificial, but still. The problem I have is that I can't get any meaningful backtrace in gdb. For example, for threaded RTS I get this (gdb) bt #0 0x0000000000560d63 in base_GHCziEventziThread_ensureIOManagerIsRunning1_info () Backtrace stopped: Cannot access memory at address 0x7fffff7fcea0 For non-threaded RTS I get this (gdb) bt #0 0x00000000007138c9 in stg_makeStablePtrzh () Backtrace stopped: Cannot access memory at address 0x7fffff7fc720 Build command: ghc --make -O2 -g -fforce-recomp fork.hs Add threaded if needed. I was able to reproduce this bug with both GHC 7.10.3 and todays HEAD with the code below. With best regards. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to:
Categories: Offsite Discussion

Richard Eisenberg: Dependent types in Haskell: Progress Report

Planet Haskell - Sun, 07/24/2016 - 12:27pm

It was drawn to my attention that there is an active Reddit thread about the future of dependent types in Haskell. (Thanks for the heads up, @thomie!) Instead of writing a long response inline in Reddit, it seems best to address the (very knowledgeable, respectful, and all around heartening) debate here.

When can we expect dependent types in GHC?

The short answer: GHC 8.4 (2018) at the very earliest. More likely 8.6 or 8.8 (2019-20).

Here is the schedule as I see it:

  • GHC 8.2: Clean up some of the lingering issues with -XTypeInType. As I will be starting a new job (Asst. Prof. at Bryn Mawr College) this fall, I simply won’t have the opportunity to do more than some cleanup work for the next release. Also, quite frankly, I need a release cycle off from the challenge of putting in a large new feature. Polishing up -XTypeInType for release took probably an extra full month of unexpected work time! I don’t regret this in the slightest, but I could use a cycle off.
  • GHC 8.4: This depends on what other research opportunities come up in the next year and how much more attention -XTypeInType needs. If all goes well this fall and I can get a few publications out in the next year (certainly possible – I have several in the works), then I could conceivably start primary implementation of -XDependentTypes next summer. The odds that it will be in a state to merge for 8.4 are slim, however.
  • GHC 8.6: We’re now talking about a real possibility here. Assuming I start the implementation next summer, this would give me a year and a half to complete it. I desperately wish to avoid merging late in the cycle (which is what made -XTypeInType so stressful) so perhaps merging soon after GHC 8.4 comes out is a good goal. If this slips, GHC 8.8 seems like quite a likely candidate.

Regardless of the schedule, I have every intention of actually doing this work.

One major oversight in the schedule above: I have completely discounted the possibility of collaborators in coding this up. Do you wish to help make this a reality? If so, let’s talk. I’ll admit that there may be a bit of a hill for an outside collaborator to climb before I really start collaborating in earnest, so be prepared to show (or create!) evidence that you’re good at getting your hands dirty in the greasy wheels of GHC’s typechecker without very much oversight. I’ve encouraged several of you on Trac/Phab – you know who you are, I hope. For others who have not yet contributed to GHC: you’re likely best served starting smaller than implementing dependent types! But let’s talk anyway, if you’re interested.

What is the design of dependent types in Haskell?

I expect to hand in my dissertation in the next two weeks. While I am developing it in the public eye (and warmly welcome issues to be posted), there is no publicly available PDF build. Building instructions are in the README. I will post a built PDF when I hand in my draft to my thesis committee. I will be defending on September 1 and will likely make some revisions (as suggested by my committee) afterward.

Readers here will likely be most interested in Chapters 3 and 4. Chapter 3 will contain (I’m still writing it!) numerous examples of dependent types in Haskell and how they might be useful. Chapter 4 presents the design of dependent types in Haskell as a diff over current Haskell. This design is not yet up to the standard of the Haskell Reports, mostly because it is unimplemented and seems not worth the effort of formalization until we know it is implementable. For the overly curious, Chapter 5 contains a new intermediate language (to replace GHC Core) and Chapter 6 contains the type inference algorithm that will deal with dependent types. Happy summer reading!

Responses to particular comments on the Reddit thread
  • @elucidatum: How radical of a change and how much of a challenge will it be to refactor existing codebases?

    No change is necessary. All code that currently compiles with -XTypeInType will compile with -XDependentTypes. (The only reason I have to set -XTypeInType as my baseline is because of the parsing annoyance around *, which must be imported to be used with -XTypeInType.) Any refactoring will be around how much you, as the Haskell author, wish to take advantage of dependent types.

  • @jlimperg: Pervasive laziness in Haskell means that we like to use a lot of coinductive types. But this is really annoying for proof purposes because coinduction, despite the nice duality with induction, is a lot less pleasant to work with.

    Yes, this is true. My approach is, essentially, to pretend that types are inductive, not coinductive. One consequence of this decision is that proofs of type equality will have to be run. This means that including dependent types will slow down your running program. Sounds horrible, doesn’t it? It doesn’t have to, though.

    Suppose you have a function proof :: ... -> a :~: b. The function proof provides a proof that type a equals type b. If this function terminates at all, it will always produce Refl. Thus, if we knew that the function terminated, then we wouldn’t have to run it. We can’t know whether it terminates. But you, the programmer, can assert that it terminates, like this: {-# RULES "proof" proof ... = unsafeCoerce Refl #-} Now, GHC will replace any use of proof with Refl directly. Note that GHC still type-checks your proof. All this RULE does is assert termination.

    “But,” you say, “I don’t want to have to merely assert termination! If I wanted to assert correctness instead of prove it, I wouldn’t use dependent types.” My response: “Touché.” Haskell indeed is less powerful than those other dependently typed languages in this regard. Nevertheless, by using dependent types in Haskell, you still get a whole lot more compile-time guarantees than you get without dependent types. You just don’t get termination. You thus have a choice: “prove” termination at runtime by actually running your proofs, or assert it at compile time and keep your dependently typed program efficient, and still with lots of guarantees. Recall that we Haskellers have never proved termination of anything, ever, so not proving termination of a function named proof shouldn’t be all that alarming.

    Note: If RULES such as the one above become pervasive, perhaps a compiler flag can make them automatic, effectively (and concisely) assuming termination for all proofs in a module.

  • @jlimperg: Proving is hard

    Yes, it is. Typechecker plugins may help here. It is easy enough, however, to implement dependent types without this advanced support. As we work through the consequences of dependent types in Haskell, I’m confident the community (including me) will come up with ways to make it easier.

  • @jlimperg: As is well-known, a dependent type system is inconsistent (i.e. everything can be proven) unless all computations terminate, which is obviously not the case for general Haskell.

    Yes, this is true. Dependent types in Haskell will be inconsistent, when we view Haskell as a logic. Dependent types will still remain type-safe however. (This is because we run the proofs!) I just wish to point out here that @jlimperg suggests a syntactic check for termination: this, sadly, will not work. Haskell has too many ways for a computation to diverge, and a syntactic check can rule out only general recursion and partial pattern matches. Haskell also has infinite data types, non-strictly-positive datatypes, TypeRep (which can be abused to cause a loop), Type :: Type, and likely more back doors. I’d love to see a termination checker for Haskell, but I’m not holding my breath.

  • @jlimperg: This point is very speculative, but I strongly dislike the current flavour of ‘almost-dependent’ type-level programming in Haskell.

    So do I. Singletons are an abomination. I hate them. These are gone with my design for dependent types, and I think the resulting language has the niceties we all want in a dependently typed language (modulo termination checking).

  • @dogodel: I think it will take a while for the change to percolate into better design. … I think the most immediate benefit will be for (no surprise) expressive DSL, which are actually quite common in any modest codebase, but maybe not the “core” of the project.

    Agreed completely. It will take time for us to figure out the best way to use dependent types.

  • @sinyesdo: The best summary I can offer is that “totality” is really really important for DT languages

    This is true for those other dependently typed languages, but not for Haskell. See my response to the first of @jlimperg’s points quoted here.

  • @ccasin: The main reasons to care that your programming language is total are to make the type system consistent as a logic and to make type checking decidable. But we’ve already given up both these things in Haskell, and it’s possible to have dependent types without them.

    Agreed in full, and with @ccasin’s full post.

  • @jmite: If you want fully Dependent-Type types, why not use Idris, Agda, Coq, or F*?

    I’m in broad agreement with the responses to this point on Reddit: basically, that none of these languages have Haskell’s ecosystem or optimizing compiler. See also Section 3.3 of my dissertation.

  • @tactics: What does “fully dependent types” even mean for something like Haskell? You would have to rework the core language entirely.

    Yes, precisely. This is Chapter 5 of my dissertation.


I hope this information helps. Do keep an eye out for my finished dissertation sometime in the next few months. And, as always, this is all a work in progress and no one should take anything as set in stone. If there’s a design decision you disagree with, please speak up!

Categories: Offsite Blogs

Neil Mitchell: me :: Standard Chartered -> Barclays

Planet Haskell - Fri, 07/22/2016 - 6:03am

Summary: I've left Standard Chartered and will be starting at Barclays shortly.

I've been working at Standard Chartered for almost 8 years, but a few weeks ago I handed in my notice. While at Standard Chartered I got to work with some very smart people, on some very interesting projects. I have learnt a lot about whether Haskell works at large scales (it does!), what mistakes you can make and how to avoid those mistakes. My work at Standard Chartered lead to the Shake build system, along with 100's of other projects that alas remain locked in proprietary banking world. I've used our in-house strict Haskell (Mu) to write lots of systems, and cemented my opinion of whether languages should be strict or lazy (lazy!). I've taught many people Haskell, and sold the values of functional programming to everyone I met.

After all that, I've decided to take a job at Barclays and will be starting mid-August. In this new role I plan to use real GHC-Haskell, all the advanced features that enables (existentials, laziness etc), with Cabal/Stack to leverage all of Hackage. I am envious of the amazing quality of Haskell libraries, and with any luck, I'll also be able to contribute some more of these libraries back to the community.

Once I officially start at Barclays I'll be hiring a team of London-based Haskell programmers to work with. More details to follow in a few weeks. For now, I will say that for hiring decisions I'm really interested in seeing actual code. If you are interested in a Haskell job anywhere you should probably have a GitHub account with some code on it. If you've done any fun projects, hacked around with an encoding of de-Bruijn indicies with type families, or tried to implement a JavaScript parser using only functions from base which have at most 1 vowel, shove it up. Having libraries on Hackage is even better. I judge people by their best code, not their worst, so more code is always better.

In case people are curious, here are a few questions I expect to be asked:

  • Does this mean Standard Chartered is going to stop using Haskell? No. Standard Chartered has lots of Haskell programmers and I assume they will be continuing with their Haskell implementation.
  • What does this mean for my open source libraries? For most, it means nothing, or they will improve because I might be using them in my day job. The one exception is Bake. I may continue to work on it, I may pass maintainership over to someone else, or I may do nothing further with it. Time will tell, but the source will remain available indefinitely.
  • I got a call from a headhunter for Barclays, is that you? No. Currently Barclays are recruiting someone to work on FPF using Haskell. That's a totally different team. My primary method of recruitment will be this blog, not headhunters. Anyone who ever wants a job with me should talk to me, not people who suggest they are working on my behalf :).
  • Are you hiring right now? No. I will be on the 15th of August once I join.
Categories: Offsite Blogs

Robin KAY: HsQML released: From Zürich

Planet Haskell - Fri, 07/22/2016 - 2:22am
Last night I arrived in Zürich for ZuriHac 2016 and, in the brief space between finding my way from the airport and falling asleep, released HsQML You can download the latest release of this Haskell binding to the Qt Quick GUI framework from Hackage as usual.

This is purely a bug-fix release, fixing building with newer versions of Cabal (1.24, GHC 8) and Qt (5.7+). It also resolves some difficulties with building the library on MacOS and I've revised the MacOS install documentation with more information.

In other news, I've decommissioned the old Trac bug-tracker as I accidentally broke it some time ago during a server upgrade and failed to notice. I take this as a bad sign for its effectiveness, so please just e-mail me with any issues instead. I enjoy hearing from people trying to use the library and I always try to reply with assistance as quickly as possible, so don't be shy.

release- - 2016.07.21

  * Added support for Cabal 1.24 API.
  * Fixed linking shared builds against MacOS frameworks (needs Cabal 1.24+).
  * Fixed building with Qt 5.7.
Categories: Offsite Blogs

Proposal: Add gcoerceWith to Data.Type.Coercion

libraries list - Fri, 07/22/2016 - 12:18am
In Data.Type.Equality, we have both castWith :: (a :~: b) -> a -> b and gcastWith :: (a :~: b) -> (a ~ b => r) -> r But in Data.Type.Coercion we only have coerceWith :: Coercion a b -> a -> b It seems to me that for the sake of consistency, we should add gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion a = a David Feuer _______________________________________________ Libraries mailing list Libraries< at >
Categories: Offsite Discussion