Planet Haskell

July 28, 2015

Mark Jason Dominus

Another ounce of theory

A few months ago I wrote an article here called an ounce of theory is worth a pound of search and I have a nice followup.

When I went looking for that article I couldn't find it, because I thought it was about how an ounce of search is worth a pound of theory, and that I was writing a counterexample. I am quite surprised to discover that that I have several times discussed how a little theory can replace a lot of searching, and not vice versa, but perhaps that is because the search is my default.

Anyway, the question came up on math StackExchange today:

John has 77 boxes each having dimensions 3×3×1. Is it possible for John to build one big box with dimensions 7×9×11?

OP opined no, but had no argument. The first answer that appeared was somewhat elaborate and outlined a computer search strategy which claimed to reduce the search space to only 14,553 items. (I think the analysis is wrong, but I agree that the search space is not too large.)

I almost wrote the search program. I have a program around that is something like what would be needed, although it is optimized to deal with a few oddly-shaped tiles instead of many similar tiles, and would need some work. Fortunately, I paused to think a little before diving in to the programming.

Order
How to Solve It
How to Solve It
with kickback
no kickback

For there is an easy answer. Suppose John solved the problem. Look at just one of the 7×11 faces of the big box. It is a 7×11 rectangle that is completely filled by 1×3 and 3×3 rectangles. But 7×11 is not a multiple of 3. So there can be no solution.

Now how did I think of this? It was a very geometric line of reasoning. I imagined a 7×11×9 carton and imagined putting the small boxes into the carton. There can be no leftover space; every one of the 693 cells must be filled. So in particular, we must fill up the bottom 7×11 layer. I started considering how to pack the bottommost 7×11×1 slice with just the bottom parts of the small boxes and quickly realized it couldn't be done; there is always an empty cell left over somewhere, usually in the corner. The argument about considering just one face of the large box came later; I decided it was clearer than what I actually came up with.

I think this is a nice example of the Pólya strategy “solve a simpler problem” from How to Solve It, but I was not thinking of that specifically when I came up with the solution.

For a more interesting problem of the same sort, suppose you have six 2×2x1 slabs. It is possible to pack them into a 3×3x3 box? (There will, of course, be some space left over.)

by Mark Dominus (mjd@plover.com) at July 28, 2015 02:48 PM

Daniil Frumin

Darcs rebase by example

Darcs is a patch-centric version control system. In Darcs, there is no “correct” linear history of a repository – rather, there is a poset of patches. That means that most of the time you are pushing and pulling changes you can cherry-pick patches without a problem. However, in some cases you cannot perform a pull (or some other operation on the repository) smoothly. Sometimes it is necessary to rewrite the “history” – i.e. modify a patch that is a dependency of one or more other patches. For those cases darcs rebase comes in handy. To put it in the words of the implementor “Rebase is a workaround for cases where commutation doesn’t do enough”.

A repository can change it’s state from rebase-in-progress back to normal if there are no suspended patches left. However, be aware that you cannot unsuspend a patch1 if you have unrecorded changes in the repository. In light of this, I suggest recording a temporary patch with current changes

darcs record -am DRAFT

You can suspend that patch at the beginning of your rebase process and apply it at the end.

General overview of rebase

darcs rebase is an operation (or, rather, a family of operations) that allows one to make changes “deep down” in the repository history. One of the crucial things that allows for rebase to work is the fact that since darcs 2.10 patches can be suspended. When one performs any of the darcs rebase commands, the repository moves to a special rebase-in-progress state. In this state repository contains a pristine, a set of patches, a working copy, and — in addition to all the usual stuff — a set of suspended patches. Suspended patches are not active in the repository — that is, they are not applied.

Let’s go over the rebase subcommands

rebase log/rebase changes

This is simple: list the suspended patches

rebase suspend

Moves selected patches into the suspended state. Once the patch is suspended it is no longer active in the repository.

Note: once you suspend a patch, it changes its identity. That means that even if you suspend a patch and unsuspend it immediately, you will get a different repository that you have started with. Let this be a good reason (one of a couple!) for doing rebase on a separate branch.

> cat file
test
123
> darcs rebase suspend
	patch 64523bc4622fad02a4bdb9261887628b7997ebdd
Author: Daniil Frumin 
Date:   Thu Jul 23 18:49:30 MSK 2015
  * 123
Shall I suspend this patch? (1/5)  [ynW…], or ? for more options: y
patch cc54d7cf4b9e3d13a24ce0b1b77b76581d98d75d
Author: Daniil Frumin 
Date:   Thu Jul 23 18:43:53 MSK 2015
  * Test
Shall I suspend this patch? (2/5)  [ynW…], or ? for more options: d
Rebase in progress: 1 suspended patches
> darcs rebase log
patch 64523bc4622fad02a4bdb9261887628b7997ebdd
Author: Daniil Frumin 
Date:   Thu Jul 23 18:49:30 MSK 2015
  * 123
Shall I view this patch? (1/?) [yN…], or ? for more options: y
[123
Daniil Frumin **20150723154930
 Ignore-this: 43e09e6503ac74688e74441dc29bce25
] hunk ./file 2
+123
Rebase in progress: 1 suspended patches
> cat file
test

rebase unsuspend

Does the opposite of suspend: applies a suspended patch to the repository and changes its state to normal.

> darcs rebase unsuspend                                                                                       
patch 64523bc4622fad02a4bdb9261887628b7997ebdd
Author: Daniil Frumin 
Date:   Thu Jul 23 18:49:30 MSK 2015
  * 123
Shall I unsuspend this patch? (1/1)  [ynW…], or ? for more options: y
Do you want to unsuspend these patches? [Yglqk…], or ? for more options: y
Rebase finished!

rebase apply

Rebase apply takes a patch bundle and tries to apply all the patches in the bundle to the current repository. If a patch from the bundle conflicts with a local patch, then the local patch gets suspended. You will thus have a chance to resolve the conflict by amending your conflicting patches, at a price of.. well, changing the identity of your local patches.

rebase pull

Sort of like rebase apply, but instead of a patch bundle it obtains the patches from a remote repository.

Specifically, rebase pull applies all the remote patches, one-by-one, suspending any local patches that conflict. We will see more of rebase pull in the second example.

Example 1: suspending local changes

Imagine the following situation: at point A you add a configuration file to your repository, then you record a patch B that updates the settings in the configuration file. After that you make some more records before you realize that you’ve included by accident your private password in patch A! You want to get rid of it in your entire history, but you can’t just unrecord A, because B depends on A, and possibly some other patches depend on B.

The contents of the configuration file after patch A:

port = 6667
host = irc.freenode.net
password = awesomevcs 

Patch B, diff:

@@ -1,3 +1,4 @@
-port = 6667
+port = 6697
+usessl = True
host = irc.freenode.net
password = awesomevcs

You cannot just amend patch A, because the patch B depends on A:

> darcs amend                                                                                                         
patch 1925d640f1f3180cb5b9e64260c1b5f374fce4ca
Author: Daniil Frumin 
Date:   Tue Jul 21 13:23:07 MSK 2015
  * B

Shall I amend this patch? [yNjk…], or ? for more options: n

Skipping depended-upon patch:
patch 22d7c8da83141f8b1f80bdd3eff02064d4f45c6b
Author: Daniil Frumin 
Date:   Tue Jul 21 13:22:24 MSK 2015
  * A

Cancelling amend since no patch was selected.

What we will have to do is temporarily suspend patch B, amend patch A, and then unsuspend B.

> darcs rebase suspend
patch 1925d640f1f3180cb5b9e64260c1b5f374fce4ca
Author: Daniil Frumin 
Date:   Tue Jul 21 13:23:07 MSK 2015
  * B

Shall I suspend this patch? (1/2)  [ynW…], or ? for more options: y
patch 22d7c8da83141f8b1f80bdd3eff02064d4f45c6b
Author: Daniil Frumin 
Date:   Tue Jul 21 13:22:24 MSK 2015
  * A

Shall I suspend this patch? (2/2)  [ynW…], or ? for more options: d
Rebase in progress: 1 suspended patches

At this point, the state of our repository is the following: there is one (active) patch A, and one suspended patch B.

> darcs rebase changes -a
patch 4c5d45230dc146932b21964aea938e2a978523eb
Author: Daniil Frumin 
Date:   Tue Jul 21 13:28:58 MSK 2015
  * B

Rebase in progress: 1 suspended patches
> darcs changes -a
patch 21f56dfb425e4c49787bae5db4f8869e96787fb2
Author: Daniil Frumin 
Date:   Tue Jul 21 13:28:49 MSK 2015
  * A

Rebase in progress: 1 suspended patches
> cat config
port = 6667
host = irc.freenode.net
password = awesomevcs
> $EDITOR config # remove the password bit
> darcs amend
patch 22d7c8da83141f8b1f80bdd3eff02064d4f45c6b
Author: Daniil Frumin 
Date:   Tue Jul 21 13:22:24 MSK 2015
  * A

Shall I amend this patch? [yNjk…], or ? for more options: y
hunk ./config 3
-password = awesomevcs
Shall I record this change? (1/1)  [ynW…], or ? for more options: y
Do you want to record these changes? [Yglqk…], or ? for more options: y
Finished amending patch:
patch 21f56dfb425e4c49787bae5db4f8869e96787fb2
Author: Daniil Frumin 
Date:   Tue Jul 21 13:28:49 MSK 2015
  * A

Rebase in progress: 1 suspended patches

Now that we’ve removed the password from the history, we can safely unsuspend patch B (in this particular situation we actually know that applying B to the current state of the repository won’t be a problem, because B does not conflict with our modified A)

> darcs rebase unsuspend
patch 1925d640f1f3180cb5b9e64260c1b5f374fce4ca
Author: Daniil Frumin 
Date:   Tue Jul 21 13:23:07 MSK 2015
  * B

Shall I unsuspend this patch? (1/1)  [ynW…], or ? for more  options: y
Do you want to unsuspend these patches? [Yglqk…], or ? for more options: y
Rebase finished!

And that’s done!

> cat config
port = 6697
usessl = True
host = irc.freenode.net

You may use this rebase strategy for removing sensitive information from the repository, for removing that 1GB binary .iso that you added to your repository by accident, or for combining two patches into one deep down in the patchset.

Example 2: developing against a changing upstream – rebase pull

Imagine you have a fork R’ of a repository R that you are working on. You are implementing a feature that involves a couple of commits. During your work you record a commit L1 that refractors some common datum from modules A.hs and B.hs. You proceed with your work recording a patch L2. At this point you realise that after you forked R, the upstream recorded two more patches U1 and U2, messing with the common datum in A.hs. If you just pull U1 into your fork R’, you will have a conflict, that you will have to resolve by recording another patch on top.

      S
     / \
    /   \
   L1   U1

Note: if you run darcs rebase pull in R’, then the only patches that will be suspended are the ones which are already in R’. Because suspended patches gain new identity, make sure that you do not have other people’s conflicting patches present in R’.

The way to solve this would be to first do darcs rebase pull, which would suspend the conflicting patches, and then start unsuspending the patches one by one, making sure that you fix any conflicts that may arise after each unsuspend.

Consider a concrete example with two repositories rep1 and rep1_0.

rep1_0 > darcs changes 
patch ebaccd5c36667b7e3ee6a49d25ef262f0c7edf2b
Author: Daniil Frumin 
Date:   Mon Jul 27 20:56:25 MSK 2015
  * commit2

patch a7e0d92a53b0523d0224ef8ffae4362adf854485
Author: Daniil Frumin 
Date:   Mon Jul 27 20:56:25 MSK 2015
  * commit1
	rep1_0 > darcs diff —from-patch=commit2
patch ebaccd5c36667b7e3ee6a49d25ef262f0c7edf2b
Author: Daniil Frumin 
Date:   Mon Jul 27 20:56:25 MSK 2015
  * commit2
diff -rN -u old-rep1_0/dir1/file2 new-rep1_0/dir1/file2
— old-rep1_0/dir1/file2	1970-01-01 03:00:00.000000000 +0300
    +++ new-rep1_0/dir1/file2	2015-07-28 12:25:54.000000000 +0300
@@ -0,0 +1 @@
+double whatsup
	rep1_0 > cd ../rep1
rep1 > darcs changes
patch e3df0e23a3915910a81eb8181d7b3669e8f270a9
Author: Daniil Frumin 
Date:   Tue Jul 28 12:27:55 MSK 2015
  * commit2’

patch a7e0d92a53b0523d0224ef8ffae4362adf854485
Author: Daniil Frumin 
Date:   Mon Jul 27 20:56:25 MSK 2015
  * commit1
rep1 > darcs diff —from-patch=“commit2’”
patch e3df0e23a3915910a81eb8181d7b3669e8f270a9
Author: Daniil Frumin 
Date:   Tue Jul 28 12:27:55 MSK 2015
  * commit2’
diff -rN -u old-rep1/dir1/file2 new-rep1/dir1/file2
— old-rep1/dir1/file2	1970-01-01 03:00:00.000000000 +0300
+++ new-rep1/dir1/file2	2015-07-28 12:28:39.000000000 +0300
@@ -0,0 +1 @@
+touch file2
\ No newline at end of file
diff -rN -u old-rep1/file1 new-rep1/file1 — old-rep1/file1	2015-07-28 12:28:39.000000000 +0300 +++ new-rep1/file1	2015-07-28 12:28:39.000000000 +0300
@@ -1 +1 @@
-whatsup
\ No newline at end of file
+double whatsup
\ No newline at end of file

The patch commit2 from rep1_0 conflicts with commit2’ from rep1.

rep1 > darcs rebase pull ../rep1_0
patch ebaccd5c36667b7e3ee6a49d25ef262f0c7edf2b
Author: Daniil Frumin 
Date:   Mon Jul 27 20:56:25 MSK 2015
  * commit2
Shall I pull this patch? (1/1)  [ynW…], or ? for more options: y
Do you want to pull these patches? [Yglqk…], or ? for more options: y
The following local patches are in conflict:
patch e3df0e23a3915910a81eb8181d7b3669e8f270a9
Author: Daniil Frumin 
Date:   Tue Jul 28 12:27:55 MSK 2015
  * commit2’
Shall I suspend this patch? (1/1)  [ynW…], or ? for more options: y
Do you want to suspend these patches? [Yglqk…], or ? for more options: y
Finished pulling.
Rebase in progress: 1 suspended patches

Now we have one patch — commit2’ — in the suspended state. We want to resolve the conflict by amending commit2’. We will do that by unsuspending it and manually editing out the conflicting lines. This will also make it depend on commit2.

rep1 > darcs rebase unsuspend
patch e3df0e23a3915910a81eb8181d7b3669e8f270a9
Author: Daniil Frumin 
Date:   Tue Jul 28 12:27:55 MSK 2015
  * commit2’
Shall I unsuspend this patch? (1/1)  [ynW…], or ? for more options: y
Do you want to unsuspend these patches? [Yglqk…], or ? for more options: d
We have conflicts in the following files:
./dir1/file2

Rebase finished!
rep1 > cat dir1/file2
v v v v v v v

=============
double whatsup
*************
touch file2
^ ^ ^ ^ ^ ^ ^
rep1 > $EDITOR dir1/file2
rep1 > darcs amend -a
patch 40b3b4123c78dba6a6797feb619572072654a9cd
Author: Daniil Frumin 
Date:   Tue Jul 28 12:32:56 MSK 2015
  * commit2’
Shall I amend this patch? [yNjk…], or ? for more options: y
Finished amending patch:
patch c35867259f187c1bc30310f1cacb34c1bb2cce41
Author: Daniil Frumin 
Date:   Tue Jul 28 12:34:30 MSK 2015
  * commit2’
rep1 > darcs mark-conflicts
No conflicts to mark.

Another repository saved from conflicting patches, yay!


  1. See this discussion for details


Tagged: darcs, haskell, rebase

by Dan at July 28, 2015 10:40 AM

July 27, 2015

LambdaCube

The LambdaCube 3D Tour

Prologue

This blog has been silent for a long time, so it’s definitely time for a little update. A lot of things happened since the last post! Our most visible achievement from this period is the opening of the official website for LambdaCube 3D at ‒ wait for it! ‒ lambdacube3d.com, which features an interactive editor among other things. The most important, on the other hand, is the fact that Péter Diviánszky joined the team in the meantime and has been very active in the development of the latest LambdaCube generation. Oh yes, we have a completely new system now, and the big change is that LambdaCube 3D is finally an independent DSL instead of a language embedded in Haskell. Consult the website for further details.

Soon we’ll be writing more about the work done recently, but the real meat of this post is to talk about our summer adventure: the LambdaCube 3D Tour. This is the short story of how Csaba and Péter presented LambdaCube 3D during a 7-week tour around Europe.

The idea

Csaba started to work on LambdaCube 3D full time in the autumn of 2014 and Péter joined him at the same time. We knew that we should advertise our work somehow, preferably without involving individual sponsors. Csaba already had experience with meetups and hackathons, and Péter had bought his first car in the summer, so it seemed feasible to travel around Europe by car and give presentations for various self-organised tech communities.

Planning

At the end of March 2015 we decided that the tour should start around ZuriHack 2015, which we wanted to participate in anyway. We had a preliminary route which was quite close to the final itinerary shown on the following map:

map

We included Munich because we knew that Haskell is used there in multiple ways and we missed it last year during the way to ZuriHack 2014. We included Paris later because a friend of us was at MGS 2015 and while chatting with Nicolas Rolland, he got interested in our tour and invited us to Paris. We included Nottingham because Ambrus Kaposi, Peter’s previous student, was doing research in HoTT there and he invited us too. We included Helsinki because Gergely, our team member and Csaba’s previous Haskell teacher, lives there and we have also heard that lots of indie game developers work in Helsinki. The other destinations were included mainly because we knew that there are Haskell communities there.

Preparation

After deciding the starting time, we made sure to fully focus on the tour. We made a detailed work schedule for 4 x 2 weeks such that we would have enough content for the presentations. The work went surprisingly well, we reached most milestones although the schedule was quite tight. We have done more for the success of LambdaCube 3D in this two-month period than in the previous half year.

We had a rehearsal presentation in Budapest at Prezi, mainly in front of our friends. It was a good idea because we got lots of feedback on our style of presentation. We felt that the presentation was not that successful but we were happy that we could learn from it.

We hardly dealt with other details like where we would sleep or how to travel. All we did was the minimum effort to kickstart the trip: Peter brought his 14 years old Peugeot 206 to a review, he sent some CouchSurfing requests and Csaba asked some of his friends whether they can host us. We bought food for the tour at the morning when we left Budapest. Two oszkar.com (car-sharing service) clients were waiting for us at the car while we were packing our stuff for the tour.

Travelling

Up until Vienna there were four of us in the car with big packs on our laps. This was rather inconvenient, so we mostly skipped transporting others later on. Otherwise, the best moments were when we occasionally gave a ride to friends or hitchhikers.

Peter was relatively new to driving but at the end of the tour he already appreciated travelling on smaller local roads because highways turned out to be a bit boring for him. Csaba was the navigator using an open-source offline navigation software running on an NVidia Shield, which we won at the Function 2014 demoscene party.

Being lazy with actual route planning hit back only once when it was combined with a bad decision: we bought an expensive EuroTunnel ticket instead of going by ferry to England. Even with this expense, the whole journey including all costs was about the same price as visiting a one-week conference somewhere in Europe. This was possible because we only paid once for accommodation, in a hostel. Otherwise we were staying at friends or CouchSurfing hosts. We slept in a tent on two occasions. We learned during our tour about the Swedish law, The Right of Public Access (Allemansrätten), which allows everyone to visit somebody else’s land, use their waters for bathing and riding boats on, and to pick the wild flowers, mushrooms, berries. We didn’t have the chance to try all these activities, though.

ferryferry2alaguttentartdaniambrushackeroutdoorhelsinki

All of our hosts were amazing and very different people, living in different conditions. We hope that we can return the hospitality either to them or to someone else in need in Budapest.

Presentations

Our main task was to give one presentation every 3-4 days on average, which was a quite convenient rate. We were lucky because our first presentation was strikingly successful in Munich. We got so many questions during and after the presentation that we could only leave 4 hours after the beginning. At first we made free-style presentations but near the end we switched to using slides because they are altogether more reliable. Sometimes it was refreshing to diverge from the presentation and speak about Agda or laziness if the audience was interested about it.

LambdaCubePresentationgoteborgrelaxjobs

Summary

We reached approximately 200 people at 12 presentations and we had lots of private discussions about our interests. This was combined with a diverse summer vacation with lots of impressions. We think of it as a total success!

In hindsight, there are a few things we would do differently if we were to begin the tour now:

  • First of all, we would arrange more private appointments. For example, we were invited to have a dinner at Microsoft Research in Cambridge by Nicolas Rolland. We wanted to greet Simon Peyton Jones so we went up to his room. We could see him through the glass talking on the phone but we didn’t want to disturb him because we had no appointment arranged with him.
  • If we had spent more time improving our presentation during the tour, it would have made a lot of difference. We couldn’t really do this because first we patched the most annoying shortages in our software and later we were not focused enough (we had to adapt to the ever-changing environment).
  • Half the time would be enough to achieve our primary goal. 7 weeks is a really long time for such a tour.
  • No meetups on Friday-Saturday-Sunday. Especially no meetups on Fridays in London…
  • No meetups in the height of summer; the beginning of June is still OK.

It matters a lot to us that the importance of our work was confirmed by the feedback we received during the trip. It’s also clear that C/C++ programmers would only be interested in an already successful system. On the other hand, functional programmers (especially Haskellers) are open to cooperation right now.

What’s next?

The tour ended two weeks ago, and by now we had enough rest to carry on with development, taking into account the all feedback from the tour. We shall write about our plans for LambdaCube 3D in another blog post soon enough. Stay tuned!

by divip at July 27, 2015 09:29 AM

Daniel Mlot (duplode)

Migrating a Project to stack

This post consists of notes on which steps I took to convert convert one of my Haskell projects to stack. It provides a small illustration of how flexible stack can be in accomodating project organisation quirks on the way towards predictable builds. If you want to see the complete results, here are links to the Bitbucket repository of Stunts Cartography, the example project I am using, and specifically to the source tree immediately after the migration.

The first decision to make when migrating a project is which Stackage snapshot to pick. It had been a while since I last updated my project, and building it with the latest versions of all its dependencies would require a few adjustments. That being so, I chose to migrate to stack before any further patches. Since one of the main dependencies was diagrams 1.2, I went for lts-2.19, the most recent LTS snapshot with that version of diagrams 1.

$ stack init --resolver lts-2.19

cabal init creates a stack.yaml file based on an existing cabal file in the current directory. The --resolver option can be used to pick a specific snapshot.

One complicating factor in the conversion to stack was that two of the extra dependencies, threepenny-gui-0.5.0.0 (one major version behind the current one) and zip-conduit wouldn’t build with the LTS snapshot plus current Hackage without version bumps in their cabal files. Fortunately, stack deals very well with situations like this, in which minor changes to some dependency are needed. I simply forked the dependencies on GitHub, pushed the version bumps to my forks and referenced the commits in the remote GitHub repository in stack.yaml. A typical entry for a Git commit in the packages section looks like this:

- location:
    git: https://github.com/duplode/zip-conduit
    commit: 1eefc8bd91d5f38b760bce1fb8dd16d6e05a671d
  extra-dep: true

Keeping customised dependencies in public remote repositories is an excellent solution. It enables users to build the package without further intervention without requiring developers to clumsily bundle bundle the source tree of the dependencies with the project, or waiting for a pull request to be accepted upstream and reach Hackage.

With the two tricky extra dependencies being offloaded to Git repositories, the next step was using stack solver to figure out the rest of them:

$ stack solver --modify-stack-yaml
This command is not guaranteed to give you a perfect build plan
It's possible that even with the changes generated below, you will still
need to do some manual tweaking
Asking cabal to calculate a build plan, please wait
extra-deps:
- parsec-permutation-0.1.2.0
- websockets-snap-0.9.2.0
Updated /home/duplode/Development/stunts/diagrams/stack.yaml

Here is the final stack.yaml:

flags:
  stunts-cartography:
    repldump2carto: true
packages:
- '.'
- location:
    git: https://github.com/duplode/zip-conduit
    commit: 1eefc8bd91d5f38b760bce1fb8dd16d6e05a671d
  extra-dep: true
- location:
    git: https://github.com/duplode/threepenny-gui
    commit: 2dd88e893f09e8e31378f542a9cd253cc009a2c5
  extra-dep: true
extra-deps:
- parsec-permutation-0.1.2.0
- websockets-snap-0.9.2.0
resolver: lts-2.19

repldump2carto is a flag defined in the cabal file. It is used to build a secondary executable. Beyond demonstrating how the flags section of stack.yaml works, I added it because stack ghci expects all possible build targets to have been built 2.

As I have GHC 7.10.1 from my Linux distribution and the LTS 2.19 snapshot is made for GHC 7.8.4, I needed stack setup as an additional step. That command locally installs (in ~/.stack) the GHC version required by the chosen snapshot.

That pretty much concludes the migration. All that is left is demonstrating: stack build to compile the project…

$ stack build
JuicyPixels-3.2.5.2: configure
Boolean-0.2.3: download
# etc. (Note how deps from Git are handled seamlessly.)
threepenny-gui-0.5.0.0: configure
threepenny-gui-0.5.0.0: build
threepenny-gui-0.5.0.0: install
zip-conduit-0.2.2.2: configure
zip-conduit-0.2.2.2: build
zip-conduit-0.2.2.2: install
# etc.
stunts-cartography-0.4.0.3: configure
stunts-cartography-0.4.0.3: build
stunts-cartography-0.4.0.3: install
Completed all 64 actions.

stack ghci to play with it in GHCi…

$ stack ghci
Configuring GHCi with the following packages: stunts-cartography
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
-- etc.
Ok, modules loaded: GameState, Annotation, Types.Diagrams, Pics,
Pics.MM, Annotation.Flipbook, Annotation.LapTrace,
Annotation.LapTrace.Vec, Annotation.LapTrace.Parser.Simple,
Annotation.Parser, Types.CartoM, Parameters, Composition, Track,
Util.Misc, Pics.Palette, Output, Util.ByteString, Util.ZipConduit,
Replay, Paths, Util.Reactive.Threepenny, Util.Threepenny.Alertify,
Widgets.BoundedInput.
*GameState> :l src/Viewer.hs -- The Main module.
-- etc.
*Main> :main
Welcome to Stunts Cartography.
Open your web browser and navigate to localhost:10000 to begin.

