Joachim Breitner's Homepage

The bootstrappable builds project tries to find ways of building all our software from source, without relying on binary artifacts. A noble goal, and one that is often thwarted by languages with self-hosting compilers, like GHC: In order to build GHC, you need GHC. A Pull Request against nixpkgs, adding first steps of the bootstrapping pipeline, reminded me of the issue with GHC, which I have noted down some thoughts about before and I played around a bit more.

The most promising attempt to bootstrap GHC was done by rekado in 2017. He observed that Hugs is maybe the most recently maintained bootstrappable (since written in C) Haskell compiler, but noticed that “it cannot deal with mutually recursive module dependencies, which is a feature that even the earliest versions of GHC rely on. This means that running a variant of GHC inside of Hugs is not going to work without major changes.” He then tries to bootstrap another very old Haskell compiler (nhc) with Hugs, and makes good but incomplete progress.

This made me wonder: What if Hugs supported mutually recursive modules? Would that make a big difference? Anthony Clayden keeps advocating Hugs as a viable Haskell implementation, so maybe if that was the main blocker, then adding support to Hugs for that is probably not too hard (at least in a compile-the-strongly-connected-component-as-one-unit mode) and worthwhile?

All of GHC in one file?

That reminded me of a situation I was in before, where I had to combine multiple Haskell modules into one before: For my talk “Lock-step simulation is child’s play” I wrote a multi-player game, a simulation environment for it, and a presentation tool around it, all in the CodeWorld programming environment, which supports only a single module. So I hacked the a small tool hs-all-in-one that takes multiple Haskell modules and combines them into one, mangling the names to avoid name clashes.

This made me wonder: Can I turn all of GHC into one module, and compile that?

At this point I have probably left the direct path towards bootstrapping, but I kinda good hooked.

1. Using GHC’s hadrian/ghci tool, I got it to produce the necessary generated files (e.g. from happy grammars) and spit out the lit of modules that make up GHC, which I could feed to hs-all-in-one.

2. It uses haskell-src-exts for parsing, and it was almost able to parse all of that. It has a different opinion about how MultiWayIf should be indented, whether EmptyCase needs {} and issues pretty-printing some promoted values, but otherwise the round-tripping worked fine, and I as able to generate a large file (680,000 loc, 41 MB) that passes GHC’s parser.

3. It also uses haskell-names to resolve names.

   This library is less up-to-date with various Haskell features, so I added support for renaming in some pragmas (ANN, SPECIALIZE), pattern signatures etc.

   For my previous use-case I could just combine all the imports, knowing that I would not introduce conflicts. For GHC, this is far from true: Some modules import Data.Map.Strict, others Data.Map.Lazy, and yet others introduce names that clash with stuff imported from the prelude… so I had to change the tool to fully qualify all imported values. This isn’t so bad, I can do that using haskell-names, if I somehow know what all the modules in base, containers, transformers and array export.

   The haskell-names library itself comes with a hard-coded database of base exports, but it is incomplete and doesn’t help me with, say, containers.

   I then wrote a little parser for the .txt files that haddock produces for the benefit of hoogle, and that are conveniently installed along the packages (at least on nix). This would have been great, if these files wouldn’t simply omit all reexported entities! I added some manual hacks (Data.Map has the same exports as Data.IntMap; Prelude exports all entities as known by haskell-names, but those that are also exported from Data.List, use the symbol from there…)

   I played this game of whack-a-mole for a while, solving many of the problems that GHC’s renamer reports, but eventually stopped to write this blog post. I am fairly confident that this could be pulled through, though.

Back to bootstrapping

So what if we could pull this through? We’d have a very large code file that GHC may be able to compile to produce a ghc binary without exhausting my RAM. But that doesn’t help with bootstrapping yet.

If lack of support for recursive modules is all that Hugs is missing, we’d be done indeed. But quite contrary, it is probably the least of our worries, given that contemporary GHC uses many many other features not supported by Hugs.

Some of them a syntactic and can easily be rewritten to more normal Haskell in a preprocessing step (e.g. MultiWayIf).

Others are deep and hard (GADTs, Pattern synonyms, Type Families), and prohibit attempting to compile a current version of GHC (even if its all one module) with Hugs. So one would certainly have to go back in time and find a version of GHC that is not yet using all these features. For example, the first use of GADTs was introduced by Simon Marlow in 2011, so this suggests going back to at least GHC 7.0.4, maybe earlier.

Still, being able to mangle the source code before passing it to Hugs is probably a useful thing. This poses the question whether Hugs can compile such a tool; in particular, is it capable of compiling haskell-src-exts, which I am not too optimistic about either. Did someone check this already?

So one plan of attack could be

1. Identify an old version of GHC that

   • One can use to bootstrap subsequent versions until today.
   • Is old enough to use as few features not supported by hugs as possible.
   • Is still new enough so that one can obtain a compatible toolchain.

2. Wrangle the build system to tell you which files to compile, with which preprocessor flags etc.

3. Boostrap all pre-processing tools used by GHC (cpphs or use plan cpp, happy, alex).

4. For every language feature not supported by Hugs, either

   • Implement it in Hugs,
   • Manually edit the source code to avoid compiling the problematic code, if it is optional (e.g. in an optimization pass)
   • Rewrite the problematic code
   • Write a pre-processing tool (like the one above) that compiles the feature away

5. Similarly, since Hugs probably ships a base that is different than what GHC, or the libraries used by GHC expects, either adjust Hugs’ base, or modify the GHC code that uses it.

My actual plan, though, for now is to throw these thoughts out, maybe make some noise on Discourse, Mastodon, Twitter and lobste.rs, and then let it sit and hope someone else will pick it up.

Just a small googleable note for those trying to set this up too:

If you try to access your “My Files” mailbox.org WebDav storage using rclone, then the URL is not just https://dav.mailbox.org/servlet/webdav.infostore/, as written on the mailbox.org documentation, but actually https://dav.mailbox.org/servlet/webdav.infostore/Userstore/Your Name.