Listening on http://127.0.0.1:10000/
[27/Jul/2015:00:55:11 -0300] Server.httpServe: START, binding to
[http://127.0.0.1:10000/]

… and looking at the build output in the depths of .stack-work:

$ .stack-work/dist/x86_64-linux/Cabal-1.18.1.5/build/sc-trk-viewer/sc-trk-viewer
Welcome to Stunts Cartography 0.4.0.3.
Open your web browser and navigate to localhost:10000 to begin.

Listening on http://127.0.0.1:10000/
[26/Jul/2015:20:02:54 -0300] Server.httpServe: START, binding to
[http://127.0.0.1:10000/]

With the upcoming stack 0.2 it will be possible to use stack build --copy-bins --local-bin-path <path> to copy any executables built as part of the project to a path. If the --local-bin-path option is omitted, the default is ~/.local/bin. (In fact, you can already copy executables to ~/.local/bin with stack 0.1.2 through stack install. However, I don’t want to overemphasise that command, as stack install not being equivalent to cabal install can cause some confusion.)

Hopefully this report will give you an idea of what to expect when migrating your projects to stack. Some details may appear a little strange, given how familiar cabal-install workflows are, and some features are still being shaped. All in all, however, stack works very well already: it definitely makes setting up reliable builds easier. The stack repository at GitHub, and specially the wiki therein, offers lots of helpful information, in case you need further details and usage tips.

<section class="footnotes">
  1. As a broader point, it just seems polite to, when possible, pick a LTS snapshot over than a nightly for a public project. It is more likely that those interested in building your project already have a specific LTS rather than an arbitrary nightly.

  2. That being so, a more natural arrangement would be treating repldump2carto as a full-blown subproject by giving it its own cabal file and adding it to the packages section. I would then be able to load only the main project in GHCi with stack ghci stunts-cartography.

</section>
Comment on GitHub (see the full post for a reddit link)

by Daniel Mlot at July 27, 2015 06:00 AM

Bill Atkins

GCD and Parallel Collections in Swift

One of the benefits of functional programming is that it's straightforward to parallelize operations. Common FP idioms like map, filter and reduce can be adapted so they run on many cores at once, letting you get instant parallelization wherever you find a bottleneck.

The benefits of these parallel combinators are huge. Wherever you find a bottleneck in your program, you can simply replace your call to map with a call to a parallel map and your code will be able to take advantage of all the cores on your system. On my eight-core system, for example, simply using a different function can theoretically yield an eight-fold speed boost. (Of course, there are a few reasons you might not see that theoretical speed improvement: namely, the overhead of creating threads, splitting up the work, synchronizing data between the threads, etc. Nevertheless, if you profile your code and focus on hotspots, you can see tremendous improvements with simple changes.)

Swift doesn't yet come with parallel collections functions, but we can build them ourselves, using Grand Central Dispatch:
// requires Swift 2.0 or higher
extension Array {
    public func pmap<t>(transform: (Element -> T)) -> [T] {</t>
        guard !self.isEmpty else {
            return []
        }
        
        var result: [(Int, [T])] = []
        
        let group = dispatch_group_create()
        let lock = dispatch_queue_create("pmap queue for result", DISPATCH_QUEUE_SERIAL)
        
        let step: Int = max(1, self.count / NSProcessInfo.processInfo().activeProcessorCount) // step can never be 0
        
        for var stepIndex = 0; stepIndex * step < self.count; stepIndex++ {
            let capturedStepIndex = stepIndex

            var stepResult: [T] = []
            dispatch_group_async(group, dispatch_get_global_queue(DISPATCH_QUEUE_PRIORITY_DEFAULT, 0)) {
                for i in (capturedStepIndex * step)..<((capturedStepIndex + 1) * step) {
                    if i < self.count {
                        let mappedElement = transform(self[i])
                        stepResult += [mappedElement]
                    }
                }

                dispatch_group_async(group, lock) {
                    result += [(capturedStepIndex, stepResult)]
                }
            }
        }
        
        dispatch_group_wait(group, DISPATCH_TIME_FOREVER)
        
        return result.sort { $0.0 < $1.0 }.flatMap { $0.1 }
   }
}

pmap takes the same arguments as map but simply runs the function across all of your system's CPUs. Let's break the function down, step by step.
  1. In the case of an empty array, pmap returns early, since the overhead of splitting up the work and synchronizing the results is non-trivial. We might take this even further by falling back to a sequential map for arrays with a very small element count.
  2. Create a Grand Central Dispatch group that we can associate with the GCD blocks we'll run later on. Since all of these blocks will be in the same group, the invoking thread can wait for the group to be empty at the end of the function and know for certain that all of the background work has finished.
  3. Create a dedicated, sequential lock queue to control access to the result array. This is a common pattern in GCD: simulating a mutex with a sequential queue. Since a sequential queue will never run two blocks simultaneously, we can be sure that whatever operations we perform in this queue will be isolated from one another.
  4. Next, pmap breaks the array up into "steps", based on the host machine's CPU count (since this is read from NSProcessInfo, this function will automatically receive performance benefits when run on machines with more cores). Each step is dispatched to one of GCD's global background queues. In the invoking thread, this for loop will run very, very quickly, since all it does is add closures to background queues.
  5. The main for loop iterates through each "step," capturing the stepIndex in a local variable. If we don't do this, the closures passed to dispatch_group_async will all refer to the same storage location - as the for loop increments, all of the workers will see stepIndex increase by one and will all operate on the same step. By capturing the variable, each worker has its own copy of stepIndex, which never changes as the for loop proceeds.
  6. We calculate the start and end indices for this step. For each array element in that range, we call transform on the element and add it to this worker's local stepResult array. Because it's unlikely that the number of elements in the array will be divisible by a given machine's processor count, we check that i never goes beyond the end of the array, which could otherwise happen in the very last step.
  7. After an entire step has been processed, we add this worker's results to the master result array. Since the order in which workers will finish is nondeterministic, each element of the result array is a tuple containing the stepIndex and the transformed elements in that step's range. We use the lock queue to ensure that all changes to the result array are synchronized. 
      • Note that we only have to enter this critical section once for each core - an alternative implementation of pmap might create a single master result array of the same size as the input and set each element to its mapped result as it goes. But this would have to enter the critical section once for every array element, instead of just once for each CPU, generating more memory and processor contention and benefiting less from spatial locality. 
      • We use dispatch_sync instead of dispatch_async because we want to be sure that the worker's changes have been applied to the masterResults array before declaring this worker to be done. If we were to use dispatch_async, the scheduler could very easily finish all of the step blocks but leave one or more of these critical section blocks unprocessed, leaving us with an incomplete result.
  8. On the original thread, we call dispatch_group_wait, which waits until all blocks in the group have completed. At this point, we know that all work has been done and all changes to the master results array have been made.
  9. The final line sorts the master array by stepIndex (since steps finish in a nondeterministic order) and then flattens the master array in that order.
To see how this works, let's create a simple profile function:

func profile(desc: String, block: () -> A) -> Void {
    let start = NSDate().timeIntervalSince1970
    block()
    
    let duration = NSDate().timeIntervalSince1970 - start
    print("Profiler: completed \(desc) in \(duration * 1000)ms")

}
We'll test this out using a simple function called slowCalc, which adds a small sleep delay before each calculation, to ensure that each map operation does enough work (in production code, you should never sleep in code submitted to a GCD queue - this is purely for demonstration purposes). Without this little delay, the overhead of parallelization would be too great:

func slowCalc(x: Int) -> Int {
    NSThread.sleepForTimeInterval(0.1)
    return x * 2
}

let smallTestData: [Int] = [Int](0..<10)
let largeTestData = [Int](0..<300)

profile("large dataset (sequential)") { largeTestData.map { slowCalc($0) } }
profile("large dataset (parallel)") { largeTestData.pmap { slowCalc($0) } }

On my eight-core machine, this results in:

Profiler: completed large dataset (sequential) in 31239.7990226746ms
Profiler: completed large dataset (parallel) in 4005.04493713379ms

an 7.8-fold increase, which is about what you'd expect.

It's important thing to remember that if each iteration doesn't do enough work, the overhead of splitting up work, setting up worker blocks and synchronizing data access will far outweigh the time savings of parallelization. The amount of overhead involved can be surprising. This code is identical to the above, except that it doesn't add the extra delay.

profile("large dataset (sequential, no delay)") { largeTestData.map { $0 * 2 } }
profile("large dataset (parallel, no delay)") { largeTestData.pmap { $0 * 2 } }

On my machine, it results in:

Profiler: completed large dataset (sequential, no delay) in 53.4629821777344ms
Profiler: completed large dataset (parallel, no delay) in 161.548852920532ms

The parallel version is three times slower than the sequential version! This is a really important consideration when using parallel collection functions:
  1. Make sure that each of your iterations does enough work to make parallelization worth it.
  2. Parallel collections are not a panacea - you can't just sprinkle them throughout your code and assume you'll get a performance boost. You still need to profile for hotspots, and it's important to focus on bottlenecks found through profiling, rather than hunches about what parts of your code are slowest.
  3. Modern CPUs are blindingly fast - an addition or multiplication operation is so fast that it's not worth parallelizing these, unless your array is very large.
You can use the same techniques to implement a parallel filter function:

// requires Swift 2.0 or higher
extension Array {
    public func pfilter(includeElement: Element -> Bool) -> [Element] {
        guard !self.isEmpty else {
            return []
        }
        
        var result: [(Int, [Element])] = []
        
        let group = dispatch_group_create()
        let lock = dispatch_queue_create("pmap queue for result", DISPATCH_QUEUE_SERIAL)
        
        let step: Int = max(1, self.count / NSProcessInfo.processInfo().activeProcessorCount) // step can never be 0
        
        for var stepIndex = 0; stepIndex * step < self.count; stepIndex++ {
            let capturedStepIndex = stepIndex
            
            var stepResult: [Element] = []
            dispatch_group_async(group, dispatch_get_global_queue(DISPATCH_QUEUE_PRIORITY_DEFAULT, 0)) {
                for i in (capturedStepIndex * step)..<((capturedStepIndex + 1) * step) {
                    if i < self.count && includeElement(self[i]) {
                        stepResult += [self[i]]
                    }
                }
                
                dispatch_group_async(group, lock) {
                    result += [(capturedStepIndex, stepResult)]
                }
            }
        }
        
        dispatch_group_wait(group, DISPATCH_TIME_FOREVER)
        
        return result.sort { $0.0 < $1.0 }.flatMap { $0.1 }
    }
}

This code is almost exactly identical to pmap - only the logic in the inner for loop is different.

We can now start using these combinators together (again, we have to use a slowed-down predicate function in order to see the benefit from parallelization):

func slowTest(x: Int) -> Bool {
    NSThread.sleepForTimeInterval(0.1)
    return x % 2 == 0
}

profile("large dataset (sequential)") { largeTestData.filter { slowTest($0) }.map { slowCalc($0) } }
profile("large dataset (sequential filter, parallel map)") { largeTestData.filter { slowTest($0) }.pmap { slowCalc($0) } }
profile("large dataset (parallel filter, sequential map)") { largeTestData.pfilter { slowTest($0) }.map { slowCalc($0) } }
profile("large dataset (parallel filter, parallel map)") { largeTestData.pfilter { slowTest($0) }.pmap { slowCalc($0) } }

which results in:

Profiler: completed large dataset (sequential) in 1572.28803634644ms
Profiler: completed large dataset (sequential filter, parallel map) in 1153.90300750732ms
Profiler: completed large dataset (parallel filter, sequential map) in 642.061948776245ms
Profiler: completed large dataset (parallel filter, parallel map) in 231.456995010376ms

Using one parallel combinator gives a slight improvement; combining the two parallel operations gives us a fivefold performance improvement over the basic sequential implementation.

Here are some other directions to pursue:
  1. Implement parallel versions of find, any/exists and all. These are tricky because their contracts stipulate that processing stops as soon as they have a result. So you'll have to find some way to stop your parallel workers as soon as the function has its answer.
  2. Implement a parallel version of reduce. The benefit of doing this is that reduce is a "primitive" higher-order function - you can easily implement pmap and pfilter given a parallel reduce function.
  3. Generalize these functions to work on all collections (not just arrays), using Swift 2's protocol extensions.

by More Indirection (noreply@blogger.com) at July 27, 2015 01:40 AM

Ken T Takusagawa

[hqoeierf] Planck frequency pitch standard

We present a fanciful alternative to the musical pitch standard A440 by having some piano key note, not necessarily A4, have a frequency that is an integer perfect power multiple of the Planck time interval.

Let Pf = Planck frequency = 1/plancktime = 1/(5.3910604e-44 s) = 1.8549226e+43 Hz.

We first consider some possibilities of modifying A = 440 Hz as little as possible.  Sharpness or flatness is given in cents, where 100 cents = 1 semitone.

F3 = Pf / 725926^7 = 174.6141 Hz, or A = 440.0000 Hz, offset = -0.00003 cents
G3 = Pf / 714044^7 = 195.9977 Hz, or A = 440.0000 Hz, offset = -0.00013 cents
E3 = Pf / 135337^8 = 164.8137 Hz, or A = 439.9999 Hz, offset = -0.00030 cents
G3 = Pf / 132437^8 = 195.9978 Hz, or A = 440.0001 Hz, offset = 0.00045 cents
D#5 = Pf / 31416^9 = 622.2542 Hz, or A = 440.0001 Hz, offset = 0.00053 cents
A#3 = Pf / 12305^10 = 233.0825 Hz, or A = 440.0011 Hz, offset = 0.00442 cents
C#5 = Pf / 1310^13 = 554.3690 Hz, or A = 440.0030 Hz, offset = 0.01176 cents
A#3 = Pf / 360^16 = 233.0697 Hz, or A = 439.9770 Hz, offset = -0.09058 cents
A#1 = Pf / 77^22 = 58.2814 Hz, or A = 440.0824 Hz, offset = 0.32419 cents
D#4 = Pf / 50^24 = 311.2044 Hz, or A = 440.1095 Hz, offset = 0.43060 cents
E1 = Pf / 40^26 = 41.1876 Hz, or A = 439.8303 Hz, offset = -0.66769 cents
B5 = Pf / 22^30 = 990.0232 Hz, or A = 441.0052 Hz, offset = 3.95060 cents
F#3 = Pf / 10^41 = 185.4923 Hz, or A = 441.1774 Hz, offset = 4.62660 cents
A7 = Pf / 7^47 = 3537.6749 Hz, or A = 442.2094 Hz, offset = 8.67126 cents
G6 = Pf / 3^84 = 1549.3174 Hz, or A = 434.7625 Hz, offset = -20.73121 cents
G#7 = Pf / 2^132 = 3406.9548 Hz, or A = 451.1929 Hz, offset = 43.48887 cents

Next some modifications of other pitch standards, used by continental European orchestras.

Modifications of A = 441 Hz:

C#6 = Pf / 106614^8 = 1111.2503 Hz, or A = 441.0000 Hz, offset = -0.00007 cents
F2 = Pf / 39067^9 = 87.5055 Hz, or A = 441.0000 Hz, offset = -0.00011 cents
G#2 = Pf / 38322^9 = 104.0620 Hz, or A = 440.9995 Hz, offset = -0.00184 cents
G1 = Pf / 6022^11 = 49.1109 Hz, or A = 441.0006 Hz, offset = 0.00240 cents
B5 = Pf / 22^30 = 990.0232 Hz, or A = 441.0052 Hz, offset = 0.02044 cents
F#3 = Pf / 10^41 = 185.4923 Hz, or A = 441.1774 Hz, offset = 0.69644 cents
A7 = Pf / 7^47 = 3537.6749 Hz, or A = 442.2094 Hz, offset = 4.74110 cents
E7 = Pf / 5^57 = 2673.2253 Hz, or A = 446.0410 Hz, offset = 19.67702 cents
G6 = Pf / 3^84 = 1549.3174 Hz, or A = 434.7625 Hz, offset = -24.66137 cents
G#7 = Pf / 2^132 = 3406.9548 Hz, or A = 451.1929 Hz, offset = 39.55871 cents

Modifications of A = 442 Hz:

D#6 = Pf / 547981^7 = 1250.1649 Hz, or A = 442.0000 Hz, offset = 0.00014 cents
G6 = Pf / 530189^7 = 1575.1097 Hz, or A = 442.0002 Hz, offset = 0.00086 cents
G#6 = Pf / 525832^7 = 1668.7709 Hz, or A = 442.0003 Hz, offset = 0.00116 cents
F#4 = Pf / 122256^8 = 371.6759 Hz, or A = 441.9996 Hz, offset = -0.00170 cents
A5 = Pf / 30214^9 = 883.9990 Hz, or A = 441.9995 Hz, offset = -0.00194 cents
F#4 = Pf / 11744^10 = 371.6767 Hz, or A = 442.0006 Hz, offset = 0.00242 cents
A7 = Pf / 217^17 = 3535.9843 Hz, or A = 441.9980 Hz, offset = -0.00769 cents
D2 = Pf / 151^19 = 73.7503 Hz, or A = 442.0024 Hz, offset = 0.00939 cents
A2 = Pf / 62^23 = 110.4885 Hz, or A = 441.9539 Hz, offset = -0.18072 cents
D#3 = Pf / 38^26 = 156.2976 Hz, or A = 442.0764 Hz, offset = 0.29903 cents
D#4 = Pf / 37^26 = 312.6662 Hz, or A = 442.1768 Hz, offset = 0.69244 cents
A7 = Pf / 7^47 = 3537.6749 Hz, or A = 442.2094 Hz, offset = 0.81985 cents
E7 = Pf / 5^57 = 2673.2253 Hz, or A = 446.0410 Hz, offset = 15.75576 cents
G6 = Pf / 3^84 = 1549.3174 Hz, or A = 434.7625 Hz, offset = -28.58262 cents
G#7 = Pf / 2^132 = 3406.9548 Hz, or A = 451.1929 Hz, offset = 35.63745 cents

Modifications of A = 443 Hz:

F#5 = Pf / 590036^7 = 745.0342 Hz, or A = 443.0000 Hz, offset = 0.00003 cents
C7 = Pf / 508595^7 = 2107.2749 Hz, or A = 443.0000 Hz, offset = -0.00007 cents
F7 = Pf / 488038^7 = 2812.8743 Hz, or A = 442.9999 Hz, offset = -0.00020 cents
B2 = Pf / 140193^8 = 124.3126 Hz, or A = 442.9998 Hz, offset = -0.00093 cents
A5 = Pf / 109676^8 = 885.9985 Hz, or A = 442.9992 Hz, offset = -0.00296 cents
B7 = Pf / 25564^9 = 3978.0160 Hz, or A = 443.0012 Hz, offset = 0.00456 cents
G#1 = Pf / 5988^11 = 52.2668 Hz, or A = 442.9982 Hz, offset = -0.00722 cents
B1 = Pf / 391^16 = 62.1581 Hz, or A = 443.0125 Hz, offset = 0.04895 cents
A6 = Pf / 226^17 = 1772.0760 Hz, or A = 443.0190 Hz, offset = 0.07422 cents
F7 = Pf / 163^18 = 2811.5701 Hz, or A = 442.7946 Hz, offset = -0.80308 cents
A#3 = Pf / 60^23 = 234.8805 Hz, or A = 443.3954 Hz, offset = 1.54462 cents
E6 = Pf / 35^26 = 1326.0401 Hz, or A = 442.5128 Hz, offset = -1.90507 cents
E2 = Pf / 34^27 = 82.8696 Hz, or A = 442.4704 Hz, offset = -2.07100 cents
C#2 = Pf / 18^33 = 69.8768 Hz, or A = 443.6902 Hz, offset = 2.69500 cents
A7 = Pf / 7^47 = 3537.6749 Hz, or A = 442.2094 Hz, offset = -3.09255 cents
E7 = Pf / 5^57 = 2673.2253 Hz, or A = 446.0410 Hz, offset = 11.84337 cents
G#7 = Pf / 2^132 = 3406.9548 Hz, or A = 451.1929 Hz, offset = 31.72506 cents

Planck time is not known to high precision due to uncertainty of the gravitational constant G.  Fortunately coincidentally, musical instruments are not tuned to greater than 7 significant digits of precision, either.

Source code in Haskell. The algorithm is not clever; it simply brute forces every perfect integer power multiple of Planck time, with base less than 1 million, and within the range of an 88-key piano.  The code also can base the fundamental frequency off the hydrogen 21 cm line or off the frequency of cesium used for atomic clocks.

Inspired by Scientific pitch, which set C4 = 2^8 Hz = 256 Hz, or A = 430.538964609902 Hz, offset = -37.631656229590796 cents.

by Ken (noreply@blogger.com) at July 27, 2015 12:56 AM

July 26, 2015

Roman Cheplyaka

Better Yaml Parsing

Michael Snoyman’s yaml package reuses aeson’s interface (the Value type and ToJSON & FromJSON classes) to specify how datatypes should be serialized and deserialized.

It’s not a secret that aeson’s primary goal is raw performance. This goal may be at odds with the goal of YAML: being human readable and writable.

In this article, I’ll explain how a better way of parsing human-written YAML may work. The second direction – serializing to YAML – also needs attention, but I’ll leave it out for now.

Example: Item

To demonstrate where the approach taken by the yaml package is lacking, I’ll use the following running example.

{-# LANGUAGE OverloadedStrings #-}
import Data.Aeson (FromJSON(..), withObject, withText, (.:), (.:?), (.!=))
import Data.Yaml (decodeEither)
import Data.Text (Text)
import Control.Applicative

data Item = Item
  Text -- title
  Int -- quantity
  deriving Show

The fully-specified Item in YAML may look like this:

title: Shampoo
quantity: 100

In our application, most of the time the quantity will be 1, so we’ll allow two alternative simplified forms. In the first one, the quantity field is omitted and defaulted to 1:

title: Shampoo

In the second form, the object will be flattened to a bare string:

Shampoo

Here’s a reasonably idiomatic way to write an aeson parser for this format:

defaultQuantity :: Int
defaultQuantity = 1

instance FromJSON Item where
  parseJSON v = parseObject v <|> parseString v
    where
      parseObject = withObject "object" $ \o ->
        Item <$>
          o .: "title" <*>
          o .:? "quantity" .!= defaultQuantity
        
      parseString = withText "string" $ \t ->
        return $ Item t defaultQuantity

Shortcomings of FromJSON

The main requirement for a format written by humans is error detection and reporting.

Let’s see how the parser we’ve defined copes with humanly errors.

> decodeEither "{title: Shampoo, quanity: 2}" :: Either String Item
Right (Item "Shampoo" 1)

Unexpected result, isn’t it? If you look closer, you’ll notice that the word quantity is misspelled. But our parser didn’t have any problem with that. Such a typo may go unnoticed for a long time and quitely affect how your application works.

For another example, let’s say I am a returning user who vaguely remembers the YAML format for Items. I might have written something like

*Main Data.ByteString.Char8> decodeEither "{name: Shampoo, quanity: 2}" :: Either String Item
Left "when expecting a string, encountered Object instead"

“That’s weird. I could swear this app accepted some form of an object where you could specify the quantity. But apparently I’m wrong, it only accepts simple strings.”

How to fix it

Check for unrecognized fields

To address the first problem, we need to know the set of acceptable keys. This set is impossible to extract from a FromJSON parser, because it is buried inside an opaque function.

Let’s change parseJSON to have type FieldParser a, where FieldParser is an applicative functor that we’ll define shortly. The values of FieldParser can be constructed with combinators:

field
  :: Text -- ^ field name
  -> Parser a -- ^ value parser
  -> FieldParser a

optField
  :: Text -- ^ field name
  -> Parser a -- ^ value parser
  -> FieldParser (Maybe a)

The combinators are analogous to the ones I described in JSON validation combinators.

So how do we implement FieldParser? One (“initial”) way is to use a free applicative functor and later interpret it in two ways: as a FromJSON-like parser and as a set of valid keys.

But there’s another (“final”) way which is to compose the applicative functor from components, one per required semantics. The semantics of FromJSON is given by ReaderT Object (Either ParseError). The semantics of a set of valid keys is given by Constant (HashMap Text ()). We take the product of these semantics to get the implementation of FieldParser:

newtype FieldParser a = FieldParser
  (Product
    (ReaderT Object (Either ParseError))
    (Constant (HashMap Text ())) a)

Notice how I used HashMap Text () instead of HashSet Text? This is a trick to be able to subtract this from the object (represented as HashMap Text Value) later.

Another benefit of this change is that it’s no longer necessary to give a name to the object (often called o), which I’ve always found awkward.

Improve error messages

Aeson’s approach to error messages is straightforward: it tries every alternative in turn and, if none succeeds, it returns the last error message.

There are two approaches to get a more sophisticated error reporting:

  1. Collect errors from all alternatives and somehow merge them. Each error would carry its level of “matching”. An alternative that matched the object but failed at key lookup matches better than the one that expected a string instead of an object. Thus the error from the first alternative would prevail. If there are multiple errors on the same level, we should try to merge them. For instance, if we expect an object or a string but got an array, then the error message should mention both object and string as valid options.

  2. Limited backtracking. This is what Parsec does. In our example, when it was determined that the object was “at least somewhat” matched by the first alternative, the second one would have been abandoned. This approach is rather restrictive: if you have two alternatives each expecting an object, the second one will never fire. The benefit of this approach is its efficiency (sometimes real, sometimes imaginary), since we never more than one alternative deeply.

It turns out, when parsing Values, we can remove some of the backtracking without imposing any restrictions. This is because we can “factor out” common parser prefixes. If we have two parsers that expect an object, this is equivalent to having a single parser expecting an object. To see this, let’s represent a parser as a record with a field per JSON “type”:

data Parser a = Parser
  { parseString :: Maybe (Text -> Either ParseError a)
  , parseArray  :: Maybe (Vector Value -> Either ParseError a)
  , parseObject :: Maybe (HashMap Text Value -> Either ParseError a)
  ...
  }

Writing a function Parser a -> Parser a -> Parser a which merges individual fields is then a simple exercise.

Why is every field wrapped in Maybe? How’s Nothing different from Just $ const $ Left "..."? This is so that we can see which JSON types are valid and give a better error message. If we tried to parse a JSON number as an Item, the error message would say that it expected an object or a string, because only those fields of the parser would be Just values.

Implementation

As you might notice, the Parser type above can be mechanically derived from the Value datatype itself. In my actual implementation, I use generics-sop with great success to reduce the boilerplate. To give you an idea, here’s the real definition of the Parser type:

newtype ParserComponent a fs = ParserComponent (Maybe (NP I fs -> Either ParseError a))
newtype Parser a = Parser (NP (ParserComponent a) (Code Value))

We can then apply a Parser to a Value using this function.


I’ve implemented this YAML parsing layer for our needs at Signal Vine. We are happy to share the code, in case someone is interested in maintaining this as an open source project.

July 26, 2015 08:00 PM

July 25, 2015

Dimitri Sabadie

Introducing Luminance, a safer OpenGL API

A few weeks ago, I was writing Haskell lines for a project I had been working on for a very long time. That project was a 3D engine. There are several posts about it on my blog, feel free to check out.

The thing is… Times change. The more it passes, the more I become mature in what I do in the Haskell community. I’m a demoscener, and I need to be productive. Writing a whole 3D engine for such a purpose is a good thing, but I was going round and round in circles, changing the whole architecture every now and then. I couldn’t make my mind and help it. So I decided to stop working on that, and move on.

If you are a Haskell developer, you might already know Edward Kmett. Each talk with him is always interesting and I always end up with new ideas and new knowledge. Sometimes, we talk about graphics, and sometimes, he tells me that writing a 3D engine from scratch and release it to the community is not a very good move.

I’ve been thinking about that, and in the end, I agree with Edward. There’re two reasons making such a project hard and not interesting for a community:

  1. a good “3D engine” is a specialized one – for FPS games, for simulations, for sport games, for animation, etc. If we know what the player will do, we can optimize a lot of stuff, and put less details into not-important part of the visuals. For instance, some games don’t really care about skies, so they can use simple skyboxes with nice textures to bring a nice touch of atmosphere, without destroying performance. In a game like a flight simulator, skyboxes have to be avoided to go with other techniques to provide a correct experience to players. Even though an engine could provide both techniques, apply that problem to almost everything – i.e. space partitionning for instance – and you end up with a nightmare to code ;
  2. an engine can be a very bloated piece of software – because of point 1. It’s very hard to keep an engine up to date regarding technologies, and make every one happy, especially if the engine targets a large audience of people – i.e. hackage.

Point 2 might be strange to you, but that’s often the case. Building a flexible 3D engine is a very hard and non-trivial task. Because of point 1, you utterly need to restrict things in order to get the required level of performance or design. There are people out there – especially in the demoscene world – who can build up 3D engines quickly. But keep in mind those engines are limited to demoscene applications, and enhancing them to support something else is not a trivial task. In the end, you might end up with a lot of bloated code you’ll eventually zap later on to build something different for another purpose – eh, demoscene is about going dirty, right?! ;)

Basics

So… Let’s go back to the basics. In order to include everyone, we need to provide something that everyone can download, install, learn and use. Something like OpenGL. For Haskell, I highly recommend using gl. It’s built against the gl.xml file – released by Khronos. If you need sound, you can use the complementary library I wrote, using the same name convention, al.

The problem with that is the fact that OpenGL is a low-level API. Especially for new comers or people who need to get things done quickly. The part that bothers – wait, no, annoys – me the most is the fact that OpenGL is a very old library which was designed two decades ago. And we suffer from that. A lot.

OpenGL is a stateful graphics library. That means it maintains a state, a context, in order to work properly. Maintaining a context or state is a legit need, don’t get it twisted. However, if the design of the API doesn’t fit such a way of dealing with the state, we come accross a lot of problems. Is there one programmer who hasn’t experienced black screens yet? I don’t think so.

The OpenGL’s API exposes a lot of functions that perform side-effects. Because OpenGL is weakly typed – almost all objects you can create in OpenGL share the same GL(u)int type, which is very wrong – you might end up doing nasty things. Worse, it uses an internal binding system to select the objects you want to operate on. For instance, if you want to upload data to a texture object, you need to bind the texture before calling the texture upload function. If you don’t, well, that’s bad for you. There’s no way to verify code safety at compile-time.

You’re not convinced yet? OpenGL doesn’t tell you directly how to change things on the GPU side. For instance, do you think you have to bind your vertex buffer before performing a render, or is it sufficient to bind the vertex array object only? All those questions don’t have direct answers, and you’ll need to dig in several wikis and forums to get your answers – the answer to that question is “Just bind the VAO, pal.”

What can we do about it?

Several attempts to enhance that safety have come up. The first thing we have to do is to wrap all OpenGL object types into proper types. For instance, we need several types for Texture and Framebuffer.

Then, we need a way to ensure that we cannot call a function if the context is not setup for. There are a few ways to do that. For instance, indexed monads can be a good start. However, I tried that, and I can tell you it’s way too complicated. You end up with very long types that make things barely unreadable. See this and this for excerpts.

Luminance

In my desperate quest of providing a safer OpenGL’s API, I decided to create a library from scratch called luminance. That library is not really an OpenGL safe wrapper, but it’s very close to being that.

luminance provides the same objects than OpenGL does, but via a safer way to create, access and use them. It’s an effort for providing safe abstractions without destroying performance down and suited for graphics applications. It’s not a 3D engine. It’s a rendering framework. There’s no light, asset managers or that kind of features. It’s just a tiny and simple powerful API.

Example

luminance is still a huge work in progress. However, I can already show an example. The following example opens a window but doesn’t render anything. Instead, it creates a buffer on the GPU and perform several simple operations onto it.

-- Several imports.
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Trans.Resource -- from the resourcet package
import Data.Foldable ( traverse_ )
import Graphics.Luminance.Buffer
import Graphics.Luminance.RW
import Graphics.UI.GLFW -- from the GLFW-b package
import Prelude hiding ( init ) -- clash with GLFW-b’s init function

windowW,windowH :: Int
windowW = 800
windowH = 600

windowTitle :: String
windowTitle = "Test"

main :: IO ()
main = do
init
-- Initiate the OpenGL context with GLFW.
windowHint (WindowHint'Resizable False)
windowHint (WindowHint'ContextVersionMajor 3)
windowHint (WindowHint'ContextVersionMinor 3)
windowHint (WindowHint'OpenGLForwardCompat False)
windowHint (WindowHint'OpenGLProfile OpenGLProfile'Core)
window <- createWindow windowW windowH windowTitle Nothing Nothing
makeContextCurrent window
-- Run our application, which needs a (MonadIO m,MonadResource m) => m
-- we traverse_ so that we just terminate if we’ve failed to create the
-- window.
traverse_ (runResourceT . app) window
terminate

-- GPU regions. For this example, we’ll just create two regions. One of floats
-- and the other of ints. We’re using read/write (RW) regions so that we can
-- send values to the GPU and read them back.
data MyRegions = MyRegions {
floats :: Region RW Float
, ints :: Region RW Int
}

-- Our logic.
app :: (MonadIO m,MonadResource m) => Window -> m ()
app window = do
-- We create a new buffer on the GPU, getting back regions of typed data
-- inside of it. For that purpose, we provide a monadic type used to build
-- regions through the 'newRegion' function.
region <- createBuffer $
MyRegions
<$> newRegion 10
<*> newRegion 5
clear (floats region) pi -- clear the floats region with pi
clear (ints region) 10 -- clear the ints region with 10
readWhole (floats region) >>= liftIO . print -- print the floats as an array
readWhole (ints region) >>= liftIO . print -- print the ints as an array
floats region `writeAt` 7 $ 42 -- write 42 at index=7 in the floats region
floats region @? 7 >>= traverse_ (liftIO . print) -- safe getter (Maybe)
floats region @! 7 >>= liftIO . print -- unsafe getter
readWhole (floats region) >>= liftIO . print -- print the floats as an array

Those read/write regions could also have been made read-only or write-only. For such regions, some functions can’t be called, and trying to do so will make your compiler angry and throw errors at you.

Up to now, the buffers are created persistently and coherently. That might cause issues with OpenGL synchronization, but I’ll wait for benchmarks before changing that part. If benchmarking spots performance bottlenecks, I’ll introduce more buffers and regions to deal with special cases.

luminance doesn’t force you to use a specific windowing library. You can then embed it into any kind of host libraries.

What’s to come?

luminance is very young. At the moment of writing this article, it’s only 26 commits old. I just wanted to present it so that people know it exists will be released as soon as possible. The idea is to provide a library that, if you use it, won’t create black screens because of framebuffers incorrectness or buffers issues. It’ll ease debugging OpenGL applications and prevent from making nasty mistakes.

I’ll keep posting about luminance as I get new features implemented.

As always, keep the vibe, and happy hacking!

by Dimitri Sabadie (noreply@blogger.com) at July 25, 2015 10:03 AM

July 23, 2015

Mark Jason Dominus

Mystery of the misaligned lowercase ‘p’

I've seen this ad on the subway at least a hundred times, but I never noticed this oddity before:

Specifically, check out the vertical alignment of those ‘p’s:

Notice that it is not simply an unusual font. The height of the ‘p’ matches the other lowercase letters exactly. Here's how it ought to look:

At first I thought the designer was going for a playful, informal logotype. Some of the other lawyers who advertise in the subway go for a playful, informal look. But it seemed odd in the context of the rest of the sign.

As I wondered what happened here, a whole story unfolded in my mind. Here's how I imagine it went down:

  1. The ‘p’, in proper position, collided with the edge of the light-colored box, or overlapped it entirely, causing the serif to disappear into the black area.

  2. The designer (Spivack's nephew) suggested enlarging the box, but there was not enough room. The sign must fit a standard subway car frame, so its size is prescribed.

  3. The designer then suggested eliminating “LAW OFFICES OF”, or eliminating some of the following copy, or reducing its size, but Spivack refused to cede even a single line. “Millions for defense,” cried Spivack, “but not one cent for tribute!”

  4. Spivack found the obvious solution: “Just move the up the ‘p’ so it doesn't bump into the edge, stupid!” Spivack's nephew complied. “Looks great!” said Spivack. “Print it!”

I have no real reason to believe that most of this is true, but I find it all so very plausible.

[ Addendum: Noted typographic expert Jonathan Hoefler says “I'm certain you are correct.” ]

by Mark Dominus (mjd@plover.com) at July 23, 2015 02:53 PM

Yesod Web Framework

Supporting HTTP/2

We are happy to announce that Warp version 3.1.0 and WarpTLS version 3.1.0 have been released. These versions include the following changes:

But the main new feature is HTTP/2 support! The latest versions of Firefox and Chrome support HTTP/2 over TLS. WarpTLS uses HTTP/2 instead of HTTP/1.1 if TLS ALPN(Application-Layer Protocol Negotiation) selects HTTP/2. So, if you upgrade Warp and WarpTLS in your site serving TLS and anyone visits your site with Firefox or Chrome, your contents are automatically transferred via HTTP/2 over TLS.

HTTP/2 retains the semantics of HTTP/1.1 such as request and response headers, meaning you don't have to modify your WAI applications, just link them to the new version of WarpTLS. Rather, HTTP/2 redesigned its transport to solve the following issues:

  1. Redundant headers: HTTP/1.1 repeatedly transfers almost exactly the same headers for every request and response, wasting bandwidth.
  2. Poor concurrency: only one request or response can be sent in one TCP connection at a time(request pipelining is not used in practice). What HTTP/1.1 can do is make use of multiple TCP connections, up to 6 per site.
  3. Head-of-line blocking: if one request is blocked on a server, no other requests can be sent in the same connection.

To solve the issue 1, HTTP/2 provides a header compression mechanism called HPACK. To fix the issue 2 and 3, HTTP/2 makes just one TCP connection per site and multiplex frames of requests and responses asynchronously. The default number of concurrency is 100.

I guess that the HTTP/2 implementors agree that the most challenging parts of HTTP/2 are HPACK and priority. HPACK is used to define reference sets as well as indices and Huffman encoding. During standardization activities, I found that reference sets make the spec really complicated, but does not contribute to the compression ratio. My big contribution to HTTP/2 was a proposal to remove reference sets from HPACK. The final HPACK became much simpler.

Since multiple requests and responses are multiplexed in one TCP connection, priority is important. Without priority, the response of a big file download would occupy the connection. I surveyed priority queues but could not find a suitable technology. Thus, I needed to invent random heaps by myself. If time allows, I would like to describe random heaps in this blog someday. The http2 library provides well-tested HPACK and structured priority queues as well as frame encoders/decoders.

My interest on implementing HTTP/2 in Haskell was how to map Haskell threads to HTTP/2 elements. In HTTP/1.1, the role of Haskell threads is clear. That is, one HTTP (TCP) connection is a Haskell thread. After trial and error, I finally reached an answer. Streams of HTTP/2 (roughly, a pair of request and response) is a Haskell thread. To avoid the overhead of spawning Haskell threads, I introduced thread pools to Warp. Yes, Haskell threads shine even in HTTP/2.

HTTP/2 provides plain (non-encrypted) communications, too. But since Firefox and Chrome require TLS, TLS is a MUST in practice. TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 is a mandate cipher suite in HTTP/2. Unfortunately, many pieces were missing in the tls library. So, it was necessary for me to implement ALPN, ECDHE(Elliptic curve Diffie-Hellman, ephemeral) and AES GCM(Galois/Counter Mode). They are already merged into the tls and cryptonite library.

My next targets are improving performance of HTTP/2 over TLS and implementing TLS 1.3.

I would like to thank Tatsuhiro Tsujikawa, the author of nghttp2 -- the reference implementation of HTTP/2 and Moto Ishizawa, the author of h2spec. Without these tools, I could not make such mature Warp/WarpTLS libraries. They also answered my countless questions. RFC 7540 says "the Japanese HTTP/2 community provided invaluable contributions, including a number of implementations as well as numerous technical and editorial contributions". I'm proud of being a member of the community.

Enjoy HTTP/2 in Haskell!

July 23, 2015 04:05 AM

Daniel Mlot (duplode)

Casual Hacking With stack

Sandboxes are exceptionally helpful not just for working in long-term Haskell projects, but also for casual experiments. While playing around, we tend to install all sorts of packages in a carefree way, which increases a lot the risk of entering cabal hell. While vanilla cabal-install sandboxes prevent such a disaster, using them systematically for experiments mean that, unless you are meticulous, you will end up either with dozens of .hs files in a single sandbox or with dozens of copies of the libraries strewn across your home directory. And no one likes to be meticulous while playing around. In that context, stack, the recently released alternative to cabal-install, can prevent trouble with installing packages in a way more manageable than through ad-hoc sandboxes. In this post, I will suggest a few ways of using stack that may be convenient for experiments. I have been using stack for only a few days, therefore suggestions are most welcome!

I won’t dwell on the motivation and philosophy behind stack 1. Suffice it to say that, at least in the less exotic workflows, there is a centralised package database somewhere in ~/.stack with packages pulled from a Stackage snapshot (and therefore known to be compatible with each other), which is supplemented by a per-project database (that is, just like cabal sandboxes) for packages not in Stackage (from Hackage or anywhere else). As that sounds like a great way to avoid headaches, we will stick to this arrangement, with only minor adjustments.

Once you have installed stack 2, you can create a new environment for experiments with stack new:

$ mkdir -p Development/haskell/playground
$ cd Development/haskell/playground
$ stack new --prefer-nightly

The --prefer-nightly option makes stack use a nightly snapshot of Stackage, as opposed to a long term support one. As we are just playing around, it makes sense to pick as recent as possible packages from the nightly instead of the LTS. (Moreover, I use Arch Linux, which already has GHC 7.10 and base 4.8, while the current LTS snapshot assumes base 4.7.) If this is the first time you use stack, it will pick the latest nightly; otherwise it will default to whatever nightly you already have in ~/.stack.

stack new creates a neat default project structure for you 3:

$ ls -R
.:
app  LICENSE  new-template.cabal  Setup.hs  src  stack.yaml  test

./app:
Main.hs

./src:
Lib.hs

./test:
Spec.hs

Of particular interest is the stack.yaml file, which holds the settings for the local stack environment. We will talk more about it soon.

flags: {}
packages:
- '.'
extra-deps: []
resolver: nightly-2015-07-19

As for the default new-template.cabal file, you can use its build-depends section to keep track of what you are installing. That will make stack build (the command which builds the current project without installing it) to download and install any dependencies you add to the cabal file automatically. Besides that, having the installed packages noted down may prove useful in case you need to reproduce your configuration elsewhere 4. If your experiments become a real project, you can clean up the build-depends without losing track of the packages you installed for testing purposes by moving their entries to a second cabal file, kept in a subdirectory:

$ mkdir xp
$ cp new-template.cabal xp/xp.cabal
$ cp LICENSE xp # Too lazy to delete the lines from the cabal file.
$ cd xp
$ vi Dummy.hs # module Dummy where <END OF FILE>
$ vi xp.cabal # Adjust accordingly, and list your extra deps.

You also need to tell stack about this fake subproject. All it takes is adding an entry for the subdirectory in stack.yaml:

packages:
- '.' # The default entry.
- 'xp'

With the initial setup done, we use stack build to compile the projects:

$ stack build
new-template-0.1.0.0: configure
new-template-0.1.0.0: build
fmlist-0.9: download
fmlist-0.9: configure
fmlist-0.9: build
new-template-0.1.0.0: install
fmlist-0.9: install
xp-0.1.0.0: configure
xp-0.1.0.0: build
xp-0.1.0.0: install
Completed all 3 actions.

In this test run, I added fmlist as a dependency of the fake package xp, and so it was automatically installed by stack. The output of stack build goes to a .stack-work subdirectory.

With the packages built, we can use GHCi in the stack environment with stack ghci. It loads the library source files of the current project by default:

$ stack ghci
Configuring GHCi with the following packages: new-template, xp
GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
[1 of 2] Compiling Lib              (
/home/duplode/Development/haskell/playground/src/Lib.hs, interpreted )
[2 of 2] Compiling Dummy            (
/home/duplode/Development/haskell/playground/xp/Dummy.hs, interpreted )
Ok, modules loaded: Dummy, Lib.
*Lib> import qualified Data.FMList as F -- Which we have just installed.
*Lib F> -- We can also load executables specified in the cabal file.
*Lib F> :l Main
[1 of 2] Compiling Lib              (
/home/duplode/Development/haskell/playground/src/Lib.hs, interpreted )
[2 of 2] Compiling Main             (
/home/duplode/Development/haskell/playground/app/Main.hs, interpreted )
Ok, modules loaded: Lib, Main.
*Main F>

Dependencies not in Stackage have to be specified in stack.yaml as well as in the cabal files, so that stack can manage them too. Alternative sources of packages include source trees in subdirectories of the project, Hackage and remote Git repositories 5:

flags: {}
packages:
- '.'
- 'xp'
- location: deps/acme-missiles-0.3 # Sources in a subdirectory.
  extra-dep: true # Mark as dep, i.e. not part of the project proper.
extra-deps:
- acme-safe-0.1.0.0 # From Hackage.
- acme-dont-1.1 # Also from Hackage, dependency of acme-safe.
resolver: nightly-2015-07-19

stack build will then install the extra dependencies to .stack-work/install. You can use stack solver to chase the indirect dependencies introduced by them. For instance, this is its output after commenting the acme-dont line in the stack.yaml just above:

$ stack solver --no-modify-stack-yaml
This command is not guaranteed to give you a perfect build plan
It's possible that even with the changes generated below, you will still
need to do some manual tweaking
Asking cabal to calculate a build plan, please wait
extra-deps:
- acme-dont-1.1

To conclude this tour, once you get bored of the initial Stackage snapshot all it takes to switch it is changing the resolver field in stack.yaml (with nightlies, that amounts to changing the date at the end of the snapshot name). That will cause all dependencies to be downloaded and built from the chosen snapshot when stack build is next ran. As of now, the previous snapshot will remain in ~/.stack unless you go there and delete it manually; however, a command for removing unused snapshots is in the plans.

I have not tested the sketch of a workflow presented here extensively, yet what I have seen was enough to convince me stack can provide a pleasant experience for casual experiments as well as full-fledged projects. Happy hacking!

Update: There is now a follow-up post about the other side of the coin, Migrating a Project to stack.

<section class="footnotes">
  1. For that, see Why is stack not cabal?, written by a member of its development team.

  2. For installation guidance, see the GitHub project wiki. Installing stack is easy, and there are many ways to do it (I simply got it from Hackage with cabal install stack).

  3. To create an environment for an existing project, with its own structure and cabal file, you would use stack init instead.

  4. In any case, you can also use stack exec -- ghc-pkg list to see all packages installed from the snapshot you are currently using. That, however, will be far messier than the build-depends list, as it will include indirect dependencies as well.

  5. For the latter, see the project wiki.

</section>
Comment on GitHub (see the full post for a reddit link)

by Daniel Mlot at July 23, 2015 02:30 AM

Oliver Charles

Another Approach to Default Function Parameters

Recently, there has been some new discussion around the issue of providing default values for function parameters in Haskell. First, Gabriel Gonzalez showed us his new optional-args library, which provides new types for optional arguments along with heavy syntactic overloading. To follow that, Dimitri Sabadie published a blog post discouraging the use of the currently popular Default type class. These are both good discussions, and as with any good discussion have been lingering around in the back of my head.

Since those discussions took place, I’ve been playing with my point in the FRP-web-framework design space - Francium. I made some big refactorings on an application using Francium, mostly extending so called “component” data types (buttons, checkboxes, etc), and was frustrated with how much code broke just from introducing new record fields. The Commercial Haskell group published an article on how to design for extensibility back in March, so I decided to revisit that.

It turns out that with a little bit of modification, the approach proposed in designing for extensibility also covers optional arguments pretty well!

First, let’s recap what it means to design for extensibility. The key points are:

  1. Functions take Settings values, which specify a general configuration.
  2. These Settings values are opaque, meaning they cannot be constructed by a data constructor, but they have a smart constructor instead. This smart constructor allows you to provide default values.
  3. Provide get/set functions for all configurable fields in your Settings data type, preventing the use of record syntax for updates (which leaks implementation details).

Regular Haskell users will already be familiar a pattern that can be seen in point 3: we often use a different piece of technology to solve this problem - lenses. Lenses are nice here because they reduce the surface area of our API - two exports can be reduced to just one, which I believe reduces the time to learn a new library. They also compose very nicely, in that they can be embedded into other computations with ease.

With point 3 ammended to use some form of lens, we end up with the following type of presentation. Take a HTTP library for example. Our hypothetical libray would have the following exports:

data HTTPSettings

httpKeepAlive :: Lens HTTPSettings Bool
httpCookieJar :: Lens HTTPSettings CookieJar

defaultHTTPSettings :: HTTPSettings

httpRequest :: HTTPSettings -> HTTPRequest -> IO Response

which might have usage

httpRequest
  (defaultHTTPSettings & httpKeepAlive .~ True)
  aRequest

This is an improvement, but I’ve never particularly liked the reverse function application stuff with &. The repeated use of & is essentially working in an Endo Writer monad, or more generally - a state monad. The lens library ships with operators for working specifically in state monads (of course it does), so let’s use that:


httpRequest :: State HTTPSettings x -> HTTPRequest -> IO Response

....

httpRequest
  (do httpKeepAlive .= True)
  aRequest

It’s a small change here, but when you are overriding a lot of parameters, the sugar offered by the use of do is hard to give up - especially when you throw in more monadic combinators like when and unless.

With this seemingly simple syntactic change, something interesting has happened; something which is easier to see if we break open httpRequest:

httpRequest :: State HTTPSettings x -> HTTPRequest -> IO Response
httpRequest mkConfig request =
  let config = execState mkConfig defaultHttpSettings
  in ...

Now the default configuration has moved inside the HTTP module, rather than being supplied by the user. All the user provides is essentially a function HTTPSettings -> HTTPSettings, dressed up in a state monad. This means that to use the default configuration, we simply provide a do-nothing state composition: return (). We can even give this a name

def :: State a ()
def = return ()

and voila, we now have the lovely name-overloading offered by Data.Default, but without the need to introduce a lawless type class!

To conclude, in this post I’ve shown that by slightly modifying the presentation of an approach to build APIs with extensibility in mind, we the main benefit of Data.Default. This main benefit - the raison d’être of Data.Default - is the ability to use the single symbol def whenever you just want a configuration, but don’t care what it is. We still have that ability, and we didn’t have to rely on an ad hoc type class to get there.

However, it’s not all rainbows and puppies: we did have to give something up to get here, and what we’ve given up is a compiler enforced consistency. With Data.Default, there is only a single choice of default configuration for a given type, so you know that def :: HTTPSettings will be the same set of defaults everywhere. With my approach, exactly what def means is down to the function you’re calling and how they want to interpret def. In practice, due to the lack of laws on def, there wasn’t much reasoning you could do about what that single instance was anyway, so I’m not sure much is given up in practice. I try and keep to a single interpretation of def in my libraries by still exporting defaultHTTPSettings, and then using execState mkConfig defaultHTTPSettings whenever I need to interpret a State HTTPConfig.

July 23, 2015 12:00 AM

July 22, 2015

Edward Kmett

On the unsafety of interleaved I/O

One area where I'm at odds with the prevailing winds in Haskell is lazy I/O. It's often said that lazy I/O is evil, scary and confusing, and it breaks things like referential transparency. Having a soft spot for it, and not liking most of the alternatives, I end up on the opposite side when the topic comes up, if I choose to pick the fight. I usually don't feel like I come away from such arguments having done much good at giving lazy I/O its justice. So, I thought perhaps it would be good to spell out my whole position, so that I can give the best defense I can give, and people can continue to ignore it, without costing me as much time in the future. :)

So, what's the argument that lazy I/O, or unsafeInterleaveIO on which it's based, breaks referential transparency? It usually looks something like this:

 
swap (x, y) = (y, x)
 
setup = do
  r1 < - newIORef True
  r2 <- newIORef True
  v1 <- unsafeInterleaveIO $ do writeIORef r2 False ; readIORef r1
  v2 <- unsafeInterleaveIO $ do writeIORef r1 False ; readIORef r2
  return (v1, v2)
 
main = do
  p1 <- setup
  p2 <- setup
  print p1
  print . swap $ p2
 

I ran this, and got:

(True, False)
(True, False)

So this is supposed to demonstrate that the pure values depend on evaluation order, and we have broken a desirable property of Haskell.

First a digression. Personally I distinguish the terms, "referential transparency," and, "purity," and use them to identify two desirable properties of Haskell. The first I use for the property that allows you to factor your program by introducing (or eliminating) named subexpressions. So, instead of:

 
f e e
 

we are free to write:

 
let x = e in f x x
 

or some variation. I have no argument for this meaning, other than it's what I thought it meant when I first heard the term used with respect to Haskell, it's a useful property, and it's the best name I can think of for the property. I also (of course) think it's better than some of the other explanations you'll find for what people mean when they say Haskell has referential transparency, since it doesn't mention functions or "values". It's just about equivalence of expressions.

Anyhow, for me, the above example is in no danger of violating referential transparency. There is no factoring operation that will change the meaning of the program. I can even factor out setup (or inline it, since it's already named):

 
main = let m = setup
        in do p1 < - m
              p2 <- m
              print p1
              print . swap $ p2
 

This is the way in which IO preserves referential transparency, unlike side effects, in my view (note: the embedded language represented by IO does not have this property, since otherwise p1 could be used in lieu of p2; this is why you shouldn't spend much time writing IO stuff, because it's a bad language embedded in a good one).

The other property, "purity," I pull from Amr Sabry's paper, What is a Purely Functional Language? There he argues that a functional language should be considered "pure" if it is an extension of the lambda calculus in which there are no contexts which observe differences in evaluation order. Effectively, evaluation order must only determine whether or not you get an answer, not change the answer you get.

This is slightly different from my definition of referential transparency earlier, but it's also a useful property to have. Referential transparency tells us that we can freely refactor, and purity tells us that we can change the order things are evaluated, both without changing the meaning of our programs.

Now, it would seem that the original interleaving example violates purity. Depending on the order that the values are evaluated, opponents of lazy I/O say, the values change. However, this argument doesn't impress me, because I think the proper way to think about unsafeInterleaveIO is as concurrency, and in that case, it isn't very strange that the results of running it would be non-deterministic. And in that case, there's not much you can do to prove that the evaluation order is affecting results, and that you aren't simply very unlucky and always observing results that happen to correspond to evaluation order.

In fact, there's something I didn't tell you. I didn't use the unsafeInterleaveIO from base. I wrote my own. It looks like this:

 
unsafeInterleaveIO :: IO a -> IO a
unsafeInterleaveIO action = do
  iv < - new
  forkIO $
    randomRIO (1,5) >>= threadDelay . (*1000) >>
    action >>= write iv
  return . read $ iv
 

iv is an IVar (I used ivar-simple). The pertinent operations on them are:

 
new :: IO (IVar a)
write :: IVar a -> a -> IO ()
read :: IVar a -> a
 

new creates an empty IVar, and we can write to one only once; trying to write a second time will throw an exception. But this is no problem for me, because I obviously only attempt to write once. read will block until its argument is actually is set, and since that can only happen once, it is considered safe for read to not require IO. [1]

Using this and forkIO, one can easily write something like unsafeInterleaveIO, which accepts an IO a argument and yields an IO a whose result is guaranteed to be the result of running the argument at some time in the future. The only difference is that the real unsafeInterleaveIO schedules things just in time, whereas mine schedules them in a relatively random order (I'll admit I had to try a few times before I got the 'expected' lazy IO answer).

But, we could even take this to be the specification of interleaving. It runs IO actions concurrently, and you will be fine as long as you aren't attempting to depend on the exact scheduling order (or whether things get scheduled at all in some cases).

In fact, thinking of lazy I/O as concurrency turns most spooky examples into threading problems that I would expect most people to consider rather basic. For instance:

  • Don't pass a handle to another thread and close it in the original.
  • Don't fork more file-reading threads than you have file descriptors.
  • Don't fork threads to handle files if you're concerned about the files being closed deterministically.
  • Don't read from the same handle in multiple threads (unless you don't care about each thread seeing a random subsequence of the stream).

And of course, the original example in this article is just non-determinism introduced by concurrency, but not of a sort that requires fundamentally different explanation than fork. The main pitfall, in my biased opinion, is that the scheduling for interleaving is explained in a way that encourages people to try to guess exactly what it will do. But the presumption of purity (and the reordering GHC actually does based on it) actually means that you cannot assume that much more about the scheduling than you can about my scheduler, at least in general.

This isn't to suggest that lazy I/O is appropriate for every situation. Sometimes the above advice means that it is not appropriate to use concurrency. However, in my opinion, people are over eager to ban lazy I/O even for simple uses where it is the nicest solution, and justify it based on the 'evil' and 'confusing' ascriptions. But, personally, I don't think this is justified, unless one does the same for pretty much all concurrency.

I suppose the only (leading) question left to ask is which should be declared unsafe, fork or ivars, since together they allow you to construct a(n even less deterministic) unsafeInterleaveIO?

[1] Note that there are other implementations of IVar. I'd expect the most popular to be in monad-par by Simon Marlow. That allows one to construct an operation like read, but it is actually less deterministic in my construction, because it seems that it will not block unless perhaps you write and read within a single 'transaction,' so to speak.

In fact, this actually breaks referential transparency in conjunction with forkIO:

 
deref = runPar . get
 
randomDelay = randomRIO (1,10) >>= threadDelay . (1000*)
 
myHandle m = m `catch` \(_ :: SomeExpression) -> putStrLn "Bombed"
 
mySpawn :: IO a -> IO (IVar a)
mySpawn action = do
  iv < - runParIO new
  forkIO $ randomDelay >> action >>= runParIO . put_ iv
  return iv
 
main = do
  iv < - mySpawn (return True)
  myHandle . print $ deref iv
  randomDelay
  myHandle . print $ deref iv
 

Sometimes this will print "Bombed" twice, and sometimes it will print "Bombed" followed by "True". The latter will never happen if we factor out the deref iv however. The blocking behavior is essential to deref maintaining referential transparency, and it seems like monad-par only blocks within a single runPar, not across multiples. Using ivar-simple in this example always results in "True" being printed twice.

It is also actually possible for unsafeInterleaveIO to break referential transparency if it is implemented incorrectly (or if the optimizer mucks with the internals in some bad way). But I haven't seen an example that couldn't be considered a bug in the implementation rather than some fundamental misbehavior. And my reference implementation here (with a suboptimal scheduler) suggests that there is no break that isn't just a bug.

by Dan Doel at July 22, 2015 03:29 PM

Yesod Web Framework

yesod-devel

Yesod-devel

A new development server is upon us. It's name is yesod-devel.
This post is about yesod-devel which is my Google Summer of Code project and not the current yesod-devel that is part of the yesod framework. It's not yet available and is still under development, meaning a lot of things in this post may change.

yesod-devel is a development server for haskell web applications that are WAI compliant.

What we expect from the application.

This is my opinion of what I expect from the web application and this may therefore change depending on what the community thinks. I think this design is good and losely coupled and leaves a lot of freedom to the web application.

At the heart of your application (the root of your web application) we expect you to have an Application.hs file which holds the Appliaction module. This is the file pointed to by your main-is section of the .cabal file.:

This Application.hs file holds the main function which fires up a warp server at a an address and port specified in an environment variable. Yesod devel will read everything it needs from the web application from environment variables and not from a config file.
It is the responsibility of the web application to set environment variables(setEnv). This way yesod-devel is very losely coupled to the web application. That is, we(yesod-devel) will not have to specify the names, paths of your config files or which serialization format it will use.

The environment variables we currently need are:

* haskellWebAddress="<ip_address>/localhost"
* haskellWebPort="<port_number>"

What you should expect from yesod-devel.

Automatic source and data file discovery.

You shouldn't expect to tell yesod-devel where your source files or data files (hamelet files and so forth) are as long as your web application knows where everything is. All you need to do is call the yesod-devel binary inside your app's root.

Building and running your code.

yesod-devel when run in your web application's working directory will run build and run your application on localhost:3000.

Automatic code reloading.

Yesod-devel supports automatic code reloading for any file modified in the current working directory. This is more proof of just how losely coupled yesod-devel will be from your application.

Newly added files don't trigger a recompile and neither do deleted files. However, file modifications do trigger a recompile. This is a deliberate design choice. Text editors as well as other programs keep adding and removing files from the file system and if we listened for any randomly created file or deleted file to trigger a recompile we would end up triggering useless recompiles.

This however means there's a trade-off. For being so losely coupled we have to manually restart yesod-devel everytime we add or delete files.

Reverse proxying.

Yesod-devel will start listening on the address and port specified in your environment variables haskellWebAddress and haskellWebPort respectively and reverse proxy it to your localhost:3000.

Report error messages to the browser.

Yesod-devel will report error messages from ghc to the web browser on localhost:3000.

Command line arguments.

Currently yesod-devel takes no command line arguments.

However, in the plans are the following.

  • --configure-with <config cabal="cabal" configure="configure" flags="flags" to="to">
  • --no-reverse-proxying
  • --show-iface fileName.hs

You should be fine without passing any of these arguments unless you have a special reason to.

Currently yesod-devel will configure your web application with the following flags to cabal.

  • -flibrary-only
  • --disable-tests
  • --disable-benchmarks
  • -fdevel
  • --disable-library-profiling
  • --with-ld=yesod-ld-wrapper
  • --with-ghc=yesod-ghc-wrapper
  • --with-ar=yesod-ar-wrapper
  • --with-hc-pkg=ghc-pkg

I assume that these arguments are self explanatory.

July 22, 2015 12:00 PM

Manuel M T Chakravarty

Don’t fight the system; exploit it!

Of course, I’m talking about the type system. A common opinion expressed by developers who are not used to languages that include strong static typing is that “types solve a problem I don’t have”, “they just get into my way”, and “the bugs crashing my shipping apps wouldn’t have been caught by a type checker anyway.”

Since the announcement of Swift about a year ago, I have heard a fair number of Objective-C programmers express that same opinion. Hence, it is interesting to listen to those who have made a leap of faith and tried to embrace types in their development process. A recent example is Ole Begemann’s Swift’s Type System. What stood out to me in Ole’s post is that he actually went to the trouble of looking at how programmers in languages, such as Haskell, ML, and Scala, work.

His take away was that types become useful if you allow them to help you write the program (as opposed to trying to impose them on the program you would have written without types). Then, the type system becomes a design tool, not an obstacle.

This idea, although born and explored in the communities around typed functional programming, is also powerful in object-oriented languages like Java, as explored in this two part post on More Typing, Less Testing. In fact, replacing tests by types is the mantra I repeated in my talk on Adopting Functional Programming in Swift (video) at Sydney CocoaHeads last year.

In summary, it is worthwhile using types to guide your program design. Moreover, to harness the power of functional programming in Swift, study how experienced programmers work in languages like Haskell, ML, Scala, F#, and so on. And finally, it occurs to me that the typed functional programming community hasn’t been very successful at communicating these ideas. We need to get better at that!

July 22, 2015 01:13 AM

July 21, 2015

Cartesian Closed Comic

The GHC Team

GHC Weekly News - 2015/07/21

Hi *,

Welcome for the latest entry in the GHC Weekly News. Today GHC HQ met to discuss the status of the imminent 7.10.2 release.

7.10.2 Status

In the past weeks we have been busily tracking down a number of regressions in the ghc-7.10 branch. At this point we have built up an impressive list of fixes. Thanks to everyone who has helped in this process!

In addition to resolving a number of simplifier regressions and portability issues (some mentioned in the Weekly News from 6 July), GHC 7.10.2 should be the first release which works out-of-the-box with GHCJS, thanks to a fix from Luite Stegeman. Moreover, we will have support for running in even the most minimal container environment (#10623).

At this point we have successfully tested the pre-release against Stackage (thanks for Michael Snoyman and Herbert Valerio Riedel for making this possible) and have found no major issues. A source tarball will be finalized and sent to the binary builders today. With luck we will have releasable binaries by the end of the week.

7.11 Things

Testing

Thomas Miedema has been doing some amazing work fixing some long-standing validation failures on the master branch. Moreover, he has been examining the viability of enabling larger swaths of the testsuite in Harbormaster validations.

In addition, Thomas has been doing some great work smoothing over a variety of rough edges in the build system and generally keeping things running smoothly. Thanks Thomas!

Typeable implementation

Another subject of discussion in this week's GHC call was Phabricator D757, a long-languishing change which moves the generation of Typeable instances from types' use sites to their definition sites. This change involves a trade-off as it moves compilation effort to the defining module, which will adversely affect compilation times of modules defining many types. Moreover, in the event that Typeable is never actually used this time is wasted effort. That being said, the current design of generating Typeable instances at the point of use makes the class a bit of a black sheep at the moment.

Runtime system matters

This week Simon Marlow will merge his D524, a rework of the runtime system's allocator which he reports has improved performance significantly in his workloads. This commit splits the concerns of reserving address space and requesting backing memory for this address space. While the former is relatively cheap, the latter can be quite expensive due to page-table setup. Consequently, his rework allocates a large chunk of addressing space up front and then incrementally commits it as needed. Interested readers are encouraged to look at the patch, which offers a nice glimpse into the inner workings of GHC's memory allocator.

Simon also has finished Phab:D1076, which should improve garbage collector performance by reworking the logic responsible for scavenging static objects. This work will be merged shortly.

Also discussed was the profiler mis-attribution issue mentioned in the Weekly News from 6 July 2015 (#10007). Peter Wortmann is currently looking at this issue, which ends up being due to an infelicity in the semantics implemented by the runtime system. Simon Marlow expressed that he did not know of a way to resolve this that isn't quite invasive. We will have to see what Peter proposes.

Applicative do

For some time now Simon Marlow has been working on implementing the ApplicativeDo proposal. Today in the call we discussed the status of this work and concluded that while some refactoring is likely possible, the work can be merged as-is. Hopefully at some point in the next few weeks this work will land.

Haddock comments for GADT constructors

It came to our attention that the GHC parser was unable to parse Haddock comments attached to GADT constructors. As it turns out, this is a rather long-standing problem. Despite this fact, the fix ended up being quite straightforward and will be in 7.12.

Backwards Compatibility

In general one should be able to compile the current GHC master branch with the last two compiler releases. Recently, however, the reality is a bit less clear-cut: while the current ghc-7.10 branch GHC will technically build with GHC 7.6 and 7.8, the tree does not necessarily pass the validate script due to a variety of imports rendered redundant by AMP and FTP. Moreover, the official policy on backwards compatibility is rather well-hidden on the Commentary/CodingStyle page.

This was discussed in today's meeting and it was decided that we will in the future maintain full validation-compatibility with the previous two releases. To ease this we will relax the use of -Werror when building the stage 1 compiler.

On a related note, this week Thomas Miedema ripped out some #ifdefs for GHC 7.6 compatibility from the master branch. Be aware that you will now need GHC 7.8 or newer to build master.

Mac OS X El Capitan support

It is well-known that the next Mac OS X release, El Capitan, will default to "root-less" mode, a security feature which restricts the operations available to even the root user. As a result of this feature some system calls in the El Capitan developer preview fail with EPERM instead of the usual EACCES. This change uncovered a bug in the unix library where EPERM was not treated similarly to EACCES. This was fixed in November 2014, a fix which is included in GHC 7.10.1.

However, there have been a few calls on ghc-devs for a bugfix release of the 7.8 series including the updated unix. We discussed this in the call today and concluded that we would not make such a release. Given that El Capitan is not yet released and the issue is fixed in 7.10, it doesn't seem worthwhile to put more developer time into 7.8. We would suggest that any El Capitan user unable to update to GHC 7.10.1 or newer disable root-less mode for the time being. This can be accomplished with,

sudo nvram boot-args="rootless=0"

Infrastructure

Recently it came to our attention that one of the build machines used by Harbormaster (Phabricator's build mechanism) was still running GHC 7.6. If you have seen strange validation issues on Harbormaster builds in the past, this is may be the cause. As of today this is fixed; all Harbormaster validations are now being built with GHC 7.8.4.

Harbormaster has historically had trouble working with Differentials which changed submodule revisions. This has made testing revisions involving submodules quite tricky. Thanks to a patch from Adam Sandberg Eriksson Harbormaster can now grab submodule commits from non-upstream repositories if set in .gitmodules.

Herbert Valerio Riedel has been making great strides improving the responsiveness of Trac. A Trac upgrade, a move to Postresql, and some fiddling with the WSGI configuration should result in a much better experience for everyone.

Have a great week!

~ Ben

by bgamari at July 21, 2015 07:20 PM

Erik de Castro Lopo

Building the LLVM Fuzzer on Debian.

I've been using the awesome American Fuzzy Lop fuzzer since late last year but had also heard good things about the LLVM Fuzzer. Getting the code for the LLVM Fuzzer is trivial, but when I tried to use it, I ran into all sorts of road blocks.

Firstly, the LLVM Fuzzer needs to be compiled with and used with Clang (GNU GCC won't work) and it needs to be Clang >= 3.7. Now Debian does ship a clang-3.7 in the Testing and Unstable releases, but that package has a bug (#779785) which means the Debian package is missing the static libraries required by the Address Sanitizer options. Use of the Address Sanitizers (and other sanitizers) increases the effectiveness of fuzzing tremendously.

This bug meant I had to build Clang from source, which nnfortunately, is rather poorly documented (I intend to submit a patch to improve this) and I only managed it with help from the #llvm IRC channel.

Building Clang from the git mirror can be done as follows:

  mkdir LLVM
  cd LLVM/
  git clone http://llvm.org/git/llvm.git
  (cd llvm/tools/ && git clone http://llvm.org/git/clang.git)
  (cd llvm/projects/ && git clone http://llvm.org/git/compiler-rt.git)
  (cd llvm/projects/ && git clone http://llvm.org/git/libcxx.git)
  (cd llvm/projects/ && git clone http://llvm.org/git/libcxxabi)

  mkdir -p llvm-build
  (cd llvm-build/ && cmake -G "Unix Makefiles" -DCMAKE_INSTALL_PREFIX=$(HOME)/Clang/3.8 ../llvm)
  (cd llvm-build/ && make install)

If all the above works, you will now have working clang and clang++ compilers installed in $HOME/Clang/3.8/bin and you can then follow the examples in the LLVM Fuzzer documentation.

July 21, 2015 10:08 AM

Mike Izbicki

Fast Nearest Neighbor Queries in Haskell

Fast Nearest Neighbor Queries in Haskell

posted on 2015-07-21

Two weeks ago at ICML, I presented a method for making nearest neighbor queries faster. The paper is called Faster Cover Trees and discusses some algorithmic improvements to the cover tree data structure. You can find the code in the HLearn library on github.

The implementation was written entirely in Haskell, and it is the fastest existing method for nearest neighbor queries in arbitrary metric spaces. (If you want a non-Haskell interface, the repo comes with a standalone program called hlearn-allknn for finding nearest neighbors.) In this blog post, I want to discuss four lessons learned about using Haskell to write high performance numeric code. But before we get to those details, let’s see some benchmarks.

The benchmarks

The benchmark task is to find the nearest neighbor of every point in the given dataset. We’ll use the four largest datasets in the mlpack benchmark suite and the Euclidean distance. (HLearn supports other distance metrics, but most of the compared libraries do not.) You can find more details about the compared libraries and instructions for reproducing the benchmarks in the repo’s bench/allknn folder.

the runtime of finding every nearest neighbor

alt alt alt alt

Notice that HLearn’s cover trees perform the fastest on each dataset except for YearPredict. But HLearn can use all the cores on your computer to parallelize the task. Here’s how performance scales with the number of CPUs on an AWS EC2 c3.8xlarge instance with 16 true cores:

alt

With parallelism, HLearn is now also the fastest on the YearPredict dataset by a wide margin. (FLANN is the only other library supporting parallelism, but in my tests with this dataset parallelism actually slowed it down for some reason.)

You can find a lot more cover tree specific benchmarks in the Faster Cover Trees paper.

The lessons learned

The Haskell Wiki’s guide to performance explains the basics of writing fast code. But unfortunately, there are many details that the wiki doesn’t cover. So I’ve selected four lessons from this project that I think summarize the state-of-the-art in high performance Haskell coding.

Lesson 1: Polymorphic code in GHC is slower than it needs to be.

Haskell makes generic programming using polymorphism simple. My implementation of the cover tree takes full advantage of this. The CoverTree_ type implements the data structure that speeds up nearest neighbor queries. It is defined in the module HLearn.Data.SpaceTree.CoverTree as:

data CoverTree_
        ( childC :: * -> * ) -- the container type to store children in
        ( leafC  :: * -> * ) -- the container type to store leaves in
        ( dp     :: *      ) -- the type of the data points
    = Node
        { nodedp                :: !dp
        , level                 :: {-#UNPACK#-}!Int
        , nodeWeight            :: !(Scalar dp)
        , numdp                 :: !(Scalar dp)
        , maxDescendentDistance :: !(Scalar dp)
        , children              :: !(childC (CoverTree_ childC leafC dp))
        , leaves                :: !(leafC dp)
        }

Notice that every field except for level is polymorphic. A roughly equivalent C++ struct (using higher kinded templates) would look like:

template < template <typename> typename childC
         , template <typename> typename leafC
         , typename dp
         >
struct CoverTree_
{
    dp                                  *nodedp;
    int                                  level;
    dp::Scalar                          *nodeWeight;
    dp::Scalar                          *numdp;
    dp::Scalar                          *maxDescendentDistance;
    childC<CoverTree_<childC,leafC,dp>> *children;
    leafC<dp>                           *leaves;
}

Notice all of those nasty pointers in the C++ code above. These pointers destroy cache performance for two reasons. First, the pointers take up a significant amount of memory. This memory fills up the cache, blocking the data we actually care about from entering cache. Second, the memory the pointers reference can be in arbitrary locations. This causes the CPU prefetcher to load the wrong data into cache.

The solution to make the C++ code faster is obvious: remove the pointers. In Haskell terminology, we call this unpacking the fields of the Node constructor. Unfortunately, due to a bug in GHC (see issues #3990 and #7647 and a reddit discussion), these polymorphic fields cannot currently be unpacked. In principle, GHC’s polymorphism can be made a zero-cost abstraction similar to templates in C++; but we’re not yet there in practice.

As a temporary work around, HLearn provides a variant of the cover tree specialized to work on unboxed vectors. It is defined in the module HLearn.Data.SpaceTree.CoverTree_Specialized as:

data CoverTree_
        ( childC :: * -> * ) -- must be set to: BArray
        ( leafC  :: * -> * ) -- must be set to: UArray
        ( dp     :: *      ) -- must be set to: Labaled' (UVector "dyn" Float) Int
    = Node
        { nodedp                :: {-#UNPACK#-}!(Labeled' (UVector "dyn" Float) Int)
        , nodeWeight            :: {-#UNPACK#-}!Float
        , level                 :: {-#UNPACK#-}!Int
        , numdp                 :: {-#UNPACK#-}!Float
        , maxDescendentDistance :: {-#UNPACK#-}!Float
        , children              :: {-#UNPACK#-}!(BArray (CoverTree_ exprat childC leafC dp))
        , leaves                :: {-#UNPACK#-}!(UArray dp)
        }

Since the Node constructor no longer has polymorphic fields, all of its fields can be unpacked. The hlearn-allknn program imports this specialized cover tree type, giving a 10-30% speedup depending on the dataset. It’s a shame that I have to maintain two separate versions of the same code to get this speedup.

Lesson 2: High performance Haskell code must be written for specific versions of GHC.

Because Haskell code is so high level, it requires aggressive compiler optimizations to perform well. Normally, GHC combined with LLVM does an amazing job with these optimizations. But in complex code, sometimes these optimizations don’t get applied when you expect them. Even worse, different versions of GHC apply these optimizations differently. And worst of all, debugging problems related to GHC’s optimizer is hard.

I discovered this a few months ago when GHC 7.10 was released. I decided to upgrade HLearn’s code base to take advantage of the new compiler’s features. This upgrade caused a number of performance regressions which took me about a week to fix. The most insidious example happened in the findNeighbor function located within the HLearn.Data.SpaceTree.Algorithms module. The inner loop of this function looks like:

go (Labeled' t dist) (Neighbor n distn) = if dist*ε > maxdist
    then Neighbor n distn
    else inline foldr' go leafres
        $ sortBy (\(Labeled' _ d1) (Labeled' _ d2) -> compare d2 d1)
        $ map (\t' -> Labeled' t' (distanceUB q (stNode t') (distnleaf+stMaxDescendentDistance t)))
        $ toList
        $ stChildren t
    where
        leafres@(Neighbor _ distnleaf) = inline foldr'
            (\dp n@(Neighbor _ distn') -> cata dp (distanceUB q dp distn') n)
            (cata (stNode t) dist (Neighbor n distn))
            (stLeaves t)

        maxdist = distn+stMaxDescendentDistance t

For our purposes right now, the important thing to note is that go contains two calls to foldr': one folds over the CoverTree_’s childC, and one over the leafC. In GHC 7.8, this wasn’t a problem. The compiler correctly specialized both functions to the appropriate container type, resulting in fast code.

But for some reason, GHC 7.10 did not want to specialize these functions. It decided to pass around huge class dictionaries for each function call, which is a well known cause of slow Haskell code. In my case, it resulted in more than a 20 times slowdown! Finding the cause of this slowdown was a painful exercise in reading GHC’s intermediate language core. The typical tutorials on debugging core use trivial examples of only a dozen or so lines of core code. But in my case, the core of the hlearn-allknn program was several hundred thousand lines long. Deciphering this core to find the slowdown’s cause was one of my more painful Haskell experiences. A tool that analyzed core to find function calls that contained excessive dictionary passing would make writing high performance Haskell code much easier.

Once I found the cause of the slowdown, fixing it was trivial. All I had to do was call the inline function on both calls to foldr. In my experience, this is a common theme in writing high performance Haskell code: Finding the cause of problems is hard, but fixing them is easy.

Lesson 3: Immutability and laziness can make numeric code faster.

The standard advice in writing numeric Haskell code is to avoid laziness. This is usually true, but I want to provide an interesting counter example.

This lesson relates to the same go function above, and in particular the call to sortBy. sortBy is a standard Haskell function that uses a lazy merge sort. Lazy merge sort is a slow algorithm—typically more than 10 times slower than in-place quicksort. Profiling hlearn-allknn shows that the most expensive part of nearest neighbor search is calculating distances (taking about 80% of the run time), and the second most expensive part is the call to sortBy (taking about 10% of the run time). But I nevertheless claim that this lazy merge sort is actually making HLearn’s nearest neighbor queries much faster due to its immutability and its laziness.

We’ll start with immutability since it is pretty straightforward. Immutability makes parallelism easier and faster because there’s no need for separate threads to place locks on any of the containers.

Laziness is a bit trickier. If the explanation below doesn’t make sense, reading Section 2 of the paper where I discuss how a cover tree works might help. Let’s say we’re trying to find the nearest neighbor to a data point we’ve named q. We can first sort the children according to their distance from q, then look for the nearest neighbors in the sorted children. The key to the cover tree’s performance is that we don’t have to look in all of the subtrees. If we can prove that a subtree will never contain a point closer to q than a point we’ve already found, then we “prune” that subtree. Because of pruning, we will usually not descend into every child. So sorting the entire container of children is a waste of time—we should only sort the ones we actually visit. A lazy sort gives us this property for free! And that’s why lazy merge sort is faster than an in-place quick sort for this application.

Lesson 4: Haskell’s standard libraries were not designed for fast numeric computing.

While developing this cover tree implementation, I encountered many limitations in Haskell’s standard libraries. To work around these limitations, I created an alternative standard library called SubHask. I have a lot to say about these limitations, but here I’ll restrict myself to the most important point for nearest neighbor queries: SubHask lets you safely create unboxed arrays of unboxed vectors, but the standard library does not. (Unboxed containers, like the UNPACK pragma mentioned above, let us avoid the overhead of indirections caused by the Haskell runtime. The Haskell wiki has a good explanation.) In my experiments, this simple optimization let me reduce cache misses by around 30%, causing the program to run about twice as fast!

The distinction between an array and a vector is important in SubHask—arrays are generic containers, and vectors are elements of a vector space. This distinction is what lets SubHask safely unbox vectors. Let me explain:

In SubHask, unboxed arrays are represented using the UArray :: * -> * type in SubHask.Algebra.Array. For example, UArray Int is the type of an unboxed array of ints. Arrays can have arbitrary length, and this makes it impossible to unbox an unboxed array. Vectors, on the other hand, must have a fixed dimension. Unboxed vectors in SubHask are represented using the UVector :: k -> * -> * type in SubHask.Algebra.Vector. The first type parameter k is a phantom type that specifies the dimension of the vector. So a vector of floats with 20 dimensions could be represented using the type UVector 20 Float. But often the size of a vector is not known at compile time. In this case, SubHask lets you use a string to identify the dimension of a vector. In hlearn-allknn, the data points are represented using the type UVector "dyn" Float. The compiler then statically guarantees that every variable of type UVector "dyn" Float will have the same dimension. This trick is what lets us create the type UArray (UVector "dyn" Float).

The hlearn-allknn program exploits this unboxing by setting the leafC parameter of CoverTree_ to UArray. Then, we call the function packCT which rearranges the nodes in leafC to use the cache oblivious van Embde Boas tree layout. Unboxing by itself gives a modest 5% performance gain from the reduced overhead in the Haskell run time system; but unpacking combined with this data rearrangement actually cuts runtime in half!

Unfortunately, due to some current limitations in GHC, I’m still leaving some performance on the table. The childC parameter to CoverTree_ cannot be UArray because CoverTree_s can have a variable size depending on their number of children. Therefore, childC is typically set to the boxed array type BArray. The GHC limitation is that the run time system gives us no way to control where the elements of a BArray exist in memory. Therefore, we do not get the benefits of the CPU prefetcher. I’ve proposed a solution that involves adding new primops to the GHC compiler (see feature request #10652). Since there are typically more elements within the childC than the leafC on any given cover tree, I estimate that the speedup due to better cache usage of BArrays would be even larger than the speedup reported above.

Conclusion

My experience is that Haskell can be amazingly fast, but it takes a lot of work to get this speed. I’d guess that it took about 10 times as much work to create my Haskell-based cover tree than it would have taken to create a similar C-based implementation. (I’m roughly as proficient in each language.) Furthermore, because of the current limitations in GHC I pointed out above, the C version would be just a bit faster.

So then why did I use Haskell? To make cover trees 10 times easier for programmers to use.

Cover trees can make almost all machine learning algorithms faster. For example, they’ve sped up SVMs, clustering, dimensionality reduction, and reinforcement learning. But most libraries do not take advantage of this optimization because it is relatively time consuming for a programmer to do by hand. Fortunately, the fundamental techniques are simple enough that they can be implemented as a compiler optimization pass, and Haskell has great support for libraries that implement their own optimizations. So Real Soon Now (TM) I hope to show you all how cover trees can speed up your Haskell-based machine learning without any programmer involvement at all.

July 21, 2015 12:00 AM

July 20, 2015

FP Complete

Package security in stack

As readers of this blog or the mailing lists are likely already aware: package security is important to both FP Complete and other members of the Commercial Haskell community. While there was quite a bit of public discussion around this during the planning phase, I was reminded in a conversation on Friday that we never announced the outcome of these plans.

tl;dr: Secure package distribution is fully implemented in stack, with some options to harden the default. We're still implementing an easy author signing story, and that will be announced soon.

The implementation we have in stack follows the plan in the above-linked proposal pretty directly. Let me just flesh it out fully here:

  • The all-cabal-hashes repository is used by default by stack for getting the collection of cabal files (known as the package index). This is downloaded over https. In addition to the raw .cabal files, this repository also contains hashes and download sizes for all tarballs available.
  • When downloading tarballs, the file size and content hash will be verified against the information provided in the index, if available. If more bytes are provided than indicated, the download is aborted. Only after verification is complete is the file moved into its final destination and available for future operations.
  • For added security (which I'd recommend), you can also turn on GPG verification and requiring hashes for this index (see the stack.yaml configuration settings).
    • GPG verification will use Git's built-in GPG support to verify the signature on the all-cabal-hashes tag before accepting the new content, and will refuse to update the index if the GPG verification fails. (You'll need to add our GPG key to your keychain.)
    • Requiring hashes means that the package index will not be accepted unless every package listed also has package hash/download size information. This is disabled by default for those who download the package index without Git support.

The story still isn't complete: we have no way to verify that the package author really is the person who uploaded the package. Stay tuned to the upload/signature author work we're doing, which will hopefully be available Real Soon Now(tm).

July 20, 2015 01:00 PM

Functional Jobs

OCaml server-side developer at Ahrefs Research (Full-time)

Who we are

Ahrefs Research is a San Francisco branch of Ahrefs Pte Ltd (Singapore), which runs an internet-scale bot that crawls whole Web 24/7, storing huge volumes of information to be indexed and structured in timely fashion. On top of that Ahrefs is building analytical services for end-users.

Ahrefs Research develops a custom petabyte-scale distributed storage to accommodate all that data coming in at high speed, focusing on performance, robustness and ease of use. Performance-critical low-level part is implemented in C++ on top of a distributed filesystem, while all the coordination logic and communication layer, along with API library exposed to the developer is in OCaml.

We are a small team and strongly believe in better technology leading to better solutions for real-world problems. We worship functional languages and static typing, extensively employ code generation and meta-programming, value code clarity and predictability, constantly seek out to automate repetitive tasks and eliminate boilerplate, guided by DRY and following KISS. If there is any new technology that will make our life easier - no doubt, we'll give it a try. We rely heavily on opensource code (as the only viable way to build maintainable system) and contribute back, see e.g. https://github.com/ahrefs . It goes without saying that our team is all passionate and experienced OCaml programmers, ready to lend a hand or explain that intricate ocamlbuild rule.

Our motto is "first do it, then do it right, then do it better".

What we need

Ahrefs Research is looking for backend developer with deep understanding of operating systems, networks and taste for simple and efficient architectural designs. Our backend is implemented mostly in OCaml and some C++, as such proficiency in OCaml is very much appreciated, otherwise a strong inclination to intensively learn OCaml in a short term will be required. Understanding of functional programming in general and/or experience with other FP languages (F#,Haskell,Scala,Scheme,etc) will help a lot. Knowledge of C++ is a plus.

The candidate will have to deal with the following technologies on the daily basis:

  • networks & distributed systems
  • 4+ petabyte of live data
  • OCaml
  • C++
  • linux
  • git

The ideal candidate is expected to:

  • Independently deal with and investigate bugs, schedule tasks and dig code
  • Make argumented technical choice and take responsibility for it
  • Understand the whole technology stack at all levels : from network and userspace code to OS internals and hardware
  • Handle full development cycle of a single component, i.e. formalize task, write code and tests, setup and support production (devops)
  • Approach problems with practical mindset and suppress perfectionism when time is a priority

These requirements stem naturally from our approach to development with fast feedback cycle, highly-focused personal areas of responsibility and strong tendency to vertical component splitting.

What you get

We provide:

  • Competitive salary
  • Modern office in San Francisco SOMA (Embarcadero)
  • Informal and thriving atmosphere
  • First-class workplace equipment (hardware, tools)
  • No dress code

Get information on how to apply for this position.

July 20, 2015 08:07 AM

Philip Wadler

Haskell in Production: Bdellium


At Medium, Fredrik (@ique) describes using Haskell in anger.
At the start of the products’ life we mostly analyzed small retirement plans with 100 to 500 plan participants. As time went on we started seeing plans with 2,000 participants and even 10,000 participants. At these numbers the execution time for the processing started going outside of acceptable bounds. Luckily, every participant could be analyzed in isolation from the others and so the problem was embarrassingly parallel.
I changed one line of code from
map outputParticipant parts
to
map outputParticipant parts `using` parListChunk 10 rdeepseq
and execution times were now about 3.7x faster on our 4-core server. That was enough to entirely fix the issue for another 6 months, during which time we could focus on further enhancing the product instead of worrying about performance. Later, we did do extensive profiling and optimization of the code to further reduce execution times significantly, but we didn’t want to prematurely optimize anything.
Spotted via Manual Chakravarty @TacticalGrace.

by Philip Wadler (noreply@blogger.com) at July 20, 2015 07:22 AM

Manuel M T Chakravarty

Type-safe Runtime Code Generation: Accelerate to LLVM

The purely functional, high-performance array language Accelerate has gained an LLVM-based backend targeting both multicore CPUs and GPUs that uses Haskell’s advanced type system to statically assure a range of safety properties. In the final version of our paper at the forthcoming 2015 Haskell Symposium, we describe (1) how we ensure these safety properties using GADTs and type families, (2) we outline the architecture of the LLVM backend (including a richly typed interface to LLVM), and (3) we provide benchmarks supporting our claim that we are able to produce competitive code.

Shoutout to the awesome Trevor McDonell who did all the hard work.

July 20, 2015 02:09 AM

July 19, 2015

Functional Programming Group at the University of Kansas

New Papers

Two papers from the University of Kansas Functional Programming Group have been accepted for publication at Haskell'15! One about using HERMIT for equational reasoning, and the other about a monad-based design pattern for remote control that externalizes monadic execution. We've put the preprints on our webpage.

Reasoning with the HERMIT: Tool support for equational reasoning on GHC core programs

(by A. Farmer, N. Sculthorpe, and A. Gill)

A benefit of pure functional programming is that it encourages equational reasoning. However, the Haskell language has lacked direct tool support for such reasoning. Consequently, reasoning about Haskell programs is either performed manually, or in another language that does provide tool support (e.g. Agda or Coq). HERMIT is a Haskell-specific toolkit designed to support equational reasoning and user-guided program transformation, and to do so as part of the GHC compilation pipeline. This paper describes HERMIT’s recently developed support for equational reasoning, and presents two case studies of HERMIT usage: checking that type-class laws hold for specific instance declarations, and mechanising textbook equational reasoning.

The Remote Monad Design Pattern

(by A. Gill, N. Sculthorpe, J. Dawson, A. Eskilson, A. Farmer, M. Grebe, J. Rosenbluth, R. Scott, and J. Stanton)

Remote Procedure Calls are expensive. This paper demonstrates how to reduce the cost of calling remote procedures from Haskell by using the remote monad design pattern, which amortizes the cost of remote calls. This gives the Haskell community access to remote capabilities that are not directly supported, at a surprisingly inexpensive cost.

We explore the remote monad design pattern through six models of remote execution patterns, using a simulated Internet of Things toaster as a running example. We consider the expressiveness and optimizations enabled by each remote execution model, and assess the feasibility of our approach. We then present a full-scale case study: a Haskell library that provides a Foreign Function Interface to the JavaScript Canvas API. Finally, we discuss existing instances of the remote monad design pattern found in Haskell libraries.

by Andy Gill (noreply@blogger.com) at July 19, 2015 10:48 PM

Neil Mitchell

Thoughts on Conduits

Summary: I'm growing increasingly fond of the Conduit library. Here I give my intuitions and some hints I'd have found useful.

Recently I've been working on converting the Hoogle database generation to use the Conduit abstraction, in an effort to reduce the memory and improve the speed. It worked - database generation has gone from 2Gb of RAM to 320Mb, and time has dropped from several minutes (or > 15 mins on memory constrained machines) to 45s. These changes are all in the context of Hoogle 5, which should hopefully be out in a month or so.

The bit that I've converted to Conduit is something that takes in a tarball of one text files per Hackage file, namely the Haddock output with one definition per line (this 22Mb file). It processes each definition, saves it to a single binary file (with compression and some processing), and returns some compact information about the definition for later processing. I don't expect the process to run in constant space as it is accumulating some return information, but it is important that most of the memory used by one definition is released before the next definition. I originally tried lazy IO, and while it somewhat worked, it was hard to abstract properly and very prone to space leaks. Converting to Conduit was relatively easy and is simpler and more robust.

The Conduit model

My mental model for a conduit Conduit a m b is roughly a function [a] -> m [b] - a values go in and b values come out (but interleaved with the monadic actions). More concretely you ask for an a with await and give back a b with yield, doing stuff in the middle in the m Monad.

A piece of conduit is always either running (doing it's actual work), waiting after a yield for the downstream person to ask for more results (with await), or waiting after an await for the upstream person to give the value (with yield). You can think of a conduit as making explicit the demand-order inherent in lazy evaluation.

Things to know about Conduit

I think it's fair to say Conduit shows its history - this is good for people who have been using it for a while (your code doesn't keep breaking), but bad for people learning it (there are lots of things you don't care about). Here are some notes I made:

  • The Data.Conduit module in the conduit library is not the right module to use - it seems generally accepted to use the Conduit module from the conduit-combinators package. However, I decided to build my own conduit-combinators style replacement in the Hoogle tree, see General.Conduit - the standard Conduit module has a lot of dependencies, and a lot of generalisations.
  • Don't use Source or Sink - use Producer and Consumer - the former are just a convenient way to get confusing error messages.
  • Don't use =$ or $=, always use =$= between conduits. The =$= operator is essentially flip (.).
  • Given a Conduit you can run it with runConduit. Alternatively, given a =$= b =$= c you can replace any of the =$= with $$ to run the Conduit as well. I find that a bit ugly, and have stuck to runConduit.
  • Conduit and ConduitM have their type arguments in different orders, which is just confusing. However, generally I use either Conduit (a connector) or Producer (something with a result). You rarely need something with a result and a return value.
  • You call await to see if a value is available to process. The most common bug I've had with conduits is forgetting to make the function processing items recursive - usually you want awaitForever, not just await.
  • The ByteString lines Conduit function was accidentally O(n^2) - I spotted and fixed that. Using difference lists does not necessarily make your code O(n)!

Useful functions

When using Conduit I found a number of functions seemingly missing, so defined them myself.

First up is countC which counts the number of items that are consumed. Just a simple definition on top of sumC.

countC :: (Monad m, Num c) => Consumer a m c
countC = sumC <| mapC (const 1)

While I recommend awaitForever in preference to await, it's occasionally useful to have awaitJust as the single-step awaitForever, if you are doing your own recursion.

awaitJust :: Monad m => (i -> Conduit i m o) -> Conduit i m o
awaitJust act = do
x <- await
whenJust x act

I regularly find zipFrom i = zip [i..] very useful in strict languages, and since Conduit can be viewed as a strict version of lazy lists (through very foggy glasses) it's no surprise a Conduit version is also useful.

zipFromC :: (Monad m, Enum c) => c -> Conduit a m (c, a)
zipFromC !i = awaitJust $ \a -> do
yield (i,a)
zipFromC (succ i)

Finally, it's useful to zip two conduits. I was surprised how fiddly that was with the standard operators (you have to use newtype wrappers and an Applicative instance), but a simple |$| definition hides that complexity away.

(|$|) :: Monad m => ConduitM i o m r1 -> ConduitM i o m r2 -> ConduitM i o m (r1,r2)
(|$|) a b = getZipConduit $ (,) <$> ZipConduit a <*> ZipConduit b

Why not Pipes?

I am curious if all Pipes users get asked "Why not use Conduit?", or if this FAQ is asymmetrical?

I realise pipes are billed as the more "principled" choice for this type of programming, but I've yet to see anywhere Conduit seems fundamentally unprincipled. I use WAI/Warp and http-conduit, so learning Conduit gives me some help there.

by Neil Mitchell (noreply@blogger.com) at July 19, 2015 02:58 PM

Eric Kidd

Proving sorted lists correct using the Coq proof assistant

About 15 years ago, I was hanging out at the MIT AI Lab, and there was an ongoing seminar on the Coq proof assistant. The idea was that you wouldn't have to guess whether your programs were correct; you could prove that they worked correctly.

The were just two little problems:

  1. It looked ridiculously intimidating.
  2. Rumor said that it took a grad student all summer to implement and prove the greatest common divisor algorithm, which sounded rather impractical.

So I decided to stick to Lispy languages, which is what I was officially supposed to be hacking on, anyway, and I never did try to sit in on the seminar.

Taking another look

I should have taken a look much sooner. This stuff provides even more twisted fun than Haskell! Also, projects like the CompCert C compiler are impressive: Imagine a C compiler where every optimization has been proven correct.

Even better, we can write code in Coq, prove it correct, then export it to Haskell or several other functional languages.

Here's an example Coq proof. Let's start with a basic theorem that says "If we know A is true, and we know B is true, then we know A /\ B (both A and B) is true."

Theorem basic_conj : forall (A B : Prop),
  A -> B -> A /\ B.
Proof.
  (* Give names to our inputs. *)
  intros A B H_A_True H_B_True.
  (* Specify that we want to prove each half
     of /\ separately. *)
  split.
  - apply H_A_True. (* Prove the left half. *)
  - apply H_B_True. (* Prove the right half. *)
Qed.

But Coq proofs are intended to be read interactively, using a tool like CoqIDE or Emacs Proof General. Let me walk you through how this proof would really look.

Proof.

At this point, the right-hand pane will show the theorem that we're trying to prove:

1 subgoals, subgoal 1 (ID 1)

  ============================
   forall A B : Prop, A -> B -> A /\ B

Read more…

July 19, 2015 11:39 AM

Mark Jason Dominus

Math.SE report 2015-04

[ Notice: I originally published this report at the wrong URL. I moved it so that I could publish the June 2015 report at that URL instead. If you're seeing this for the second time, you might want to read the June article instead. ]

A lot of the stuff I've written in the past couple of years has been on Mathematics StackExchange. Some of it is pretty mundane, but some is interesting. I thought I might have a little meta-discussion in the blog and see how that goes. These are the noteworthy posts I made in April 2015.

  • Languages and their relation : help is pretty mundane, but interesting for one reason: OP was confused about a statement in a textbook, and provided a reference, which OPs don't always do. The text used the symbol . OP had interpreted it as meaning , but I think what was meant was .

    I dug up a copy of the text and groveled over it looking for the explanation of , which is not standard. There was none that I could find. The book even had a section with a glossary of notation, which didn't mention . Math professors can be assholes sometimes.

  • Is there an operation that takes and , and returns is more interesting. First off, why is this even a reasonable question? Why should there be such an operation? But note that there is an operation that takes and and returns , namely, multiplication, so it's plausible that the operation that OP wants might also exist.

    But it's easy to see that there is no operation that takes and and returns : just observe that although , the putative operation (call it ) should take and yield , but it should also take and yield . So the operation is not well-defined. And you can take this even further: can be written as , so should also take and yield .

    They key point is that the representation of a number, or even an integer, in the form is not unique. (Jargon: "exponentiation is not injective".) You can raise , but having done so you cannot look at the result and know what and were, which is what needs to do.

    But if can't do it, how can multiplication do it when it multiplies and and gets ? Does it somehow know what is? No, it turns out that it doesn't need in this case. There is something magical going on there, ultimately related to the fact that if some quantity is increasing by a factor of every units of time, then there is some for which it is exactly doubling every units of time. Because of this there is a marvelous group homomophism $$\log : \langle \Bbb R^+, \times\rangle \to \langle \Bbb R ,+\rangle$$ which can change multiplication into addition without knowing what the base numbers are.

    In that thread I had a brief argument with someone who thinks that operators apply to expressions rather than to numbers. Well, you can say this, but it makes the question trivial: you can certainly have an "operator" that takes expressions and and yields the expression . You just can't expect to apply it to numbers, such as and , because those numbers are not expressions in the form . I remembered the argument going on longer than it did; I originally ended this paragraph with a lament that I wasted more than two comments on this guy, but looking at the record, it seems that I didn't. Good work, Mr. Dominus.

  • how 1/0.5 is equal to 2? wants a simple explanation. Very likely OP is a primary school student. The question reminds me of a similar question, asking why the long division algorithm is the way it is. Each of these is a failure of education to explain what division is actually doing. The long division answer is that long division is an optimization for repeated subtraction; to divide you want to know how many shares of three cookies each you can get from cookies. Long division is simply a notation for keeping track of removing shares, leaving cookies, then further shares, leaving none.

    In this question there was a similar answer. is because if you have one cookie, and want to give each kid a share of cookies, you can get out two shares. Simple enough.

    I like division examples that involve giving cookies to kids, because cookies are easy to focus on, and because the motivation for equal shares is intuitively understood by everyone who has kids, or who has been one.

    There is a general pedagogical principle that an ounce of examples are worth a pound of theory. My answer here is a good example of that. When you explain the theory, you're telling the student how to understand it. When you give an example, though, if it's the right example, the student can't help but understand it, and when they do they'll understand it in their own way, which is better than if you told them how.

  • How to read a cycle graph? is interesting because hapless OP is asking for an explanation of a particularly strange diagram from Wikipedia. I'm familiar with the eccentric Wikipedian who drew this, and I was glad that I was around to say "The other stuff in this diagram is nonstandard stuff that the somewhat eccentric author made up. Don't worry if it's not clear; this author is notorious for that."

  • In Expected number of die tosses to get something less than 5, OP calculated as follows: The first die roll is a winner of the time. The second roll is the first winner of the time. The third roll is the first winner of the time. Summing the series we eventually obtain the answer, . The accepted answer does it this way also.

    But there's a much easier way to solve this problem. What we really want to know is: how many rolls before we expect to have seen one good one? And the answer is: the expected number of winners per die roll is , expectations are additive, so the expected number of winners per die rolls is , and so we need rolls to expect one winner. Problem solved!

    I first discovered this when I was around fifteen, and wrote about it here a few years ago.

    As I've mentioned before, this is one of the best things about mathematics: not that it works, but that you can do it by whatever method that occurs to you and you get the same answer. This is where mathematics pedagogy goes wrong most often: it proscribes that you must get the answer by method X, rather than that you must get the answer by hook or by crook. If the student uses method Y, and it works (and if it is correct) that should be worth full credit.

    Bad instructors always say "Well, we need to test to see if the student knows method X." No, we should be testing to see if the student can solve problem P. If we are testing for method X, that is a failure of the test or of the curriculum. Because if method X is useful, it is useful because for some problems, it is the only method that works. It is the instructor's job to find one of these problems and put it on the test. If there is no such problem, then X is useless and it is the instructor's job to omit it from the curriculum. If Y always works, but X is faster, it is the instructor's job to explain this, and then to assign a problem for the test where Y would take more time than is available.

    I see now I wrote the same thing in 2006. It bears repeating. I also said it again a couple of years ago on math.se itself in reply to a similar comment by Brian Scott:

    If the goal is to teach students how to write proofs by induction, the instructor should damned well come up with problems for which induction is the best approach. And if even then a student comes up with a different approach, the instructor should be pleased. ... The directions should not begin [with "prove by induction"]. I consider it a failure on the part of the instructor if he or she has to specify a technique in order to give students practice in applying it.

by Mark Dominus (mjd@plover.com) at July 19, 2015 12:28 AM

July 17, 2015

Danny Gratzer

Coinduction in JonPRL for Low Low Prices

Posted on July 17, 2015
Tags: jonprl

So as a follow up to my prior tutorial on JonPRL I wanted to demonstrate a nice example of JonPRL being used to prove something

  1. Interesting
  2. Unreasonably difficult in Agda or the like

    I think I’m asking to be shown up when I say stuff like this…

I would like to implement the conatural numbers in JonPRL but without a notion of general coinductive or even inductive types. Just the natural numbers. The fun bit is that we’re basically going to lift the definition of a coinductively defined set straight out of set theory into JonPRL!

Math Stuff

First, let’s go through some math. How can we formalize the notion of an coinductively defined type as we’re used to in programming languages? Recall that something is coinductively if it contains all terms so that we can eliminate the term according to the elimination form for our type. For example, Martin-Lof has proposed we view functions (Π-types) as coinductively defined. That is,

x : A ⊢ f(x) : B(x)
————————————————————
 f : Π x : A. B(x)

In particular, there’s no assertion that f needs to be a lambda, just that f(x) is defined and belongs to the right type. This view of “if we can use it, it’s in the type” applies to more than just functions. Let’s suppose we have a type with the following elimination form

L : List  M : A  x : Nat, y : List : A
——————————————————————————————————————
      case(L; M; x.y.N) : A

This is more familiar to Haskellers as

case L of
  [] -> M
  x :: y -> N

Now if we look at the coinductively defined type built from this elimination rule we have not finite lists, but streams! There’s nothing in this elimination rule that specifies that the list be finite in length for it to terminate. All we need to be able to do is evaluate the term to either a :: of a Nat and a List or nil. This means that

fix x. cons(0; x) : List

Let’s now try to formalize this by describing what it means to build a coinductively type up as a set of terms. In particular the types we’re interested in here are algebraic ones, constructed from sums and products.

Now unfortunately I’m going to be a little handwavy. I’m going to act is if we’ve worked out a careful set theoretic semantics for this programming language (like the one that exists for MLTT). This means that All the equations you see here are across sets and that these sets contain programs so that ⊢ e : τ means that e ∈ τ where τ on the right is a set.

Well we start with some equation of the form

Φ = 1 + Φ

This particular equation a is actually how we would go about defining the natural numbers. If I write it in a more Haskellish notation we’d have

data Φ = Zero | Succ Φ

Next, we transform this into a function. This step is a deliberate move so we can start applying the myriad tools we know of for handling this equation.

Φ(X) = 1 + X

We now want to find some X so that Φ(X) = X. If we can do this, then I claim that X is a solution to the equation given above since

X = Φ(X)
X = 1 + X

precisely mirrors the equation we had above. Such an X is called a “fixed point” of the function Φ. However, there’s a catch: there may well be more than one fixed point of a function! Which one do we choose? The key is that we want the coinductively defined version. Coinduction means that we should always be able to examine a term in our type and its outermost form should be 1 + ???. Okay, let’s optimistically start by saying that X is (the collection of all terms).

Ah okay, this isn’t right. This works only so long as we don’t make any observations about a term we claim is in this type. The minute we pattern match, we might have found we claimed a function was in our type! I have not yet managed to pay my rent by saying “OK, here’s the check… but don’t try to use it and it’s rent”. So perhaps we should try something else. Okay, so let’s not say , let’s say

X = ⊤ ⋂ Φ(⊤)

Now, if t ∈ X, we know that t ∈ 1 + ???. This means that if we run e ∈ X, we’ll get the correct outermost form. However, this code is still potentially broken:

    case e of
      Inl _ -> ...
      Inr x -> case e of
                 Inl _ -> ...
                 Inr _ -> ...

This starts off as being well typed, but as we evaluate, it may actually become ill typed. If we claimed that this was a fixed point to our language, our language would be type-unsafe. This is an unappealing quality in a type theory.

Okay, so that didn’t work. What if we fixed this code by doing

X = ⊤ ⋂ Φ(⊤) ⋂ Φ(Φ(⊤))

Now this fixes the above code, but can you imagine a snippet of code where this still gets stuck? So each time we intersect X with Φ(X) we get a new type which behaves like the real fixed point so long as we only observe n + 1 times where X behaves like the fixed point for n observations. Well, we can only make finitely many observations so let’s just iterate such an intersection

X = ⋂ₙ Φⁿ(⊤)

So if e ∈ X, then no matter how many times we pattern match and examine the recursive component of e we know that it’s still in ⋂ₙ Φⁿ(⊤) and therefore still in X! In fact, it’s easy to prove that this is the case with two lemmas

  1. If X ⊆ Y then Φ(X) ⊆ Φ(Y)
  2. If I have a collection S of sets, then ⋂ Φ(S) = Φ(⋂ S) where we define Φ on a collection of sets by applying Φ to each component.

These two properties state the monotonicity and cocontinuity of Φ. In fact, cocontinuity should imply monotonicity (can you see how?). We then may show that

Φ(⋂ₙ Φⁿ(⊤)) = ⋂ₙ Φ(Φⁿ(⊤))
             = ⊤ ⋂ (⋂ₙ Φ(Φⁿ(⊤)))
             = ⋂ₙ Φⁿ(⊤)

As desired.

The Code

Now that we have some idea of how to formalize coinduction, can we port this to JonPRL? Well, we have natural numbers and we can take the intersection of types… Seems like a start. Looking at that example, we first need to figure out what corresponds to. It should include all programs, which sounds like the type base in JonPRL. However, it also should be the case that x = y ∈ ⊤ for all x and y. For that we need an interesting trick:

    Operator top : ().
    [top] =def= [isect(void; _.void)].

In prettier notation,

top ≙ ⋂ x : void. void

Now x ∈ top if x ∈ void for all _ ∈ void. Hey wait a minute… No such _ exists so the if is always satisfied vacuously. Ok, that’s good. Now x = y ∈ top if for all _ ∈ void, x = y ∈ void. Since no such _ exists again, all things are in fact equal in void. We can even prove this within JonPRL

    Theorem top-is-top :
      [isect(base; x.
       isect(base; y.
       =(x; y; top)))] {
      unfold <top>; auto
    }.

This proof is really just:

  1. Unfold all the definitions.
  2. Hey! There’s a x : void in my context! Tell me more about that.

Now the fact that x ∈ top is a trivial corollary since our theorem tells us that x = x ∈ top and the former is just sugar for the latter. With this defined, we can now write down a general operator for coinduction!

    Operator corec : (1).
    [corec(F)] =def= [isect(nat; n. natrec(n; top; _.x. so_apply(F;x)))].

To unpack this, corec takes one argument which binds one variable. We then intersect the type natrec(n; top; _.x.so_apply(F;x)) for all n ∈ nat. That natrec construct is really saying Fⁿ(⊤), it’s just a little obscured. Especially since we have to use so_apply, a sort of “meta-application” which lets us apply a term binding a variable to another term. This should look familiar, it’s just how we defined fixed point of a Φ!

For a fun demo, let’s define an F so that cofix(F) will give us the conatural numbers. I know that the natural numbers come from the least fixed point of X ↦ 1 + X (because I said so above, so it must be so) so let’s define that.

    Operator conatF : (0).
    [conatF(X)] =def= [+(unit; X)].

This is just that X ↦ 1 + X I wrote above in JonPRL land instead of math notation. Next we need to actually define conatural numbers using corec.

    Operator conat : ().
    [conat] =def= [corec(R. conatF(R))].

Now I’ve defined this, but that’s no fun unless we can actual build some terms so that member(X; conat). Specifically I want to prove two things to start

  1. member(czero; conat)
  2. fun(member(M; conat); _.member(csucc(M); conat))

This states that conat is closed under some zero and successor operations. Now what should those operations be? Remember what I said before, that we had this correspondence?

X    ↦   1   +   X
Nat     Zero   Suc X

Now remember that conat is isect(nat; n....) and when constructing a member of isect we’re not allowed to mention that n in it (as opposed to fun where we do exactly that). So that means czero has to be a member of top and sum(unit; ...). The top bit is easy, everything is in top! That diagram above suggests inl of something in unit

    Operator czero : ().
    [czero] =def= [inl(<>)].

So now we want to prove that this in fact in conat.

    Theorem zero-wf : [member(czero; conat)] {

    }.

Okay loading this into JonPRL gives

⊢ czero ∈ conat

From there we start by unfolding all the definitions

    {
       unfold <czero conat conatF corec top>
    }

This gives us back the desugared goal

⊢ inl(<>) ∈ ⋂n ∈ nat. natrec(n; top; _.x.+(unit; x))

Next let’s apply all the obvious introductions so that we’re in a position to try to prove things

    unfold <czero conat conatF corec top>; auto

This gives us back

1. [n] : nat
⊢ inl(<>) = inl(<>) ∈ natrec(n; top; _.x.+(unit; x))

Now we’re stuck. We want to show inl is in something, but we’re never going to be able to do that until we can reduce that natrec(n; top; _.x.+(unit; x)) to a canonical form. Since it’s stuck on n, let’s induct on that n. After that, let’s immediately reduce.

    {
      unfold <czero conat conatF corec top>; auto; elim #1; reduce
    }

Now we have to cases, the base and inductive case.

1. [n] : nat
⊢ inl(<>) = inl(<>) ∈ top


1. [n] : nat
2. n' : nat
3. ih : inl(<>) = inl(<>) ∈ natrec(n'; top; _.x.+(unit; x))
⊢ inl(<>) = inl(<>) ∈ +(unit; natrec(n'; top; _.x.+(unit; x)))

Now that we have canonical terms on the right of the m, let’s let auto handle the rest.

    Theorem zero-wf : [member(czero; conat)] {
      unfold <czero conat conatF corec top>; auto; elim #1; reduce; auto
    }.

So now we have proven that czero is in the correct type. Let’s figure out csucc? Going by our noses, inl corresponded to czero and our diagram says that inr should correspond to csucc. This gives us

    Operator csucc : (0).
    [csucc(M)] =def= [inr(M)].

Now let’s try to prove the corresponding theorem for csucc

    Theorem succ-wf : [isect(conat; x. member(csucc(x); conat))] {
    }.

Now we’re going to start off this proof like we did with our last one. Unfold everything, apply the introduction rules, and induct on n.

    {
      unfold <csucc conat conatF corec top>; auto; elim #2; reduce
    }

Like before, we now have two subgoals:

1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
⊢ inr(x) = inr(x) ∈ ⋂_ ∈ void. void


1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
3. n' : nat
4. ih : inr(x) = inr(x) ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ inr(x) = inr(x) ∈ +(unit; natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x)))

The first one looks pretty easy, that’s just foo ∈ top, I think auto should handle that.

    {
      unfold <csucc conat conatF corec top>; auto; elim #2; reduce;
      auto
    }

This just leaves one goal to prove

1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
3. n' : nat
4. ih : inr(x) = inr(x) ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ x = x ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))

Now, as it turns out, this is nice and easy: look at what our first assumption says! Since x ∈ isect(nat; n.Foo) and our goal is to show that x ∈ Foo(n') this should be as easy as another call to elim.

    {
      unfold <csucc conat conatF corec top>; auto; elim #2; reduce;
      auto; elim #1 [n']; auto
    }

Note that the [n'] bit there lets us supply the term we wish to substitute for n while eliminating. This leaves us here:

1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
3. n' : nat
4. ih : inr(x) = inr(x) ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
5. y : natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
6. z : y = x ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ x = x ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))

Now a small hiccup: we know that y = x is in the right type. so x = x in the right type. But how do we prove this? The answer is to substitute all occurrences of x for y. This is written

    {
      unfold <csucc conat conatF corec top>; auto; elim #2; reduce;
      auto; elim #1 [n']; auto;
      hyp-subst ← #6 [h.=(h; h; natrec(n'; isect(void; _.void); _.x.+(unit;x)))];
    }

There are three arguments here, a direction to substitute, an index telling us which hypothesis to use as the equality to substitute with and finally, a term [h. ...]. The idea with this term is that each occurrence of h tells us where we want to substitute. In our case we used h in two places: both where we use x, and the direction says to replace the right hand side of the equality with the left side of the equality.

Actually running this gives

1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
3. n' : nat
4. ih : inr(x) = inr(x) ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
5. y : natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
6. z : y = x ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ y = y ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))


1. [x] : ⋂n ∈ nat. natrec(n; ⋂_ ∈ void. void; _.x.+(unit; x))
2. [n] : nat
3. n' : nat
4. ih : inr(x) = inr(x) ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
5. y : natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
6. z : y = x ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
7. h : natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ h = h ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x)) ∈ U{i}

The first goal is the result of our substitution and it’s trivial; auto will handle this now. The second goal is a little strange. It basically says that the result of our substitution is still a well-formed type. JonPRL’s thought process is something like this

You said you were substituting for things of this type here. However, I know that just because x : A doesn’t mean we’re using it in all those spots as if it has type A. What if you substitute things equal in top (always equal) for when they’re being used as functions! This would let us prove that zero ∈ Π(...) or something silly. Convince me that when we fill in those holes with something of the type you mentioned, the goal is still a type (in a universe).

However, these well-formedness goals usually go away with auto. This completes our theorem in fact.

    Theorem succ-wf : [isect(conat; x. member(csucc(x); conat))] {
      unfold <csucc conat conatF corec top>; auto; elim #2; reduce;
      auto; elim #1 [n']; auto;
      hyp-subst ← #6 [h.=(h; h; natrec(n'; isect(void; _.void); _.x.+(unit;x)))];
      auto
    }.

Okay so we now have something kind of number-ish, with zero and successor. But in order to demonstrate that this is the conatural numbers there’s one big piece missing.

The Clincher

The thing that distinguishes the conatural numbers from the inductive variety is the fact that we include infinite terms. In particular, I want to show that Ω (infinitely many csuccs) belongs in our type.

In order to say Ω in JonPRL we need recursion. Specifically, we want to write

    [omega] =def= [csucc(omega)].

But this doesn’t work! Instead, we’ll define the Y combinator and say

    Operator omega : ().
    [omega] =def= [Y(x.csucc(x))].

So what should this Y be? Well the standard definition of Y is

Y(F) = (λ x. F (x x)) (λ x. F (x x))

Excitingly, we can just say that in JonPRL; remember that we have a full untyped computation system after all!

    Operator Y : (1).
    [Y(f)] =def= [ap(lam(x.so_apply(f;ap(x;x)));lam(x.so_apply(f;ap(x;x))))].

This is more or less a direct translation, we occasionally use so_apply for the reasons I explained above. As a fun thing, try to prove that this is a fixed point, eg that

    isect(U{i}; A. isect(fun(A; _.A); f . ceq(Y(f); ap(f; Y(f)))))

The complete proof is in the JonPRL repo under example/computational-equality.jonprl. Anyways, we now want to prove

    Theorem omega-wf : [member(omega; conat)] {

    }.

Let’s start with the same prelude

    {
      *{unfold <csucc conat conatF corec top omega Y>}; auto; elim #1;
    }

Two goals just like before

1. [n] : nat
⊢ (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(zero; ⋂_ ∈ void. void; _.x.+(unit; x))


1. [n] : nat
2. n' : nat
3. ih : (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(succ(n'); ⋂_ ∈ void. void; _.x.+(unit; x))

The goals start to get fun now. I’ve also carefully avoided using reduce ike we did before. The reason is simple, if we reduce in the second goal, our ih will reduce as well and we’ll end up completely stuck in a few steps (try it and see). So instead we’re going to finesse it a bit.

First let’s take care of that first goal. We can tell JonPRL to apply some tactics to just the first goal with the focus tactic

    {
      *{unfold <csucc conat conatF corec top omega Y>}; auto; elim #1;
      focus 0 #{reduce 1; auto};
    }

Here reduce 1 says “reduce by only one step” since really omega will diverge if we just let it run. This takes care of the first goal leaving just

1. [n] : nat
2. n' : nat
3. ih : (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(succ(n'); ⋂_ ∈ void. void; _.x.+(unit; x))

Here’s the proof sketch for what’s left

  1. Reduce the goal by one step but carefully avoid touching the ih
  2. Step everything by one
  3. The result follows by intro and assumption

You can stop here or you can see how we actually do this. It’s somewhat tricky. The basic complication is that there’s no built-in tactic for 1. Instead we use a new type called ceq which is “computational equality”. It ranges between two terms, no types involved here. It’s designed to work thusly if ceq(a; b), either

  1. a and b run to weak-head normal form (canonical verifications) with the same outermost form, and all the inner operands are ceq
  2. a and b both diverge

So if ceq(a; b) then a and b “run the same”. What’s a really cool upshot of this is that if ceq(a; b) then if a = a ∈ A and b = b ∈ A then a = b ∈ A! ceq is the strictest equality in our system and we can rewrite with it absolutely everywhere without regards to types. Proving this requires showing the above definition forms a congruence (two things are related if their subcomponents are related).

This was a big deal because until Doug Howe came up with this proof NuPRL/CTT was awash with rules trying to specify this idea chunk by chunk and showing those rules were valid wasn’t trivial. Actually, you should read that paper: it’s 6 pages and the proof concept comes up a lot.

So, in order to do 1. we’re going to say “the goal and the goal if we step it twice are computationally equal” and then use this fact to substitute for the stepped version. The tactic to use here is called csubst. It takes two arguments

  1. The ceq we’re asserting
  2. Another h. term to guide the rewrite
    {
      *{unfold <csucc conat conatF corec top omega Y>}; auto; elim #1;
      focus 0 #{reduce 1; auto};
      csubst [ceq(ap(lam(x.inr(ap(x;x))); lam(x.inr(ap(x;x))));
                  inr(ap(lam(x.inr(ap(x;x))); lam(x.inr(ap(x;x))))))]
         [h.=(h;h; natrec(succ(n'); isect(void; _. void); _.x.+(unit; x)))];
    }

This leaves us with two goals

1. [n] : nat
2. n' : nat
3. ih : (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ ceq((λx. inr(x[x]))[λx. inr(x[x])]; inr((λx. inr(x[x]))[λx. inr(x[x])]))


1. [n] : nat
2. n' : nat
3. ih : (λx. inr(x[x]))[λx. inr(x[x])] = (λx. inr(x[x]))[λx. inr(x[x])] ∈ natrec(n'; ⋂_ ∈ void. void; _.x.+(unit; x))
⊢ inr((λx. inr(x[x]))[λx. inr(x[x])]) = inr((λx. inr(x[x]))[λx. inr(x[x])]) ∈ natrec(succ(n'); ⋂_ ∈ void. void; _.x.+(unit; x))

Now we have two goals. The first is that ceq proof obligation. The second is our goal post-substitution. The first one can easily be dispatched by step. step let’s us prove ceq by saying

  1. ceq(a; b) holds if
  2. a steps to a' in one step
  3. ceq(a'; b)

This will leave us with ceq(X; X) which auto can handle. The second term is.. massive. But also simple. We just need to step it once and we suddenly have inr(X) = inr(X) ∈ sum(_; A) where X = X ∈ A is our assumption! So that can also be handled by auto as well. That means we need to run step on the first goal, reduce 1 on the second, and auto on both.

    Theorem omega-wf : [member(omega; conat)] {
      unfolds; unfold <omega Y>; auto; elim #1;
      focus 0 #{reduce 1; auto};
      csubst [ceq(ap(lam(x.inr(ap(x;x))); lam(x.inr(ap(x;x))));
                  inr(ap(lam(x.inr(ap(x;x))); lam(x.inr(ap(x;x))))))]
             [h.=(h;h; natrec(succ(n'); isect(void; _. void); _.x.+(unit; x)))];
      [step, reduce 1]; auto
    }.

And we’ve just proved that omega ∈ conat, a term that is certainly the canonical (heh) example of coinduction in my mind.

Wrap Up

Whew, I actually meant for this to be a short blog post but that didn’t work out so well. Hopefully this illustrated a cool trick in computer science (intersect your way to coinduction) and in JonPRL.

Funnily enough before this was written no one had actually realized you could do coinduction in JonPRL. I’m still somewhat taken with the fact that a very minimal proof assistant like JonPRL is powerful enough to let you do this by giving you such general purpose tools as family intersection and a full computation system to work with. Okay that’s enough marketing from me.

Cheers.

Huge thanks to Jon Sterling for the idea on how to write this code and then touching up the results

<script type="text/javascript"> var disqus_shortname = 'codeco'; (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus

July 17, 2015 12:00 AM

July 16, 2015

Dimitri Sabadie

Don’t use Default

Don’t use Default

Background knowledge: typeclasses and laws

In Haskell, we have a lot of typeclasses. Those are very handy and – in general – come with laws. Laws are very important and give hints on how we are supposed to use a typeclass.

For instance, the Semigroup typeclass exposes an operator ((<>)) and has an associativity law. If a, b and c have the same type T, if we know that T is a Semigroup, we have the following law:

a <> b <> c = (a <> b) <> c = a <> (b <> c)

If T is a Monoid, which is a Semigroup with an identity (called mempty), we have a law for monoids:

a <> mempty = mempty <> a = a

Those laws can – have – to be used in our code base to take advantage over the structures, optimize or avoid boilerplate.

The Default typeclass

In some situations, we want a way to express default values. That’s especially true in OO languages, like in the following C++ function signature:

void foo(float i = 1);

In Haskell, we cannot do that, because we have to pass all arguments to a function. The following doesn’t exist:

foo :: Float -> IO ()
foo (i = 1) = -- […]

And there’s more. Even in C++, how do you handle the case when you have several arguments and want only the first one to be defaulted? You cannot.

So, so… Some Haskellers decided to solve that problem with a typeclass. After all, we can define the following typeclass:

class Default a where
def :: a

We can then implement Default and have a default value for a given type.

instance Default Radians where
def = Radians $ 2*pi

instance Default Fullscreen where
def = Fullscreen False

However, there is an issue with that. You cannot use Default without creating newtypes to overload them. Why? Well, consider the following Default instance:

instance Default Float where
def = -- what should we put here?

Remember that, in Haskell, an instance is defined only once and is automatically imported when you import the module holding it. That means you cannot have the following:

-- in a module A
instance Default Float where
def = 0

-- in a module B
instance Default Float where
def = 1

-- in a module C
import A
import B

-- What instances should we use?

Hey, that’s easy. We just have to keep the modules apart, and import the one we want to use!

Yeah, well. No. No.

Orphan instances are wrong. You should read this for further explanations.

That’s why we have to use newtypes everywhere. And that’s boring. Writing code should always have a goal. When we write as much boilerplate code as real code, we can start thinking there’s something wrong. Worse, if we have more boilerplate than real code, well, something is terribly wrong. In our case, we’re introducing a lot of newtypes for only being able to use def at a few spots. Is that even worth it? Of course not.

Default is evil

The Default typeclass is evil. It’s shipped with default instances, like one for [a], which defaults to the empty list – []. It might be clear for you but why would I want to default to the empty list? Why not to [0]? Or a more complex list? I really doubt someone ever uses def :: [a].

Another reason why Default is wrong? There’s absolutely no law. You just have a default value, and that’s all.

bar :: (Default a) => a -> Maybe String

Can you say what the default is for? Of course you cannot. Because there’s no law. The instance has no real meaning. A default value makes sense only for the computation using it. For instance, the empty list makes sense if we glue it to the list concatenation.

We already have a lot of defaults

In base, there’re already several ways to express defaulted values.

The Monoid’s mempty is a way to express a default value regarding its binary operation ((<>)).

The Alternative’s empty provides a similar default, but for first-class types.

The MonadZero’s mzero provides a different default, used to absorb everything. That’s a law of MonadZero:

mzero >>= f = mzero
a >> mzero = mzero

Those defaults are interesting because we can reason about. If I see mzero in a monadic code, I know that whatever is following will be discarded.

Conclusion

So please. Stop using Default. It doesn’t bring any sense to your codebase. It actually removes some! If you want to provide functions with defaulted arguments, consider partially applied functions.

data-default is a very famous package – look at the downloads! You can now have some hindsight about it before downloading it and ruining your design. ;)

Happy hacking. :)

by Dimitri Sabadie (noreply@blogger.com) at July 16, 2015 01:57 PM

Tom Schrijvers

MonadPlus and Alternative are just near-semirings in the category of endofunctors, what's the problem?

I have presented a new paper at PPDP 2015
From monoids to near-semirings: the essence of MonadPlus and Alternative
Exequiel Rivas, Mauro Jaskelioff and Tom Schrijvers
It is well-known that monads are monoids in the category of endofunctors, and in fact so are applicative functors. Unfortunately, the benefits of this unified view are lostwhen the additional non-determinism structure of MonadPlus or Alternative is required.  
This article recovers the essence of these two type classes by extending monoids to near-semirings with both additive and multiplicative structure. This unified algebraic view enables us to generically define the free construction as well as a novel double Cayley representation that optimises both left-nested sums and left-nested products.
The following slogan summarises the paper:
MonadPlus and Alternative are just near-semirings in the category of endofunctors, what's the problem?

by Tom Schrijvers (noreply@blogger.com) at July 16, 2015 08:51 AM

July 15, 2015

Bryn Keller

Higher Order Type Theory Resources

Recently there’s been an outpouring of useful resources folks have found for learning Homotopy Type Theory (aka HoTT). These have come mainly from the HoTT Cafe Google Group.

The main resource is of course, the book, but these videos and other resources seem useful enough that I want a consolidated list of them for myself. So I thought maybe you might, too.

Group threads that provided these links:

Note that I’m likely to update this page in the future with other resources as I find them, and those links may or may not come from the Groups threads just mentioned.

Useful resources, in no particular order:

Related:

by Bryn Keller at July 15, 2015 12:00 AM

Christopher Done

Use the REPL, Luke

There was an online discussion about iteration times in Haskell and whether and why they are slow. For me, it’s not slow. I do all my Haskell development using a REPL. Here are some tips I wrote up in that discussion.

Prepare for GHCi use

The first thing you want to do before writing anything for your project is make sure you can load your code in the REPL; GHCi. Sometimes you have special configuration options or whatnot (cabal repl and stack ghci make this much easier than in the past). The sooner you start the better. It can be a PITA to load some projects that expect to just be a “start, run and die” process, they often launch threads without any clean-up procedure; in this way the REPL makes you think about cleaner architecture.

Make sure it scales

Learn how to make GHCi fast for your project so that you don’t hit a wall as your project scales. Loading code with byte-code is much faster than object code, but loading with object code has a cache so that in a 100 module project if you only need to reload one, it’ll just load one. Make sure this is happening for you, when you need it. Dabble with the settings.

Write small, parametrized functions

Code that is good for unit tests is code that is good for the REPL. Write small functions that take state as arguments (dependency injection) rather than loading their own state, then they can be ran in the REPL and used in a test suite easily. Regard functions that you can’t just call directly with suspicion.

Test work-in-progress implementations in the REPL

While writing, test your function in the REPL with typical arguments it will expect, rather than implementing a function and then immediately using it in the place you want to ultimately use it. You can skip this for trivial “glue” functions, but it’s helpful for non-trivial functions.

Setup/teardown helpers

Write helpful setup/teardown code for your tests and REPL code. For example, if you have a function that needs a database and application configuration to do anything, write a function that automatically and conveniently gets you a basic development config and database connection for running some action.

Make data inspectable

Make sure to include Show instances for your data types, so that you can inspect them in the REPL. Treat Show as your development instance, it’s for you, don’t use it for “real” serialization or for “user-friendly” messages. Develop a distaste for data structures that are hard to inspect.

Figure out the fastest iteration for you

Use techniques like :reload to help you out. For example, if I’m working on hindent, then I will test a style with HIndent.test chrisDone "x = 1", for example, in the REPL, and I’ll see the output pretty printed as Haskell in my Emacs REPL. But I work on module HIndent.Style.ChrisDone. So I first :load HIndent and then for future work I use :reload to reload my .ChrisDone changes and give me the HIndent environment again.

Configuration

Make sure you know about the .ghci file which you can put in your ~/ and also in the project directory where GHCi is run from. You can use :set to set regular GHC options including packages (-package foo) and extensions (-XFoo), and any special include directories (-ifoo).

More advanced tricks

Consider tricks like live reloading; if you can support it. I wrote an IRC server and I can run it in the REPL, reload the code, and update the handler function without losing any state. If you use foreign-store you can make things available, like the program’s state, in an IORef or MVar.

This trick is a trick, so don’t use it in production. But it’s about as close as we can get to Lisp-style image development.

In summary

Haskell’s lucky to have a small REPL culture, but you have to work with a Lisp or Smalltalk to really know what’s possible when you fully “buy in”. Many Haskellers come from C++ and “stop program, edit file, re-run compiler, re-run whole program” cycles and don’t have much awareness or interest in it. If you are such a person, the above probably won’t come naturally, but try it out.

July 15, 2015 12:00 AM

July 13, 2015

Brent Yorgey

The Species of Bracelets

Summary: The species package now has support for bracelets, i.e. equivalence classes of lists up to rotation and reversal. I show some examples of their use and then explain the (very interesting!) mathematics behind their implementation.


I recently released a new version of my species package which adds support for the species of bracelets. A bracelet is a (nonempty) sequence of items which is considered equivalent up to rotation and reversal. For example, the two structures illustrated below are considered equivalent as bracelets, since you can transform one into the other by a rotation and a flip:

In other words, a bracelet has the same symmetry as a regular polygon—that is, its symmetry group is the dihedral group D_{2n}. (Actually, this is only true for n \geq 3—I’ll say more about this later.)

Bracelets came up for me recently in relation to a fun side project (more on that soon), and I am told they also show up in applications in biology and chemistry (for example, bracelet symmetry shows up in molecules with cycles, which are common in organic chemistry). There was no way to derive the species of bracelets from what was already in the library, so I added them as a new primitive.

Let’s see some examples (later I discuss how they work). First, we set some options and imports.

ghci> :set -XNoImplicitPrelude
ghci> :m +NumericPrelude
ghci> :m +Math.Combinatorics.Species

Unlabelled bracelets, by themselves, are completely uninteresting: there is only a single unlabelled bracelet shape of any positive size. (Unlabelled species built using bracelets can be interesting, however; we’ll see an example in just a bit). We can ask the library to tell us how many distinct size-n unlabelled bracelets there are for n \in \{0, \dots, 9\}:

ghci> take 10 $ unlabelled bracelets
  [0,1,1,1,1,1,1,1,1,1]

Labelled bracelets are a bit more interesting. For n \geq 3 there are (n-1)!/2 labelled bracelets of size n: there are (n-1)! cycles of size n (there are n! lists, which counts each cycle n times, once for each rotation), and counting cycles exactly double counts bracelets, since each bracelet can be flipped in one of two ways. For example, there are (5-1)!/2 = 24/2 = 12 labelled bracelets of size 5.

ghci> take 10 $ labelled bracelets
  [0,1,1,1,3,12,60,360,2520,20160]

In addition to counting these, we can exhaustively generate them (this is a bit annoying with the current API; I hope to improve it):

ghci> enumerate bracelets [0,1] :: [Bracelet Int]
  [<<0,1>>]

ghci> enumerate bracelets [0..2] :: [Bracelet Int]
  [<<0,1,2>>]

ghci> enumerate bracelets [0..3] :: [Bracelet Int]
  [<<0,1,2,3>>,<<0,1,3,2>>,<<0,2,1,3>>]

And here are all 12 of the size-5 bracelets, where I’ve used a different color to represent each label (see here for the code used to generate them):

As a final example, consider the species B \times E^2, the Cartesian product of bracelets with ordered pairs of sets. That is, given a set of labels, we simultaneously give the labels a bracelet structure and also partition them into two (distinguishable) sets. Considering unlabelled structures of this species—that is, equivalence classes of labelled structures under relabelling—means that we can’t tell the labels apart, other than the fact that we can still tell which are in the first set and which are in the second. So, if we call the first set “purple” and the second “green”, we are counting the number of bracelets made from (otherwise indistinguishable) purple and green beads. Let’s call these binary bracelets. Here’s how many there are of sizes 0 through 14:

ghci> let biBracelets = bracelet >< (set * set)
ghci> take 15 $ unlabelled biBracelets
  [0,2,3,4,6,8,13,18,30,46,78,126,224,380,687]

Let’s use the OEIS to check that we’re on the right track:

ghci> :m +Math.OEIS
ghci> let res = lookupSequence (drop 1 . take 10 $ unlabelled biBracelets)
ghci> fmap description res
  Just "Number of necklaces with n beads of 2 colors, allowing turning over."

Unfortunately the species library can’t currently enumerate unlabelled structures of species involving Cartesian product, though I hope to fix that. But for now we can draw these purple-green bracelets with some custom enumeration code. You can see the numbers 2, 3, 4, 6, 8, 13 show up here, and it’s not too hard to convince yourself that each row contains all possible binary bracelets of a given size.

If you’re just interested in what you can do with bracelets, you can stop reading now. If you’re interested in the mathematical and algorithmic details of how they are implemented, read on!

Exponential generating functions

The exponential generating function (egf) associated to a combinatorial species F is defined by

\displaystyle F(x) = \sum_{n \geq 0} |F[n]| \frac{x^n}{n!}.

That is, the egf is an (infinite) formal power series where the coefficient of x^n/n! is the number of distinct labelled F-structures on n labels. We saw above that for n \geq 3 there are (n-1)!/2 labelled bracelets of size n, and there is one bracelet each of sizes 1 and 2. The egf for bracelets is thus:

\displaystyle B(x) = x + \frac{x^2}{2} + \sum_{n \geq 3} \frac{(n-1)!}{2} \frac{x^n}{n!} = x + \frac{x^2}{2} + \sum_{n \geq 3} \frac{x^n}{2n}.

(Challenge: show this is also equivalent to \frac{1}{2}(x + x^2/2 - \ln(1-x)).) This egf is directly encoded in the species library, and this is what is being used to evaluate labelled bracelets in the example above.

Incidentally, the reason (n-1)!/2 only works for n \geq 3 is in some sense due to the fact that the dihedral groups D_2 = Z_2 and D_4 = K_4 are a bit weird: every dihedral group D_{2n} is a subgroup of the symmetric group \mathcal{S}_n except for D_2 and D_4. The problem is that for n < 3, “flips” actually have no effect, as you can see below:

So, for example, D_4 has 4 elements, corresponding to the identity, a 180 degree rotation, a flip, and a rotation + flip; but the symmetric group \mathcal{S}_2 only has two elements, in this case corresponding to the identity and a 180 degree rotation. The reason (n-1)!/2 doesn’t work, then, is that the division by two is superfluous: for n < 3, counting cycles doesn’t actually overcount bracelets, because every cycle is already a flipped version of itself. So it would also be correct (if rather baroque) to say that for n < 3 there are actually (n-1)! bracelets.

I find this fascinating; it’s almost as if for bigger n the dihedral symmetry has “enough room to breathe” whereas for small n it doesn’t have enough space and gets crushed and folded in on itself, causing weird things to happen. It makes me wonder whether there are other sorts of symmetry with a transition from irregularity to regularity at even bigger n. Probably this is an easy question for a group theorist to answer but I’ve never thought about it before.

Ordinary generating functions

The ordinary generating function (ogf) associated to a species F is defined by

\displaystyle \tilde F(x) = \sum_{n \geq 0} |F[n]/\mathord{\sim}| x^n

where \sim is the equivalence relation on F-structures induced by permuting the labels. That is, the coefficient of x^n is the number of equivalence classes of F-structures on n labels up to relabelling. There is only one unlabelled bracelet of any size n \geq 1, that is, any bracelet of size n can be transformed into any other just by switching labels around. The unique unlabelled bracelet of a given size can be visualized as a bracelet of uniform beads:

though it’s occasionally important to keep in mind the more formal definition as an equivalence class of labelled bracelets. Since there’s just one unlabelled bracelet of each size, the ogf for bracelets is rather boring:

\displaystyle \tilde B(x) = x + x^2 + x^3 + \dots = \frac{x}{x - 1}.

This is encoded in the species library too, and was used to compute unlabelled bracelets above.

egfs, ogfs, and homomorphisms

egfs are quite natural (in fact, species can be seen as a categorification of egfs), and the mapping from species to their associated egf is a homomorphism that preserves many operations such as sum, product, Cartesian product, composition, and derivative. ogfs, however, are not as nice. The mapping from species to ogfs preserves sum and product but does not, in general, preserve other operations like Cartesian product, composition or derivative. In some sense ogfs throw away too much information. Here’s a simple example to illustrate this: although the ogfs for bracelets and cycles are the same, namely, x/(1-x) (there is only one unlabelled bracelet or cycle of each size), the ogfs for binary bracelets and binary cycles are different:

ghci> -- recall biBracelets = bracelet >< (set * set)
ghci> let biCycles = cycles >< (set * set)
ghci> take 15 $ unlabelled biBracelets
  [0,2,3,4,6,8,13,18,30,46,78,126,224,380,687]

ghci> take 15 $ unlabelled biCycles
  [0,2,3,4,6,8,14,20,36,60,108,188,352,632,1182]

(Puzzle: why are these the same up through n=5? Find the unique pair of distinct binary 6-cycles which are equivalent as bracelets.)

Clearly, there is no way to take equal ogfs, apply the same operation to both, and get different results out. So the species library cannot be working directly with ogfs in the example above—something else must be going on. That something else is cycle index series, which generalize both egfs and ogfs, and retain enough information that they once again preserve many of the operations we care about.

Cycle index series

Let \mathcal{S}_n denote the symmetric group of order n, that is, the group of permutations on \{1, \dots, n\} under composition. It is well-known that every permutation \sigma \in \mathcal{S}_n can be uniquely decomposed as a product of disjoint cycles. The cycle type of \sigma is the sequence of natural numbers \sigma_1, \sigma_2, \sigma_3, \dots where \sigma_i is the number of i-cycles in the cycle decomposition of \sigma. For example, the permutation (132)(45)(78)(6) has cycle type 1,2,1,0,0,0,\dots since it has one 1-cycle, two 2-cycles, and one 3-cycle.

For a species F and a permutation \sigma \in \mathcal{S}_n, let \mathrm{fix}\ F[\sigma] denote the number of F-structures that are fixed by the action of \sigma, that is,

\displaystyle \mathrm{fix}\ F[\sigma] = \#\{ f \in F[n] \mid F[\sigma] f = f \}.

The cycle index series of a combinatorial species F is a formal power series in an infinite set of variables x_1, x_2, x_3, \dots defined by

\displaystyle Z_F(x_1, x_2, x_3, \dots) = \sum_{n \geq 0} \frac{1}{n!} \sum_{\sigma \in \mathcal{S}_n} \mathrm{fix}\ F[\sigma] x_1^{\sigma_1} x_2^{\sigma_2} x_3^{\sigma_3} \dots

We also sometimes write x^\sigma as an abbreviation for x_1^{\sigma_1} x_2^{\sigma_2} x_3^{\sigma_3} \dots. As a simple example, consider the species of lists, i.e. linear orderings. For each n, the identity permutation (with cycle type n,0,0,\dots) fixes all n! lists of length n, whereas all other permutations do not fix any lists. Therefore

\displaystyle Z_L(x_1, x_2, x_3, \dots) = \sum_{n \geq 0} \frac{1}{n!} n! x_1^n = \sum_{n \geq 0} x_1^n = \frac{1}{1 - x_1}.

(This is not really that great of an example, though—since lists are regular species, that is, they have no nontrivial symmetry, their cycle index series, egf, and ogf are all essentially the same.)

Cycle index series are linked to both egfs and ogfs by the identities

\displaystyle \begin{array}{rcl}F(x) &=& Z_F(x,0,0,\dots) \\ \tilde F(x) &=& Z_F(x,x^2,x^3, \dots)\end{array}

To show the first, note that setting all x_i to 0 other than x_1 means that the only terms that survive are terms with only x_1 raised to some power. These correspond to permutations with only 1-cycles, that is, identity permutations. Identity permutations fix all F-structures of a given size, so we have

\begin{array}{rcl}  Z_F(x,0,0,\dots) &=& \displaystyle \sum_{n \geq 0} \frac{1}{n!} \mathrm{fix}\ F[\mathit{id}] x^n \\  &=& \displaystyle \sum_{n \geq 0} |F[n]| \frac{x^n}{n!}. \end{array}

To prove the link to ogfs, note first that for any permutation \sigma \in \mathcal{S}_n with cycle type \sigma_1,\sigma_2,\sigma_3,\dots we have \sigma_1 + 2\sigma_2 + 3\sigma_3 + \dots = n. Thus:

\begin{array}{rcl}  Z_F(x,x^2,x^3,\dots) &=& \displaystyle \sum_{n \geq 0} \frac{1}{n!} \sum_{\sigma  \in \mathcal{S}_n} \mathrm{fix}\ F[\sigma]  x^{\sigma_1}x^{2\sigma_2}x^{3\sigma_3}\dots \\  &=& \displaystyle \sum_{n \geq 0} \frac{1}{n!} \sum_{\sigma \in \mathcal{S}_n} \mathrm{fix}\ F[\sigma] x^n \\  &=& \displaystyle \sum_{n \geq 0} |F[n]/\mathord{\sim}| x^n \end{array}

where the final step is an application of Burnside’s Lemma.

The important point is that the mapping from species to cycle index series is again a homomorphism for many of the operations we care about, including Cartesian product and composition. So in order to compute an ogf for some species defined in terms of operations that are not compatible with ogfs, one can start out computing with cycle index series and then project down to an ogf at the end.

Cycle index series for bracelets

Let’s now see how to work out the cycle index series for the species of bracelets. For n=1, the single bracelet is fixed by the only element of \mathcal{S}_1, giving a term of x_1. For n=2, the single bracelet is fixed by both elements of \mathcal{S}_2, one of which has cycle type 2,0,0,\dots and the other 0,1,0,\dots. Bracelets of size n \geq 3, as discussed previously, have the dihedral group D_{2n} as their symmetry group. That is, every one of the (n-1)!/2 size-n bracelets is fixed by the action of each element of D_{2n}, and no bracelets are fixed by the action of any other permutation. Putting this all together, we obtain

\begin{array}{rcl} Z_B(x_1, x_2, x_3, \dots) &=& \displaystyle \sum_{n \geq 0}  \frac{1}{n!} \sum_{\sigma \in \mathcal{S}_n} \mathrm{fix}\ B[\sigma]  x_1^{\sigma_1}x_2^{\sigma_2}x_3^{\sigma_3}\dots \\ &=& \displaystyle x_1 + \frac{1}{2}(x_1^2 + x_2) + \sum_{n \geq 3}  \frac{1}{n!} \sum_{\sigma \in D_{2n}} \frac{(n-1)!}{2} x^\sigma \\ &=& \displaystyle x_1 + \frac{1}{2}(x_1^2 + x_2) + \sum_{n \geq 3}  \frac{1}{2n} \sum_{\sigma \in D_{2n}} x^\sigma. \end{array}

Our remaining task is thus to compute \sum_{\sigma \in D_{2n}} x^\sigma, that is, to compute the cycle types of elements of D_{2n} for n \geq 3. I don’t know whether there’s a nice closed form for Z_B, but for our purposes it doesn’t matter: it suffices to come up with a finite algorithm to generate all its terms with their coefficients. A closed form might be important if we want to compute with Z_B symbolically, but if we just want to generate coefficients, an algorithm is good enough.

In general, D_{2n} has n elements corresponding to rotations (including the identity element, which we think of as a rotation by 0 degrees) and n elements corresponding to reflections across some axis. Below I’ve drawn illustrations showing the symmetries of bracelets of size 5 and 6; each symmetry corresponds to an element of D_{2n}.

The lines indicate reflections. You can see that in general there are n lines of reflection. The curved arrows indicate clockwise rotations; taking any number of consecutive arrows from 0 to n-1 gives a distinct rotational symmetry. Let’s label the rotations R_k (for k \in \{0, \dots, n-1\}), where R_k indicates a rotation by k/n of a turn (so R_0 is the identity element). We won’t bother labelling the reflections since it’s not clear how we would choose canonical names for them, and in any case (as we’ll see) we don’t have as much of a need to give them names as we do for the rotations. The only thing we will note is that for even n there are two distinct types of reflections, as illustrated by the dark and light blue lines on the right: the dark blue lines pass through two vertices, and the light blue ones pass through two edges. In the odd case, on the other hand, every line of reflection passes through one vertex and one edge. If you haven’t studied dihedral groups before, you might want to take a minute to convince yourself that this covers all the possible symmetries. It’s clear that a rotation followed by a rotation is again a rotation; what may be less intuitively clear is that a reflection followed by a reflection is a rotation, and that a rotation followed by a reflection is a reflection.

So the name of the game is to consider each group element as a permutation of the labels, and compute the cycle type of the permutation. Let’s tackle the reflections first; we have to separately consider the cases when n is odd and even. We saw above that when n = 2m+1 is odd, each line of reflection passes through exactly one vertex. As a permutation, that means the reflection will fix the label at the vertex it passes through, and swap the labels on other vertices in pairs, as shown in the leftmost diagram below:

So the permutation has cycle type 1,m,0,0,\dots. There is one 1-cycle, and the remaining n-1 = 2m elements are paired off in 2-cycles. There are n of these reflections in total, yielding a term of nx_1x_2^m (where m = \lfloor n/2 \rfloor).

When n = 2m is even, half of the reflections (the light blue ones) have no fixed points, as in the middle diagram above; they put everything in 2-cycles. The other half of the even reflections fix two vertices, with the rest in 2-cycles, as in the rightmost diagram above. In all, this yields terms mx_1^2x_2^{m-1} + mx_2^m.

Now let’s tackle the rotations. One could be forgiven for initially assuming that each rotation will just yield one big n-cycle… a rotation is just cycling the vertices, right? But it is a bit more subtle than that. Let’s look at some examples. In each example below, the green curved arrow indicates a rotation R_k applied to the bracelet. As you can check, the other arrows show the resulting permutation on the labels, that is, each arrow points from one node to the node where it ends up under the action of the rotation.

Do you see the pattern? In the case when k=1 (the first example above), or more generally when n and k are relatively prime (the second example above, with n=5 and k=2), R_k indeed generates a single n-cycle. But when n and k are not relatively prime, it generates multiple cycles. By symmetry the cycles must all be the same size; in general, the rotation R_k generates (n,k) cycles of size n/(n,k) (where (n,k) denotes the greatest common divisor of n and k). So, for example, 2 cycles are generated when n=6 and k=2 or k=4 (the next two examples above). The last example shows n=12 and k=3; we can see that three 4-cycles are generated. Note this even works when k=0: we have (n,0) = n, so we get n cycles of size n/n = 1, i.e. the identity permutation.

So R_k contributes a term x_{n/(n,k)}^{(n,k)}. However, we can say something a bit more concise than this. Note, for example, when n=12, as the contribution of all the R_k we get

x_1^{12} + x_{12} + x_6^2 + x_4^3 + x_3^4 + x_{12} + x_2^6 + x_{12} + x_3^4 + x_4^3 + x_6^2 + x_{12}

but we can collect like terms to get

x_1^{12} + x_2^6 + 2x_3^4 + 2x_4^3 + 2x_6^2 + 4x_{12}

For a given divisor d \mid n, the coefficient of x_{n/d}^d is the number of nonnegative integers less than n whose \gcd with n is equal to d. For example, the coefficient of x_{6}^2 is 2, since there are two values of k for which (n,k) = 12/6 = 2 and hence generate a six-cycle, namely, 2 and 10. So as the contribution of the R_k we could write something like

\displaystyle \sum_{d \mid n} \left( \#\{ 1 \leq k \leq n \mid (k,n) = d \} \right) x_{n/d}^d

but there is a better way. Note that

\displaystyle \#\{ 1 \leq k \leq n \mid (k,n) = d \} = \#\{ 1 \leq j \leq n/d \mid (j,n/d) = 1 \}

since multiplying and dividing by d establishes a bijection between the two sets. For example, we saw that 2 and 10 are the two numbers whose \gcd with 12 is 2; this corresponds to the fact that 2/2 = 1 and 10/2 = 5 are relatively prime to 12/2 = 6.

But counting relatively prime numbers is precisely what Euler’s totient function (usually written \varphi) does. So we can rewrite the coefficient of x_{n/d}^d as

\displaystyle \varphi(n/d) x_{n/d}^d.

Finally, since we are adding up these terms for all divisors d \mid n, we can swap d and n/d (divisors of n always come in pairs whose product is n), and rewrite this as

\displaystyle \varphi(d) x_d^{n/d}.

To sum up, then, we have for each n \geq 3:

  1. When n is odd, n x_1 x_2^{\lfloor n/2 \rfloor}.
  2. When n is even, (n/2) x_1^2 x_2^{n/2 - 1} + (n/2)x_2^{n/2}.
  3. For each d \mid n, we have \varphi(d) x_d^{n/d}.

The only overlap is between (2) and (3): when d = 2 both generate x_2^{n/2} terms. Using Iverson brackets (the notation [P] is equal to 1 if the predicate P is true, and 0 if it is false), we can thus write the sum of the above for a particular n as

\displaystyle [n\text{ odd}](n x_1 x_2^{\lfloor n/2 \rfloor}) + [n\text{ even}]\left(\frac n 2 x_1^2 x_2^{n/2 - 1}\right) + \sum_{d \mid n} \left(\varphi(d) + [d = 2]\frac n 2\right) x_d^{n/d}.

Substituting this for \displaystyle \sum_{\sigma \in D_{2n}} x^\sigma yields a full definition of Z_B. You can see the result encoded in the species library here. Here’s the beginning of the full expanded series:

ghci> :m +Math.Combinatorics.Species.Types
ghci> take 107 $ show (bracelets :: CycleIndex)
  "CI x1 + 1 % 2 x2 + 1 % 2 x1^2 + 1 % 3 x3 + 1 % 2 x1 x2 + 1 % 6 x1^3 + 1 % 4 x4 + 3 % 8 x2^2 + 1 % 4 x1^2 x2"

This, then, is how unlabelled biBracelets (for example) is calculated, where biBracelets = bracelet >< (set * set). The cycle index series for bracelet and set are combined according to the operations on cycle index series corresponding to * and ><, and then the resulting cycle index series is mapped down to an ogf by substituting x^k for each x_k.

Bracelet generation

The final thing to mention is how bracelet generation works. Of course we can’t really generate actual bracelets, but only lists. Since bracelets can be thought of as equivalence classes of lists (under rotation and reversal), the idea is to pick a canonical representative element of each equivalence class, and generate those. A natural candidate is the lexicographically smallest among all rotations and reversals (assuming the labels have an ordering; if they don’t we can pick an ordering arbitrarily). One easy solution would be to generate all possible lists and throw out the redundant ones, but that would be rather inefficient. It is surprisingly tricky to do this efficiently. Fortunately, there is a series of papers by Joe Sawada (Generating bracelets with fixed content; A fast algorithm to generate necklaces with fixed content; Generating bracelets in constant amortized time) describing (and proving correct) some efficient algorithms for generating things like cycles and bracelets. In fact, they are as efficient as possible, theoretically speaking: they do only O(1) work per cycle or bracelet generated. One problem is that the algorithms are very imperative, so they cannot be directly transcribed into Haskell. But I played around with benchmarking various formulations in Haskell and got it as fast as I could. (Interestingly, using STUArray was a lot slower in practice than a simple functional implementation, even though the imperative solution is asymptotically faster in theory—my functional implementation is at least O(\lg n) per bracelet, and quite possibly O(n), though since n is typically quite small it doesn’t really matter very much. Of course it’s also quite possible that there are tricks to make the array version go faster that I don’t know about.) The result is released in the multiset-comb package; you can see the bracelet generation code here.


by Brent at July 13, 2015 07:26 PM

Dominic Steinitz

Conditional Expectation under Change of Measure

Theorem

Let \mathbb{P} and \mathbb{Q} be measures on (\Omega, {\mathcal{F}}) with \mathbb{Q} \ll \mathbb{P}, {\mathcal{G}} \subset {\mathcal{F}} a sub \sigma-algebra and X an integrable random variable (\mathbb{P}\lvert{X}\rvert < \infty) then

\displaystyle   \mathbb{P}(X\vert {\mathcal{G}}) =  \frac  {\mathbb{Q}\bigg(X\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)}  {\mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)}

Proof

\displaystyle   \begin{aligned}  \mathbb{Q}\bigg(\mathbb{I}_A \mathbb{Q}\bigg(X \frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{P}}\bigg\vert {\mathcal{G}}\bigg)\bigg)  &=  \mathbb{Q}\bigg(\mathbb{I}_A X \frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{P}}\bigg) \\  &=  \mathbb{P}\big(\mathbb{I}_A X \big) \\  &=  \mathbb{P}\big(\mathbb{I}_A \mathbb{P}(X \vert {\mathcal{G}})\big) \\  &=  \mathbb{Q}\bigg(\mathbb{I}_A \frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\mathbb{P}(X \vert {\mathcal{G}})\bigg) \\  &=  \mathbb{Q}\bigg(\mathbb{I}_A \mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)\mathbb{P}(X \vert {\mathcal{G}})\bigg) \\  \end{aligned}

Thus

\displaystyle   \mathbb{Q}\bigg(\mathbb{I}_A\mathbb{P}(X\vert {\mathcal{G}}){\mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)}\bigg) =  \mathbb{Q}\bigg(\mathbb{I}_A \mathbb{Q}\bigg(X\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)\bigg)\quad \mathrm{for\,all}\, A \in {\mathcal{G}}

Hence

\displaystyle   \mathbb{P}(X\vert {\mathcal{G}}){\mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)} =  \mathbb{Q}\bigg(X\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)\quad {\mathbb{Q}-\mathrm{a.s.}}

We note that

\displaystyle   A = \bigg\{\omega \,\bigg\vert\, \mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg)\bigg\}

is {\mathcal{G}}-measurable (it is the result of a projection) and that

\displaystyle   0  =  \mathbb{Q}\bigg(\mathbb{I}_A\mathbb{Q}\bigg(  \frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}  \bigg\vert {\mathcal{G}}\bigg)\bigg)  =  \mathbb{Q}\bigg(\mathbb{I}_A  \frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}  \bigg)  =  \mathbb{P}(\mathbb{I}_A)

Hence

\displaystyle   \mathbb{P}(X\vert {\mathcal{G}}) =  \frac  {\mathbb{Q}\bigg(X\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)}  {\mathbb{Q}\bigg(\frac{\mathrm{d}\mathbb{P}}{\mathrm{d}\mathbb{Q}}\bigg\vert {\mathcal{G}}\bigg)}\quad {\mathbb{P}-\mathrm{a.s.}}

as required.


by Dominic Steinitz at July 13, 2015 08:11 AM

July 12, 2015

Daniil Frumin

Darcs 2.10.1 (Mac OSX build)

Darcs 2.10.1 has been released!

Citing the official release notes

> The darcs team is pleased to announce the release of darcs 2.10.1 !
> ..
> 
> # What's new in 2.10.1 (since 2.10.0) #
> 
> - generalized doFastZip for darcsden support
> - support terminfo 0.4, network 2.6, zlib 0.6, quickcheck 2.8 and
> attoparsec 0.13
> - errorDoc now prints a stack trace (if profiling was enabled) (Ben Franksen)
> - beautified error messages for command line and default files (Ben Franksen)
> - fixed the following bugs:
>       - issue2449: test harness/shelly: need to handle
> mis-encoded/binary data (Ganesh Sittampalam)
>       - issue2423: diff only respecting --diff-command when a diff.exe
> is present (Alain91)
>       - issue2447: get contents of deleted file (Ben Franksen)
>       - issue2307: add information about 'darcs help manpage' and
> 'darcs help markdown' (Dan Frumin)
>       - issue2461: darcs log --repo=remoterepo creates and populates
> _darcs (Ben Franksen)
>       - issue2459: cloning remote repo fails to use packs if cache is
> on a different partition (Ben Franksen)
> 
> # Feedback #
> 
> If you have an issue with darcs 2.10.0, you can report it on
> http://bugs.darcs.net/ . You can also report bugs by email to
> bugs at darcs.net, or come to #darcs on irc.freenode.net.

I’ve updated Mac OS to version 2.10.1. You can install it with

brew install http://darcs.covariant.me/darcs.rb

Tagged: darcs, haskell, homebrew

by Dan at July 12, 2015 06:13 PM

July 11, 2015

Daniil Frumin

HTTP Basic auth in Snap

Recently, I’ve implemented HTTP Basic auth for darcsden and wrote a simple wreq test for it. In this post I would like to outline the main technical details.

Server side

Transient storage

A lot of darcsden code is (especially the parts that are closer to the users’ web browser — handlers, pages, so on) is written around sessions. Sessions are stored in a special storage — implemented by the DarcsDen.Backend.Transient, but if we abstract away from the details we have a Session datatype. Authorization and authentication information is handled by sessions using functions setUser :: (BTIO bt) => Maybe User -> Session -> Snap Session, notice :: (BTIO bt) => String -> Session -> Snap () (display a message to the user) and others. The BTIO bt part is just a synonym for

type BTIO bt = (BackendTransient bt, ?backendTransient :: bt, MonadIO (BackendTransientM bt))

Which basically says that we are operating with a transient backend that supports all of necessary operations, and we can also do IO in it. Right now there are only two transient backends (read: two ways of storing sessions): Redis and in-process memory.

Running sessions

If we have a piece of Snap code that we want to “sessionify” we use the following interface:

withSession :: (BTIO bt) => (Session -> Snap ()) -> Snap ()

What this does is it basically checks for a cookie — in case it is present it grabs the session information from the storage (in accordance with the cookie); if the cookie is not present it creates a new session and stores it in a cookie.

If we have a page of a type Session -> Snap (), we might want to give user an option to do HTTP authentication on that page. We introduce another function

withBasicAuth :: (BP bp, BTIO bt) 
              => (Session -> Snap ()) 
              -> (Session -> Snap ())
withBasicAuth act s = do
    rq  do
          rawHeader <- maybe throwChallenge return $ getHeader “Authorization” rq
          let (Just (usr,pw)) = getCredentials rawHeader
          c  errorPage “Unknown user”
            Just u -> if checkPassword (fromBS pw) u
                         then doLogin (fromBS usr)
                         else errorPage “Bad password”
      _ -> act s

So, what is going on in here? First of all, we check if the “login” parameter is set to “true”. If it does, we try to get the “Authorization” header, de-encode it, and check whether the credentials are good.

throwChallenge :: Snap a
throwChallenge = do
    modifyResponse $ (setResponseStatus 401 “Unauthorized”) .
                     (setHeader “WWW-Authenticate” “Basic realm=darcsdenrealm”)
    getResponse >>= finishWith

If the response header is present, it is of a form Basic x, where x is a base64 encoded string user:password. We can extract the credentials from the header like this:

import qualified Data.ByteString          as B
import qualified Data.ByteString.Base64   as B
…
getCredentials :: B.ByteString  — ^ Header
               -> Maybe (B.ByteString, B.ByteString) — ^ Possibly (username, password)
getCredentials header =
    if (isInfixOf “Basic “ header)
      then fmap extract (hush (B.decode (B.drop 6 header)))
      else Nothing
  where
    extract cred = case (B.breakByte (c2w ‘:’) cred) of
                     (usr, pw) -> (usr, safeTail pw)

On the client

The tests that I am currently writing for darcsden are all of the same form: I use wreq to do requests to the darcsden server, then, if necessary, I run taggy to extract information from the webpage, and compare it to the “canonical” information.

As it turns out, doing HTTP Basic Auth is very easy with wreq! First of all, we define a function for doing a GET request that will do some exception handling for us:

getSafeOpts :: Options -> String -> IO (Either Status (Response ByteString))
getSafeOpts opts url = fmap Right (getWith opts url) `catch` hndlr
  where
    hndlr (StatusCodeException s _ _) = return (Left s)
    hndlr e = throwIO e

This way, we won’t get a runtime exception when accessing a non-existing page or getting a server error. Doing a GET request with HTTP Basic Auth is now very easy:

getWithAuth :: (String, String) -> String -> IO (Either Status (Response ByteString))
getWithAuth (username,pw) url = getSafeOpts opts url
  where
    opts = defaults & auth ?~ basicAuth (toBS username) (toBS pw)
                    & param “login” .~ [“true”]

In that snippet we use lenses to set up an auth header and an HTTP parameter (?login=true).

Finally, after obtaining a Response ByteString, we can parse it with taggy-lens:

parsed :: Fold (Response L.ByteString) Text.Taggy.Node
parsed = responseBody 
       . to (decodeUtf8With lenientDecode)
       . html

We can then play with it in GHCi

*Main> Right r  r ^.. parsed
[NodeElement (Element {eltName = “DOCTYPE”, eltAttrs = fromList [(“html”,””)], eltChildren = [NodeElement (Element {eltName = “html”, eltAttrs = fromList [], eltChildren = [NodeElement (Element {eltName = “head”, eltAttrs = fromList [], eltChildren = [NodeElement (Element {eltName = “title”, eltAttrs = fromList [], eltChildren = [NodeContent “localhost”]}),NodeElement (Element {eltName = “link”, eltAttrs = fromList [(“href”,”http://localhost:8900/public/images/favicon.ico”),…

If we want to check that we are indeed logged in correctly, we should look for the “log out” button. Taggy does all the heavy lifting for us, we just have to write down a lens (more precisely, a fold) to “extract” a logout button from the page

logoutButton :: HasElement e => Fold e Text
logoutButton = allAttributed (ix “class” . only “logout”)
             . allNamed (only “a”)
             . contents

logoutButton searches for <div class=“logout”> and returns the text in the link inside the div. There might be many such links inside the node, hence we use a fold.

*Main> r ^.. parsed . logoutButton
[“log out”]

In this case, since we only care if such link is present, we can use a preview

*Main> r ^? parsed . logoutButton
Just “log out”

Conclusion

Well, that’s about it for now. I regret taking way too much time writing this update, and I hope to deliver another one soon. Meanwhile, some information regarding the darcsden SoC project can be found on the wiki.


Tagged: darcs, haskell

by Dan at July 11, 2015 09:27 AM

July 09, 2015

Darcs

darcs 2.10.1 release

Hi all,

The darcs team is pleased to announce the release of darcs 2.10.1 !

Downloading

The easiest way to install darcs 2.10.1 from source is by first installing the Haskell Platform (http://www.haskell.org/<wbr></wbr>platform). If you have installed the Haskell Platform or cabal-install, you can install this release by doing:

$ cabal update
$ cabal install darcs-2.10.1

Alternatively, you can download the tarball from http://darcs.net/releases/darcs-2.10.1.tar.gz and build it by hand as explained in the README file.

The 2.10 branch is also available as a darcs repository from http://darcs.net/releases/<wbr></wbr>branch-2.10

What's new in darcs 2.10.1 (since darcs 2.10.0)



  • support terminfo 0.4, network 2.6, zlib 0.6, quickcheck 2.8 and attoparsec 0.13
  • errorDoc now prints a stack trace (if profiling was enabled) (Ben Franksen)
  • beautified error messages for command line and default files (Ben Franksen)
  • generalized doFastZip for darcsden support
  • fixed the following bugs:
    • issue2449: test harness/shelly: need to handle mis-encoded/binary data (Ganesh Sittampalam)
    • issue2423: diff only respecting --diff-command when a diff.exe is present (Alain91)
    • issue2447: get contents of deleted file (Ben Franksen)
    • issue2307: add information about 'darcs help manpage' and 'darcs help markdown' (Dan Frumin)
    • issue2461: darcs log --repo=remoterepo creates and populates _darcs (Ben Franksen)
    • issue2459: cloning remote repo fails to use packs if cache is on a different partition (Ben Franksen)

Feedback

If you have an issue with darcs 2.10.1, you can report it on http://bugs.darcs.net/ . You can also report bugs by email to bugs@darcs.net, or come to #darcs on irc.freenode.net.

by guillaume (noreply@blogger.com) at July 09, 2015 05:10 PM

Bryn Keller

Working with Hakyll

WordPress was nice for some time. There were lots of nice themes to choose from, installation was easy, things mostly worked. However, the need to keep updating it with security patches, and the need to keep sifting through comment spam, became tiresome.

I always wish I had time to work on something in Haskell, so I decided to put the need for a new blog platform together with that: I’ve switched to Hakyll, at least for now.

This means I generate the site statically, as HTML pages. This means my site requires very little compute power to run, and it’s even easier for me to administer than the WP site was. It also means I don’t have support for comments, which is sad but saves me lots of time sifting through spam. My contact information is on the contact page, please reach out directly if you have comments. Maybe I’ll add some third-party discussion site pointers at a future date. Let me know if you have opinions about that.

Creating the site was fairly simple and took about a day, and took the following steps:

  • Download and install stack (not cabal). This is the build tool we’ll use to fetch and install hakyll and its dependencies. Stack is now the preferred build tool for Haskell. They have binaries available for lots of platforms.
  • Follow the hakyll installation tutorial, substituting “stack” for “cabal”.

Now you have a (very) bare bones site. I then:

  • Added Bootstrap. I basically copied in the HTML from the template and modified it as needed to make it work with Hakyll.
  • Added RSS and Atom feeds using the snapshots tutorial
  • Changed the landing page to show teasers rather than full articles or just links. The teaser tutorial was very helpful for that. Definitely read this after getting the RSS feeds working, it will make more sense.
  • Other minor things like adding favicons

All in all, quite a bit simpler than I expected. The fact that it was so easy to use stack instead of cabal was a nice surprise along the way. The tutorials for Hakyll are really helpful, though there are some details missing, so be patient.

It turns out not to need as much actual Haskell programming time as I expected, but maybe when I need to make something fancier I’ll get to work on an actual Haskell project.

by Bryn Keller at July 09, 2015 12:00 AM

July 08, 2015

Well-Typed.Com

Hackage Security Alpha Release

Well-Typed is very happy to announce the first alpha release of the Hackage Security library, along with integration into both cabal-install and the Hackage server and a tool for managing file-based secure repositories. This release is not yet ready for general use, but we would like to invite interested parties to download and experiment with the library and its integration. We expect a beta release running on the central Hackage server will soon follow.

Hackage Security and related infrastructure is a project funded by the Industrial Haskell Group to secure Hackage, the central Haskell package server. A direct consequence of this work is that we can have untrusted Hackage mirrors (mirror selection is directly supported by the library). A minor but important additional side goal is support for incremental updates of the central Hackage index (only downloading information about new packages, rather than all packages).

TL;DR: Hackage will be more secure, more reliable and faster, and cabal update should generally finish in seconds.

Security architecture

Security is notoriously difficult to get right, so rather than concocting something ad-hoc the Hackage Security framework is based on TUF, The Update Framework. TUF is a collaboration between security researches at the University of Arizona, the University of Berkeley and the Univerity of Washington, as well as various developers of the Tor project. It is a theory specifically designed for securing software update systems, and suits the needs of Hackage perfectly.

TUF covers both index signing and author signing. Index signing provides the means to verify that something we downloaded from a mirror is the same as what is available from the central server (along with some other security properties), thus making it possible to set up untrusted mirrors. It does not however deal with compromise of the central server. Author signing allows package authors to sign packages, providing a guarantee that the package you download is the one that the author uploaded. These two concerns are largely orthogonal, and the current project only adds support for index signing. Author signing will be the subject of a later project.

Very briefly, here is how it works. The bits in red refer to new features added as part of the Hackage Security work.

  1. Hackage provides a file 00-index.tar.gz (known as “the index”) which contains the .cabal files for all versions of all packages on the server. It is this file that cabal update downloads, and it is this file that cabal install uses to find out which packages are available and what their dependencies are.

    Hackage additionally provides a signed file /snapshot.json (“the snapshot”), containing a hash of the index. When cabal downloads the index it computes its hash and verifies it against the hash recorded in the snapshot. Since mirrors do not have the key necessary to sign the snapshot (“ the snapshot key”), if the hash matches we know that the index we downloaded, and hence all files within, was the same as on the central server.
  2. When you cabal install one or more packages, the index provides cabal with a list of packages and their dependencies. However, the index does not contain the packages themselves.

    The index does however contain package.json files for each version of each package, containing a hash for the .tar.gz of that package version. Since these files live in the index they are automatically protected by the snapshot key. When cabal downloads a package it computes the hash of the package and compares it against the hash recorded in the index; if it matches, we are guaranteed that the package is the same as the package on the central server, as the central server is the only one with access to the snapshot key.
  3. The client does not have built-in knowledge of the snapshot key. Instead, it can download /root.json (“the root metadata”) from the server, which contains the public snapshot key. The root metadata itself is signed by the root keys, of which the client does have built-in knowledge. The private root keys must be kept very securely (e.g. encrypted and offline).

This description leaves out lots of details, but the purpose of this blog post is not to give a full overview of TUF. See the initial announcement or the website of The Update Framework for more details on TUF; the Hackage Security project README provides a very detailed discussion on how our implemention of TUF relates to the official TUF specification.

Software architecture

Most of the functionality is provided through a new library called hackage-security, available from github, designed to be used by clients and servers alike.

Client-side

Although we have integrated it in cabal-install, the hackage-security library is expressly designed to be useable by different clients as well. For example, it generalizes over the library to use for HTTP requests; cabal uses hackage-security-HTTP, a thin layer around the HTTP library. However, if a client such as stack wants to use the hackage-security library to talk to Hackage it may prefer to use hackage-security-http-client instead, a thin layer around the http-client library.

Using the library is very simple. After importing Hackage.Security.Client three functions become available, corresponding to points 1, 2 and 3 above:

checkForUpdates :: Repository -> CheckExpiry -> IO HasUpdates
downloadPackage :: Repository -> PackageId -> (TempPath -> IO a) -> IO a
bootstrap       :: Repository -> [KeyId] -> KeyThreshold -> IO ()

Some comments:

  • A Repository is an object describing a (local or remote) repository.
  • The CheckExpiry argument describes whether we should check expiry dates on metadata. Expiry dates are important to prevent attacks where a malicious mirror provides outdated data (see A Look In the Mirror: Attacks on Package Managers, Section 3, Threat Model) but we may occassionally want to accept expired data (for instance, when the central server is down for an extended period of time).
  • The [KeyId] and KeyThreshold arguments to bootstrap represent the client’s “built-in” knowledge of the root keys we alluded to above. In the case of cabal-install these come from the cabal config file, which may contain a section such as

    remote-repo hackage.haskell.org
      url: http://hackage.haskell.org/
      secure: True
      root-keys: 2ae741f4c4a5f70ed6e6c48762e0d7a493d8dd265e9cbc6c4037dfc7ceaec70e
                 32d3db5b4403935c0baf52a2bcb05031784a971ee2d43587288776f2e90609db
                 eed36d2bb15f94628221cde558e99c4e1ad36fd243fe3748e1ee7ad00eb9d628
      key-threshold: 2

    (this syntax for specifying repositories in the cabal config is new.)

We have written an example client that demonstrates how to use this API; the example client supports both local and remote repositories and can use HTTP, http-client or curl, and yet is only just over 100 lines of code.

Server-side

The server-side support provided by Hackage.Security.Server comes primarily in the form of datatypes corresponding to the TUF metadata, along with functions for constructing them.

It is important to realize that servers need not be running the Hackage software; mirrors of the central Hackage server may (and typically will) be simple HTTP file servers, and indeed company-internal package servers may choose not to use the Hackage software at all, using only file servers. We provide a hackage-security utility for managing such file-based repositories; see below for details.

Trying it out

There are various ways in which you can try out this alpha release, depending on what precisely you are interested in.

Resources at a glance

hackage-security library github tag “pre-release-alpha”
cabal-install github branch “using-hackage-security”
hackage github branch “using-hackage-security”

Secure Hackage snapshots

We provide two almost-complete secure (but mostly static) Hackage snapshots, located at

http://hackage.haskell.org/security-alpha/mirror1
http://hackage.haskell.org/security-alpha/mirror2

If you want to use cabal to talk to these repositories, you will need to download and build it from the using-hackage-security branch. Then change your cabal config and add a new section:

remote-repo alpha-snapshot
  url: http://hackage.haskell.org/security-alpha/mirror1
  secure: True
  root-keys: 89e692e45b53b575f79a02f82fe47359b0b577dec23b45d846d6e734ffcc887a
             dc4b6619e8ea2a0b72cad89a3803382f6acc8beda758be51660b5ce7c15e535b
             1035a452fd3ada87956f9e77595cfd5e41446781d7ba9ff9e58b94488ac0bad7
  key-threshold: 2

It suffices to point cabal to either mirror; TUF and the hackage-security library provide built-in support for providing clients with a list of mirrors. During the first check for updates cabal will download this list, and then use either mirror thereafter. Note that if you wish you can set the key-threshold to 0 and not specify any root keys; if you do this, the initial download of the root information will not be verified, but all access will be secure after that.

These mirrors are almost complete, because the first mirror has an intentional problem: the latest version of generics-sop does not match its signed hash (simulating an evil attempt from an attacker to replace the generics-sop library with DoublyEvil-0.3.142). If you attempt to cabal get this library cabal should notice something is amiss on this mirror, and automatically try again from the second mirror (which has not been “compromised”):

# cabal get generics-sop
Downloading generics-sop-0.1.1.2...
Selected mirror http://hackage.haskell.org/security-alpha/mirror1
Downloading package generics-sop-0.1.1.2
Exception Invalid hash for .../generics-sop-0.1.1.2.tar45887.gz
when using mirror http://hackage.haskell.org/security-alpha/mirror1
Selected mirror http://hackage.haskell.org/security-alpha/mirror2
Downloading package generics-sop-0.1.1.2
Unpacking to generics-sop-0.1.1.2/

(It is also possible to use the example client to talk to these mirrors, or indeed to a secure repo of your own.)

Setting up a secure file-based repo

If you want to experiment with setting up your own secure repository, the easiest way to do this is to set up a file based repository using the hackage-security utility. A file based repository (as opposed to one running the actual Hackage software) is much easier to set up and will suffice for many purposes.

  1. Create a directory ~/my-secure-repo containing a single subdirectory ~/my-secure-repo/package. Put whatever packages you want to make available from your repo in this subdirectory. At this point your repository might look like

    ~/my-secure-repo/package/basic-sop-0.1.0.5.tar.gz
    ~/my-secure-repo/package/generics-sop-0.1.1.1.tar.gz
    ~/my-secure-repo/package/generics-sop-0.1.1.2.tar.gz
    ~/my-secure-repo/package/json-sop-0.1.0.4.tar.gz
    ~/my-secure-repo/package/lens-sop-0.1.0.2.tar.gz
    ~/my-secure-repo/package/pretty-sop-0.1.0.1.tar.gz

    (because obviously the generics-sop packages are the first things to come to mind when thinking about which packages are important to secure.) Note the flat directory structure: different packages and different versions of those packages all live in the one directory.

  2. Create public and private keys:

    # hackage-security create-keys --keys ~/my-private-keys

    This will create a directory structure such as

    ~/my-private-keys/mirrors/id01.private
    ~/my-private-keys/mirrors/..
    ~/my-private-keys/root/id04.private
    ~/my-private-keys/root/..
    ~/my-private-keys/snapshot/id07.private
    ~/my-private-keys/target/id08.private
    ~/my-private-keys/target/..
    ~/my-private-keys/timestamp/id11.private

    containing keys for all the various TUF roles (proper key management is not part of this alpha release).

    Note that these keys are stored outside of the repository proper.

  3. Create the initial TUF metadata and construct an index using

    # hackage-security bootstrap \
                       --repo ~/my-secure-repo \
                       --keys ~/my-private-keys

    This will create a directory ~/my-secure-repo/index containing the .cabal files (extracted from the package tarballs) and TUF metadata for all packages

    ~/my-secure-repo/index/basic-sop/0.1.0.5/basic-sop.cabal
    ~/my-secure-repo/index/basic-sop/0.1.0.5/package.json
    ~/my-secure-repo/index/generics-sop/0.1.1.1/generics-sop.cabal
    ~/my-secure-repo/index/generics-sop/0.1.1.1/package.json
    ...

    and package the contents of that directory up as the index tarball ~/my-secure-repo/00-index.tar.gz; it will also create the top-level metadata files

    ~/my-secure-repo/mirrors.json
    ~/my-secure-repo/root.json
    ~/my-secure-repo/snapshot.json
    ~/my-secure-repo/timestamp.json
  4. The timestamp and snapshot are valid for three days, so you will need to resign these files regularly using

    # hackage-security update \
                       --repo ~/my-secure-repo \
                       --keys ~/my-private-keys

    You can use the same command whenever you add any additional packages to your repository.

  5. If you now make this directory available (for instance, by pointing Apache at it) you should be able to use cabal to access it, in the same way as described above for accessing the secure Hackage snapshots. You can either set key-threshold to 0, or else copy in the root key IDs from the generated root.json file.

Setting up a secure Hackage server

If you are feeling adventurous you can also try to set up your own secure Hackage server. You will need to build Hackage from the using-secure-hackage branch.

You will need to create a subdirectory TUF inside Hackage’s datafiles/ directory, containing 4 files:

datafiles/TUF/mirrors.json
datafiles/TUF/root.json
datafiles/TUF/snapshot.private
datafiles/TUF/timestamp.private

containing the list of mirrors, the root metadata, and the private snapshot and timestamp keys. You can create these files using the hackage-security utility:

  1. Use the create-keys as described above to create a directory with keys for all roles, and then copy over the snapshot and timestamp keys to the TUF directory.
  2. Use the create-root and create-mirrors commands to create the root and mirrors metadata. The create-mirrors accepts an arbitrary list of mirrors to be added to the mirrors metadata, should you wish to do so.

Note that the root.json and mirrors.json files are served as-is by Hackage, they are not used internally; the snapshot and timestamp keys are of course used to sign the snapshot and the timestamp.

Once you have created and added these files, everything else should Just Work(™). When you start up your server it will create TUF metadata for any existing packages you may have (if you are migrating an existing database). It will create a snapshot and a timestamp file; create metadata for any new packages you upload and update the snapshot and timestamp; and resign the snapshot and timestamp nightly. You can talk to the repository using cabal as above.

If you a have Hackage server containing a lot of packages (a full mirror of the central Hackage server, for instance) then migration will be slow; it takes approximately an hour to compute hashes for all packages on Hackage. If this would lead to unacceptable downtime you can use the precompute-fileinfo tool to precompute hashes for all packages, given a recent backup. Copy the file created by this tool to datafiles/TUF/md5-to-sha256.map before doing the migration. If all hashes are precomputed migration only takes a few minutes for a full Hackage snapshot.

Integrating hackage-security

If you want to experiment with integrating the hackage-security library into your own software, the example client is probably the best starting point for integration in client software, and the hackage-security utility is probably a good starting point for integration in server software.

Bugs

Please report any bugs or comments you may have as GitHub issues.

Roadmap

This is an alpha release, intended for testing by people with a close interest in the Hackage Security work. The issue tracker contains a list of issues to be resolved before the beta release, at which point we will make the security features available on the central Hackage server and make a patched cabal available in a more convenient manner. Note that the changes to Hackage are entirely backwards compatible, so existing clients will not be affected.

After the beta release there are various other loose ends to tie up before the official release of Phase 1 of this project. After that Phase 2 will add author signing.

by edsko at July 08, 2015 12:56 PM

July 06, 2015

Roman Cheplyaka

How Haskell handles signals

How is it possible to write signal handlers in GHC Haskell? After all, the set of system calls allowed inside signal handlers is rather limited. In particular, it is very hard to do memory allocation safely inside a signal handler; one would have to modify global data (and thus not be reentrant), call one of the banned syscalls (brk, sbrk, or mmap), or both.

On the other hand, we know that almost any Haskell code requires memory allocation. So what’s the trick?

The trick is that a Haskell handler is not installed as a true signal handler. Instead, a signal is handled by a carefully crafted RTS function generic_handler (rts/posix/Signals.c). All that function does (assuming the threaded RTS) is write the signal number and the siginfo_t structure describing the signal to a special pipe (called the control pipe, see GHC.Event.Control).

The other end of this pipe is being watched by the timer manager thread (GHC.Event.TimerManager). When awaken by a signal message from the control pipe, it looks up the handler corresponding to the signal number and, in case it’s an action, runs it in a new Haskell thread.

The signal handlers are stored in a global array, signal_handlers (GHC.Conc.Signal). When you install a signal action in Haskell, you put a stable pointer to the action’s code into the array cell corresponding to the signal number, so that the timer thread could look it up later when an actual signal is delivered.

See also https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/Signals.

July 06, 2015 08:00 PM

Daniel Mlot (duplode)

Applicative Archery

It is widely agreed that the laws of the Applicative class are not pretty to look at.

pure id <*> v = v                            -- identity
pure f <*> pure x = pure (f x)               -- homomorphism
u <*> pure y = pure ($ y) <*> u              -- interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- composition

Monad laws, in comparison, not only look less odd to begin with but can also be stated in a much more elegant way in terms of Kleisli composition (<=<). Shouldn’t there be an analogous nice presentation for Applicative as well? That became a static question in my mind while I was studying applicative functors many moons ago. After finding surprisingly little commentary on this issue, I decided to try figuring it out by myself. 1

Let’s cast our eye over Applicative:

class Functor t => Applicative t where
    pure  :: a -> t a
    (<*>) :: t (a -> b) -> t a -> t b

If our inspiration for reformulating Applicative is Kleisli composition, the only sensible plan is to look for a category in which the t (a -> b) functions-in-a-context from the type of (<*>) are the arrows, just like a -> t b functions are arrows in a Kleisli category. Here is one way to state that plan in Haskell terms:

> class Applicative t => Starry t where
>     idA  :: t (a -> a)
>     (.*) :: t (b -> c) -> t (a -> b) -> t (a -> c)
> 
>     infixl 4 .*
> -- The Applicative constraint is wishful thinking:
> -- When you wish upon a star...

The laws of Starry are the category laws for the t (a -> b) arrows:

idA .* v = v                -- left identity
u .* idA = u                -- right identity
u .* v .* w = u .* (v .* w) -- associativity

The question, then, is whether it is possible to reconstruct Applicative and its laws from Starry. The answer is a resounding yes! The proof is in this manuscript, which I have not transcribed here as it is a little too long for a leisurely post like this one 2. The argument is set in motion by establishing that pure is an arrow mapping of a functor from Hask to a Starry category, and that both (<*>) and (.*) are arrow mappings of functors in the opposite direction. That leads to several naturality properties of those functors, from which the Applicative laws can be obtained. Along the way, we also get definitions for the Starry methods in terms of the Applicative ones…

>     idA = pure id
>     u .* v = fmap (.) u <*> v

… and vice-versa:

pure x = fmap (const x) idA
u <*> v = fmap ($ ()) (u .* fmap const v)

Also interesting is how the property relating fmap and (<*>)

fmap f u = pure f <*> u

… now tells us that a Functor results from composing the pure functor with the (<*>) functor. That becomes more transparent if we write it point-free:

fmap = (<*>) . pure

In order to ensure Starry is equivalent to Applicative we still need to prove the converse, that is, obtain the Starry laws from the Applicative laws plus the definitions of idA and (.*) just above. That is not difficult; all it takes is substituting the definitions in the Starry laws and:

  • For left identity, noticing that (id .) = id.

  • For right identity, applying the interchange law and noticing that ($ id) . (.) is id in a better disguise.

  • For associativity, using the laws to move all (.) to the left of the (<*>) and then verifying that the resulting messes of dots in both sides are equivalent.

As a tiny example, here is the Starry instance of Maybe

instance Starry Maybe where
    idA              = Just id
    Just g .* Just f = Just (g . f)
    _      .* _      = Nothing

… and the verification of the laws for it:

-- Left identity:
idA .* u = u
Just id .* u = u
-- u = Nothing
Just id .* Nothing = Nothing
Nothing = Nothing
-- u = Just f
Just id .* Just f = Just f
Just (id . f) = Just f
Just f = Just f

-- Right identity:
u .* idA = u
u .* Just id = u
-- u = Nothing
Nothing .* Just id = Nothing
Nothing = Nothing
-- u = Just g
Just g .* Just id = Just g
Just (g .* id) = Just g
Just g = Just g

-- Associativity:
u .* v .* w = u .* (v .* w)
-- If any of u, v and w are Nothing, both sides will be Nothing.
Just h .* Just g .* Just f = Just h .* (Just g .* Just f)
Just (h . g) .* Just f = Just h .* (Just (g . f))
Just (h . g . f) = Just (h . (g . f))
Just (h . g . f) = Just (h . g . f)

It works just as intended:

GHCi> Just (2*) .* Just (subtract 3) .* Just (*4) <*> Just 5
Just 34
GHCi> Just (2*) .* Nothing .* Just (*4) <*> Just 5
Nothing

I do not think there will be many opportunities to use the Starry methods in practice. We are comfortable enough with applicative style, through which we see most t (a -> b) arrows as intermediates generated on demand, rather than truly meaningful values. Furthermore, the Starry laws are not really easier to prove (though they are certainly easier to remember!). Still, it was an interesting exercise to do, and it eases my mind to know that there is a neat presentation of the Applicative laws that I can relate to.

This post is Literate Haskell, in case you wish to play with Starry in GHCi (here is the raw .lhs file ).

> instance Starry Maybe where
> instance Starry [] where
> instance Starry ((->) a) where
> instance Starry IO where

As for proper implementations in libraries, the closest I found was Data.Semigroupoid.Static, which lives in Edward Kmett’s semigroupoids package. “Static arrows” is the actual technical term for the t (a -> b) arrows. The module provides…

newtype Static f a b = Static { runStatic :: f (a -> b) }

… which uses the definitions shown here for idA and (.*) as id and (.) of its Category instance.

<section class="footnotes">
  1. There is a reasonably well-known alternative formulation of Applicative: the Monoidal class as featured in this post by Edward Z. Yang. While the laws in this formulation are much easier to grasp, Monoidal feels a little alien from the perspective of a Haskeller, as it shifts the focus from function shuffling to tuple shuffling.

  2. Please excuse some oddities in the manuscript, such as off-kilter terminology and weird conventions (e.g. consistently naming arguments in applicative style as w <*> v <*> u rather than u <*> v <*> w in applicative style). The most baffling choice was using id rather than () as the throwaway argument to const. I guess I did that because ($ ()) looks bad in handwriting.

</section>
Comment on GitHub (see the full post for a reddit link)

by Daniel Mlot at July 06, 2015 08:00 PM

The GHC Team

GHC Weekly News - 2015/07/06

Hi *,

Welcome for the latest entry in the GHC Weekly News. The past week, GHC HQ met up to discuss the status of the approaching 7.10.2 release.

7.10.2 status

After quite some delay due to a number of tricky regressions in 7.10.1, 7.10.2 is nearing the finish line. Austin cut release candidate 2 on Friday and so far the only reports of trouble appear to be some validation issues, most of which have already been fixed thanks to Richard Eisenberg.

7.10.2 will include a number of significant bug-fixes. These include,

  • #10521, where overlap of floating point STG registers weren't properly accounted for, resulting in incorrect results in some floating point computations. This was fixed by the amazing Reid Barton.
  • #10534, a type-safety hole enabling a user to write unsafeCoerce with data families and coerce. Fix due to the remarkable Richard Eisenberg.
  • #10538, where some programs would cause the simplifier to emit an empty case, resulting in runtime crashes. Fix due to the industrious Simon Peyton Jones.
  • #10527, where the simplifier would expend a great deal of effort simplifying arguments which were never demanded by the callee.
  • #10414, where a subtle point of the runtime system's black-holing mechanism resulting in hangs on a carefully constructed testcase.
  • #10236, where incorrect DWARF annotations would be generated, resulting in incorrect backtraces. Fixed by Peter Wortmann
  • #7450, where cached free variable information was being unnecessarily dropped by the specialiser, resulting in non-linear compile times for some programs.

See the status page for a complete listing of issues fixed in this release.

In the coming days we will being working with FP Complete to test the pre-release against Stackage. While Hackage tends to be too large to build in bulk, the selection of packages represented in Stackage is feasible to build and is likely to catch potential regressions. Hopefully this sort of large-scale validation will become common-place for future releases.

If all goes well, 7.10.2 will mark the end of the 7.10 series. However, there is always the small possibility that a major regression will be found. In this case we will cut a 7.10.3 release which will include a few patches which didn't make it into 7.10.2.

Other matters

It has been suggested in #10601 that GHC builds should ship with DWARF symbols for the base libraries and runtime system. While we all want to see this new capability in users' hands, 7.10.2 will, like 7.10.1, not be shipping with debug symbols. GHC HQ will be discussing the feasibility of including debug symbols with 7.12 in the future. In the meantime, we will be adding options to build.mk to make it easier for users to build their own compilers with debug-enabled libraries.

In this week's GHC meeting the effort to port GHC's build system to the Shake? build system briefly came up. Despite the volume of updates on the Wiki Simon reports that the project is still moving along. The current state of the Shake-based build system can be found on Github.

While debugging #7540 it became clear that there may be trouble lurking in the profiler. Namely when profiling GHC itself lintAnnots is showing up strongly where it logically should not. This was previously addressed in #10007, which was closed after a patch by Simon Marlow was merged. As it appears that this did not fully resolve the issue I'll be looking further into this.

~ Ben

by bgamari at July 06, 2015 04:25 PM

Well-Typed.Com

Dependencies for Cabal Setup.hs files and other goodies

No untracked dependencies!

Years ago, back when Isaac Potoczny-Jones and others were defining the Cabal specification, the big idea was to make Haskell software portable to different environments. One of the mantras was “no untracked dependencies!”.

The problem at the time was that Haskell code had all kinds of implicit dependencies which meant that while it worked for you, it wouldn’t build for me. For example, I might not have some other module that it needed, or the right version of the module.

So of course that’s what the build-depends in .cabal files is all about, requiring that the author of the code declare just what the code requires of its environment. The other important part is that the build system only lets your code see the dependencies you’ve declared, so that you don’t accidentally end up with these untracked dependencies.

This mantra of no untracked dependencies is still sound. If we look at a system like nix, part of what enables it to work so well is that it is absolutely fanatical about having no untracked dependencies.

Untracked dependencies?!

One weakness in the original Cabal specification is with Setup.hs scripts. These scripts are defined in the spec to be the entry point for the system. According to the Cabal spec, to build a package you’re required to compile the Setup.hs script and then use its command line interface to get things done. Because in the original spec the Setup.hs is the first entry point, it’s vital that it be possible to compile Setup.hs without any extra fuss (the runhaskell tool was invented just to make this possible, and to make it portable across compilers).

But by having the Setup.hs as the primary entry point, it meant that it’s impossible to reliably use external code in a Setup.hs script, because you cannot guarantee that that code is pre-installed. Going back to the “no untracked dependencies” mantra, we can see of course that all dependencies of Setup.hs scripts are in fact untracked!

This isn’t just a theoretical problem. Haskell users that do have complex Setup.hs scripts often run into versioning problems, or need external tools to help them get the pre-requisite packages installed. Or as another example: Michael Snoyman noted earlier this year in a diagnosis of an annoying packaging bug that:

As an aside, this points to another problematic aspect of our toolchain: there is no way to specify constraints on dependencies used in custom Setup.hs files. That’s actually caused more difficulty than it may sound like, but I’ll skip diving into it for now.

The solution: track dependencies!

As I said, the mantra of no untracked dependencies is still sound, we just need to apply it more widely.

These days the Setup.hs is effectively no longer a human interface, it is now a machine interface used by other tools like cabal or by distro’s install scripts. So we no longer have to worry so much about Setup.hs scripts always compiling out of the box. It would be acceptable now to say that the first entry point for a tool interacting with a package is the .cabal file, which might list the dependencies of the Setup.hs. The tool would then have to ensure that those dependencies are available when compiling the Setup.hs.

So this is exactly what we have now done. Members of the Industrial Haskell Group have funded us to fix this long standing problem and we have recently merged the solution into the development version of Cabal and cabal-install.

From a package author’s point of view, the solution looks like this: in your .cabal file you can now say:

build-type: Custom

custom-setup
  setup-depends: base >= 4.6,
                 directory >= 1.0,
                 Cabal >= 1.18 && < 1.22,
                 acme-setup-tools == 0.2.*

So it’s a new stanza, like libraries or executables, and like these you can specify the library dependencies of the Setup.hs script.

Now tools like cabal will compile the Setup.hs script with these and only these dependencies, just like it does normally for executables. So no more untracked dependencies in Setup.hs scripts. Newer cabal versions will warn about not using this new section. Older cabal versions will ignore the new section (albeit with a warning). So over time we hope to encourage all packages with custom setup scripts to switch over to this.

In addition, the Setup.hs script gets built with CPP version macros (MIN_VERSION_{pkgname}) available so that the code can be made to work with a wider range of versions of its dependencies.

In the solver…

So on the surface this is all very simple and straightforward, a rather minor feature even. In fact it’s been remarkably hard to implement fully for reasons I’ll explain, but the good news is that it works and the hard work has also gotten us solutions to a couple other irksome problems.

Firstly, why isn’t it trivial? It’s inevitable that sooner or later you will find that your application depends on one package that has setup deps like Cabal == 1.18.* and another with setup deps like Cabal == 1.20.*. At that point we have a problem. Classically we aim to produce a build plan that uses at most one version of each package. We do that because otherwise there’s a danger of type errors from using multiple versions of the same package. Here with setup dependencies there is no such danger: it’s perfectly possible for me to build one setup script with one version of the Cabal library and another script with a different Cabal version. Because these are executables and not libraries, the use of these dependencies does not “leak”, and so we would be safe to use different versions in different places.

So we have extended the cabal solver to allow for limited controlled use of multiple versions of the same package. The constraint is that all the “normal” libraries and exes all use the same single version, just as before, but setup scripts are allowed to introduce their own little world where independent choices about package versions are allowed. To keep things sane, the solver tries as far as possible not to use multiple versions unless it really has to.

If you’re interested in the details in the solver, see Edsko’s recent blog post.

Extra goodies

This work in the solver has some extra benefits.

Improve Cabal lib API without breaking everything

In places the Cabal library is a little crufty, and the API it exposes was never really designed as an API. It has been very hard to fix this because changes in the Cabal library interface break Setup.hs scripts, and there was no way for packages to insulate themselves from this.

So now that we can have packages have proper dependencies for their custom Setup.hs, the flip side is that we have an opportunity to make breaking changes to the Cabal library API. We have an opportunity to throw out the accumulated cruft, clean up the code base and make a library API that’s not so painful to use in Setup.hs scripts.

Shim (or compat) packages for base

Another benefit is that the new solver is finally able to cope with having “base shim” packages, as we used in the base 3.x to 4.x transition. For two GHC releases, GHC came with both base-3.x and base-4.x. The base-4 was the “true” base, while the base-3 was a thin wrapper that re-exported most of base-4 (and syb), but with some changes to implement the old base-3 API. At the time we adapted cabal to cope with this situation of having two versions of a package in a single solution.

When the new solver was implemented however support for this situation was not added (and the old solver implementation was retained to work with GHC 6.12 and older).

This work for setup deps has made it relatively straightforward to add support for these base shims. So next time GHC needs to make a major bump to the version of base then we can use the same trick of using a shim package. Indeed this might also be a good solution in other cases, perhaps cleaner than all these *-compat packages we’ve been accumulating.

It has also finally allowed us to retire the old solver implementation.

Package cycles involving test suites and benchmarks

Another feature that is now easy to implement (though not actually implemented yet) is dealing with the dependency cycles in packages’ test suites and benchmarks.

Think of a core package like bytestring, or even less core like Johan’s cassava csv library. These packages have benchmarks that use the excellent criterion library. But of course criterion is a complex beast and itself depends on bytestring, cassava and a couple dozen other packages.

This introduces an apparent cycle and cabal will fail to find an install plan. I say apparent cycle because there isn’t really a cycle: it’s only the benchmark component that uses criterion, and nothing really depends on that.

Here’s another observation: when benchmarking a new bytestring or cassava, it does not matter one bit that criterion might be built against an older stable version of bytestring or cassava. Indeed it’s probably sensible that we use a stable version. It certainly involves less rebuilding: I don’t really want to rebuild criterion against each minor change in bytestring while I’m doing optimisation work.

So here’s the trick: we break the cycle by building criterion (or say QuickCheck or tasty) against another version of bytestring, typically some existing pre-installed one. So again this means that our install plan has two versions of bytestring in it: the one we mean to build, and the one we use as a dependency for criterion. And again this is ok, just as with setup dependencies, because dependencies of test suites and benchmarks do not “leak out” and cause diamond dependency style type errors.

One technical restriction is that the test suite or benchmark must not depend on the library within the same package, but must instead use the source files directly. Otherwise there would genuinely be a cycle.

Now in general when we have multiple components in a .cabal file we want them to all use the same versions of their dependencies. It would be deeply confusing if a library and an executable within the same package ended up using different versions of some dependency that might have different behaviour. Cabal has always enforced this, and we’re not relaxing it now. The rule is that if there are dependencies of a test suite or benchmark that are not shared with the library or executable components in the package, then we are free to pick different versions for those than we might pick elsewhere within the same solution.

As another example – that’s nothing to do with cycles – we might pick different versions of QuickCheck for different test suites in different packages (though only where necessary). This helps with the problem that one old package might require QuickCheck == 2.5.* while another requires QuickCheck == 2.8.*. But it’d also be a boon if we ever went through another major QC-2 vs QC-3 style of transition. We would be able to have both QC-2 and QC-3 installed and build each package’s test suite against the version it requires, rather than freaking out that they’re not the same version.

Private dependencies in general

Technically, this work opens the door to allowing private dependencies more generally. We’re not pursuing that at this stage, in part because it is not clear that it’s actually a good idea in general.

Mark Lentczner has pointed out the not-unreasonable fear that once you allow multiple versions of packages within the same solution it will in practice become impossible to re-establish the situation where there is just one version of each package, which is what distros want and what most people want in production systems.

So that’s something we should consider carefully as a community before opening those flood gates.

by duncan at July 06, 2015 03:10 PM

Ken T Takusagawa

[dcqhszdf] ChaCha cipher example

The ChaCha cipher seems not to get as much love as Salsa20. Here is a step-by-step example of the ChaCha round function operating on a matrix. The format of the example is loosely based on the analogous example in section 4.1 of this Salsa20 paper: D. J. Bernstein. The Salsa20 family of stream ciphers. Document ID: 31364286077dcdff8e4509f9ff3139ad. URL: http://cr.yp.to/papers.html#salsafamily. Date: 2007.12.25.

original column [a;b;c;d]
61707865
04030201
14131211
00000007

after first line of round function
65737a66
04030201
14131211
7a616573

after second line of round function
65737a66
775858a7
8e747784
7a616573

after third line of round function
dccbd30d
775858a7
8e747784
aab67ea6

after all 4 lines of round function, i.e., quarter round
dccbd30d
395746a7
392af62a
aab67ea6

original matrix, with the same original column above
61707865 3320646e 79622d32 6b206574
04030201 08070605 0c0b0a09 100f0e0d
14131211 18171615 1c1b1a19 201f1e1d
00000007 00000000 01040103 06020905

one round (4 quarter rounds on columns)
dccbd30d 109b031b 0eb5ed20 4483ec2b
395746a7 d88a8f5f 7a292fab b06c9135
392af62a 6ac28db6 dfbce7ba a234a188
aab67ea6 e8383c7a 8d694938 0791063e

after shift rows
dccbd30d 109b031b 0eb5ed20 4483ec2b
d88a8f5f 7a292fab b06c9135 395746a7
dfbce7ba a234a188 392af62a 6ac28db6
0791063e aab67ea6 e8383c7a 8d694938

after another 4 quarter rounds on columns
06b44c34 69a94c11 2ce99b08 216830d1
29b215bd 721e2a33 f0a18097 708e1ee5
2b0e8de3 b801251f 42265fb2 696de1c2
e6fef362 c96c6325 c6cc126e 82c0635a

unshifting rows (concludes 1 double round)
06b44c34 69a94c11 2ce99b08 216830d1
708e1ee5 29b215bd 721e2a33 f0a18097
42265fb2 696de1c2 2b0e8de3 b801251f
c96c6325 c6cc126e 82c0635a e6fef362

after 8 rounds (4 double rounds)
f6093fbb efaf11c6 8bd2c9a4 bf1ff3da
bf543ce8 c46c6b5e c717fe59 863195b1
2775d1a0 babe2495 1b5c653e df7dc23c
5f3e08d7 041df75f f6e58623 abc0ab7e

Adding the original input to the output of 8 rounds
5779b820 22cf7634 0534f6d6 2a40594e
c3573ee9 cc737163 d3230862 9640a3be
3b88e3b1 d2d53aaa 37777f57 ff9ce059
5f3e08de 041df75f f7e98726 b1c2b483

reading the above as bytes, little endian
20 b8 79 57 34 76 cf 22 d6 f6 34 05 4e 59 40 2a
e9 3e 57 c3 63 71 73 cc 62 08 23 d3 be a3 40 96
b1 e3 88 3b aa 3a d5 d2 57 7f 77 37 59 e0 9c ff
de 08 3e 5f 5f f7 1d 04 26 87 e9 f7 83 b4 c2 b1

same as above but with 20000 rounds (10000 double rounds)
11 a3 0a d7 30 d2 a3 dc d8 ad c8 d4 b6 e6 63 32
72 c0 44 51 e2 4c ed 68 9d 8d ff 27 99 93 70 d4
30 2e 83 09 d8 41 70 49 2c 32 fd d9 38 cc c9 ae
27 97 53 88 ec 09 65 e4 88 ff 66 7e be 7e 5d 65

The example was calculated using an implementation of ChaCha in Haskell, whose end results agree with Bernstein's C reference implementation. The Haskell implementation is polymorphic, allowing as matrix elements any data type (of any word width) implementing Bits, and parametrizable to matrices of any size 4xN. (Security is probably bad for N not equal to 4. For word width different from 32, you probably want different rotation amounts.) The flexibility comes at a cost: the implemention is 3000 times slower than Bernstein's reference C implementation (which is in turn is slower than SIMD optimized assembly-language implementations).

Also included in the same project is a similar Haskell implementation of Salsa20, parametrized to matrices of any size MxN because of the more regular structure of the Salsa20 quarter round function compared to ChaCha. We demonstrate taking advantage of polymorphism to use the same code both to evaluate Salsa20 on Word32 and to generate C code for the round function.

by Ken (noreply@blogger.com) at July 06, 2015 04:15 AM

Yesod Web Framework

yesod-table

Announcing yesod-table

Over the last two years, I've seen the need for safe dynamic table-building in half a dozen yesod projects I've worked on. After several design iterations, the result of this experience is yesod-table, which saw its first stable release last week. This blog post will contain code excerpts, but you can also look at the documentation the full example app on github, which can be compiled and run.

Naive Solution

Before getting into specifics about yesod-table, I want to take a look at the naive table-building strategy and identify the common pitfalls. Let's say that you have a data types Color and Person:

data Color = Red | Green | Blue | Purple
  deriving (Show)
data Person = Person
  { firstName     :: Text
  , lastName      :: Text
  , age           :: Int
  , favoriteColor :: Color
  }

We have a list of Person (let's call it people), and we want to show them all in a table. You could write out a hamlet file like this:

<table>
  <thead>
    <tr>
      <th>First Name</th>
      <th>Last Name</th>
      <th>Age</th>
  <tbody>
    $forall p <- people
      <tr>
        <td>#{firstName p}
        <td>#{lastName p}
        <td>#{show (age p)}

And there it is. This is the simplest solution to building a table. In fact, if you've worked on web applications for any length of time, you've probably written code like this before. I've implemented this pattern in PHP+html, in rails+haml, and in yesod+hamlet projects. And every time, it is unsatisfactory.

Problems With Naive Solution

Let's take a look at three reasons why this solution leaves us wanting something more:

  • Duplication. After building a few tables this way, you realize that you are copying the HTML elements and the list iteration ($forall) every time.
  • Non-composability. If I want to build a similar table, one that shows the same fields but additionally has a column for favoriteColor, I have to copy the whole thing. I can't glue another piece onto the end.
  • Breakable Invariant. If we do decide to add a favoriteColor column, we might try simply adding <td>#{show (favoriteColor p)} to the end. This would cause incorrect behavior at runtime, because we would have forgotten to add <th>Favorite Color to the table header. The problem is that we have an invariant not captured by the type system: thead and the tbody loop must have the same number of <th>/<td> elements, and the order must match.

In particular, the last issue (breakable invariant) has been a source of great pains to me before. On a three-column table, you are less likely to forget the <th> or put it in the wrong place. As the table gets larger though (six or more columns), these mistakes become easier to make, and it's harder to be sure that you did the right thing until you see it at runtime.

Example with yesod-table

So let's take a look at how yesod-table addresses these issues. The module it provides should be imported as follows:

import Yesod.Table (Table)
import qualified Yesod.Table as Table

Let's build the same table we saw earlier:

peopleBasicInfoTable :: Table site Person
peopleBasicInfoTable = mempty
  <> Table.text   "First Name" firstName
  <> Table.text   "Last Name"  lastName
  <> Table.string "Age"        (show . age)

And then we can feed it data and render it with buildBootstrap:

-- Although it's called buildBootstrap, it builds a table just fine
-- if you aren't using bootstrap. It just adds bootstrap's table classes.
getExamplePeopleR = defaultLayout $ Table.buildBootstrap peopleTable people

Explanation of Internals

The key to this approach is looking at a table pattern (called a Table in this library) as a collection of columns, not a collection of rows. From the yesod-table source, we have:

newtype Table site a = Table (Seq (Column site a))
  deriving (Monoid)

data Column site a = Column
  { header :: !(WidgetT site IO ())
  , cell :: !(a -> WidgetT site IO ()) 
  }

Each column is just the content that will go in the <th> (the value of header) and a function that, given the data for a table row, will produce the content that belongs in the <td>. A table is trivially a collection of columns and gets a Monoid instance from Seq for free (for those unfamiliar, Seq a is like [a] but with different performance characteristics). Consequently, any two Tables that are parameterized over the same types can be concatenated. As a final note of explanation, the Table.text function that we saw above just a helper for building singleton tables. So, the three Tables below are equivalant:

import qualified Data.Sequence as Seq
import qualified Data.Text as Text
-- These three generate a single-column table that displays the age.
reallyEasyToReadTable, easyToReadTable, hardToReadTable :: Table site Person
reallyEasyToReadTable = Table.int "Age" age
easyToReadTable = Table.text "Age" (Text.pack . show . age)
hardToReadTable = Table.Table $ Seq.singleton $ Table.Column 
  (toWidget $ toHtml "Age")
  (toWidget . toHtml . show . age)

As should be clear, the convenience functions for singleton Tables should always be preferred.

How Is This Better?

Now to address the most important question: Why is this better than what we had earlier? Firstly, consider the issue of the breakable invariant. This is now a non-issue. Imagine that we modified the earlier table to show a person's favorite color as well:

peopleFullInfoTable1 :: Table site Person
peopleFullInfoTable1 = mempty
  <> Table.text   "First Name"     firstName
  <> Table.text   "Last Name"      lastName
  <> Table.text   "Age"            (show . age)
  <> Table.string "Favorite Color" (show . favoriteColor)

The table is correct by construction. You cannot forget the column header because it's part of the Column data type. You're less likely to make this mistake, because now that information is directly beside the content-extracting function, but even if you somehow typed this instead, you would get a compile-time error:

  <> Table.string (show . favoriteColor)

Secondly, we can look at duplication. All the table-rendering logic is moved into buildBootstrap (and you can write your own table renderer if that one is not satisfactory). The Table that we are using now has neither the HTML elements nor the list iteration that we dealt with earlier.

Finally, we can look at composability. As an alternative way of adding the column for a person's favorite color, we could write:

peopleFullInfoTable2 :: Table site Person
peopleFullInfoTable2 = mempty
  <> peopleBasicInfoTable
  <> Table.string "Favorite Color" (show . favoriteColor)

Additionally, if we need to promote this Table to work on something like Entity Person (if it was backed by persistent), we could do this:

-- You need to use ekmett's contravariant package
peopleEntityFullInfoTable :: Table site (Entity Person)
peopleEntityFullInfoTable = contramap entityVal peopleFullInfoTable2

I won't go into contravariant functors here, but it's a very useful pattern for working with Tables. The astute reader will notice that the monoidal composition pattern shown earlier means that we can only append or prepend columns. We cannot inject them into the middle. I'll give yesod-table a B minus on to composability objective.

Closing Notes and Acknowledgements

One final closing note. You may have noticed that all of the Tables in this post were parameterized over site. This is because they don't depend on a particular foundation type. Usually, the way that this can happen is that you use a route in one of the columns:

-- Assume that our foundation type was named App
peopleTableWithLink :: Table App (Entity Person)
peopleTableWithLink = mempty
  <> peopleEntityFullInfoTable
  <> Table.linked "Profile Page" (const "View") (PersonProfileR . entityKey)

The above example must be parameterized over App (or whatever your foundation type is named), not over site.

This monoidal approach to building tables was inspired by Gabriel Gonzalez's Equational Reasoning at Scale and by the classic diagrams paper. I hope that others find the library useful. I am very open to pull requests and suggestions, so if you have an idea for a convenience function, feel free to open up an issue on the github page.

July 06, 2015 12:00 AM

Danny Gratzer

A Basic Tutorial on JonPRL

Posted on July 6, 2015
Tags: jonprl, types

JonPRL switched to ASCII syntax so I’ve updated this post accordingly

I was just over at OPLSS for the last two weeks. While there I finally met Jon Sterling in person. What was particularly fun is that for that last few months he’s been creating a proof assistant called JonPRL in the spirit of Nuprl. As it turns out, it’s quite a fun project to work on so I’ve implemented a few features in it over the last couple of days and learned more or less how it works.

Since there’s basically no documentation on it besides the readme and of course the compiler so I thought I’d write down some of the stuff I’ve learned. There’s also a completely separate post on the underlying type theory for Nuprl and JonPRL that’s very interesting in its own right but this isn’t it. Hopefully I’ll get around to scribbling something about that because it’s really quite clever.

Here’s the layout of this tutorial

  • First we start with a whirlwind tutorial. I’ll introduce the basic syntax and we’ll go through some simple proofs together
  • I’ll then dive into some of the rational behind JonPRL’s theory. This should help you understand why some things work how they do
  • I’ll show off a few of JonPRL’s more unique features and (hopefully) interest you enough to start fiddling on your own

Getting JonPRL

JonPRL is pretty easy to build and install and having it will make this post more enjoyable. You’ll need smlnj since JonPRL is currently written in SML. This is available in most package managers (including homebrew) otherwise just grab the binary from the website. After this the following commands should get you a working executable

  • git clone ssh://git@github.com/jonsterling/jonprl
  • cd jonprl
  • git submodule init
  • git submodule update
  • make (This is excitingly fast to run)
  • make test (If you’re doubtful)

You should now have an executable called jonprl in the bin folder. There’s no prelude for jonprl so that’s it. You can now just feed it files like any reasonable compiler and watch it spew (currently difficult-to-decipher) output at you.

If you’re interested in actually writing JonPRL code, you should probably install David Christiansen’s Emacs mode. Now that we’re up and running, let’s actually figure out how the language works

The Different Languages in JonPRL

JonPRL is composed of really 3 different sorts of mini-languages

  • The term language
  • The tactic language
  • The language of commands to the proof assistant

In Coq, these roughly correspond to Gallina, Ltac, and Vernacular respectively.

The Term Language

The term language is an untyped language that contains a number of constructs that should be familiar to people who have been exposed to dependent types before. The actual concrete syntax is composed of 3 basic forms:

  • We can apply an “operator” (I’ll clarify this in a moment) with op(arg1; arg2; arg3).
  • We have variables with x.
  • And we have abstraction with x.e. JonPRL has one construct for binding x.e built into its syntax, that things like lam or fun are built off of.

An operator in this context is really anything you can imagine having a node in an AST for a language. So something like lam is an operator, as is if or pair (corresponding to (,) in Haskell). Each operator has a piece of information associated with it, called its arity. This arity tells you how many arguments an operator takes and how many variables x.y.z. ... each is allowed to bind. For example, with lam has an arity is written (1) since it takes 1 argument which binds 1 variable. Application (ap) has the arity (0; 0). It takes 2 arguments neither of which bind a variable.

So as mentioned we have functions and application. This means we could write (lamx.x) y in JonPRL as ap(lam(x.x); y). The type of functions is written with fun. Remember that JonPRL’s language has a notion of dependence so the arity is (0; 1). The construct fun(A; x.B) corresponds to (x : A) → B in Agda or forall (x : A), B in Coq.

We also have dependent sums as well (prods). In Agda you would write (M , N) to introduce a pair and prod A lam x → B to type it. In JonPRL you have pair(M; N) and prod(A; x.B). To inspect a prod we have spread which let’s us eliminate a pair pair. Eg spread(0; 2) and you give it a prod in the first spot and x.y.e in the second. It’ll then replace x with the first component and y with the second. Can you think of how to write fst and snd with this?

There’s sums, so inl(M), inr(N) and +(A; B) corresponds to Left, Right, and Either in Haskell. For case analysis there’s decide which has the arity (0; 1; 1). You should read decide(M; x.N; y.P) as something like

    case E of
      Left x -> L
      Right y -> R

In addition we have unit and <> (pronounced axe for axiom usually). Neither of these takes any arguments so we write them just as I have above. They correspond to Haskell’s type- and value-level () respectively. Finally there’s void which is sometimes called false or empty in theorem prover land.

You’ll notice that I presented a bunch of types as if they were normal terms in this section. That’s because in this untyped computation system, types are literally just terms. There’s no typing relation to distinguish them yet so they just float around exactly as if they were lam or something! I call them types because I’m thinking of later when we have a typing relation built on top of this system but for now there are really just terms. It was still a little confusing for me to see fun(unit; _.unit) in a language without types, so I wanted to make this explicit.

Now we can introduce some more exotic terms. Later, we’re going to construct some rules around them that are going to make it behave that way we might expect but for now, they are just suggestively named constants.

  • U{i}, the ith level universe used to classify all types that can be built using types other than U{i} or higher. It’s closed under terms like fun and it contains all the types of smaller universes
  • =(0; 0; 0) this is equality between two terms at a type. It’s a proposition that’s going to precisely mirror what’s going on later in the type theory with the equality judgment
  • member(0; 0) this is just like = but internalizes membership in a type into the system. Remember that normally “This has that type” is a judgment but with this term we’re going to have a propositional counterpart to use in theorems.

In particular it’s important to distinguish the difference between the judgment and member the term. There’s nothing inherent in member above that makes it behave like a typing relation as you might expect. It’s on equal footing with flibbertyjibberty(0; 0; 0).

This term language contains the full untyped lambda calculus so we can write all sorts of fun programs like

    lam(f.ap(lam(x.ap(f;(ap(x;x)))); lam(x.ap(f;(ap(x;x)))))

which is just the Y combinator. In particular this means that there’s no reason that every term in this language should normalize to a value. There are plenty of terms in here that diverge and in principle, there’s nothing that rules out them doing even stranger things than that. We really only depend on them being deterministic, that e ⇒ v and e ⇒ v' implies that v = v'.

Tactics

The other big language in JonPRL is the language of tactics. Luckily, this is very familiarly territory if you’re a Coq user. Unluckily, if you’ve never heard of Coq’s tactic mechanism this will seem completely alien. As a quick high level idea for what tactics are:

When we’re proving something in a proof assistant we have to deal with a lot of boring mechanical details. For example, when proving A → B → A I have to describe that I want to introduce the A and the B into my context, then I have to suggest using that A the context as a solution to the goal. Bleh. All of that is pretty obvious so let’s just get the computer to do it! In fact, we can build up a DSL of composable “proof procedures” or /tactics/ to modify a particular goal we’re trying to prove so that we don’t have to think so much about the low level details of the proof being generated. In the end this DSL will generate a proof term (or derivation in JonPRL) and we’ll check that so we never have to trust the actual tactics to be sound.

In Coq this is used to great effect. In particular see Adam Chlipala’s book to see incredibly complex theorems with one-line proofs thanks to tactics.

In JonPRL the tactic system works by modifying a sequent of the form H ⊢ A (a goal). Each time we run a tactic we get back a list of new goals to prove until eventually we get to trivial goals which produce no new subgoals. This means that when trying to prove a theorem in the tactic language we never actually see the resulting evidence generated by our proof. We just see this list of H ⊢ As to prove and we do so with tactics.

The tactic system is quite simple, to start we have a number of basic tactics which are useful no matter what goal you’re attempting to prove

  • id a tactic which does nothing
  • t1; t2 this runs the t1 tactic and runs t2 on any resulting subgoals
  • *{t} this runs t as long as t does something to the goal. If t ever fails for whatever reason it merely stops running, it doesn’t fail itself
  • ?{t} tries to run t once. If t fails nothing happens
  • !{t} runs t and if t does anything besides complete the proof it fails. This means that !{id} for example will always fail.
  • t1 | t2 runs t1 and if it fails it runs t2. Only one of the effects for t1 and t2 will be shown.
  • t; [t1, ..., tn] first runs t and then runs tactic ti on subgoal ith subgoal generated by t
  • trace "some words" will print some words to standard out. This is useful when trying to figure out why things haven’t gone your way.
  • fail is the opposite of id, it just fails. This is actually quite useful for forcing backtracking and one could probably implement a makeshift !{} as t; fail.

It’s helpful to see this as a sort of tree, a tactic takes one goal to a list of a subgoals to prove so we can imagine t as this part of a tree

      H
      |
———–————————— (t)
H'  H''  H'''

If we have some tactic t2 then t; t2 will run t and then run t2 on H, H', and H''. Instead we could have t; [t1, t2, t3] then we’ll run t and (assuming it succeeds) we’ll run t1 on H', t2 on H'', and t3 on H'''. This is actually how things work under the hood, composable fragments of trees :)

Now those give us a sort of bedrock for building up scripts of tactics. We also have a bunch of tactics that actually let us manipulate things we’re trying to prove. The 4 big ones to be aware of are

  • intro
  • elim #NUM
  • eq-cd
  • mem-cd

The basic idea is that intro modifies the A part of the goal. If we’re looking at a function, so something like H ⊢ fun(A; x.B), this will move that A into the context, leaving us with H, x : A ⊢ B.

If you’re familiar with sequent calculus intro runs the appropriate right rule for the goal. If you’re not familiar with sequent calculus intro looks at the outermost operator of the A and runs a rule that applies when that operator is to the right of a the .

Now one tricky case is what should intro do if you’re looking at a prod? Well now things get a bit dicey. We’d might expect to get two subgoals if we run intro on H ⊢ prod(A; x.B), one which proves H ⊢ A and one which proves H ⊢ B or something, but what about the fact that x.B depends on whatever the underlying realizer (that’s the program extracted from) the proof of H ⊢ A! Further, Nuprl and JonPRL are based around extract-style proof systems. These mean that a goal shouldn’t depend on the particular piece of evidence proving of another goal. So instead we have to tell intro up front what we want the evidence for H ⊢ A to be is so that the H ⊢ B section may use it.

To do this we just give intro an argument. For example say we’re proving that · ⊢ prod(unit; x.unit), we run intro [<>] which gives us two subgoals · ⊢ member(<>; unit) and · ⊢ unit. Here the [] let us denote the realizer we’re passing to intro. In general any term arguments to a tactic will be wrapped in []s. So the first goal says “OK, you said that this was your realizer for unit, but is it actually a realizer for unit?” and the second goal substitutes the given realizer into the second argument of prod, x.unit, and asks us to prove that. Notice how here we have to prove member(<>; unit)? This is where that weird member type comes in handy. It let’s us sort of play type checker and guide JonPRL through the process of type checking. This is actually very crucial since type checking in Nuprl and JonPRL is undecidable.

Now how do we actually go about proving member(<>; unit)? Well here mem-cd has got our back. This tactic transforms member(A; B) into the equivalent form =(A; A; B). In JonPRL and Nuprl, types are given meaning by how we interpret the equality of their members. In other words, if you give me a type you have to say

  1. What canonical terms are in that terms
  2. What it means for two canonical members to be equal

Long ago, Stuart Allen realized we could combine the two by specifying a partial equivalence relation for a type. In this case rather than having a separate notion of membership we check to see if something is equal to itself under the PER because when it is that PER behaves like a normal equivalence relation! So in JonPRL member is actually just a very thin layer of sugar around = which is really the core defining notion of typehood. To handle = we have eq-cd which does clever things to handle most of the obvious cases of equality.

Finally, we have elim. Just like intro let us simplify things on the right of the ⊢, elim let’s us eliminate something on the left. So we tell elim to “eliminate” the nth item in the context (they’re numbered when JonPRL prints them) with elim #n.

Just like with anything, it’s hard to learn all the tactics without experimenting (though a complete list can be found with jonprl --list-tactics). Let’s go look at the command language so we can actually prove some theorems.

Commands

So in JonPRL there are only 4 commands you can write at the top level

  • Operator
  • [oper] =def= [term] (A definition)
  • Tactic
  • Theorem

The first three of these let us customize and extend the basic suite of operators and tactics JonPRL comes with. The last actually lets us state and prove theorems.

The best way to see these things is by example so we’re going to build up a small development in JonPRL. We’re going to show that products are monoid with unit up to some logical equivalence. There are a lot of proofs involved here

  1. prod(unit; A) entails A
  2. prod(A; unit) entails A
  3. A entails prod(unit; A)
  4. A entails prod(A; unit)
  5. prod(A; prod(B; C)) entails prod(prod(A; B); C)
  6. prod(prod(A; B); C) entails prod(A; prod(B; C))

I intend to prove 1, 2, and 5. The remaining proofs are either very similar or fun puzzles to work on. We could also prove that all the appropriate entailments are inverses and then we could say that everything is up to isomorphism.

First we want a new snazzy operator to signify nondependent products since writing prod(A; x.B) is kind of annoying. We do this using operator

    Operator prod : (0; 0).

This line declares prod as a new operator which takes two arguments binding zero variables each. Now we really want JonPRL to know that prod is sugar for prod. To do this we use =def= which gives us a way to desugar a new operator into a mess of existing ones.

    [prod(A; B)] =def= [prod(A; _.B)].

Now we can change any occurrence of prod(A; B) for prod(A; _.B) as we’d like. Okay, so we want to prove that we have a monoid here. What’s the first step? Let’s verify that unit is a left identity for prod. This entails proving that for all types A, prod(unit; A) ⊃ A and A ⊃ prod(unit; A). Let’s prove these as separate theorems. Translating our first statement into JonPRL we want to prove

    fun(U{i}; A.
    fun(prod(unit; A); _.
    A))

In Agda notation this would be written

    (A : Set) → (_ : prod(unit; A)) → A

Let’s prove our first theorem, we start by writing

    Theorem left-id1 :
      [fun(U{i}; A.
       fun(prod(unit; A); _.
       A))] {
      id
    }.

This is the basic form of a theorem in JonPRL, a name, a term to prove, and a tactic script. Here we have id as a tactic script, which clearly doesn’t prove our goal. When we run JonPRL on this file (C-c C-l if you’re in Emacs) you get back

[XXX.jonprl:8.3-9.1]: tactic 'COMPLETE' failed with goal:
⊢ funA ∈ U{i}. (prod(unit; A)) => A

Remaining subgoals:
⊢ funA ∈ U{i}. (prod(unit; A)) => A

So focus on that Remaining subgoals bit, that’s what we have left to prove, it’s our current goal. Now you may notice that this outputted goal is a lot prettier than our syntax! That’s because currently in JonPRL the input and outputted terms may not match, the latter is subject to pretty printing. In general this is great because you can read your remaining goals, but it does mean copying and pasting is a bother. There’s nothing to the left of that ⊢ yet so let’s run the only applicable tactic we know. Delete that id and replace it with

    {
      intro
    }.

The goal now becomes

Remaining subgoals:

1. A : U{i}
⊢ (prod(unit; A)) => A

⊢ U{i} ∈ U{i'}

Two ⊢s means two subgoals now. One looks pretty obvious, U{i'} is just the universe above U{i} (so that’s like Set₁ in Agda) so it should be the case that U{i} ∈ U{i'} by definition! So the next tactic should be something like [???, mem-cd; eq-cd]. Now what should that ??? be? Well we can’t use elim because there’s one thing in the context now (A : U{i}), but it doesn’t help us really. Instead let’s run unfold <prod>. This is a new tactic that’s going to replace that prod with the definition that we wrote earlier.

    {
      intro; [unfold <prod>, mem-cd; eq-cd]
    }

Notice here that , behinds less tightly than ; which is useful for saying stuff like this. This gives us

Remaining subgoals:

1. A : U{i}
⊢ (unit × A) => A

We run intro again

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro
    }

Now we are in a similar position to before with two subgoals.

    Remaining subgoals:

    1. A : U{i}
    2. _ : unit × A
    ⊢ A


    1. A : U{i}
    ⊢ unit × A ∈ U{i}

The first subgoal is really what we want to be proving so let’s put a pin in that momentarily. Let’s get rid of that second subgoal with a new helpful tactic called auto. It runs eq-cd, mem-cd and intro repeatedly and is built to take care of boring goals just like this!

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto]
    }

Notice that we used what is a pretty common pattern in JonPRL, to work on one subgoal at a time we use []’s and ids everywhere except where we want to do work, in this case the second subgoal.

Now we have

Remaining subgoals:

1. A : U{i}
2. _ : unit × A
⊢ A

Cool! Having a pair of unit × A really ought to mean that we have an A so we can use elim to get access to it.

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto];
      elim #2
    }

This gives us

Remaining subgoals:

1. A : U{i}
2. _ : unit × A
3. s : unit
4. t : A
⊢ A

We’ve really got the answer now, #4 is precisely our goal. For this situations there’s assumption which is just a tactic which succeeds if what we’re trying to prove is in our context already. This will complete our proof

    Theorem left-id1 :
      [fun(U{i}; A.
       fun(prod(unit; A); _.
       A))] {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto];
      elim #2; assumption
    }.

Now we know that auto will run all of the tactics on the first line except unfold <prod>, so what we just unfold <prod> first and run auto? It ought to do all the same stuff.. Indeed we can shorten our whole proof to unfold <prod>; auto; elim #2; assumption. With this more heavily automated proof, proving our next theorem follows easily.

    Theorem right-id1 :
      [fun(U{i}; A.
       fun(prod(A; unit); _.
       A))] {
      unfold <prod>; auto; elim #2; assumption
    }.

Next, we have to prove associativity to complete the development that prod is a monoid. The statement here is a bit more complex.

    Theorem assoc :
      [fun(U{i}; A.
       fun(U{i}; B.
       fun(U{i}; C.
       fun(prod(A; prod(B;C)); _.
       prod(prod(A;B); C)))))] {
      id
    }.

In Agda notation what I’ve written above is

    assoc : (A B C : Set) → A × (B × C) → (A × B) × C
    assoc = ?

Let’s kick things off with unfold <prod>; auto to deal with all the boring stuff we had last time. In fact, since x appears in several nested places we’d have to run unfold quite a few times. Let’s just shorten all of those invocations into *{unfold <prod>}

    {
      *{unfold <prod>}; auto
    }

This leaves us with the state

Remaining subgoals:

1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ A


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ B


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ C

In each of those goals we need to take apart the 4th hypothesis so let’s do that

    {
      *{unfold <prod>}; auto; elim #4
    }

This leaves us with 3 subgoals still

1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ A


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ B


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ C

The first subgoal is pretty easy, assumption should handle that. In the other two we want to eliminate 6 and then we should be able to apply assumption. In order to deal with this we use | to encode that disjunction. In particular we want to run assumption OR elim #6; assumption leaving us with

    {
      *{unfold <prod>}; auto; elim #4; (assumption | elim #6; assumption)
    }

This completes the proof!

    Theorem assoc :
      [fun(U{i}; A.
       fun(U{i}; B.
       fun(U{i}; C.
       fun(prod(A; prod(B;C)); _.
       prod(prod(A;B); C)))))] {
      *{unfold <prod>}; auto; elim #4; (assumption | elim #6; assumption)
    }.

As a fun puzzle, what needs to change in this proof to prove we can associate the other way?

What on earth did we just do!?

So we just proved a theorem.. but what really just happened? I mean how did we go from “Here we have an untyped computation system which types just behaving as normal terms” to “Now apply auto and we’re done!”. In this section I’d like to briefly sketch the path from untyped computation to theorems.

The path looks like this

  • We start with our untyped language and its notion of computation

    We already discussed this in great depth before.

  • We define a judgment a = b ∈ A.

    This is a judgment, not a term in that language. It exists in whatever metalanguage we’re using. This judgment is defined across 3 terms in our untyped language (I’m only capitalizing A out of convention). This is supposed to represent that a and b are equal elements of type A. This also gives meaning to typehood: something is a type in CTT precisely when we know what the partial equivalence relation defined by - = - ∈ A on canonical values is.

    Notice here that I said partial. It isn’t the case that a = b ∈ A presupposes that we know that a : A and b : A because we don’t have a notion of : yet!

    In some sense this is where we depart from a type theory like Coq or Agda’s. We have programs already and on top of them we define this 3 part judgment which interacts which computation in a few ways I’m not specifying. In Coq, we would specify one notion of equality, generic over all types, and separately specify a typing relation.

  • From here we can define the normal judgments of Martin Lof’s type theory. For example, a : A is a = a ∈ A. We recover the judgment A type with A = A ∈ U (where U here is a universe).

This means that inhabiting a universe A = A ∈ U, isn’t necessarily inductively defined but rather negatively generated. We specify some condition a term must satisfy to occupy a universe.

Hypothetical judgments are introduced in the same way they would be in Martin-Lof’s presentations of type theory. The idea being that H ⊢ J if J is evident under the assumption that each term in H has the appropriate type and furthermore that J is functional (respects equality) with respect to what H contains. This isn’t really a higher order judgment, but it will be defined in terms of a higher order hypothetical judgment in the metatheory.

With this we have something that walks and quacks like normal type theory. Using the normal tools of our metatheory we can formulate proofs of a : A and do normal type theory things. This whole development is building up what is called “Computational Type Theory”. The way this diverges from Martin-Lof’s extensional type theory is subtle but it does directly descend from Martin-Lof’s famous 1979 paper “Constructive Mathematics and Computer Programming” (which you should read. Instead of my blog post).

Now there’s one final layer we have to consider, the PRL bit of JonPRL. We define a new judgment, H ⊢ A [ext a]. This is judgment is cleverly set up so two properties hold

  • H ⊢ A [ext a] should entail that H ⊢ a : A or H ⊢ a = a ∈ A
  • In H ⊢ A [ext a], a is an output and H and A are inputs. In particular, this implies that in any inference for this judgment, the subgoals may not use a in their H and A.

This means that a is completely determined by H and A which justifies my use of the term output. I mean this in the sense of Twelf and logic programming if that’s a more familiar phrasing. It’s this judgment that we see in JonPRL! Since that a is output we simply hide it, leaving us with H ⊢ A as we saw before. When we prove something with tactics in JonPRL we’re generating a derivation, a tree of inference rules which make H ⊢ A evident for our particular H and A! These rules aren’t really programs though, they don’t correspond one to one with proof terms we may run like they would in Coq. The computational interpretation of our program is bundled up in that a.

To see what I mean here we need a little bit more machinery. Specifically, let’s look at the rules for the equality around the proposition =(a; b; A). Remember that we have a term <> lying around,

     a = b ∈ A
————————————————————
<> = <> ∈ =(a; b; A)

So the only member of =(a; b; A) is <> if a = b ∈ A actually holds. First off, notice that <> : A and <> : B doesn’t imply that A = B! In another example, lam(x. x) ∈ fun(A; _.A) for all A! This is a natural consequence of separating our typing judgment from our programming language. Secondly, there’s not really any computation in the e of H ⊢ =(a; b; A) (e). After all, in the end the only thing e could be so that e : =(a; b; A) is <>! However, there is potentially quite a large derivation involved in showing =(a; b; A)! For example, we might have something like this

x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption

Now we write derivations of this sequent up side down, so the thing we want to show starts on top and we write each rule application and subgoal below it (AI people apparently like this?). Now this was quite a derivation, but if we fill in the missing [ext e] for this derivation from the bottom up we get this

x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry     [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption   [ext x]

Notice how at the bottom there was some computational content (That x signifies that we’re accessing a variable in our context) but than we throw it away right on the next line! That’s because we find that no matter what the extract was that let’s us derive =(b; a; A), the only realizer it could possible generate is <>. Remember our conditions, if we can make evident the fact that b = a ∈ A then <> ∈ =(b; a; A). Because we somehow managed to prove that b = a ∈ A holds, we’re entitled to just use <> to realize our proof. This means that despite our somewhat tedious derivation and the bookkeeping that we had to do to generate that program, that program reflects none of it.

This is why type checking in JonPRL is woefully undecidable: in part, the realizers that we want to type check contain none of the helpful hints that proof terms in Coq would. This also means that extraction from JonPRL proofs is built right into the system and we can actually generate cool and useful things! In Nuprl-land, folks at Cornell actually write proofs and use this realizers to run real software. From what Bob Constable said at OPLSS they can actually get these programs to run fast (within 5x of naive C code).

So to recap, in JonPRL we

  • See H ⊢ A
  • Use tactics to generate a derivation of this judgment
  • Once this derivation is generated, we can extract the computational content as a program in our untyped system

In fact, we can see all of this happen if you call JonPRL from the command line or hit C-c C-c in emacs! On our earlier proof we see

Operator prod : (0; 0).
⸤prod(A; B)⸥ ≝ ⸤A × B⸥.

Theorem left-id1 : ⸤⊢ funA ∈ U{i}. (prod(unit; A)) => A⸥ {
  fun-intro(A.fun-intro(_.prod-elim(_; _.t.t); prod⁼(unit⁼; _.hyp⁼(A))); U⁼{i})
} ext {
  lam_. lam_. spread(_; _.t.t)
}.

Theorem right-id1 : ⸤⊢ funA ∈ U{i}. (prod(A; unit)) => A⸥ {
  fun-intro(A.fun-intro(_.prod-elim(_; s._.s); prod⁼(hyp⁼(A); _.unit⁼)); U⁼{i})
} ext {
  lam_. lam_. spread(_; s._.s)
}.

Theorem assoc : ⸤⊢ funA ∈ U{i}. funB ∈ U{i}. funC ∈ U{i}. (prod(A; prod(B; C))) => prod(prod(A; B); C)⸥ {
  fun-intro(A.fun-intro(B.fun-intro(C.fun-intro(_.independent-prod-intro(independent-prod-intro(prod-elim(_;
  s.t.prod-elim(t; _._.s)); prod-elim(_; _.t.prod-elim(t;
  s'._.s'))); prod-elim(_; _.t.prod-elim(t; _.t'.t')));
  prod⁼(hyp⁼(A); _.prod⁼(hyp⁼(B); _.hyp⁼(C)))); U⁼{i}); U⁼{i});
  U⁼{i})
} ext {
  lam_. lam_. lam_. lam_. ⟨⟨spread(_; s.t.spread(t; _._.s)), spread(_; _.t.spread(t; s'._.s'))⟩, spread(_; _.t.spread(t; _.t'.t'))⟩
}.

Now we can see that those Operator and bits are really what we typed with =def= and Operator in JonPRL, what’s interesting here are the theorems. There’s two bits, the derivation and the extract or realizer.

{
  derivation of the sequent · ⊢ A
} ext {
  the program in the untyped system extracted from our derivation
}

We can move that derivation into a different proof assistant and check it. This gives us all the information we need to check that JonPRL’s reasoning and helps us not trust all of JonPRL (I wrote some of it so I’d be a little scared to trust it :). We can also see the computational bit of our proof in the extract. For example, the computation involved in taking A × unit → A is just lam_. lam_. spread(_; s._.s)! This is probably closer to what you’ve seen in Coq or Idris, even though I’d say the derivation is probably more similar in spirit (just ugly and beta normal). That’s because the extract need not have any notion of typing or proof, it’s just the computation needed to produce a witness of the appropriate type. This means for a really tricky proof of equality, your extract might just be <>! Your derivation however will always exactly reflect the complexity of your proof.

Killer features

OK, so I’ve just dumped about 50 years worth of hard research in type theory into your lap which is best left to ruminate for a bit. However, before I finish up this post I wanted to do a little bit of marketing so that you can see why one might be interested in JonPRL (or Nuprl). Since we’ve embraced this idea of programs first and types as PERs, we can define some really strange types completely seamlessly. For example, in JonPRL there’s a type ⋂(A; x.B), it behaves a lot like fun but with one big difference, the definition of - = - ∈ ⋂(A; x.B) looks like this

a : A ⊢ e = e' ∈ [a/x]B
————————————————————————
   e = e' ∈ ⋂(A; x.B)

Notice here that e and e' may not use a anywhere in their bodies. That is, they have to be in [a/x]B without knowing anything about a and without even having access to it.

This is a pretty alien concept that turned out to be new in logic as well (it’s called “uniform quantification” I believe). It turns out to be very useful in PRL’s because it lets us declare things in our theorems without having them propogate into our witness. For example, we could have said

    Theorem right-id1 :
          [⋂(U{i}; A.
           fun(prod(A; unit); _.
           A))] {
          unfold <prod>; auto; elim #2; assumption
        }.

With the observation that our realizer doesn’t need to depend on A at all (remember, no types!). Then the extract of this theorem is

lamx. spread(x; s._.s)

There’s no spurious lam _. ... at the beginning! Even more wackily, we can define subsets of an existing type since realizers need not have unique types

e = e' ∈ A  [e/x]P  [e'/x]P
————————————————————————————
  e = e' ∈ subset(A; x.P)

And in JonPRL we can now say things like “all odd numbers” by just saying subset(nat; n. ap(odd; n)). In intensional type theories, these types are hard to deal with and still the subject of open research. In CTT they just kinda fall out because of how we thought about types in the first place. Quotients are a similarly natural conception (just define a new type with a stricter PER) but JonPRL currently lacks them (though they shouldn’t be hard to add..).

Finally, if you’re looking for one last reason to dig into **PRL, the fact that we’ve defined all our equalities extensionally means that several very useful facts just fall right out of our theory

    Theorem fun-ext :
      [⋂(U{i}; A.
       ⋂(fun(A; _.U{i}); B.
       ⋂(fun(A; a.ap(B;a)); f.
       ⋂(fun(A; a.ap(B;a)); g.

       ⋂(fun(A; a.=(ap(f; a); ap(g; a); ap(B; a))); _.
       =(f; g; fun(A; a.ap(B;a))))))))] {
      auto; ext; ?{elim #5 [a]}; auto
    }.

This means that two functions are equal in JonPRL if and only if they map equal arguments to equal output. This is quite pleasant for formalizing mathematics for example.

Wrap Up

Whew, we went through a lot! I didn’t intend for this to be a full tour of JonPRL, just a taste of how things sort of hang together and maybe enough to get you looking through the examples. Speaking of which, JonPRL comes with quite a few examples which are going to make a lot more sense now.

Additionally, you may be interested in the documentation in the README which covers most of the primitive operators in JonPRL. As for an exhaustive list of tactics, well….

Hopefully I’ll be writing about JonPRL again soon. Until then, I hope you’ve learned something cool :)

A huge thanks to David Christiansen and Jon Sterling for tons of helpful feedback on this

<script type="text/javascript"> var disqus_shortname = 'codeco'; (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus

July 06, 2015 12:00 AM

July 04, 2015

Edwin Brady

Cross-platform Compilers for Functional Languages

I’ve just submitted a new draft, Cross-platform Compilers for Functional Languages. Abstract:

Modern software is often designed to run on a virtual machine, such as the JVM or .NET’s CLR. Increasingly, even the web browser is considered a target platform with the Javascript engine as its virtual machine. The choice of programming language for a project is therefore restricted to the languages which target the desired platform. As a result, an important consideration for a programming language designer is the platform to be targetted. For a language to be truly cross-platform, it must not only support different operating systems (e.g. Windows, OSX and Linux) but it must also target different virtual machine environments such as JVM, .NET, Javascript and others. In this paper, I describe how this problem is addressed in the Idris programming language. The overall compilation process involves a number of intermediate representations and Idris exposes an interface to each of these representations, allowing back ends for different target platforms to decide which is most appropriate. I show how to use these representations to retarget Idris for multiple platforms, and further show how to build a generic foreign function interface supporting multiple platforms.

Constructive comments and suggestions are welcome, particularly if you’ve tried implementing a code generator for Idris.


by edwinb at July 04, 2015 11:06 AM

July 03, 2015

Brandon Simmons

Translating some stateful bit-twiddling to haskell

I just started implementing SipHash in hashabler and wanted to share a nice way I found to translate stateful bit-twiddling code in C (which makes heavy use of bitwise assignment operators) to haskell.

I was working from the reference implementation. As you can see statefulness and mutability are an implicit part of how the algorithm is defined, as it modifies the states of the v variables.

#define SIPROUND                                        \
  do {                                                  \
    v0 += v1; v1=ROTL(v1,13); v1 ^= v0; v0=ROTL(v0,32); \
    v2 += v3; v3=ROTL(v3,16); v3 ^= v2;                 \
    v0 += v3; v3=ROTL(v3,21); v3 ^= v0;                 \
    v2 += v1; v1=ROTL(v1,17); v1 ^= v2; v2=ROTL(v2,32); \
  } while(0)

int  siphash( uint8_t *out, const uint8_t *in, uint64_t inlen, const uint8_t *k )
{

  /* ... */

  for ( ; in != end; in += 8 )
  {
    m = U8TO64_LE( in );
    v3 ^= m;

    TRACE;
    for( i=0; i<cROUNDS; ++i ) SIPROUND;

    v0 ^= m;
  }

I wanted to translate this sort of code as directly as possible (I’d already decided if it didn’t work on the first try I would burn my laptop and live in the woods, rather than debug this crap).

First we’ll use name shadowing to “fake” our mutable variables, making it easy to ensure we’re always dealing with the freshest values.

{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

We’ll also use RecordWildCards to make it easy to capture the “current state” of these values, through folds and helper functions.

{-# LANGUAGE RecordWildCards #-}

And finally we use the trivial Identity monad (this trick I learned from Oleg) which gets us the proper scoping we want for our v values:

import Data.Functor.Identity

Here’s a bit of the haskell:

siphash :: Hashable a => SipKey -> a -> Word64
siphash (k0,k1) = \a-> runIdentity $ do
    let v0 = 0x736f6d6570736575
        v1 = 0x646f72616e646f6d
        v2 = 0x6c7967656e657261
        v3 = 0x7465646279746573

    ...

    v3 <- return $ v3 `xor` k1;
    v2 <- return $ v2 `xor` k0;
    v1 <- return $ v1 `xor` k1;
    v0 <- return $ v0 `xor` k0;

    ...

    -- Initialize rest of SipState:
    let mPart          = 0
        bytesRemaining = 8
        inlen          = 0
    SipState{ .. } <- return $ hash (SipState { .. }) a

    let !b = inlen `unsafeShiftL` 56

    v3 <- return $ v3 `xor` b
    -- for( i=0; i<cROUNDS; ++i ) SIPROUND;
    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3
    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3
    v0 <- return $ v0 `xor` b

    ...

    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3

    return $! v0 `xor` v1 `xor` v2 `xor` v3

If you were really doing a lot of this sort of thing, you could even make a simple quasiquoter that could translate bitwise assignment into code like the above.

July 03, 2015 05:58 PM

Philip Wadler

Don Syme awarded Silver Medal by Royal Academy of Engineering

 Congratulations, Don!
For over two decades, the Academy’s Silver Medals have recognised exceptional personal contributions from early- to mid-career engineers who have advanced the cause of engineering in the UK.
Three of the UK’s most talented engineers are to receive the Royal Academy of Engineering’s coveted Silver Medal for remarkable technical  achievements in their fields, coupled with commercial success.
They are the inventor of 3D printed surgical instruments, an
indoor location-tracking technology pioneer, and the creator of the F#
computer programming language.
 Full RAE Announcement. Spotted by Kevin Hammond.

by Philip Wadler (noreply@blogger.com) at July 03, 2015 04:28 PM

Mark Jason Dominus

The annoying boxes puzzle: solution

I presented this logic puzzle on Wednesday:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

Can you figure out which box contains the treasure?

It's not too late to try to solve this before reading on. If you want, you can submit your answer here:

The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:

Results

There were 506 total responses up to Fri Jul 3 11:09:52 2015 UTC; I kept only the first response from each IP address, leaving 451. I read all the "something else" submissions and where it seemed clear I recoded them as votes for "red", for "not enough information", or as spam. (Several people had the right answer but submitted "other" so they could explain themselves.) There was also one post attempted to attack my (nonexistent) SQL database. Sorry, Charlie; I'm not as stupid as I look.

	 66.52%  300 red
	 25.72   116 not-enough-info
	  3.55    16 green
	  2.00     9 other
	  1.55     7 spam
	  0.44     2 red-with-qualification
	  0.22     1 attack

	100.00   451 TOTAL
One-quarter of respondents got the right answer, that there is not enough information given to solve the problem, Two-thirds of respondents said the treasure was in the red box. This is wrong. The treasure is in the green box.

What?

Let me show you. I stated:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

The labels are as I said. Everything I told you was literally true.

The treasure is definitely not in the red box.

No, it is actually in the green box.

(It's hard to see, but one of the items in the green box is the gold and diamond ring made in Vienna by my great-grandfather, which is unquestionably a real treasure.)

So if you said the treasure must be in the red box, you were simply mistaken. If you had a logical argument why the treasure had to be in the red box, your argument was fallacious, and you should pause and try to figure out what was wrong with it.

I will discuss it in detail below.

Solution

The treasure is undeniably in the green box. However, correct answer to the puzzle is "no, you cannot figure out which box contains the treasure". There is not enough information given. (Notice that the question was not “Where is the treasure?” but “Can you figure out…?”)

(Fallacious) Argument A

Many people erroneously conclude that the treasure is in the red box, using reasoning something like the following:

  1. Suppose the red label is true. Then exactly one label is true, and since the red label is true, the green label is false. Since it says that the treasure is in the green box, the treasure must really be in the red box.
  2. Now suppose that the red label is false. Then the green label must also be false. So again, the treasure is in the red box.
  3. Since both cases lead to the conclusion that the treasure is in the red box, that must be where it is.

What's wrong with argument A?

Here are some responses people commonly have when I tell them that argument A is fallacious:

"If the treasure is in the green box, the red label is lying."

Not quite, but argument A explicitly considers the possibility that the red label was false, so what's the problem?

"If the treasure is in the green box, the red label is inconsistent."

It could be. Nothing in the puzzle statement ruled this out. But actually it's not inconsistent, it's just irrelevant.

"If the treasure is in the green box, the red label is meaningless."

Nonsense. The meaning is plain: it says “exactly one of these labels is true”, and the meaning is that exactly one of the labels is true. Anyone presenting argument A must have understood the label to mean that, and it is incoherent to understand it that way and then to turn around and say that it is meaningless! (I discussed this point in more detail in 2007.)

"But the treasure could have been in the red box."

True! But it is not, as you can see in the pictures. The puzzle does not give enough information to solve the problem. If you said that there was not enough information, then congratulations, you have the right answer. The answer produced by argument A is incontestably wrong, since it asserts that the treasure is in the red box, when it is not.

"The conditions supplied by the puzzle statement are inconsistent."

They certainly are not. Inconsistent systems do not have models, and in particular cannot exist in the real world. The photographs above demonstrate a real-world model that satisfies every condition posed by the puzzle, and so proves that it is consistent.

"But that's not fair! You could have made up any random garbage at all, and then told me afterwards that you had been lying."

Had I done that, it would have been an unfair puzzle. For example, suppose I opened the boxes at the end to reveal that there was no treasure at all. That would have directly contradicted my assertion that "One [box] contains a treasure". That would have been cheating, and I would deserve a kick in the ass.

But I did not do that. As the photograph shows, the boxes, their colors, their labels, and the disposition of the treasure are all exactly as I said. I did not make up a lie to trick you; I described a real situation, and asked whether people they could diagnose the location of the treasure.

(Two respondents accused me of making up lies. One said:

There is no treasure. Both labels are lying. Look at those boxes. Do you really think someone put a treasure in one of them just for this logic puzzle?
What can I say? I _did_ do this. Some of us just have higher standards.)

"But what about the labels?"

Indeed! What about the labels?

The labels are worthless

The labels are red herrings; the provide no information. Consider the following version of the puzzle:

There are two boxes on a table, one red and one green. One contains a treasure.

Which box contains the treasure?

Obviously, the problem cannot be solved from the information given.

Now consider this version:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "gcoadd atniy fnck z fbi c rirpx hrfyrom". The green box is labelled "ofurb rz bzbsgtuuocxl ckddwdfiwzjwe ydtd."

Which box contains the treasure?

One is similarly at a loss here.

(By the way, people who said one label was meaningless: this is what a meaningless label looks like.)

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

But then the janitor happens by. "Don't be confused by those labels," he says. "They were stuck on there by the previous owner of the boxes, who was an illiterate shoemaker who only spoke Serbian. I think he cut them out of a magazine because he liked the frilly borders."

Which box contains the treasure?

The point being that in the absence of additional information, there is no reason to believe that the labels give any information about the contents of the boxes, or about labels, or about anything at all. This should not come as a surprise to anyone. It is true not just in annoying puzzles, but in the world in general. A box labeled “fresh figs” might contain fresh figs, or spoiled figs, or angry hornets, or nothing at all.
Order
What is the Name of this Book?
What is the Name of this Book?
with kickback
no kickback

Why doesn't every logic puzzle fall afoul of this problem?

I said as part of the puzzle conditions that there was a treasure in one box. For a fair puzzle, I am required to tell the truth about the puzzle conditions. Otherwise I'm just being a jerk.

Typically the truth or falsity of the labels is part of the puzzle conditions. Here's a typical example, which I took from Raymond Smullyan's What is the name of this book? (problem 67a):

… She had the following inscriptions put on the caskets:
GoldSilverLead
THE PORTRAIT IS IN THIS CASKET THE PORTRAIT IS NOT IN THIS CASKET THE PORTRAIT IS NOT IN THE GOLD CASKET
Portia explained to the suitor that of the three statements, at most one was true.

Which casket should the suitor choose [to find the portrait]?

Notice that the problem condition gives the suitor a certification about the truth of the labels, on which he may rely. In the quotation above, the certification is in boldface.

A well-constructed puzzle will always contain such a certification, something like “one label is true and one is false” or “on this island, each person always lies, or always tells the truth”. I went to _What is the Name of this Book?_ to get the example above, and found more than I had bargained for: problem 70 is exactly the annoying boxes problem! Smullyan says:

Good heavens, I can take any number of caskets that I please and put an object in one of them and then write any inscriptions at all on the lids; these sentences won't convey any information whatsoever.
(Page 65)

Had I known that ahead of time, I doubt I would have written this post at all.

But why is this so surprising?

I don't know.

Final notes

16 people correctly said that the treasure was in the green box. This has to be counted as a lucky guess, unacceptable as a solution to a logic puzzle.

One respondent referred me to a similar post on lesswrong.

I did warn you all that the puzzle was annoying.

I started writing this post in October 2007, and then it sat on the shelf until I got around to finding and photographing the boxes. A triumph of procrastination!

by Mark Dominus (mjd@plover.com) at July 03, 2015 12:15 PM

July 01, 2015

Mark Jason Dominus

The annoying boxes puzzle

Here is a logic puzzle. I will present the solution on Friday.

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

Can you figure out which box contains the treasure?

The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:
Starting on 2015-07-03, the solution will be here.

by Mark Dominus (mjd@plover.com) at July 01, 2015 03:13 PM

Philip Wadler

The Thrilling Adventures of Lovelace and Babbage

Sydney Padua explores an alternate universe wherein Ada Lovelace and Charles Babbage complete the Analytical Engine and use it to (at the order of Queen Victoria) fight crime. I've blogged before about the web comic, but the book is even better.

Padua's tome reconciles hilarity with accuracy. I am not normally a fan of footnotes: if it is worth saying, say it inline; don't force your poor reader to break the flow of thought and eye, and leap to the bottom of the page. But here is the glorious exception, where the footnotes supplement, argue with, and occasionally threaten to overflow the comic. Even the footnotes have footnotes: endnotes cite sources for the dialogue, present pocket biographies of Ada and Charles' contemporaries Isambard Kingdom Brunel, Charles Dodgson, and George Boole, quote at length from original sources, and explain the workings of the Analytic Engine. In the midst of an illustrated fantasia riff on Alice in Wonderland, the footnotes pursue an academic war as to whether or not Babbage truly considered Lovelace to be the Empress of Number. Padua makes pursuit of Victorian arcana a thrilling adventure of its own. Highly recommended!


by Philip Wadler (noreply@blogger.com) at July 01, 2015 10:29 AM

Douglas M. Auclair (geophf)

1HaskellADay June 2015 Problems and Solutions

June 2015

  • June 30th, 2015: Count Dracula has just enough time for a quickie, and today's #haskell problem http://lpaste.net/8137099602819022848 
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/n70vAulsh6I/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/n70vAulsh6I?feature=player_embedded" width="320"></iframe>
    Count Dracula: "Vithd you, never a quickie ... alwayz a longie! Bla-blah-blaaaah!" ... and the solution http://lpaste.net/7601734639496986624
  • June 29th, 2015: Toodle-pip! Word-frequency of a novel purportedly written in 'Hinglish, don't you know!' http://lpaste.net/7805322136641339392 Today's #haskell problem That solution is SO my bag!http://lpaste.net/7435942974816518144
  • June 26th, 2015: THUGs hate code duplication. I bet you didn't know that about THUGs. #thuglife With today's #haskell problem, you do. http://lpaste.net/87111690633609216 The solution is awesome, because reasons. http://lpaste.net/3951774515419152384
  • June 25th, 2015: We solve today's #haskell problem like a Thug. A CANADIAN Thug http://lpaste.net/183406472317632512 … #ThugLife When a THUG wants a cup-o-joe, it just makes sense to give'm dat cup-o-joe when he throws down dat Hamilton http://lpaste.net/8960298568350957568 #thuglife
  • June 24th, 2015: Today's #haskell problem shows us Mad Dad is Sad ... http://lpaste.net/1360790418425380864 … ... AND CANADIAN! AND SO ARE YOU! #whendidthathappen
  • June 23rd, 2015: Banana Fish! I don't know what that means, but: http://lpaste.net/4698665561507233792 (I also don't know what map 'a'-"apple" 'b'-"banana" means, either). Dad even got the banana WITH TAXES! http://lpaste.net/51803352903712768 But is Dad happy? Oh, no! See today's problem (forthcoming)
  • June 22nd, 2015: A couple of range-like thingies for today's #haskell problem http://lpaste.net/9214672078085554176 'Thingies' is a technical term. Arrows for ranges? http://lpaste.net/3818460590272151552 Who knew that could be a 'thing'? (Again, technical term. It means: 'thing.')
  • June 19th, 2015: 
♫ Grease is the word,
is the word,
is the word,
that you heard,..
http://lpaste.net/5444203916235374592
... and is today's #haskell problem. #graph 
O! What a tangled web we weave! http://lpaste.net/1406493831142047744 Contracts between corporations #graph Using #neo4j to show complex interrelationships between corporations #haskell
  • June 18th, 2015: Graph owners of companies ... LIKE A BOSS for today's #haskell problem http://lpaste.net/8745167156892663808 def #NSFW-youtube-link: 
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/NisCkxU544c/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/NisCkxU544c?feature=player_embedded" width="320"></iframe>
    Take this #graph and shove it; I don' work here anymore! A solution http://lpaste.net/497988783522709504

  • June 17th, 2015: What does Hannibal Lecter have to do with today's #Haskell problem? http://lpaste.net/3911201767555072000 Well, actually nothing. Good for name-dropping ;)
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/vyGSaTC5rdc/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/vyGSaTC5rdc?feature=player_embedded" width="320"></iframe>
    Ooh! pritti colours! Lines and circles! ME. LIKEY! http://lpaste.net/1108939510487449600 Visualizing relations between companies and their employees in #neo4j #graph database #bigdata

  • June 16th 2015: Business. Commerce. Relationships. And the plot thickens for today's #haskell problem http://lpaste.net/2159896812155043840 You scratched my back, so the solution will scratch yours: http://lpaste.net/6209720607693602816
  • June 15th, 2015: We're told to 'mind our own business.' For today's #haskell problem, however, we don't. http://lpaste.net/409939376974331904 If all the world were 450 businesses ...huh, don't know how to end that couplet, so I'll just share the solution: http://lpaste.net/4134898821270339584
  • June 12th, 2015: Today's Haskell problem is really simple: http://lpaste.net/176873973089304576 Write a Haskell Database. ;)
  • June 11th, 2015: A mapping of a map of categories to various sets of symbols. Not at all a Graph. Nope. Not at all. http://lpaste.net/106990139309293568 So, forewarning: there is wootage to be found in the solution http://lpaste.net/1443717939034324992 
  • June 10th, 2015: FREE LATIN LESSONS with today's #haskell problem! AND curl, but as long as you don't sudo bash you should be okay ... http://lpaste.net/8023684639111512064
  • June 9th, 2015: LET'S PRETEND! that today is yesterday, huh? So 'today's #haskell problem is about Options Tradinghttp://lpaste.net/3308567286981328896 ... not really.
  • June 8th, 2015: Improving the accuracy of the stddev modifier is the topic for today's #haskell problem http://lpaste.net/2181777565994188800
  • June 5th, 2015: Today's #haskell problem is kinda from Haskell by Example http://lpaste.net/1846897956607754240 Maps don't love you like I love you 
<iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/oIIxlgcuQRU/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/oIIxlgcuQRU?feature=player_embedded" width="320"></iframe>
Hey, did you just make a map from a map and a multimap? http://lpaste.net/1944556995998646272 Is that even allowed? Yes, ... yes, it is.
  • June 4th, 2015: Peano's big TOE has a #haskell problem for you today, rollin' on the river http://lpaste.net/8694895204643110912 Types can be ... helpful in modeling solutions. Yeah. http://lpaste.net/6112991888283795456
  • June 3rd, 2015: As we're not going to do switch for today's #haskell problem (Why? BECAUSE I SAID SO), let's deredundancify an array. http://lpaste.net/2725173830396936192 An array by any other name is just a graph http://lpaste.net/6699309431617748992 ... hey, it's possible!
  • June 2nd, 2015: Today's #haskell problem is called 'twixt' and is inspired from a tweet by @jamestanton http://lpaste.net/4168110918607044608 Betwixt a rock and a prime place lies the solution http://lpaste.net/5331587919524134912
  • June 1st, 2015: These factorials are prime for ... primes. Erhm, yeah. http://lpaste.net/6303441488491577344 Today's #haskell problem from @jamestanton

by geophf (noreply@blogger.com) at July 01, 2015 09:38 AM

Thiago Negri

Haskell is just some steps away from Java

Start with Java, then:
  1. Forbid using null;
  2. Use only immutable objects, add "final" modifier to everything;
  3. Swap methods by static functions with the the original "this" as the first argument, e.g. "foo.bar()" turns into "bar(foo)";
  4. Add a lot of features to the type system;
  5. Remove type annotations, i.e. "Foo bar(Foo self)" turns into "bar(self)";
  6. Remove useless parens, i.e. "bar(foo)" turns into "bar foo";
  7. Add call-by-need evaluation;
  8. Done, you have Haskell.
It's not that hard, is it?

One, using null references is a recognized bad practice, see "Null References: The Billion Dollar Mistake." Java 8 already provides the Optional type to stop using nulls.

Two, immutable objects are a win strategy, see posts by Hirondelle Systems, IBM, Yegor, and others.

Three, as you only have immutable objects, there is no reason to use methods instead of static functions, considering you maintain polymorphism (not quite the case for Java, but for the sake of this rant, consider as if it has this feature).

Four, improve the type system. The type system used by Java language misses a lot of features. If you don't feel it, just consider this as an added bonus. When you start using the type system features in your favor, you end up with much better code.

Five, imagine the Java compiler could infer the type of the arguments, so you don't need to type them everywhere. You still have the same static typing language, you just don't need to write the types. Shorter code means less liability to haunt you.

Six, why all those parens? Just drop them. Less code to write, hurray!

Seven, call-by-need just makes a lot of things easier (also makes a lot of things harder), but I really think it is a winner when you talk about productivity. When coding, I feel it a lot easier to express things in terms of values instead of steps (mathematicians have been doing this since long before computers). Expressing things in terms of values in a universe without call-by-need will result in a lot of useless computations, so call-by-need is a must.

Eight, done! This is Haskell. No functors, monads, arrows, categories or lists needed.

Why this post? Well, I don't know. It just occurred to me that if you really go into following good coding practices in Java (e.g. avoid null, use immutable objects), you will eventually feel familiar with functional code. Add some more things to the mix, and you end up with Haskell. I think people feel a bit scared at first contact with Haskell (and family) because of the academic and mathematical atmosphere it has, but in the end it is just a lot of good practices that you are kind of required to comply with.

by Thiago Negri (noreply@blogger.com) at July 01, 2015 01:35 AM

June 30, 2015

Functional Jobs

Senior Developer at Elsen, Inc. (Full-time)

Elsen is building the next generation of market simulation software at the intersection of high performance computing, machine learning, and quantitative finance. We're a small, tight-knit team located in the financial district of downtown Boston.

We are looking for a senior software developer to help extend our infrastructure which is written in Haskell, C, and Python. Although substantial knowledge of Haskell is desired, we are primarily looking for individuals with demonstrated experience in financial modeling and the ability to implement ideas quickly and accurately.

Some things we look for in an candidate:

  • Open source involvement
  • Deep understanding of quantitative modeling
  • PostgreSQL or similar database familiarity
  • Understanding of various parallelism techniques (threads, software transactional memory, GPUs, distributed computing)
  • Technical analysis with ta-lib
  • Use of iteratee Haskell libraries (conduit/pipes)
  • Experience with modern C development
  • NumPy/SciPy/Pandas experience
  • Open to playing complex board games from time to time
  • Overall fun-loving personality and good sense of humor

Get information on how to apply for this position.

June 30, 2015 08:36 PM

Dimitri Sabadie

smoothie-0.3, Bézier curves and new user interface

Bezier curves

It’s been a while I’ve been wanting to do that. Now it’s done! smoothie, a Haskell package for dealing with curves and splines, updated to version 0.3.

That version introduces several changes. If you’re a good programmer, you might already have noticed that the major version got incremented. That means there’re compatibility breaking changes. If you don’t know what I’m talking about, you should definitely read this.

The first – non-breaking – change is that the package now supports Bézier interpolation! I’ve been reading about Bézier curves for a while because there’re very present and important for animation purposes – think of Blender. Feel free to dig in the documentation on hackage for further details.

The second – breaking – change is that the interface has changed, especially the implementation of splines. However, the interface is now simpler and doesn’t require a lot of change in your code if you’ve been using older versions.

Feel free to read the CHANGELOG for technical hints.

As always, tell me what you think of the library, and keep the vibe!

by Dimitri Sabadie (noreply@blogger.com) at June 30, 2015 05:28 PM

June 29, 2015

Dimitri Sabadie

Mac OS X support in al-0.1.4

Support for Mac users!

This will be a short announcement about al, a Haskell wrapper to the OpenAL C library.

Currently, the wrapper has been successfully tested on Linux – at least it works well on my Archlinux distro. I made a little program that reads from an .ogg file and streams the PCM signal to the wrapper – see libvorbis for further details. I’ll release the program later on if I find the spare time.

The wrapper might also work on Windows as long as you have pkg-config installed. I’d be very happy with feedback from people working on Windows. I don’t want anyone be put apart with my packages.

However, I’ve never tested the wrapper on Mac OS X. I guessed it wouldn’t work out of the box because Mac OS X doesn’t use regular libraries to compile and link – that would have been too easy otherwise, and hell, think different right? They use something called a framework. It’s possible to include a framework in a Haskell project by fulfilling the frameworks field in the .cabal file. I received a simple patch to do that – here, and I merged it upstream.

Then, Mac OS X is now officially supported. The release version is the 0.1.4.

About stackage

There’s something else I’d like to discuss. Quickly after the first release of al, I decided to push it onto stackage. Unfortunately, there’s a problem with the package and Ubuntu. For a very dark reason, Ubuntu doesn’t expose anything when invoking pkg-confg --cflags, even if the files are there – on Ubuntu they can be found in /usr/include/AL.

That’s very silly because I don’t want to hardcode the location – it might be something else on other Linux distro. The problem might be related to the OpenAL support in Ubuntu – the .pc file used by pkg-config might be incomplete. So if you experience that kind of issue, you can fix it by passing the path to your OpenAL headers:

cabal install al --extra-include-dirs=/usr/include/AL

If OpenAL is installed somewhere else, consider using:

find / -name al.h

I’ll do my best to quickly fix that issue.

by Dimitri Sabadie (noreply@blogger.com) at June 29, 2015 06:43 PM

Douglas M. Auclair (geophf)

Tabular and Visual Representations of Data using Neo4J

Corporate and Employee Relationships
Both Graphical and Tabular Results

So, there are many ways to view data, and people may have different needs for representing that data, either for visualization (in a graph:node-edges-view) or for tabulation/sorting (in your standard spreadsheet view).

So, can Neo4J cater to both these needs?

Yes, it can.

Scenario 1: Relationships of owners of multiple companies

Let's say I'm doing some data exploration, and I wish to know who has interest/ownership in multiple companies? Why? Well, let's say I'm interested in the Peter-Paul problem: I want to know if Joe, who owns company X is paying company Y for whatever artificial scheme to inflate or to deflate the numbers of either business and therefore profit illegally thereby.

Piece of cake. Neo4J, please show me the owners, sorted by the number of companies owned:

MATCH (o:OWNER)--(p:PERSON)-[r:OWNS]->(c:CORP)
RETURN p.ssn AS Owner, collect(c.name) as Companies, count(r) as Count 
ORDER BY Count DESC


Diagram 1: Owners by Company Ownership

Boom! There you go. Granted, this isn't a very exciting data set, as I did not have many owners owning multiple companies, but there you go.

What does it look like as a graph, however?

MATCH (o:OWNER)--(p:PERSON)-[r:OWNS]->(c:CORP)-[:EMPLOYS]->(p1) 
WHERE p.ssn in [2879,815,239,5879] 
RETURN o,p,c,p1


Diagram 2: Some companies with multiple owners

To me, this is a richer result, because it now shows that owners of more than one company sometimes own shares in companies that have multiple owners. This may yield interesting results when investigating associates who own companies related to you. This was something I didn't see in the tabular result.

Not a weakness of Neo4J: it was a weakness on my part doing the tabular query. I wasn't looking for this result in my query, so the table doesn't show it.

Tellingly, the graph does.

Scenario 2: Contract-relationships of companies 

Let's explore a different path. I wish to know, by company, the contractual-relationships between companies, sorted by companies with the most contractual-relationships on down. How do I do that in Neo4J?

MATCH (c:CORP)-[cc:CONTRACTS]->(c1:CORP) 
RETURN c.name as Contractor, collect(c1.name) as Contractees, count(cc) as Count 
ORDER BY Count DESC


Diagram 3: Contractual-Relationships between companies

This is somewhat more fruitful, it seems. Let's, then, put this up into the graph-view, looking at the top contractor:

MATCH (p:PERSON)--(c:CORP)-[:CONTRACTS*1..2]->(c1:CORP)--(p1:PERSON) 
WHERE c.name in ['YFB'] 
RETURN p,c,c1,p1


Diagram 4: Contractual-Relationships of YFB

Looking at YFB, we can see contractual-relationships 'blossom-out' from it, as it were, and this is just immediate, then distance 1 from that out! If we go out even just distance 1 more in the contracts, the screen fills with employees, so then, again, you have the forest-trees problem where too much data is hiding useful results with data.

Let's prune these trees, then. Do circular relations appear?

MATCH (c:CORP)-[:CONTRACTS*1..5]->(c1:CORP) WHERE c.name in ['YFB'] RETURN c,c1


Diagram 5: Circular Relationship found, but not in YFB! Huh!

Well, would you look at that. This shows the power of the visualization aspect of graph databases. I was examining a hot-spot in corporate trades, YFB, looking for irregularities there. I didn't find any, but as I probed there, a circularity did surface in downstream, unrelated companies: the obvious one being between AZB and MZB, but there's also a circular-relationship that becomes apparent starting with 4ZB, as well. Yes, this particular graph is noisy, but it did materialize an interesting area to explore that may very well have been overlooked with legacy methods of investigation.

Graph Databases.


BAM.

by geophf (noreply@blogger.com) at June 29, 2015 06:25 PM

Philip Wadler

A brief bibliography on parametricity

Henry Story asked HoTT Cafe about parametricity, prompting creation of a handy, short bibliography including Hermida, Reddy, and Robinson; Ahmed; Dreyer; Milewski (artist of the elegant diagram above); and Shulman.

by Philip Wadler (noreply@blogger.com) at June 29, 2015 09:40 AM

Yesod Web Framework

stack support for yesod devel

Since the release of the stack build tool, I think I've received four different requests and bug reports about stack support in Yesod. The sticking point is that yesod devel has not- until now- had support for using stack. The original plan was to wait for Njagi Mwaniki's Google Summer of Code project to finish the new ide-backend based yesod devel. However, demand for this feature was too high, so I'm happy to announce official stack support in yesod-bin-1.4.11.

This blog post should be consider a beta announcement for using Yesod with stack. Please test and report issues. Also, the workflow is not yet perfected. Once we get stack new written and add ide-backend support, things will be much smoother. For now, here's the workflow:

# Install both yesod-bin and cabal-install. Both are still necessary
$ stack install yesod-bin-1.4.11 cabal-install
# Initialize your project
$ stack exec yesod init
$ cd new-directory
# Create stack.yaml
$ stack init
# Build your project to get al dependencies
# Also rebuild yesod-bin with the current GHC, just to be safe
$ stack build yesod-bin-1.4.11 .
# Now run yesod devel
$ stack exec yesod devel

Like I said, this is a little kludgy right now, but will smooth out over time.

Technical details

If you're curious in how I added this support, the commit is really short. And there's not actually anything stack-specific in here, it's just working around a well known limitation in cabal which makes it incompatible with the GHC_PACKAGE_PATH environment variable. All we do in yesod devel is:

  • Detect the GHC_PACKAGE_PATH variable
  • Turn it into --package-db arugments to cabal configure
  • Remove GHC_PACKAGE_PATH from the environment of the cabal process

It would be nice if cabal got this functionality itself in the future, but I believe the current implementation was a design goal of the cabal team.

June 29, 2015 12:00 AM