(You can start with https://dav.mailbox.org/servlet/webdav.infostore/ and then use rclone ls to find out the full path, but then it may be more convenient to change it to point directly to the “My Files” space where you can actually create files.)

For a little more than two decades, I have been running one or two dedicated servers for a fair number of services. At some time or the other, it was hosting

• A web server for my personal website
• A web server for various private and professional webpages for friends and family
• An email server with IMAP, SMTP, Spam filtering, for me and family
• A mailing list server for various free software project
• A DNS server
• A Half-Life and Counter Strike server, with a statistics web page
• The web page for my Counter Strike clan, running on a custom Perl-and-Mysql based CMS
• The web page for my high school class, running on the same system (this was before everyone used, or had used, Facebook, and even supported tagging people on images…)
• A Docbook-and-SVN-based documentation management system that my brother and I built and even sold to a few customers.
• A custom SVN-, Perl and Template-Toolkit based static site generating CMS, before that was cool, also with one or two actual customers.
• A SVN- and later Git based site for collaborative editing of math and computer science lecture notes; back then there was no Overleaf
• A Jabber server
• The backend for an online adaption of the board game “Sim Serim” which got the author to gift me the real thing
• An SVN server
• A darcs server
• A git server
• A tool to track darcs patches that were submitted by mailing lists
• A blog aggregator (a “planet”) for friends, and one for Ghana’s Free Software community
• An Owncloud instance for family
• Virtual machines maintained by friends, to share resources more cheaply
• A OpenVPN and later tinc based VPN for my machines
• Jobs that RSS feeds to IMAP (using feed2imap and later feed2imap-go)
• Jobs that send email greetings to a friend of mine that I have collected from his wedding guests, and are now delivered at decreasing rate over the next decades.
• Online questionnaires to gather data for a genealogy project
• Jobs that send an email with a daily summary of family events from that date.
• A Django app to organize a larger family gathering
• Multiple Mediawiki instances
• A freenet node and a tor node
• Code that demonstrated the Cross-site authentication attack
• … and probably more stuff that I don’t remember anymore

It’s not you, it’s me

Running this kind of service on my own was great fun and a huge learning experience, and in some cases at that time the only way to have a certain feature. But in recent years my interests shifted a bit, more into Programming Languages Theory (and practice) than Devops, and I was no longer paying attention as much as these services require. This gave me a bad conscience, especially in terms of security updates.

Especially running your own email server, while still possible, isn’t fire-and-forget: One has to stay on top of spam protection measures, both on the receiving end (spamassassin etc.) as well as when sending email (DKIM, configuring mailing lists to rewrite sender etc.)

Also some family members were commercially relying on these servers and services working, which was no longer tenable.

Weaning off

Therefore, more than a year ago, I decided to wind this down. Turns out that getting rid of responsibilities takes at least as long as taking them on, especially if your “customers” are content and a move to something else is but an annoyance. But last weekend I was finally able to turn the machines, called quimby and fry, off.

Many of the services above were already no longer active when I started the weaning off (Jabber, Freenet, Tor). So what happened to the rest?

• For emails, we all moved to https://mailbox.org. Happy to pay for such a crucial service.
• For the mailing lists, especially for the Tip-Toi-Hacking project , https://jpberlin.de/ has decent enough rates that I don’t feel bad for paying for it.
• Managing DNS is made super easy by dnscontrol; I’m using Hetzner’s DNS servers, but thanks to that tool that does not matter a lot
• For those websites that are static enough, Github pages is nice. This includes the lecture notes site.
• For those websites that need a little bit of server-side logic, e.g. for complex redirects and normalization procedures, or access control, but no state, I found that netlify introduced their Edge functions feature just in time. This was crucial for my main website.
• I got rid of the backend of the two-player game Sum Serum completely, by using WebRTC. In terms of hosting, it is now just a boring static website, which is the best kind of website.
• I converted all SVN and Darcs repositories to git, and pushed them to GitHub.
• Although I was mildly proud to have kept the websites of my high school class and Counter Strike clan live and functional for many years after anyone stopped caring about them, I decided it is silly to keep doing that. I briefly thought about entombing that running system in a locked down virtual machine or so, but in the end simply used wget to create a static mirror of them, which is now hosted on netlify (using Edge Functions to restrict public access to a few pages).

In the end, I was not able to get rid of all services, so there is still a server running for me (smaller now, and virtual):

• My photo album, https://bilder.joachim-breitner.de/, which is a bit too big for something like netlify.
• Some dumb static webspace used by a family member’s business for internal reasons, which likewise is a bit too large for something like netlify or github actions, and not as critical as other sites.
• The feed2imap jobs
• For one Mediawiki instanced used for a genealogy project of a relative of mine I could not find a suitable hosted alternative. However, it is HTTP-AUTH-password-protected, so I am a bit less worried about staying on top of security updates for this PHP-drive site.
• Also, I am still running the daily email job from the genealogy project, but now through nullmailer and Amazon SNS, to worry a bit less about the intricacies of modern email.

Debian → Nix

I took this opportunity to set up a new server for the residual services. I have been using Debian since 2001 and was a Debian Developer from 2003 to 2022, and it is a great operating system and a great project.

But after learning about Nix at DFINITY, and using NixOS on my laptop for almost two years, managing a system in a non-declarative way simply feels … wrong. Similar to programming in a non-functional programming language.

Hence I have shut down my Debian-based systems (two virtual machines called quimby and fry and the surrounding Dom0 freddy – my machines are named after Simpsons side kicks and (sometimes) Futurama characters), and am using the NixOS-based aarch64 host richard (because of the [“Nix” in the name]) instead.

Because it seemed useful, and it seems it did not exist yet, I created a small tool called git-multisect. You point it to a git repo, give it a version range and a command to run, and it will list those commits that affect the output of the command.

Here is an example (with a slightly complex invocation):

$ git-multisect.py \
	-C ~/build/nixpkgs \
	-f $(nix flake metadata ~/nixos --json|jq -r ".locks.nodes[.locks.nodes[.locks.root].inputs.nixpkgs].locked.rev") \
	-t release-22.11 \
	-c 'nix path-info --derivation '\
	   '~/nixos#nixosConfigurations.richard.config.system.build.toplevel '\
	   '--no-update-lock-file '\
	   '--override-input nixpkgs ~/"build/nixpkgs?rev=$REV"' \
	--hide-stderr --log-option=--pretty=medium
Found 39 commits
[39 total,  0 relevant,  0 irrelevant,  0 skipped, 39 unknown] inspecing 2fb7d74 ...
[39 total,  0 relevant,  0 irrelevant,  0 skipped, 39 unknown] inspecing 569163e ...
[39 total,  0 relevant,  0 irrelevant,  0 skipped, 39 unknown] inspecing 5642ce8 ...
[39 total,  0 relevant,  0 irrelevant,  0 skipped, 39 unknown] inspecing e0c8cf8 ...
[39 total,  0 relevant,  1 irrelevant,  8 skipped, 30 unknown] inspecing 89d0361 ...
[39 total,  0 relevant,  1 irrelevant,  8 skipped, 30 unknown] inspecing d1c7e63 ...
[39 total,  0 relevant,  2 irrelevant,  9 skipped, 28 unknown] inspecing e6d5772 ...
[39 total,  0 relevant,  3 irrelevant,  9 skipped, 27 unknown] inspecing a099526 ...
[39 total,  1 relevant,  4 irrelevant,  9 skipped, 25 unknown] inspecing 854312a ...
[39 total,  1 relevant,  5 irrelevant, 10 skipped, 23 unknown] inspecing 95043dc ...
[39 total,  1 relevant,  6 irrelevant, 10 skipped, 22 unknown] inspecing 0cf4274 ...
[39 total,  2 relevant,  8 irrelevant, 29 skipped,  0 unknown] done

commit a0995268af8ba0336a81344a3bf6a50d6d6481b2
Author: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Date:   Sat Feb 18 10:45:11 2023 -0800

    linux_{5_15,6_1}: revert patch to fix Equinix Metal bonded networking with `ice` driver (#216955)
…
commit 0cf4274b5d06325bd16dbf879a30981bc283e58a
Merge: 95043dc713d 532f3aa6052
Author: Pierre Bourdon <delroth@gmail.com>
Date:   Sun Feb 19 23:37:48 2023 +0900

    Merge pull request #217121 from NixOS/backport-216463-to-release-22.11

    [Backport release-22.11] sudo: 1.9.12p2 -> 1.9.13

As you can see it tries to be clever to not even look at commits that come between two commits where the output is equal (like git-bisect).

Over at https://github.com/nomeata/git-multisect you’ll find more explanations and examples. Hope you’ll maybe remember this when you find you’ll need it, and that it will prove to be useful.

A few times last year I was asked to help out with some software project – debugging a particularly gnarly nix issue, helping with GHC internals or reviewing Canister code of applications running on the Internet Computer. Usually, these are relatively small jobs, at least reasonably interesting, and it was often friends that approached me.

So I do want to help.

But I did not want to help for free. Incentives matter, and I wanted to incentivize careful use of my time. And of course I like to see my work valued. So normally, one would just charge an hourly fee.

But having to go through all the necessary legalese (setting up a contract, maybe an NDA, thinking about taxes and liabilities, possibly getting permission from the current employer) tilts the scale and would not made it worth it for me anymore.

But instead of just turning it down, a few times now already I used the following model: pro-charity consulting, where you still pay for what you get, but you don’t pay me, but instead a charity.

The rules of pro-charity consulting

The rough rules are as follows:

• There is no contract. I trust you and you trust me, else we wouldn’t even be doing this.
• There is no liability. You probably have a rough idea of what I can deliver and you trust me, so you don’t get to sue me if I screw up.
• There is (usually) no NDA. Of course I’ll keep your secrets, but again you don’t get to sue me if I screw up.
• I tell you about my usual hourly rate if this was a commercial agreement. (This may depend a lot on the field I’m helping you in.)
• Afterwards I’ll also let you know how much time I have spend on helping you.
• You’ll make a donation on a charity of our choosing. We’ll pick something that we both find worth supporting.
• You can donate whatever the work was worth to you, but the expectation is that it shouldn’t be cheaper for you than if you’d have hired me commercially. (Unless I failed to fulfill your expectations.)
• Legally, the donation is by you (e.g. you get to keep any tax benefits).
• Morally, it is by me. For example if donations can come with a message (like on https://donate.openstreetmap.org/) it would be appreciated to mention me.
• According to the German saying “Tue Gutes und rede darüber!” we both get to brag about this donation (target charity, amount, client, kind of work), e.g. on Blogs, Mastodon, Twitter, unless we have a different agreement. See below for some examples.

I’m writing the rules out here so that I can just point to this blog post when I next have to explain this scheme.

Pro-charity gigs so far

• April 2022: 3000€ to the Haskell Foundation for helping the Active Group with a GHC Plugin issue (my tweet, their tweet)
• August 2022: 50€ to the NixOS Foundation for helping FinDeck with a Nix issue (my tweet)
• September 2022: 1400€ to Reporters without Borders for helping StalkedICP by reviewing their Motoko code (my tweet, their tweet)
• September 2022: 1100€ to Amnesty International for helping btcflower by reviewing their Motoko code (their tweet)
• January 2023: 1050$ to Mediciens sans Borders for helping finterest.ooo by reviewing their Motoko code
• March 2023: 1046$ to UNICEF for helping CycleOps by reviewing their Motoko code (my toot, my tweet, their tweet)

For over two decades I have maintained a personal dedicated server, and hosted a fair number of websites, such as my homepage, various projects, sites of friends and family, and during its heyday even servers for DNS, email, mailing lists, Jabber, cloud storage…

But it turns out just because interests shift a bit, such running services don’t simply disappear, but keep running, just less well maintained, and then become a burdensome responsibility. So over the last year I have been moving them, one by one, off my server and elsewhere™.

Most websites are static and can easily be hosted on something convenient like Github Pages or netlify. Some are “mostly static” and require a bit more work (I might blog about that some other time), but still doable. But I had one website that I thought will be hard to host elsewhere:

On https://sumserum.nomeata.de/ you can play a small abstract two-player game. It’s implementing the mechanics of “Sim Serim” by Heinrich Glumpler, and I built it out of a whim 9 years ago, after gifting it away and then wanting to play it. I later did get my own copy of the game, when the author discovered the online version and sent me the real thing.

You can play Sum Serum locally, then it is simply a static webpage with a bit of JavaScript code. But you can also play it with a friend remotely. It connects via WebSockets to a small NodeJS service, which makes the connection and relays messages. It works nicely, but “running a WebSocket service” is usually not part of these simple static-website-from-git services, so this was getting into the way of (eventually) decomissioning my server.

But web technology has advanced, and WebRTC, which allows browsers to talk to each other, has become widely available. So indeed, I found the trystero JS libray which provides a very simple API to connect with someone else over the internet, and using instead of my little WebSocket service was a relatively small change. Now the Sum Serum code is a purely static webpage that I can very easily host on netlify! Neat!

Granted, there are still servers involved to make the connection, as the library is using the BitTorrent network to find the peers. But as far as I am concered, that is nothing I need to worry about. Furthermore, trystero is quite easy to use, so maybe I can create more simply fun multi-use interactive thingies, now that I know I don’t have to worry about hosting a backend.

I’m on the train back from MuniHac, where I gave a talk about the rec-def library that I have excessively blogged about recently (here, here, here and here). I got quite flattering comments about that talk, so if you want to see if they were sincere, I suggest you watch the recording of “Getting recursive definitions off their bottoms” (but it’s not necessary for the following).

After the talk, Franz Thoma approached me and told me a story of how we was once implementing the game Minesweeper in Haskell, and in particular the part of the logic where, after the user has uncovered a field, the game would automatically uncover all fields that are next to a “neutral” field, i.e. one with zero adjacent bombs. He was using a comonadic data structure, which makes a “context-dependent parallel computation” such as uncovering one field quite natural, and was hoping that using a suitable fix-point operator, he can elegantly obtain not just the next step, but directly the result of recursively uncovering all these fields. But, much to his disappointment, that did not work out: Due to the recursion inherent in that definition, a knot-tying fixed-point operator will lead to a cyclic definition.

He was wondering if the rec-def library could have helped him, and we sat down to find out, and this is the tale of this blog post. I will avoid the comonadic abstractions and program it more naively, though, to not lose too many readers along the way. Maybe read Chris Penner’s blog post and Finch’s functional pearl “Getting a Quick Fix on Comonads” if you are curious about that angle.

Minesweeper setup

Let’s start with defining a suitable data type for the grid of the minesweeper board. I’ll use the Array data type, it’s Ix-based indexing is quite useful for grids:

import Data.Array

type C = (Int,Int)
type Grid a = Array C a

The library lacks a function to generate an array from a generating function, but it is easy to add:

genArray :: Ix i => (i,i) -> (i -> e) -> Array i e
genArray r f = listArray r $ map f $ range r

Let’s also fix the size of the board, as a pair of lower and upper bounds (this is the format that the Ix type class needs):

size :: (C,C)
size = ((0,0), (3,3))

Now board is simply a grid of boolean values, with True indicating that a bomb is there:

type Board = Grid Bool

board1 :: Board
board1 = listArray size
  [ False, False, False, False
  , True,  False, False, False
  , True,  False, False, False
  , False, False, False, False
  ]

It would be nice to be able to see these board in a nicer way. So let us write A function that prints a grid, including a frame, given a function that prints something for each coordinate. Together with a function that prints a bomb (as *), we can print the board:

pGrid :: (C -> String) -> String
pGrid p = unlines
    [ concat [ p' (y,x) | x <- [lx-1 .. ux+1] ]
    | y  <- [ly-1 .. uy+1] ]
  where
    ((lx,ly),(ux,uy)) = size

    p' c | inRange size c = p c
    p'  _ = "#"

pBombs :: Board -> String
pBombs b = pGrid $ \c -> if b ! c then "*" else " "

The expression b ! c looks up a the coordinate in the array, and is True when there is a bomb at that coordinate.

So here is our board, with two bombs:

ghci> putStrLn $ pBombs board1
######
#    #
#*   #
#*   #
#    #
######

But that’s not what we want to show to the user: Every field should have have a number that indicates the number of bombs in the surrounding fields. To that end, we first define a function that takes a coordinate, and returns all adjacent coordinates. This also takes care of the border, using inRange:

neighbors :: C -> [C]
neighbors (x,y) =
    [ c
    | (dx, dy) <- range ((-1,-1), (1,1))
    , (dx, dy) /= (0,0)
    , let c = (x + dx, y + dy)
    , inRange size c
    ]

With that, we can calculate what to display in each cell – a bomb, or a number:

data H = Bomb | Hint Int deriving Eq

hint :: Board -> C -> H
hint b c | b ! c = Bomb
hint b c = Hint $ sum [ 1 | c' <- neighbors c, b ! c' ]

With a suitable printing function, we can now see the full board:

hint :: Board -> C -> H
hint b c | b ! c = Bomb
hint b c = Hint $ sum [ 1 | c' <- neighbors c, b ! c' ]

pCell :: Board -> C -> String
pCell b c = case hint b c of
    Bomb -> "*"
    Hint 0 -> " "
    Hint n -> show n

pBoard :: Board -> String
pBoard b = pGrid (pCell b)

And here it is:

ghci> putStrLn $ pBoard board1
######
#11  #
#*2  #
#*2  #
#11  #
######

Next we have to add masks: We need to keep track of which fields the user already sees. We again use a grid of booleans, and define a function to print a board with the masked fields hidden behind ?:

type Mask = Grid Bool

mask1 :: Mask
mask1 = listArray size
  [ True,  True,  True,  False
  , False, False, False, False
  , False, False, False, False
  , False, False, False, False
  ]

pMasked :: Board -> Mask -> String
pMasked b m = pGrid $ \c -> if m ! c then pCell b c else "?"

So this is what the user would see

ghci> putStrLn $ pMasked board1 mask1
######
#11 ?#
#????#
#????#
#????#
######

Uncovering some fields

With that setup in place, we now implement the piece of logic we care about: Uncovering all fields that are next to a neutral field. Here is the first attempt:

solve0 :: Board -> Mask -> Mask
solve0 b m0 = m1
  where
    m1 :: Mask
    m1 = genArray size $ \c ->
      m0 ! c || or [ m0 ! c' | c' <- neighbors c, hint b c' == Hint 0 ]

The idea is that we calculate the new mask m1 from the old one m0 by the following logic: A field is visible if it was visible before (m0 ! c), or if any of its neighboring, neutral fields are visible.

This works so far: I uncovered the three fields next to the one neutral visible field:

ghci> putStrLn $ pMasked board1 $ solve0 board1 mask1
######
#11  #
#?2  #
#????#
#????#
######

But that’s not quite what we want: We want to keep doing that to uncover all fields.

Uncovering all fields

So what happens if we change the logic to: A field is visible if it was visible before (m0 ! c), or if any of its neighboring, neutral fields will be visible.

In the code, this is just a single character change: Instead of looking at m0 to see if a neighbor is visible, we look at m1:

solve1 :: Board -> Mask -> Mask
solve1 b m0 = m1
  where
    m1 :: Mask
    m1 = genArray size $ \c ->
      m0 ! c || or [ m1 ! c' | c' <- neighbors c, hint b c' == Hint 0 ]

(This is roughly what happened when Franz started to use the kfix comonadic fixed-point operator in his code, I believe.)

Does it work? It seems so:

ghci> putStrLn $ pMasked board1 $ solve1 board1 mask1
######
#11  #
#?2  #
#?2  #
#?1  #
######

Amazing, isn’t it!

Unfortunately, it seems to work by accident. If I start with a different mask:

mask2 :: Mask
mask2 = listArray size
  [ True,  True,  False, False
  , False, False, False, False
  , False, False, False, False
  , False, False, False, True
  ]

which looks as follows:

ghci> putStrLn $ pMasked board1 mask2
######
#11??#
#????#
#????#
#??? #
######

Then our solve1 function does not work, and just sits there:

ghci> putStrLn $ pMasked board1 $ solve1 board1 mask2
######
#11^CInterrupted.

Why did it work before, but now now?

It fails to work because as the code tries to figure out if a field, it needs to know if the next field will be uncovered. But to figure that out, it needs to know if the present field will be uncovered. With the normal boolean connectives (|| and or), this does not make progress.

It worked with mask1 more or less by accident: None of the fields on in the first column don’t have neutral neighbors, so nothing happens there. And for all the fields in the third and forth column, the code will know for sure that they will be uncovered based on their upper neighbors, which come first in the neighbors list, and due to the short-circuting properties of ||, it doesn’t have to look at the later cells, and the vicious cycle is avoided.

rec-def to the rescue

This is where rec-def comes in: By using the RBool type in m1 instead of plain Bool, the recursive self-reference is not a problem, and it simply works:

import qualified Data.Recursive.Bool as RB

solve2 :: Board -> Mask -> Mask
solve2 b m0 = fmap RB.get m1
  where
    m1 :: Grid RB.RBool
    m1 = genArray size $ \c ->
      RB.mk (m0 ! c) RB.|| RB.or [ m1 ! c' | c' <- neighbors c, hint b c' == Hint 0 ]

Note that I did not change the algorithm, or the self-reference through m1; I just replaced Bool with RBool, || with RB.|| and or with RB.or. And used RB.get at the end to get a normal boolean out. And 🥁, here we go:

ghci> putStrLn $ pMasked board1 $ solve2 board1 mask2
######
#11  #
#?2  #
#?2  #
#?1  #
######

That’s the end of this repetition of “let’s look at a tying-the-knot-problem and see how rec-def helps”, which always end up a bit anti-climatic because it “just works”, at least in these cases. Hope you enjoyed it nevertheless.

More ICFP-inspired experiments using the rec-def library: In Norman Ramsey’s very nice talk about his Functional Pearl “Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control Flow”, he had the following slide showing the equation for the dominators of a node in a graph:

He said “it’s ICFP and I wanted to say the dominance relation has a beautiful set of equations … you can read all these algorithms how to compute this, but the concept is simple”.

This made me wonder: If the concept is simple and this formula is beautiful – shouldn’t this be sufficient for the Haskell programmer to obtain the dominator relation, without reading all those algorithms?

Before we start, we have to clarify the formula a bit: If a node is an entry node (no predecessors) then the big intersection is over the empty set, and that is not a well-defined concept. For these nodes, we need that big intersection to return the empty set, as entry nodes are not dominated by any other node. (Let’s assume that the entry nodes are exactly those with no predecessors.)

Let’s try, first using plain Haskell data structures. We begin by implementing this big intersection operator on Data.Set, and also a function to find the predecessors of a node in a graph:

import qualified Data.Set as S
import qualified Data.Map as M

intersections :: [S.Set Int] -> S.Set Int
intersections [] = S.empty
intersections xs = foldl1 S.intersection xs

preds :: [(Int,Int)] -> M.Map Int [Int]
preds edges = M.fromListWith (<>) $
    [ (v1, [])   | (v1, _) <- edges ] ++ -- to make the map total
    [ (v2, [v1]) | (v1, v2) <- edges ]

Now we can write down the formula that Norman gave, quite elegantly:

domintors1 :: [(Int,Int)] -> M.Map Int [Int]
domintors1 edges = fmap S.toList doms
  where
    doms :: M.Map Int (S.Set Int)
    doms = M.mapWithKey
        (\v vs -> S.insert v (intersections [ doms M.! v' | v' <- vs]))
        (preds edges)

Does this work? It seems it does:

ghci> domintors1 []
fromList []
ghci> domintors1 [(1,2)]
fromList [(1,[1]),(2,[1,2])]
ghci> domintors1 [(1,2),(1,3),(2,4),(3,4)]
fromList [(1,[1]),(2,[1,2]),(3,[1,3]),(4,[1,4])]

But – not surprising if you have read my previous blog posts – it falls over once we have recursion:

ghci> domintors1 [(1,2),(1,3),(2,4),(3,4),(4,3)]
fromList [(1,[1]),(2,[1,2]),(3,^CInterrupted.

So let us reimplement it with Data.Recursive.Set.

import qualified Data.Recursive.Set as RS

intersections :: [RS.RSet Int] -> RS.RSet Int
intersections [] = RS.empty
intersections xs = foldl1 RS.intersection xs

domintors2 :: [(Int,Int)] -> M.Map Int [Int]
domintors2 edges = fmap (S.toList . RS.get) doms
  where
    doms :: M.Map Int (RS.RSet Int)
    doms = M.mapWithKey
        (\v vs -> RS.insert v (intersections [ doms M.! v' | v' <- vs]))
        (preds edges)

The hope is that we can simply replace the operations, and that now it can suddenly handle cyclic graphs as well. Let’s see:

ghci> domintors2 [(1,2),(1,3),(2,4),(3,4),(4,3)]
fromList [(1,[1]),(2,[1,2]),(3,[3]),(4,[4])]

It does! Well, it does return a result… but it looks strange. Clearly node 3 and 4 are also dominated by 1, but the result does not reflect that.

But the result is a solution to Norman’s equation. Was the equation wrong? No, but we failed to notice that the desired solution is the largest, not the smallest. And Data.Recursive.Set calculates, as documented, the least fixed point.

What now? Until the library has code for RDualSet a, we can work around this by using the dual formula to calculate the non-dominators. To do this, we

• use union instead of intersection
• delete instead of insert,
• S.empty, use the set of all nodes (which requires some extra plumbing)
• subtract the result from the set of all nodes to get the dominators

and thus the code turns into:

unions' :: S.Set Int -> [RS.RSet Int] -> RS.RSet Int
unions' univ [] = mkR univ
unions' _ xs = foldl1 RS.union xs

domintors3 :: [(Int,Int)] -> M.Map Int [Int]
domintors3 edges = fmap (S.toList . S.difference nodes . RS.get) nonDoms
  where
    nodes = S.fromList [v | (v1,v2) <- edges, v <- [v1,v2]]
    nonDoms :: M.Map Int (RS.RSet Int)
    nonDoms = M.mapWithKey
        (\v vs -> RS.delete v (unions' nodes [ nonDoms M.! v' | v' <- vs]))
        (preds edges)

And with this, now we do get the correct result:

ghci> domintors3 [(1,2),(1,3),(2,4),(3,4),(4,3)]
fromList [(1,[1]),(2,[1,2]),(3,[1,3]),(4,[1,4])]

We worked a little bit on how to express the “beautiful formula” to Haskell, but at no point did we have to think about how to solve it. To me, this is the essence of declarative programming.

At this week’s International Conference on Functional Programming I showed my rec-def Haskell library to a few people. As this crowd appreciates writing compilers, and example from the realm of program analysis is quite compelling.

To Throw or not to throw

Here is our little toy language to analyze: It has variables, lambdas and applications, non-recursive (lazy) let bindings and, so that we have something to analyze, a way to throw and to catch exceptions:

type Var = String

data Exp
  = Var Var
  | Throw
  | Catch Exp
  | Lam Var Exp
  | App Exp Exp
  | Let Var Exp Exp

Given such an expression, we would like to know whether it might throw an exception. Such an analysis is easy to write: We traverse the syntax tree, remembering in the env which of the variables may throw an exception:

canThrow1 :: Exp -> Bool
canThrow1 = go M.empty
  where
    go :: M.Map Var Bool -> Exp -> Bool
    go env (Var v)       = env M.! v
    go env Throw         = True
    go env (Catch e)     = False
    go env (Lam v e)     = go (M.insert v False env) e
    go env (App e1 e2)   = go env e1 || go env e2
    go env (Let v e1 e2) = go env' e2
      where
        env_bind = M.singleton v (go env e1)
        env' = M.union env_bind env

The most interesting case is the one for Let, where we extend the environment env with the information about the additional variable env_bind, which is calculated from analyzing the right-hand side e1.

So far so good:

ghci> someVal = Lam "y" (Var "y")
ghci> canThrow1 $ Throw
True
ghci> canThrow1 $ Let "x" Throw someVal
False
ghci> canThrow1 $ Let "x" Throw (App (Var "x") someVal)
True

Let it rec

To spice things up, let us add a recursive let to the language:

data Exp
  …
  | LetRec [(Var, Exp)] Exp

How can we support this new constructor in canThrow1? Let use naively follow the pattern used for Let: Calculate the analysis information for the variables in env_bind, extend the environment with that, and pass it down:

    go env (LetRec binds e) = go env' e
      where
        env_bind = M.fromList [ (v, go env' e) | (v,e) <- binds ]
        env' = M.union env_bind env

Note that, crucially, we use env', and not just env, when analyzing the right-hand sides. It has to be that way, as all the variables are in scope in all the right-hand sides.

In a strict language, such a mutually recursive definition, where env_bind uses env' which uses env_bind is basically unthinkable. But in a lazy language like Haskell, it might just work.

Unfortunately, it works only as long as the recursive bindings are not actually recursive, or if they are recursive, they are not used:

ghci> canThrow1 $ LetRec [("x", Throw)] (Var "x")
True
ghci> canThrow1 $ LetRec [("x", App (Var "y") someVal), ("y", Throw)] (Var "x")
True
ghci> canThrow1 $ LetRec [("x", App (Var "x") someVal), ("y", Throw)] (Var "y")
True

But with genuine recursion, it does not work, and simply goes into a recursive cycle:

ghci> canThrow1 $ LetRec [("x", App (Var "x") someVal), ("y", Throw)] (Var "x")
^CInterrupted.

That is disappointing! Do we really have to toss that code and somehow do an explicit fixed-point calculation here? Obscuring our nice declarative code? And possibly having to repeat work (such as traversing the syntax tree) many times that we should only have to do once?

rec-def to the rescue

Not with rec-def! Using RBool from Data.Recursive.Bool instead of Bool, we can write the exact same code, as follows:

import qualified Data.Recursive.Bool as RB

canThrow2 :: Exp -> Bool
canThrow2 = RB.get . go M.empty
  where
    go :: M.Map Var RBool -> Exp -> R Bool
    go env (Var v)       = env M.! v
    go env Throw         = RB.true
    go env (Catch e)     = RB.false
    go env (Lam v e)     = go (M.insert v RB.false env) e
    go env (App e1 e2)   = go env e1 RB.|| go env e2
    go env (Let v e1 e2) = go env' e2
      where
        env_bind = M.singleton v (go env e1)
        env' = M.union env_bind env
    go env (LetRec binds e) = go env' e
      where
        env_bind = M.fromList [ (v, go env' e) | (v,e) <- binds ]
        env' = M.union env_bind env

And it works!

ghci> canThrow2 $ LetRec [("x", App (Var "x") someVal), ("y", Throw)] (Var "x")
False
ghci> canThrow2 $ LetRec [("x", App (Var "x") Throw), ("y", Throw)] (Var "x")
True

I find this much more pleasing than the explicit naive fix-pointing you might do otherwise, where you stabilize the result at each LetRec independently: Not only is all that extra work hidden from the programmer, but now also a single traversal of the syntax tree creates, thanks to the laziness, a graph of RBool values, which are then solved “under the hood”.

The issue with x=x

There is one downside worth mentioning: canThrow2 fails to produce a result in case we hit x=x:

ghci> canThrow2 $ LetRec [("x", Var "x")] (Var "x")
^CInterrupted.

This is, after all the syntax tree has been processed and all the map lookups have been resolved, equivalent to

ghci> let x = x in RB.get (x :: RBool)
^CInterrupted.

which also does not work. The rec-def machinery can only kick in if at least one of its function is used on any such cycle, even if it is just a form of identity (which I ~ought to add to the library~ since have added to the library):

ghci> idR x = RB.false ||| x
ghci> let x = idR x in getR (x :: R Bool)
False

And indeed, if I insert a call to idR in the line

        env_bind = M.fromList [ (v, idR (go env' e)) | (v,e) <- binds ]

then our analyzer will no longer stumble over these nasty recursive equations:

ghci> canThrow2 $ LetRec [("x", Var "x")] (Var "x")
False

It is a bit disappointing to have to do that, but I do not see a better way yet. I guess the def-rec library expects the programmer to have a similar level of sophistication as other tie-the-know tricks with laziness (where you also have to ensure that your definitions are productive and that the sharing is not accidentally lost).

A week ago I wrote about the rec-def Haskell library, which allows you to write more recursive definitions, such as in this small example:

let s1 = RS.insert 23 s2
    s2 = RS.insert 42 s1
in RS.get s1

This will not loop (as it would if you’d just used Data.Set), but rather correctly return the set S.fromList [23,42]. See the previous blog post for more examples and discussion of the user-facing side of this.

For quick reference, these are the types of the functions involved here:

insert :: Ord a => a -> RSet a -> RSet a
get :: RSet a -> Set a

The type of s1 and s2 above is not Set Int, but rather RSet Int, and in this post I’ll explain how RSet works internally.

Propagators, in general

The conceptual model behind an recursive equation like above is

• There are a multiple cells that can hold values of an underlying type (here Set)
• These cells have relations that explain how the values in the cells should relate to each other
• After registering all the relations, some form of solving happens.
• If the solving succeeds, we can read off the values from the cells, and they should satisfy the registered relation.

This is sometimes called a propagator network, and is a quite general model that can support different kind of relations (e.g. equalities, inequalities, functions), there can be various solving strategies (iterative fixed-points, algebraic solution, unification, etc.) and information can flow on along the edges (and hyper-edges) possibly in multiple directions.

For our purposes, we only care about propagator networks where all relations are functional, so they have a single output cell that is declared to be a function of multiple (possibly zero) input cells, without affecting these input cells. Furthermore, every cell is the output of exactly one such relation.

IO-infested propagator interfaces

This suggests that an implementation of such a propagator network could provide an interface with the following three operations:

• Functions to declare cells
• Functions to declare relations
• Functions to read values off cells

This is clearly an imperative interface, so we’ll see monads, and we’ll simply use IO. So concretely for our small example above, we might expect

data Cell a
newCell :: IO (Cell a)
-- declareInsert x c1 c2 declares that the value of c1 ought to be S.insert x c2
declareInsert :: Ord a => a -> Cell a -> Cell a -> IO ()
getCell :: Cell a -> IO (Set a)

There is no need for an explicit “solve” function: solving can happen when declareInsert or getCell is called – as a User I do not care about that.

You might be curious about the implementation of newCell, declareInsert and getCell, but I have to disappoint you: This is not the topic of this article. Instead, I want to discuss how to turn this IO-infested interface into the pure interface seen above?

Pure, but too strict

Obviously, we have to get rid of the IO somehow, and have to use unsafePerformIO :: IO a -> a somehow. This dangerous function creates a pure-looking value that, when used the first time, will run the IO-action and turn into that action’s result.

So maybe we can simply write the following:

type RSet a = Cell a
insert x c2 = unsafePerformIO $ do
  c1 <- newCell
  declareInsert x c1 c2
  return c1
get c = unsafePerformIO $
  getCell c

Indeed, the types line up, but if we try to use that code, nothing will happen. Our insert is too strict to be used recursively: It requires the value of c2 (as it is passed to declareInsert, which we assume to be strict in its arguments) before it can return c1, so the recursive example at the top of this post will not make any progress.

Pure, lazy, but forgetful

To work around this, maybe it suffices if we do not run declareInsert right away, but just remember that we have to do it eventually? So let’s introduce a new data type for RSet a that contains not just the cell (Cell a), but also an action that we still have to run before getting a value:

data RSet a = RSet (Cell a) (IO ())
insert x r2 = unsafePerformIO $ do
  c1 <- newCell
  let todo = do
        let (RSet c2 _) = r2
        declareInsert x c1 c2
  return (RSet c1 todo)
get (RSet c todo) = unsafePerformIO $ do
  todo
  getCell c

This is better: insert is now lazy in its arguments (for this it is crucial to pattern-match on RSet only inside the todo code, not in the pattern of insert!) This means that our recursive code above does not get stuck right away.

Pure, lazy, but runs in circles

But it is still pretty bad: Note that we do not run get s2 in the example above, so that cell’s todo, which would declareInsert 42, will never run. This cannot work! We have to (eventually) run the declaration code from all involved cells before we can use getCell!

We can try to run the todo action of all the dependencies as part of a cell’s todo action:

data RSet a = RSet (Cell a) (IO ())
insert x r2 = unsafePerformIO $ do
  c1 <- newCell
  let todo = do
        let (RSet c2 todo2) = r2
        declareInsert x c1 c2
        todo2
  return (RSet c1 todo)
get (RSet c todo) = unsafePerformIO $ do
  todo
  getCell c

Now we certainly won’t forget to run the second cell’s todo action, so that is good. But that cell’s todo action will run the first cell’s todo action, and that again the second cell’s, and so on.

Pure, lazy, terminating, but not thread safe

This is silly: We only need (and should!) run that code once! So let’s keep track of whether we ran it already:

data RSet a = RSet (Cell a) (IO ()) (IORef Bool)
insert x r2 = unsafePerformIO $ do
  c1 <- newCell
  done <- newIORef False
  let todo = do
        is_done <- readIORef done
        unless is_done $ do
          writeIORef done True
          let (RSet c2 todo2 _) = r2
          declareInsert x c1 c2
          todo2
  return (RSet c1 todo done)
get (RSet c todo _) = unsafePerformIO $ do
  todo
  getCell c

Ah, much better: It works! Our call to get c1 will trigger the first cell’s todo action, which will mark it as done before calling the second cell’s todo action. When that now invokes the first cell’s todo action, it is already marked done and we break the cycle, and by the time we reach getCell, all relations have been correctly registered.

In a single-threaded world, this would be all good and fine, but we have to worry about multiple threads running get concurrently, on the same or on different cells.

In fact, because we use unsafePerformIO, we have to worry about this even when the program is not using threads.

And the above code has problems. Imagine a second call to get c1 while the first one has already marked it as done, but has not finished processing all the dependencies yet: It will call getCell before all relations are registered, which is bad.

Recursive do-once IO actions

Making this thread-safe seems to be possible, but would clutter both the code and this blog post. So let’s hide that problem behind a nice and clean interface. Maybe there will be a separate blog post about its implementation (let me know if you are curious), or you can inspect the code in System.IO.RecThunk module yourself). The interface is simply

data Thunk
thunk :: IO [Thunk] -> IO Thunk
force :: Thunk -> IO ()

and the idea is that thunk act will defer the action act until the thunk is passed to force for the first time, and force will not return until the action has been performed (possibly waiting if another thread is doing that at the moment), and also until the actions of all the thunks returned by act have performed, recursively, without running into cycles.

We can use this in our definition of RSet and get to the final, working solution:

data RSet a = RSet (Cell a) Thunk
insert x r2 = unsafePerformIO $ do
  c1 <- newCell
  t1 <- thunk $ do
    let (RSet c2 t2) = r2
    declareInsert x c1 c2
    return [t2]
  return (RSet c1 t1)
get (RSet c t) = unsafePerformIO $ do
  force t
  getCell c

This snippet captures the essential ideas behind rec-def:

• Use laziness to allow recursive definition to describe the propagator graph naturally
• Use a form of “explicit thunk” to register the propagator graph relations at the right time (not too early/strict, not too late)

And that’s all?

The actual implementation in rec-def has a few more moving parts.

In particular, it tries to support different value types (not just sets), possibly with different implementations, and even mixing them (e.g. in member :: Ord a => a -> RSet a -> RBool), so the generic code is in Data.Propagator.Purify, and supports various propagators underneath. The type RSet is then just a newtype around that, defined in Data.Recursive.Internal to maintain the safety of the abstraction,

I went back and forth on a few variants of the design here, including one where there was a generic R type constructor (R (Set a), R Bool etc.), but then monomorphic interface seems simpler.

Does it really work?

The big remaining question is certainly: Is this really safe and pure? Does it still behave like Haskell?

The answer to these questions certainly depends on the underlying propagator implementation. But it also depends on what we actually mean by “safe and pure”? For example, do we expect the Static Argument Transformation be semantics preserving? Or is it allowed to turn undefined values into defined ones (as it does here)?

I am unsure myself yet, so I’ll defer this discussion to a separate blog post, after I hopefully had good discussions about this here at ICFP 2022 in Ljubljana. If you are around and want to discuss, please hit me up!