QuickCheck vs SmallCheck

QuickCheck and SmallCheck are the two classical libraries for property testing in Haskell. There are newer developments, like SmartCheck and Hedgehog, but I haven’t tried them much yet.

So here is my take on the comparative strengths and weaknesses of the current versions of QuickCheck and SmallCheck (2.11.3 and 1.1.4, respectively). Being the maintainer of SmallCheck, I am obviously somewhat biased towards it. But quite often I would prefer QuickCheck to SmallCheck for a specific task. It also sometimes happens that I think QuickCheck would work better in principle for a given task, but in practice SmallCheck is more convenient for that task — usually it has to do with generic instances or failure reporting. So here are the considerations I take into account when choosing between the two.

If you do not know much about QuickCheck and/or SmallCheck, the main difference between them is that QuickCheck generates random test cases, whereas SmallCheck enumerates test cases exhaustively up to some depth. Some (though not all) of the pros and cons come from this fundamental difference in paradigms.

Advantages of QuickCheck

Control over the number of tests/execution time

With SmallCheck, the number of tests is usually exponential in their depth. Say, when enumerating trees (from Data.Tree), depth 5 gives you 189 tests in less then 0.01s, while depth 6 gives 6479 tests in 4s. If you only have the patience to run 1000 tests, you have to settle for 189. QuickCheck, on the other hand, allows you to set the exact number of tests independently from their depth (which is called size in QuickCheck).

Floating-point numbers

SmallCheck has instances for floating-point numbers, e.g.

> listSeries 5 :: [Positive Float]
[1.0,2.0,0.5,4.0,0.25,8.0,0.125,16.0,3.0,6.25e-2,6.0,1.5,12.0,0.75,24.0,0.375,48.0,0.1875]

These are probably enough if you need to fill some fractional field in a data type, but the logic of your functions doesn’t depend on the number in a complex way.

But if you are testing any truly numerical code (say, matrix operations or physics simulation), it is much more useful to have QuickCheck generate random floating-point numbers.

Advantages of SmallCheck

Generic deriving

If you have a couple of types that rarely change, writing the instances by hand may not a big deal.

Often, especially when writing tests for commercial code, there is a big number of nested algebraic data types. And even if you have the patience to write the instances, they will become incomplete the next time a constructor is added to one of the types (and the compiler won’t warn you).

So it is essential to be able to derive most of the instances. SmallCheck has had generic instances since 2011, thanks to the contribution from Bas van Dijk. QuickCheck still does not have them (github issue).

There is a separate package, generic-arbitrary, but it doesn’t seem to support recursive data types. The recursive types also seem to be the reason why QuickCheck itself doesn’t have the generic implementation.

The solution to the recursive type problem is straightforward: reduce the depth (size) every time you descend into a nested type. As an example, here’s an instance for trees from Data.Tree:

instance Arbitrary a => Arbitrary (Tree a) where
  arbitrary = scale (\n -> max (n-1) 0) $
    Node <$> arbitrary <*> arbitrary

This approach is not ideal (your size may get down to 0 too quickly), but IMO it is better than no generic instances at all.

Failure reporting

Say we have a property

prop x = reverse (reverse x) == x

By default, both SmallCheck and QuickCheck only tell you the generated values that led to the failure (i.e. x). But I would also like to know why the test failed — in this case, what reverse (reverse x) was.

There is a StackOverflow question about this with two answers, neither of which is perfect.

Edward Z. Yang says:

Because QuickCheck gives you the inputs to the function, and because the code under test is pure (it is, right?), you can just feed those inputs to the function and get the result. This is more flexible, because with those inputs you can also repeatedly test with tweaks to the original function until it’s correct.

There are many reasons why this may not work:

1. The code may not be pure by design — both SmallCheck and QuickCheck are capable of testing IO code.
2. The code may be intended to be pure, but the very bug you are trying to fix may lead to it being impure/non-deterministic.
3. Copy-pasting values may not be very convenient: think large matrices.
4. Also, strings produced by Show do not always map back to the original values effortlessly. E.g. Maps, Sets, and Vectors all result in fromList [...] when shown. If you have several of them in the same structure, you’ll have to disambiguate those fromLists.

The other answer, by Paul Johnson, gives a working solution (using MkResult), but it is rather unwieldy, and you have to include the parameter values manually if you need them.

In SmallCheck, you can return Either String String instead of Bool, where the Strings give explanation for failure and success, respectively. For example, this property

prop_reverse :: [Int] -> Bool
prop_reverse x = reverse x == x

results in the message

there exists [0,1] such that
  condition is false

But we can change the property to explain itself

prop_reverse :: [Int] -> Either String String
prop_reverse x =
  if reverse x == x
    then Right "Match"
    else Left $ "reverse x == " ++ show (reverse x)

which results in

there exists [0,1] such that
  reverse x = [1,0]

Better than shrinking

QuickCheck tends to produce complex counterexamples and then tries to shrink them to find simpler ones. While shrinking does lead to somewhat simpler examples, they are usually not minimal. Also, it’s on you to implement the shrinking function for your own types.

Because SmallCheck enumerates the values in order, from smaller to bigger, it automatically produces the minimal example.

Determinism and exhaustiveness

Because QuickCheck generates its examples randomly, the set of test cases your property is tested on is rather arbitrary. (It also changes from run to run by default, though this can be fixed by suppplying a fixed seed.)

Sometimes that’s good: if you have a high- or infinite-dimensional space of possibilities, all you can hope for is to test on a few diverse samples from that space. But other times, that space is narrow, and it’s better to test deterministically and exhaustively.

May 25, 2018 08:00 PM

Building packages outside snapshots

A question popped up the other day on Stack Overflow, and I thought I'd write up in a bit more detail how to solve it. There are some packages that we'd like to install, but which are not in Stackage snapshots. Trying to build them may end up with an error message like this:

$ stack install idris

Error: While constructing the build plan, the following exceptions were encountered:

In the dependencies for idris-1.2.0:
    ansi-terminal-0.8.0.4 from stack configuration does not match <0.8  (latest matching version is 0.7.1.1)
needed since idris is a build target.

Some different approaches to resolving this:

  * Set 'allow-newer: true' to ignore all version constraints and build anyway.

  * Consider trying 'stack solver', which uses the cabal-install solver to attempt to find some working build
    configuration. This can be convenient when dealing with many complicated constraint errors, but results may be
    unpredictable.

  * Recommended action: try adding the following to your extra-deps in /home/michael/.stack/global-project/stack.yaml:

- ansi-terminal-0.7.1.1

Plan construction failed.

(Note: depending on when you run these commands, view the pages below, and local settings, you may get different output.)

What this is saying is that Stack is currently configured to use a snapshot which includes ansi-terminal-0.8.0.4. However, idris-1.2.0 has an upper bound on ansi-terminal that prevents that usage. There are probably two solutions to this problem that you'd think of (especially since the error message mentions them):

1. Ignore the dependency bounds and hope for the best with --allow-newer
2. Use a dependency solver (via cabal-install) to try to come up with a complete new build plan

Both of these approaches run the risk of coming up with a build plan that doesn't work, resulting in wasted time ending in a failed compilation. However, in some cases, there's another option in some cases. If I look at the package page for Idris on Stackage, I see the following:

It turns out that Idris 1.2.0 already appeared in a Stackage snapshot. At the very least, it was in LTS Haskell 10.10 and Stackage Nightly 2018-03-10. We can follow that link at the bottom to get a complete list of snapshots Idris appears in.

With this in mind, it's easy to build Idris:

$ stack install --resolver lts-10.10 idris

This gives you a way to tell Stack about a known good build plan and avoid spinning your wheels. This approach works best for packages providing executables you want to use, as opposed to libraries you want to build on. For the latter, this approach would likely end up pointing you at multiple conflicting snapshots. Overall, the best bet there is to get the missing packages added to Stackage.

You may ask: couldn't Stack automatically do this for me? Well, it can't guess what you want in this case. It would be ambiguous if you're trying to build a package with your currently selected snapshot so that it's available to your code, for example, versus just creating an executable. But it would also be possible to add a flag like --select-latest-snapshot or similar to automatically choose the snapshot with the best chance of building the package. stack init already does something like this.

May 23, 2018 01:06 PM

The diameter of German+English

Languages never map directly onto each other. The English word fresh can mean frisch or frech, but frish can also be cool. Jumping from one words to another like this yields entertaining sequences that take you to completely different things. Here is one I came up with:

frech – fresh – frish – cool – abweisend – dismissive – wegwerfend – trashing – verhauend – banging – Geklopfe – knocking – …

And I could go on … but how far? So here is a little experiment I ran:

1. I obtained a German-English dictionary. Conveniently, after registration, you can get dict.cc’s translation file, which is simply a text file with three columns: German, English, Word form.

2. I wrote a program that takes these words and first canonicalizes them a bit: Removing attributes like [ugs.] [regional], {f}, the to in front of verbs and other embellishment.

3. I created the undirected, bipartite graph of all these words. This is a pretty big graph – ~750k words in each language, a million edges. A path in this graph is precisely a sequence like the one above.

4. In this graph, I tried to find a diameter. The diameter of a graph is the longest path between two nodes that you cannot connect with a shorter path.

Because the graph is big (and my code maybe not fully optimized), it ran a few hours, but here it is: The English expression be annoyed by sb. and the German noun Icterus are related by 55 translations. Here is the full list:

• be annoyed by sb.
• durch jdn. verärgert sein
• be vexed with sb.
• auf jdn. böse sein
• be angry with sb.
• jdm. böse sein
• have a grudge against sb.
• jdm. grollen
• bear sb. a grudge
• jdm. etw. nachtragen
• hold sth. against sb.
• jdm. etw. anlasten
• charge sb. with sth.
• jdn. mit etw. [Dat.] betrauen
• entrust sb. with sth.
• jdm. etw. anvertrauen
• entrust sth. to sb.
• jdm. etw. befehlen
• tell sb. to do sth.
• jdn. etw. heißen
• call sb. names
• jdn. beschimpfen
• abuse sb.
• jdn. traktieren
• pester sb.
• jdn. belästigen
• accost sb.
• jdn. ansprechen
• address oneself to sb.
• sich an jdn. wenden
• approach
• erreichen
• hit
• Treffer
• direct hit
• Volltreffer
• bullseye
• Hahnenfuß-ähnlicher Wassernabel
• pennywort
• Mauer-Zimbelkraut
• Aaron's beard
• Großkelchiges Johanniskraut
• Jerusalem star
• Austernpflanze
• goatsbeard
• Geißbart
• goatee
• Ziegenbart
• buckhorn plantain
• Breitwegerich / Breit-Wegerich
• birdseed
• Acker-Senf / Ackersenf
• yellows
• Gelbsucht
• icterus
• Icterus

Pretty neat!

So what next?

I could try to obtain an even longer chain by forgetting whether a word is English or German (and lower-casing everything), thus allowing wild jumps like hat – hut – hütte – lodge.

Or write a tool where you can enter two arbitrary words and it finds such a path between them, if there exists one. Unfortunately, it seems that the terms of the dict.cc data dump would not allow me to create such a tool as a web site (but maybe I can ask).

Or I could throw in additional languages!

What would you do?

by Joachim Breitner (mail@joachim-breitner.de) at May 23, 2018 06:35 AM

Ertugrul Söylemez: 1985-2018

I do not know many details, but IRC user mupf joined the #haskell-ops channel yesterday to tell us that Ertugrul Söylemez died unexpectedly on May 12. This is a great loss for the Haskell community. Going variously by mm_freak, ertes, ertesx or ertes-w, Ertugrul has been very active on the #haskell IRC channel for almost 11 years—since June 2007—and he will be remembered as a knowledgeable, generous, and patient teacher. In addition to teaching on IRC, he wrote several tutorials, such as this one on foldr and this one on monoids. The thing Ertugrul was probably most well-known for in the Haskell community was his netwire FRP package, which he had developed since 2011, and more recently its successor package wires. I think it is no exaggeration to say that his work on and insights into FRP helped shape a whole generation of approaches.

He will be greatly missed. I will leave the comments open for anyone to share memories of Ertugrul, his writing, or his code.

by Brent at May 22, 2018 02:02 AM

How I evaluate Haskell packages

<html xmlns="http://www.w3.org/1999/xhtml"><head> <meta content="text/html; charset=utf-8" http-equiv="Content-Type"/> <meta content="text/css" http-equiv="Content-Style-Type"/> <meta content="pandoc" name="generator"/> <style type="text/css">code{white-space: pre;}</style></head><body>

This post summarizes the rough heuristics that I use for evaluating Haskell packages. Usually I use these rules of thumb when:

• choosing between multiple similar packages
• deciding whether to depend on a package at all

Some of these guidelines work for other programming languages, too, but some of them are unique to Haskell. Even if you are a veteran programmer in another language you still might find some useful tidbits here when approaching the Haskell ecosystem for the first time.

I've organized the metrics I use into five categories:

• "Large positive" - Things that impress me
• "Small positive" - Positive features that make me more likely to adopt
• "Irrelevant" - Things I never pay attention to when judging package quality
• "Small negative" - Things that turn me off
• "Large negative" - Huge red flags

Large positive

• High quality documentation

  Excellent documentation is one of the strongest signals of maintainer commitment to a package. Extensive documentation is very expensive to keep up to date with a package because documentation is difficult to machine check in general.

  You can definitely have the build check that type signatures or doctests are correct, but anything more elaborate usually requires human intervention to keep up to date.

  Disclaimer: I'm biased here because I'm a huge proponent of documenting things well.

• Impossible to use incorrectly

  One of the nice features of Haskell is that you can use the type system to make impossible states unrepresentable or enforce invariants to guarantee proper use. I strongly prefer libraries that take advantage of this to rule out errors at compile time so that I can sleep soundly at night knowing that my work built on top of a solid foundation.

• On Stackage

  All packages on Stackage are guaranteed to build and have a known good build plan (called a Stackage "resolver") that both stack and cabal can reuse. All packages on Stackage "play nice" with each other, which greatly reduces the total cost of ownership for depending on these Haskell packages.

  Being on Stackage is also a good signal that the package is maintained by somebody because packages require some upkeep to ensure that they continue to build against the latest version of other packages.

• Competitive Benchmarks

  I strongly prefer packages that post benchmarks comparing their package to their competitors. Such a comparison implies that the author went to the trouble of using and understanding alternative packages and using them idiomatically. That perspective often improves the quality and design of their own package.

  Also, competitive benchmarks are rare and require significant upkeep, so they double as strong signal of maintainer commitment.

• 100+ reverse dependencies

  You can check the packages that depend on a given package (a.k.a. "reverse dependencies") using the following URL:

  https://packdeps.haskellers.com/reverse/${package-name}

  Packages that have a 100 or more reverse dependencies have substantial buy-in from the Haskell ecosystem and are safe to depend on. You're also likely to depend on these packages anyway through your transitive dependencies.

  (Suggested by: Tim Humphries)

Small positive

• One complete example

  This means that the package has one "end-to-end" example showing how all the pieces fit together. I prefer packages that do this because they don't force me to waste a large amount of time reinventing what the author could have communicated in a much shorter amount of time.

  You would be surprised how many Haskell packages have extensive Haddock coverage but still lack that one overarching example showing how to use the package.

• 100+ downloads in last 30 days

  Download statistics are not a very strong signal of activity on Hackage since most Haskell build tools (i.e. cabal, stack, Nix) will cache dependencies. These tools also don't require frequent cache invalidations like some other build tools which shall not be named.

  However, having 100+ downloads in the last 30 days is a reasonable signal that enough people were recently able to get the package working. That means that if anything goes wrong then I assume that there must be some solution or workaround.

• Maintained/used/endorsed by a company

  I think this is a pretty obvious signal. Similar to download metrics, this implies that somebody was able to extract something commercially valuable from this package.

• Pure or mostly pure API

  Packages that provide pure APIs are easier to test and easier to integrate into a code base. This reduces the total cost of ownership for that dependency.

• Upper bounds on dependencies that are up to date

  I'm not going to take a strong stance on the "great PVP war" in this post. All I will note is that if a package has upper bounds that are up to date then that is a good sign that the package is actively maintained (whether or not you agree that upper bounds are a good idea).

  In other words, upper bounds are one way that a package author can "virtue signal" that they have the time and resources to maintain a package.

Irrelevant

• On Hackage

  Many people new to Haskell ecosystem assume that there is some sort of quality bar to be on Hackage just because Hackage is not GitHub. There is no such quality bar; anybody can obtain a Hackage account and upload their packages (even joke packages).

• Stability field

  The stability field of packages fell out of fashion years ago. Also, in my experience people are poor judges of whether or not their own packages will be stable. I prefer to look at the frequency of releases and how often they are breaking changes as empirical evidence of a package's stability.

• Version number

  First off, make sure you understand PVP. The key bit is that the first two components of a version number represent the major version of a package. That means that if the package goes from version 1.0 to 1.1 then that signals just as much of a breaking change to the API as if the package went from version 1.0 to 2.0. The usual rule of thumb for interpreting version numbers is:

  X.Y.Z.A
  ↑ ↑ ↑ ↑
  | | | |
  | | | Non-breaking change that is invisible (i.e. documentation or refactor)
  | | | Note: Not all packages use a fourth number in their versions
  | | |
  | | Non-breaking change
  | |
  | Breaking change without fanfare
  |
  Breaking change with great fanfare

  The absolute version number basically does not matter. There are many widely used and mature packages on Hackage that are still version 0.*. This can be jarring coming from another language ecosystem where people expect a mature package to be at least version 1.0.

• Votes

  Hackage 2 supports voting on packages but I've never consulted a package's votes when deciding whether or not to adopt. I prefer quality signals that cannot be easily faked or gamed.

• Tests

  I've never checked whether or not I'm using a well-tested package or not. Maybe that's not a good idea, but I'm being honest about how I evaluate packages.

  This probably comes as a surprise to a person coming to Haskell from another language ecosystem, especially a dynamically typed language that rely heavily on tests to ensure quality. Haskell programmers lean much more on the type system to enforce and audit quality. For example, type signatures show me at a glance if a package is overusing side effects or deals with too many states or corner cases that I need to account for.

Small negative

• Upper bounds that are not up to date

  The other nice thing about adding upper bounds to a package is that they also accurately signal when a package is no longer maintained. They require constant "gardening" to keep up to date so when an author abandons a package they naturally transform from a positive signal into a negative signal simply by virtue of inaction.

• Large dependency footprint

  This used to be a much bigger issue before the advent of Stackage. People would aggressively trim their dependency trees out of fear that one bad dependency would cause them to waste hours finding a valid build plan.

  I still spend some time these days trying to minimize my dependency footprint, mainly so that I don't need to respond as often to breaking changes in my immediate dependencies. However, this is a relative minor concern in comparison to how bad things used to be.

• Uses linked lists inappropriately

  The #1 source of Haskell performance degradation is keeping too many objects on the heap and linked lists trash your heap if you materialize the entire list into memory (as opposed to streaming over the list so that you only materialize at most one element at any time).

  I try to avoid dependencies that use linked lists unless they are the optimal data structure because I will be paying the price for those dependencies every time my program runs a garbage collection.

• Frequent breaking API changes

  Breaking API changes are not a really big deal in Haskell due to the strong type system. Breaking API changes are mainly a minor maintenance burden: if you depend on a library that releases breaking changes all the time you usually only need to spend a few minutes updating your package to build against the latest API.

  This matters more if you maintain a large number of packages or if you have a huge number of dependencies, but if you don't then this is a relatively small concern.

• Idiosyncratic behavior

  "Idiosyncratic" means that the package author does something weird unique to them. Some examples include using a private utility library or custom Prelude that nobody else uses or naming all of their classes C and all their types T (you know who you are).

  When I see this I assume that the package author has no interest in building consensus or being a "well-behaved" member of the Haskell ecosystem. That sort of package is less likely to respond or adapt to user feedback.

Large negative

• Uses String inappropriately

  This is a special case of "Uses linked lists inappropriately" since the default String type in Haskell is stored as a linked list of characters.

  Strings tend to be rather large linked lists of characters that are commonly fully materialized. This implies that even modest use of them will add lots of objects to the heap and tax the garbage collector.

• No documentation

  If I see no documentation on a package I "nope" right out of there. I assume that if a maintainer does not have time to document the package then they do not have time to address user feedback.

• Not on Hackage

  I assume that if a package is not on Hackage that the maintainer has no interest in supporting or maintaining the package. The bar for adding a package to Hackage is so low that the absence of a package on Hackage is a red flag.

  Note that this does not imply that packages on Hackage will be supported. There are packages on Hackage where the author does not intend to support the package.

  Note: a reader pointed out that this is confusing given that I treat "on Hackage" as "Irrelevant". Perhaps another way to phrase this is that being on Hackage is a necessary but not sufficient signal of maintainer support.

• Maintainer ignoring pull requests

  This is obviously the clearest sign that a maintainer does not respond to user feedback. There are fewer things that upset me more than a maintainer that completely ignores volunteers who submit pull requests to fix bugs.

Conclusion

Hopefully that gives you some quick and dirty heuristics you can use when evaluating Haskell packages for the first time. If you think that I missed something important just let me know and I'll update this post.

</body></html>

by Gabriel Gonzalez (noreply@blogger.com) at May 22, 2018 12:56 AM

Frontend Engineer at Trivium Real Estate (Full-time)

TriviumRE is an investor-backed, data-mining startup for the commercial real estate industry; we're making data entry jobs less painful. Our MVP is moments away from launching and customers are queuing to take it for a spin. As such, we're growing our team to tackle the challenges ahead.

What about the team? We have a high emphasis on continual learning. If you're not learning something new on the job its time for a new one. Our tech stack reflects this; Haskell and Elm are the main languages. We don't mind if its your first exposure to either. We're not afraid of experimenting or making mistakes. The most important quality of anyone on our team is their ability to learn and teach.

Since we're still young, working with us means you have a lot of influence in shaping the culture and direction of the company. You'll also a chance to grow your skill set faster than somewhere else.

The product We're building a data mining tool that can explicitly learn a relational data model based on sample inputs. It's radically improves data entry and data cleaning for financial analysts. Customers have loved our demos and we're understandably coy in our public descriptions.

Front-End Engineer

This is for someone who:

• is comfortable in functional programming, especially Elm; and
• is experienced shipping front-end software to production; and
• has empathy for users and loves friendly UX; and
• has an eagerness to learn and willingness to share knowledge.

Benefits

• £50-70k DOE. + Equity.
• Highly intelligent, supportive team.
• 20+ holidays per year.
• Support for conferences & other tech related education.

A Typical Day

• Start off writing a feature that requires elm-ports. These can be tricky, so you pair with another developer who has shipped such code before.

• After lunch you're requested to review a Pull Request that fixes a bug you accidentally introduced a couple weeks back. There's no blame, instead some discussion about how our tests and review process could have caught this earlier.

• The afternoon is spent with the Product guys around a whiteboard. You're helping them sketch out a realistic wire-frame for a feature we plan to deliver in a couple of weeks.

Some Tech we like:

We're more interested in a willingness and ability to learn than what you currently know. But in case you're interested in the stack we're using:

• Haskell
• Elm
• PostgreSQL
• Javascript
• Python / scikit-learn
• Tensorflow / Deep learning
• AWS
• CircleCI
• Automated Testing

Get information on how to apply for this position.

May 21, 2018 04:42 PM

More about disabling standard I/O buffering

In yesterday's article I described a simple and useful feature that could have been added to the standard I/O library, to allow an environment variable to override the default buffering behavior. This would allow the invoker of a program to request that the program change its buffering behavior even if the program itself didn't provide an option specifically for doing that.

Simon Tatham directed me to the GNU Coreutils stdbuf command which does something of this sort. It is rather like the pseudo-tty-pipe program I described, but instead of using the pseudo-tty hack I suggested, it works by forcing the child program to dynamically load a custom replacement for stdio. There appears to be a very similar command in FreeBSD.

Roderick Schertler pointed out that Dan Bernstein wrote a utility program, pty, in 1990, atop which my pseuto-tty-pipe program could easily be built; or maybe its ptybandage utility is exactly what I wanted. Jonathan de Boyne Pollard has a page explaining it in detail, and related packages.

A later version of pty is still available. Here's M. Bernstein's blurb about it:

ptyget is a universal pseudo-terminal interface. It is designed to be used by any program that needs a pty.

ptyget can also serve as a wrapper to improve the behavior of existing programs. For example, ptybandage telnet is like telnet but can be put into a pipeline. nobuf grep is like grep but won't block-buffer if it's redirected.

Previous pty-allocating programs — rlogind, telnetd, sshd, xterm, screen, emacs, expect, etc. — have caused dozens of security problems. There are two fundamental reasons for this. First, these programs are installed setuid root so that they can allocate ptys; this turns every little bug in hundreds of thousands of lines of code into a potential security hole. Second, these programs are not careful enough to protect the pty from access by other users.

ptyget solves both of these problems. All the privileged code is in one tiny program. This program guarantees that one user can't touch another user's pty.

ptyget is a complete rewrite of pty 4.0, my previous pty-allocating package. pty 4.0's session management features have been split off into a separate package, sess.

Finally, Leonardo Taccari informed me that NetBSD's stdio actually has the environment variable feature I was asking for! Christos Zoulas suggested adding stdbuf similar to the GNU and FreeBSD implementations, but the NetBSD people observed, as I did, that it would be simpler to just control stdio directly with an environment variable. Here's the relevant part of the NetBSD setbuf(3) man page:

The default buffer settings can be overwritten per descriptor (STDBUFn) where n is the numeric value of the file descriptor represented by the stream, or for all descriptors (STDBUF). The environment variable value is a letter followed by an optional numeric value indicating the size of the buffer. Valid sizes range from 0B to 1MB. Valid letters are:

U unbuffered

L line buffered

F fully buffered

Here's the discussion from the NetBSD tech-userlevel mailing list. The actual patch looks almost exactly the way I imagined it would.

Mariusz Ceier pointed out that there is an ancient bug report in glibc suggesting essentially the same environment variable mechanism that I suggested and that was adopted in NetBSD. The suggestion was firmly and summarily rejected. (“Hell, no … this is a terrible idea.”) Interesting wrinkle: the bug report was submitted by Pádraig Brady, who subsequently wrote the stdbuf command I described above.

Thank you, Gentle Readers!

by Mark Dominus (mjd@plover.com) at May 21, 2018 03:19 PM

Proposal for turning off standard I/O buffering

Some Unix commands, such as grep, will have a command-line flag to say that you want to turn off the buffering that is normally done in the standard I/O library. Some just try to guess what you probably want. Every command is a little different and if the command you want doesn't have the flag you need, you are basically out of luck.

Maybe I should explain the putative use case here. You have some command (or pipeline) X that will produce dribbles of data at uncertain intervals. If you run it at the terminal, you see each dribble timely, as it appears. But if you put X into a pipeline, say with

    X | tee ...

or

    X | grep ...

then the dribbles are buffered and only come out of X when an entire block is ready to be written, and the dribbles could be very old before the downstream part of the pipeline, including yourself, sees them. Because this is happening in user space inside of X, there is not a damn thing anyone farther downstream can do about it. The only escape is if X has some mode in which it turns off standard I/O buffering. Since standard I/O buffering is on by default, there is a good chance that the author of X did not think to affirmatively add this feature.

Note that adding the --unbuffered flag to the downstream grep does not solve the problem; grep will produce its own output timely, but it's still getting its input from X after a long delay.

One could imagine a program which would interpose a pseudo-tty, and make X think it is writing to a terminal, and then the standard I/O library would stay in line-buffered mode by default. Instead of running

    X | tee some-file | ...

or whatever, one would do

    pseudo-tty-pipe -c X | tee some-file | ...

which allocates a pseudo-tty device, attaches standard output to it, and forks. The child runs X, which dribbles timely into the pseudo-tty while the parent runs a read loop to remove dribbles from the master end of the TTY and copy them timely into the pipe. This would work. Although tee itself also has no --unbuffered flag so you might even have to:

    pseudo-tty-pipe -c X | pseudo-tty-pipe -c 'tee some-file' | ...

I don't think such a program exists, and anyway, this is all ridiculous, a ridiculous abuse of the standard I/O library's buffering behavior: we want line buffering, the library will only give it to us if the process is attached to a TTY device, so we fake up a TTY just to fool stdio into giving us what we want. And why? Simply because stdio has no way to explicitly say what we want.

But it could easily expose this behavior as a controllable feature. Currently there is a branch in the library that says how to set up a buffering mode when a stream is opened for the first time:

• if the stream is for writing, and is attached to descriptor 2, it should be unbuffered; otherwise …

• if the stream is for writing, and connects descriptor 1 to a terminal device, it should be line-buffered; otherwise …

• if the moon is waxing …

• …

• otherwise, the stream should be block-buffered

To this, I propose a simple change, to be inserted right at the beginning:

If the environment variable STDIO_BUF is set to "line", streams default to ine buffering. If it's set to "none", streams default to no buffering. If it's set to "block", streams default to block buffered. If it's anything else, or unset, it is ignored.

Now instead of this:

    pseudo-tty-pipe --from X | tee some-file | ...

you write this:

    STDIO_BUF=line X | tee some-file | ...

Problem solved.

Or maybe you would like to do this:

    export STDIO_BUF=line

which then it affects every program in every pipeline in the rest of the session:

    X | tee some-file | ...

Control is global if you want it, and per-process if you want it.

This feature would cost around 20 lines of C code in the standard I/O library and would impose only an insigificant run-time cost. It would effectively add an --unbuffered flag to every program in the universe, retroactively, and the flag would be the same for every program. You would not have to remember that in mysql the magic option is -n and that in GNU grep it is --line-buffered and that for jq is is --unbuffered and that Python scripts can be unbuffered by supplying the -u flag and that in tee you are just SOL, etc. Setting STDIO_BUF=line would Just Work.

Programming languages would all get this for free also. Python already has PYTHONUNBUFFERED but in other languages you have to do something or other; in Perl you use some horrible Perl-4-ism like

    { my $ofh = select OUTPUT; $|++; select $ofh }

This proposal would fix every programming language everywhere. The Perl code would become:

    $ENV{STDIO_BUF} = 'line';

and every other language would be similarly simple:

    /* In C */
    putenv("STDIO_BUF=line");

[ Addendum 20180521: Mariusz Ceier corrects me, pointing out that this will not work for the process’ own standard streams, as they are pre-opened before the process gets a chance to set the variable. ]

It's easy to think of elaborations on this: STDIO_BUF=1:line might mean that only standard output gets line-buffering by default, everything else is up to the library.

This is an easy thing to do. I have wanted this for twenty years. How is it possible that it hasn't been in the GNU/Linux standard library for that long?

[ Addendum 20180521: it turns out there is quite a lot to say about the state of the art here. In particular, NetBSD has the feature very much as I described it. ]

by Mark Dominus (mjd@plover.com) at May 20, 2018 04:27 PM

Future of Coding podcast interview

I recently did an interview with my friend and former student Steve Krouse for his Future of Coding podcast. I think I still agree with almost everything I said, and I didn’t say anything too embarrassing, so if you want to listen to it I won’t stop you! We chatted about teaching and learning, functional programming and type systems, how to read academic papers, and a bunch of other things. You can listen to it here.

by Brent at May 19, 2018 03:16 PM

Cartography in Haskell

Introduction

This blog started off life as a blog post on how I use nix but somehow transformed itself into a “how I do data visualisation” blog post. The nix is still here though quietly doing its work in the background.

Suppose you want to analyze your local election results and visualize them using a choropleth but you’d like to use Haskell. You could try using the shapefile package but you will have to do a lot of the heavy lifting yourself (see here for an extended example). But you know folks using R can produce such things in a few lines of code and you also know from experience that unless you are very disciplined large R scripts can quickly become unmaintainable. Can you get the best of both worlds? It seems you can if you use inline-r. But now you have a bit of configuration problem: how do you make sure that all the Haskell packages that you need and all the R packages that you need are available and how can you make sure that your results are reproducible? My answer to use nix.

Acknowledgements

I’d like to thank all my colleagues at Tweag who have had the patience to indulge my questions especially zimbatm and also all folks on the #nixos irc channel.

Downloading and Building

The sources are on github.

You’ll have to build my Include pandoc filter somehow and then

pandoc -s HowIUseNix.lhs --filter=./Include -t markdown+lhs > HowIUseNixExpanded.lhs
BlogLiterately HowIUseNixExpanded.lhs > HowIUseNixExpanded.html

Analysing the Data

Before looking at the .nix file I use, let’s actually analyse the data. First some preamble

> {-# OPTIONS_GHC -Wall                    #-}
> {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}

> {-# LANGUAGE TemplateHaskell   #-}
> {-# LANGUAGE QuasiQuotes       #-}
> {-# LANGUAGE DataKinds         #-}
> {-# LANGUAGE FlexibleContexts  #-}
> {-# LANGUAGE TypeOperators     #-}
> {-# LANGUAGE OverloadedStrings #-}

> import Prelude as P

> import qualified Language.R as R
> import Language.R.QQ

> import System.Directory
> import System.FilePath

> import Control.Monad
> import Data.List (stripPrefix, nub)

> import qualified Data.Foldable as Foldable
> import Frames hiding ( (:&) )
> import Control.Lens
> import qualified Data.FuzzySet as Fuzzy
> import Data.Text (pack, unpack)
> import qualified Control.Foldl as Foldl
> import Pipes.Prelude (fold)

We can scrape the data for the Kington on Thames local elections and put it in a CSV file. Using the Haskell equivalent of data frames / pandas, Frames, we can “read” in the data. I say “read” in quotes because if this were a big data set (it’s not) then it might not fit in memory and we’d have to process it as a stream. I’ve included the sheet in the github repo so you can try reproducing my results.

> tableTypes "ElectionResults" "data/Election Results 2018 v1.csv"

> loadElectionResults :: IO (Frame ElectionResults)
> loadElectionResults = inCoreAoS (readTable "data/Election Results 2018 v1.csv")

We could analyse the data set in order to find the ward (aka electoral district) names but I happen to know them.

> wardNames :: [Text]
> wardNames = [ "Berrylands"
>             , "Norbiton"
>             , "Old Malden"
>             , "Coombe Hill"
>             , "Beverley"
>             , "Chessington North & Hook"
>             , "Tolworth and Hook Rise"
>             , "Coombe Vale"
>             , "St James"
>             , "Tudor"
>             , "Alexandra"
>             , "Canbury"
>             , "Surbiton Hill"
>             , "Chessington South"
>             , "Grove"
>             , "St Marks"
>             ]

We need a query to get both the total number of votes cast in the ward and the number of votes cast for what is now the party which controls the borough. We can create two filters to run in parallel, summing as we go.

> getPartyWard :: Text -> Text -> Foldl.Fold ElectionResults (Int, Int)
> getPartyWard p w =
>   (,) <$> (Foldl.handles (filtered (\x -> x ^. ward == w)) .
>            Foldl.handles votes) Foldl.sum
>       <*> (Foldl.handles (filtered (\x -> x ^. ward == w &&
>                                           x ^. party == p)) .
>            Foldl.handles votes) Foldl.sum

We can combine all the filters and sums into one big query where they all run in parallel.

> getVotes :: Foldl.Fold ElectionResults [(Int, Int)]
> getVotes = sequenceA $ map (getPartyWard "Liberal Democrat") wardNames

I downloaded the geographical data from here but I imagine there are many other sources.

First we read all the shapefiles in the directory we downloaded.

> root :: FilePath
> root = "data/KingstonuponThames"

> main :: IO ()
> main = do
>   ns <- runSafeT $ Foldl.purely fold getVotes (readTable "data/Election Results 2018 v1.csv")
>   let ps :: [Double]
>       ps = map (\(x, y) -> 100.0 * fromIntegral y / fromIntegral x) ns
>   let percentLD = zip (map unpack wardNames) ps
> 
>   ds <- getDirectoryContents root
>   let es = filter (\x -> takeExtension x == ".shp") ds
>   let fs = case xs of
>              Nothing -> error "Ward prefix does not match"
>              Just ys -> ys
>            where
>              xs = sequence $
>                   map (fmap dropExtension) $
>                   map (stripPrefix "KingstonuponThames_") es

Sadly, when we get the ward names from the file names they don’t match the ward names in the electoral data sheet. Fortunately, fuzzy matching resolves this problem.

>   rs <- loadElectionResults
>   let wardSet :: Fuzzy.FuzzySet
>       wardSet = Fuzzy.fromList . nub . Foldable.toList . fmap (^. ward) $ rs
> 
>   let gs = case sequence $ map (Fuzzy.getOne wardSet) $ map pack fs of
>              Nothing -> error "Ward name and ward filename do not match"
>              Just xs -> xs

Rather than making the colour of each ward vary continuously depending on the percentage share of the vote, let’s create 4 buckets to make it easier to see at a glance how the election results played out.

>   let bucket :: Double -> String
>       bucket x | x < 40    = "whitesmoke"
>                | x < 50    = "yellow1"
>                | x < 60    = "yellow2"
>                | otherwise = "yellow3"
> 
>   let cs :: [String]
>       cs = case sequence $ map (\w -> lookup w percentLD) (map unpack gs) of
>              Nothing -> error "Wrong name in table"
>              Just xs -> map bucket xs

Now we move into the world of R, courtesy of inline-r. First we load up the required libraries. Judging by urls like this, it is not always easy to install the R binding to GDAL (Geospatial Data Abstraction Library). But with nix, we don’t even have to use install.packages(...).

>   R.runRegion $ do
>     [r| library(rgdal)   |]
>     [r| library(ggplot2) |]
>     [r| library(dplyr)   |]

Next we create an empty map (I have no idea what this would look like if it were plotted).

>     map0 <- [r| ggplot() |]

And now we can fold over the shape data for each ward and its colour to build the basic map we want.

>     mapN <- foldM
>       (\m (f, c) -> do
>           let wward = root </> f
>           shapefileN <- [r| readOGR(wward_hs) |]
>           shapefileN_df <- [r| fortify(shapefileN_hs) |]
>           withColours <- [r| mutate(shapefileN_df_hs, colour=rep(c_hs, nrow(shapefileN_df_hs))) |]
>           [r| m_hs +
>               geom_polygon(data = withColours_hs,
>                            aes(x = long, y = lat, group = group, fill=colour),
>                            color = 'gray', size = .2) |]) map0 (zip es cs)

Now we can annotate the map with all the details needed to make it intelligible.

>     map_projected <- [r| mapN_hs + coord_map() +
>                          ggtitle("Kingston on Thames 2018 Local Election\nLib Dem Percentage Vote by Ward") +
>                          theme(legend.position="bottom", plot.title = element_text(lineheight=.8, face="bold", hjust=0.5)) +
>                          scale_fill_manual(values=c("whitesmoke", "yellow1", "yellow2", "yellow3"),
>                                            name="Vote (%)",
>                                            labels=c("0%-40% Lib Dem", "40%-50% Lib Dem", "50%-60% Lib Dem", "60%-100% Lib Dem")) |]

And finally save it in a file.

>     [r| jpeg(filename="diagrams/kingston.jpg") |]
>     [r| print(map_projected_hs)               |]
>     [r| dev.off()                             |]
>     return ()

How I Really Use nix

I haven’t found a way of interspersing text with nix code so here are some comments.

1. I use neither all the Haskell packages listed nor all the R packages. I tend to put a shell.nix file in the directory where I am working and then nix-shell shell.nix -I nixpkgs=~/nixpkgs as at the moment I seem to need packages which were recently added to nixpkgs.

2. I couldn’t get the tests for inline-r to run on MACos so I added dontCheck.

3. Some Haskell packages in nixpkgs have their bounds set too strictly so I have used doJailbreak.

{ pkgs ? import  {}, compiler ? "ghc822", doBenchmark ? false }:

let

f = { mkDerivation, haskell, base, foldl, Frames, fuzzyset
    , inline-r, integration, lens
    , pandoc-types, plots
    , diagrams-rasterific
    , diagrams
    , diagrams-svg
    , diagrams-contrib
    , R, random, stdenv
    , template-haskell, temporary }:
mkDerivation {
  pname = "mrp";
  version = "1.0.0";
  src = ./.;
  isLibrary = false;
  isExecutable = true;
  executableHaskellDepends = [
    base
    diagrams
    diagrams-rasterific
    diagrams-svg
    diagrams-contrib
    (haskell.lib.dontCheck inline-r)
    foldl
    Frames
    fuzzyset
    integration
    lens
    pandoc-types
    plots
    random
    template-haskell
    temporary
  ];
  executableSystemDepends = [
    R
    pkgs.rPackages.dplyr
    pkgs.rPackages.ggmap
    pkgs.rPackages.ggplot2
    pkgs.rPackages.knitr
    pkgs.rPackages.maptools
    pkgs.rPackages.reshape2
    pkgs.rPackages.rgeos
    pkgs.rPackages.rgdal
    pkgs.rPackages.rstan
    pkgs.rPackages.zoo];
  license = stdenv.lib.licenses.bsd3;
};

haskellPackages = if compiler == "default"
  then pkgs.haskellPackages
  else pkgs.haskell.packages.${compiler};

myHaskellPackages = haskellPackages.override {
  overrides = self: super: with pkgs.haskell.lib; {
    diagrams-rasterific = doJailbreak super.diagrams-rasterific;
    diagrams-svg = doJailbreak super.diagrams-svg;
    diagrams-contrib = doJailbreak super.diagrams-contrib;
    diagrams = doJailbreak super.diagrams;
    inline-r = dontCheck super.inline-r;
    pipes-group = doJailbreak super.pipes-group;
  };
};

variant = if doBenchmark then pkgs.haskell.lib.doBenchmark else pkgs.lib.id;

drv = variant (myHaskellPackages.callPackage f {});

in

  if pkgs.lib.inNixShell then drv.env else drv

by Dominic Steinitz at May 19, 2018 11:18 AM

Performance and Feature Case Studies in Ecstasy

In my (copious) spare time, I've been working on an RTS game written in Haskell. It's using my entity-component system library ecstasy in anger, for what is likely the library's first time. As a result, I'm learning a lot about doing performance haggling with the compiler, as well as getting opportunities for even more type-trickery. I thought both might make for interesting topics of discussion.

Overview of ecstasy's internals

Before diving into what I've been changing recently, it's probably a good idea to quickly talk inside baseball about how ecstasy works. The basic idea is this, you define a "world" higher-kinded data (HKD) corresponding to the components you care about. The library instantiates your HKD world in different ways to form a structure-of-arrays corresponding to the high-efficiency storage of the ECS, and to form just a structure corresponding to an actual entity.

This machinery is built via the Component type family:

type family Component (s :: StorageType)
                      (c :: ComponentType)
                      (a :: *) :: *

Using DataKinds, Component is parameterized by three types. s :: StorageType describes how the library wants to use this component -- possibly in the "structure-of-arrays" format consumed by the library, or as an entity structure, to be used by the application programmer. s is left polymorphic when defining the HKD.

The c :: ComponentType parameter is used to indicate the semantics of the field; some options include "each entity may or may not have this field" or "at most one entity may have this field." The former might be used for something like position, while the latter could be focusedOnByTheCamera.

Finally, a :: * is the actual type you want the field to have.

Having data is a great first step, but it's currently just an opaque blob to the library. This is where GHC.Generics comes in -- given an (auto-derivable) Generic instance for our world, we can use use GHC.Generics to automatically further derive more specialized machinery for ourselves.

As an example, assume our world looked like this (absent the Component trickery):

data World f = World
  { position :: f (V2 Double)
  , graphics :: f Graphics
  }

we can use GHC.Generics to automatically generate the equivalent to a function:

getEntity :: Int -> World Data.IntMap.IntMap -> World Maybe
getEntity ent storage =
  World (Data.IntMap.lookup ent $ position storage)
        (Data.IntMap.lookup ent $ graphics storage)

which converts from a structure-of-arrays representation to a structure-of-maybes. The actual technique behind implementing these generic functions is out of scope for today's topic, but I've written on it previously.

For its part, ecstasy exposes the SystemT monad, which at its heart is just a glorified Control.Monad.Trans.State.StateT (Int, World 'Storage). The Int keeps track of the next ID to give out for a newly created entity.

To a rough approximation, this is all of the interesting stuff inside of ecstasy. So armed with this knowledge, we're ready to tackle some of the problems that have been unearthed recently.

Stupid space leaks

My original test for ecstasy was a small platformer -- a genre not known for the sheer number of entities all interacting at once. As a result, ecstasy performed terribly, but I didn't notice because I hadn't benchmarked it or actually stress-tested it whatsoever. But that's OK, I wrote it to scratch an itch while hanging out in a Thai airport; I've never claimed to write titanium-grade software :)

But in my RTS, the library was obvious struggling after allocating only 100 dudes. The thing was leaking memory like crazy, which was because I used lazy state and containers. Oopsie daisies! Replacing Control.Monad.Trans.State and Data.IntMap with their strict versions cleared it up.

Honestly I'm not sure why the lazy versions are the default, but I guess that's the world we live in. SANDY'S HOT PRO TIPS: don't use lazy maps or state unless you've really thought about it.

Virtual components

While working on my RTS, I realized that I was going to need fast spacial queries to answer questions like "is there anyone around that I should attack?" The result was some sort of Frankenstein bastard child of a quadtree and a reverse index to answer both "where am I?" and "who's nearby?"

This worked well to answer the queries I asked of it, but posed a problem; in order to maintain its indices, my datastructure needed to be the source of truth on who was where. Having a position component wasn't going to cut it anymore, since the ECS was no longer responsible for this data. I briefly considered trying to write a shim to keep the two datasources in sync, but it felt simultaneously like an ad-hoc hack and a maintenance nightmare, so I gave up and removed the component.

Unfortunately, all was not well. I added some monadic getters and setters to help shuffle the position information around, but oh god this became a garbage fire. Things that were before atomic updates now had extra calls to get and set the bastard, and everything was miserable.

I realized what I really wanted was the capability for ecstasy to be aware of components without necessarily being the owner of them. Which is to say, components whose reads and writes invisibly dispatched out to some other monadic system.

OK, great, I knew what I wanted. Unfortunately, the implementation was not so straightforward. The problem was the functions I wanted:

vget :: Ent -> m (Maybe a)
vset :: Ent -> Update a -> m ()

had this troublesome m parameter, and there was no clear place to put it. The monad to dispatch virtual calls to is a property of the interpretation of the data (actually running the sucker), not the data itself.

As a result, it wasn't clear where to actually keep the m type parameter. For example, assuming we want position to be virtual in our world:

data World s = World
  { position :: Component s 'Virtual (V2 Double)
  }

Somehow, after unifying s ~ 'Storage, we want this to come out as:

data World 'Storage = World
  { position :: ( Ent -> m (Maybe (V2 Double)        -- vget
                , Ent -> Update (V2 Double) -> m ()  -- vset
                )
  }

But where do we get the m from? There's no obvious place.

We could add it as a mandatory parameter on World, but that forces an implementation detail on people who don't need any virtual fields.

We could existentialize it, and then unsafeCoerce it back, but... well, I stopped following that line of thought pretty quickly.

My first solution to this problem was to add a Symbol to the Virtual component-type token, indicating the "name" of this component, and then using a typeclass instance to actually connect the two:

data World s = World
  { position :: Component s ('Virtual "position") (V2 Double)
  }

-- we put the monad here: `m`
instance VirtualAccess "position" m (V2 Double) where
  vget = ...
  vset = ...

While it worked, this was obviously a hack and my inner muse of library design was so offended that I spent another few days looking for a better solution. Thankfully, I came up with one.

The solution is one I had already skirted around, but failed to notice. This monad is a property only of the interpretation of the data, which is to say it really only matters when we're building the world storage. Which means we can do some janky dependency-injection stuff and hide it inside of the storage-type token.

Which is to say, that given a world of the form:

data World s = World
  { position :: Component s 'Virtual (V2 Double)
  }

we could just pass in the appropriate monad when instantiating the world for its storage. Pseudocode:

data World (Storage m) = World
  { position :: Component (Storage m) 'Virtual (V2 Double)
  }

All of a sudden, the Component type family now has access to m, and so it can expand into the vget/vset pair in a type-safe way. And the best part is that this is completely invisible to the user who never needs to care about our clever implementation details.

Spectacular! I updated all of the code generated via GHC.Generics to run in m so it could take advantage of this virtual dispatch, and shipped a new version of ecstasy.

Polymorphic performance woes

While all of this virtual stuff worked, it didn't work particularly quickly. I noticed some significant regressions in performance in my RTS upon upgrading to the new version. What was up? I dug in with the profiler and saw that my GHC.Generics-derived code was no longer being inlined. HKD was performing more terribly than I thought!

All of my INLINE pragmas were still intact, so I wasn't super sure what was going on. I canvassed #ghc on freenode, and the ever-helpful glguy had this to say:

<glguy> generics can't optimize away when that optimization relies on GHC applying Monad laws to do it

Oh. Lame. That's why my performance had gone to shit!

I'm not sure if this is true, but my understanding is that the problem is that my monad was polymorphic, and thus the inliner wasn't getting a chance to fire. glguy pointed me towards the aptly-named confusing lens combinator, whose documentation reads:

Fuse a Traversal by reassociating all of the <*> operations to the left and fusing all of the fmap calls into one. This is particularly useful when constructing a Traversal using operations from GHC.Generics...

confusing exploits the Yoneda lemma to merge their separate uses of fmap into a single fmap and it further exploits an interesting property of the right Kan lift (or Curried) to left associate all of the uses of <*> to make it possible to fuse together more fmaps.

This is particularly effective when the choice of functor f is unknown at compile time or when the Traversal in the above description is recursive or complex enough to prevent inlining.

That sounds exactly like the problem I was having, doesn't it? The actual confusing combinator itself was no help in this situation, so I dug in and looked at its implementation. It essentially lifts your m-specific actions into Curried (Yoneda m) (Yoneda m) (don't ask me!), and then lowers it at the very end. My (shaky) understanding is this:

Yoneda f is a functor even when f itself is not, which means we have a free functor instance, which itself means that fmap on Yoneda f can't just lift fmap from f. This is cool if fmaping over f is expensive -- Yoneda just fuses all fmaps into a single one that gets performed when you lower yourself out of it. Essentially it's an encoding that reduces an O(n) cost of doing n fmaps down to O(1).

Curried f f similarly has a free Applicative instance, which, he says waving his hands furiously, is where the <*> improvements come from.

So I did a small amount of work to run all of my GHC.Generics code in Curried (Yoneda m) (Yoneda m) rather than in m directly, and looked at my perf graphs. While I was successful in optimizing away my GHC.Generics code, I was also successful in merely pushing all of the time and allocations out of it and into Yoneda.fmap. Curiously, this function isn't marked as INLINE which I suspect is why the inliner is giving up (the isomorphic Functor instance for Codensity is marked as INLINE, so I am very hesitantly rallying the hubris to suggest this is a bug in an Ed Kmett library.)

Despite the fact that I've been saying "we want to run virtual monadic actions," throughout this post, I've really meant "we want to run virtual applicative actions." Which is why I thought I could get away with using Curried (Yoneda m) (Yoneda m) to solve my optimization problems for me.

So instead I turned to Codensity, which legend tells can significantly improve the performance of free monads by way of the same mystical category-theoretical encodings. Lo and behold, moving all of my monadic actions into Codensity m was in fact enough to get the inliner running again, and as a result, getting our HKD once more to be less terrible.

If you're curious in how Codensity and friends work their magic, glguy pointed me to a tutorial he wrote explaining the technique. Go give it a read if you're feeling plucky and adventurous.

May 18, 2018 01:37 PM

Proof reuse in Coq using existential variables

This is another technical post that is only of interest only to Coq users.

TL;DR: Using existential variable for hypotheses allows you to easily refactor a complicated proof into an induction schema and the actual proofs.

Setup

As a running example, I will use a small theory of “bags”, which you can think of as lists represented as trees, to allow an O(1) append operation:

Require Import Coq.Arith.Arith.
Require Import Psatz.
Require FunInd.

(* The data type *)
Inductive Bag a : Type :=
  | Empty : Bag a
  | Unit  : a -> Bag a
  | Two   : Bag a -> Bag a -> Bag a.

Arguments Empty {_}.
Arguments Unit {_}.
Arguments Two {_}.

Fixpoint length {a} (b : Bag a) : nat :=
  match b with
  | Empty     => 0
  | Unit _    => 1
  | Two b1 b2 => length b1 + length b2
  end.

(* A smart constructor that ensures that a [Two] never
   has [Empty] as subtrees. *)
Definition two {a} (b1 b2 : Bag a) : Bag a := match b1 with
  | Empty => b2
  | _ => match b2 with | Empty => b1
                       | _ => Two b1 b2 end end.

Lemma length_two {a} (b1 b2 : Bag a) :
  length (two b1 b2) = length b1 + length b2.
Proof. destruct b1, b2; simpl; lia. Qed.

(* A first non-trivial function *)
Function take {a : Type} (n : nat) (b : Bag a) : Bag a :=
  if n =? 0
  then Empty
  else match b with
       | Empty     => b
       | Unit x    => b
       | Two b1 b2 => two (take n b1) (take (n - length b1) b2)
       end.

The theorem

The theorem that I will be looking at in this proof describes how length and take interact:

Theorem length_take''':
  forall {a} n (b : Bag a),
  length (take n b) = min n (length b).

Before I dive into it, let me point out that this example itself is too simple to warrant the techniques that I will present in this post. I have to rely on your imagination to scale this up to appreciate the effect on significantly bigger proofs.

Naive induction

How would we go about proving this lemma? Surely, induction is the way to go! And indeed, this is provable using induction (on the Bag) just fine:

Proof.
  intros.
  revert n.
  induction b; intros n.
  * simpl.
    destruct (Nat.eqb_spec n 0).
    + subst. rewrite Nat.min_0_l. reflexivity.
    + rewrite Nat.min_0_r. reflexivity.
  * simpl.
    destruct (Nat.eqb_spec n 0).
    + subst. rewrite Nat.min_0_l. reflexivity.
    + simpl. lia.
  * simpl.
    destruct (Nat.eqb_spec n 0).
    + subst. rewrite Nat.min_0_l. reflexivity.
    + simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.

But there is a problem: A proof by induction on the Bag argument immediately creates three subgoals, one for each constructor. But that is not how take is defined, which first checks the value of n, independent of the constructor. This means that we have to do the case-split and the proof for the case n = 0 three times, although they are identical. It’s a one-line proof here, but imagine something bigger...

Proof by fixpoint

Can we refactor the proof to handle the case n = 0 first? Yes, but not with a simple invocation of the induction tactic. We could do well-founded induction on the length of the argument, or we can do the proof using the more primitive fix tactic. The latter is a bit hairy, you won’t know if your proof is accepted until you do Qed (or check with Guarded), but when it works it can yield some nice proofs.

Proof.
  intros a.
  fix IH 2.
  intros.
  rewrite take_equation.
  destruct (Nat.eqb_spec n 0).
  + subst n. rewrite Nat.min_0_l. reflexivity.
  + destruct b.
    * rewrite Nat.min_0_r. reflexivity.
    * simpl. lia.
    * simpl. rewrite length_two, !IH. lia.
Qed.

Nice: we eliminated the duplication of proofs!

A functional induction lemma

Again, imagine that we jumped through more hoops here ... maybe some well-founded recursion with a tricky size measure and complex proofs that the measure decreases ... or maybe you need to carry around an invariant about your arguments and you have to work hard to satisfy the assumption of the induction hypothesis.

As long as you do only one proof about take, that is fine. As soon as you do a second proof, you will notice that you have to repeat all of that, and it can easily make up most of your proof...

Wouldn’t it be nice if you can do the common parts of the proofs only once, obtain a generic proof scheme that you can use for (most) proofs about take, and then just fill in the blanks?

Incidentally, the Function command provides precisely that:

take_ind
     : forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
       (forall (n : nat) (b : Bag a), (n =? 0) = true -> P n b Empty) ->
       (forall (n : nat) (b : Bag a), (n =? 0) = false -> b = Empty -> P n Empty b) ->
       (forall (n : nat) (b : Bag a), (n =? 0) = false -> forall x : a, b = Unit x -> P n (Unit x) b) ->
       (forall (n : nat) (b : Bag a),
        (n =? 0) = false ->
        forall b1 b2 : Bag a,
        b = Two b1 b2 ->
        P n b1 (take n b1) ->
        P (n - length b1) b2 (take (n - length b1) b2) ->
        P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
       forall (n : nat) (b : Bag a), P n b (take n b)

which is great if you can use Function (although not perfect – we’d rather see n = 0 instead of (n =? 0) = true), but often Function is not powerful enough to define the function you care about.

Extracting the scheme from a proof

We could define our own take_ind' by hand, but that is a lot of work, and we may not get it right easily, and when we change out functions, there is now this big proof statement to update.

Instead, let us use existentials, which are variables where Coq infers their type from how we use them, so we don’t have to declare them. Unfortunately, Coq does not support writing just

Lemma take_ind':
  forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
  forall (IH1 : ?) (IH2 : ?) (IH3 : ?) (IH4 : ?),
  forall n b, P n b (take n b).

where we just leave out the type of the assumptions (Isabelle does...), but we can fake it using some generic technique.

We begin with stating an auxiliary lemma using a sigma type to say “there exist some assumption that are sufficient to show the conclusion”:

Lemma take_ind_aux:
  forall a (P : _ -> _ -> _ -> Prop),
  { Hs : Prop |
    Hs -> forall n (b : Bag a), P n b (take n b)
  }.

We use the [eexist tactic])(https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacv.eexists) (existential exists) to construct the sigma type without committing to the type of Hs yet.

Proof.
  intros a P.
  eexists.
  intros Hs.

This gives us an assumption Hs : ?Hs – note the existential type. We need four of those, which we can achieve by writing

  pose proof Hs as H1. eapply proj1 in H1. eapply proj2 in Hs.
  pose proof Hs as H2. eapply proj1 in H2. eapply proj2 in Hs.
  pose proof Hs as H3. eapply proj1 in H3. eapply proj2 in Hs.
  rename Hs into H4.

we now have this goal state:

1 subgoal
a : Type
P : nat -> Bag a -> Bag a -> Prop
H4 : ?Goal2
H1 : ?Goal
H2 : ?Goal0
H3 : ?Goal1
______________________________________(1/1)
forall (n : nat) (b : Bag a), P n b (take n b)

At this point, we start reproducing the proof of length_take: The same approach to induction, the same case splits:

  fix IH 2.
  intros.
  rewrite take_equation.
  destruct (Nat.eqb_spec n 0).
  + subst n.
    revert b.
    refine H1.
  + rename n0 into Hnot_null.
    destruct b.
    * revert n Hnot_null.
      refine H2.
    * rename a0 into x.
      revert x n Hnot_null.
      refine H3.
    * assert (IHb1 : P n b1 (take n b1)) by apply IH.
      assert (IHb2 : P (n - length b1) b2 (take (n - length b1) b2)) by apply IH.
      revert n b1 b2 Hnot_null IHb1 IHb2.
      refine H4.
Defined. (* Important *)

Inside each case, we move all relevant hypotheses into the goal using revert and refine with the corresponding assumption, thus instantiating it. In the recursive case (Two), we assert that P holds for the subterms, by induction.

It is important to end this proofs with Defined, and not Qed, as we will see later.

In a next step, we can remove the sigma type:

Definition take_ind' a P := proj2_sig (take_ind_aux a P).

The type of take_ind' is as follows:

take_ind'
     : forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
       proj1_sig (take_ind_aux a P) ->
       forall n b, P n b (take n b)

This looks almost like an induction lemma. The assumptions of this lemma have the not very helpful type proj1_sig (take_ind_aux a P), but we can already use this to prove length_take:

Theorem length_take:
  forall {a} n (b : Bag a),
  length (take n b) = min n (length b).
Proof.
  intros a.
  intros.
  apply take_ind' with (P := fun n b r => length r = min n (length b)).
  repeat apply conj; intros.
  * rewrite Nat.min_0_l. reflexivity.
  * rewrite Nat.min_0_r. reflexivity.
  * simpl. lia.
  * simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.

In this case I have to explicitly state P where I invoke take_ind', because Coq cannot figure out this instantiation on its own (it requires higher-order unification, which is undecidable and unpredictable). In other cases I had more luck.

After I apply take_ind', I have this proof goal:

______________________________________(1/1)
proj1_sig (take_ind_aux a (fun n b r => length r = min n (length b)))

which is the type that Coq inferred for Hs above. We know that this is a conjunction of a bunch of assumptions, and we can split it as such, using repeat apply conj. At this point, Coq needs to look inside take_ind_aux; this would fail if we used Qed to conclude the proof of take_ind_aux.

This gives me four goals, one for each case of take, and the remaining proofs really only deals with the specifics of length_take – no more general dealing with worrying about getting the induction right and doing the case-splitting the right way.

Also note that, very conveniently, Coq uses the same name for the induction hypotheses IHb1 and IHb2 that we used in take_ind_aux!

Making it prettier

It may be a bit confusing to have this proj1_sig in the type, especially when working in a team where others will use your induction lemma without knowing its internals. But we can resolve that, and also turn the conjunctions into normal arrows, using a bit of tactic support. This is completely generic, so if you follow this procedure, you can just copy most of that:

Lemma uncurry_and: forall {A B C}, (A /\ B -> C) -> (A -> B -> C).
Proof. intros. intuition. Qed.
Lemma under_imp:   forall {A B C}, (B -> C) -> (A -> B) -> (A -> C).
Proof. intros. intuition. Qed.
Ltac iterate n f x := lazymatch n with
  | 0 => x
  | S ?n => iterate n f uconstr:(f x)
end.
Ltac uncurryN n x :=
  let n' := eval compute in n in
  lazymatch n' with
  | 0 => x
  | S ?n => let uc := iterate n uconstr:(under_imp) uconstr:(uncurry_and) in
            let x' := uncurryN n x in
            uconstr:(uc x')
end.

With this in place, we can define our final proof scheme lemma:

Definition take_ind'' a P
  := ltac:(let x := uncurryN 3 (proj2_sig (take_ind_aux a P)) in exact x).
Opaque take_ind''.

The type of take_ind'' is now exactly what we’d wish for: All assumptions spelled out, and the n =? 0 already taken of (compare this to the take_ind provided by the Function command above):

take_ind''
     : forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
       (forall b : Bag a, P 0 b Empty) ->
       (forall n : nat, n <> 0 -> P n Empty Empty) ->
       (forall (x : a) (n : nat), n <> 0 -> P n (Unit x) (Unit x)) ->
       (forall (n : nat) (b1 b2 : Bag a),
        n <> 0 ->
        P n b1 (take n b1) ->
        P (n - length b1) b2 (take (n - length b1) b2) ->
        P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
       forall (n : nat) (b : Bag a), P n b (take n b)

At this point we can mark take_ind'' as Opaque, to hide how we obtained this lemma.

Our proof does not change a lot; we merely no longer have to use repeat apply conj:

Theorem length_take''':
  forall {a} n (b : Bag a),
  length (take n b) = min n (length b).
Proof.
  intros a.
  intros.
  apply take_ind'' with (P := fun n b r => length r = min n (length b)); intros.
  * rewrite Nat.min_0_l. reflexivity.
  * rewrite Nat.min_0_r. reflexivity.
  * simpl. lia.
  * simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.

Is it worth it?

It was in my case: Applying this trick in our ongoing work of verifying parts of the Haskell compiler GHC separated a somewhat proof into a re-usable proof scheme (go_ind), making the actual proofs (go_all_WellScopedFloats, go_res_WellScoped) much neater and to the point. It saved “only” 60 lines (if I don’t count the 20 “generic” lines above), but the pay-off will increase as I do even more proofs about this function.

by Joachim Breitner (mail@joachim-breitner.de) at May 18, 2018 12:51 PM

Controlling access to Nomad clusters

There are many benefits to running your infrastructure in the cloud, as well as isolating your components from one another with containers in your DevOps infrastructure. However, when you reach a certain scale of operations, it becomes necessary to use tools that ensure you make best use of compute resources. These are commonly called application schedulers, and they allocate your compute units — be they containers, virtual machines, isolated forked processes — across multiple servers.

by Yghor Kerscher (yghor@fpcomplete.com) at May 17, 2018 08:21 PM

Objects with special collection routines in GHC's GC

A generational copying garbage collector, in its most basic form, is quite simple. However, as we’ll see, not all objects can be copied, and some objects require more bookkeeping by the RTS. In this post we’re going to look at these type of objects that require special treatment from the garbage collector (GC in short). For each type of object we’ll look at how they’re allocated and collected. Each of these objects solves a particular problem:

• Large objects solve the problem with expensive copying of e.g. large arrays.
• Pinned objects solve the problem of sharing data with foreign code.
• Compact objects solve the problem of expensive scanning of large boxed heap objects.
• Weak pointers allow finalizers and non-leaky memo tables.
• Threads with special collection rules allow BlockedIndefinitelyOnMVar async exceptions.
• Stable pointers solve the problem with sharing references to Haskell objects with foreign code.
• Stable names allow pointer equality.
• Static objects allow efficient collection of data allocated in compile-time by not allocating them in the heap.

This post is mostly intended for GHC hackers, but may also be useful for Haskell developers who develop performance-critical systems and need to know about impacts of these objects to GC and allocation pauses.

1. Large objects

A unit of allocation in GHC’s storage manager is a block, which is 2¹² bytes (4k) large. A large object is an object that is at least as large as 80% of a block (3277 bytes). Because these objects are expensive to copy, GHC’s RTS treats them as immovable, and does not use the usual copying GC routines to collect them.

Allocation: Allocation is done via the RTS function allocateMightFail. If the size parameter is smaller than 80% of a block allocateMightFail allocates in the nursery. Otherwise it allocates enough blocks to hold the requested amount, marks allocated blocks as BF_LARGE, adds the blocks to the first generation’s large_objects list. One example where this happens is when newArray# is called with large-enough size argument.

Because large object allocation requires allocating new blocks, this requires synchronization via sm_mutex (sm for “storage manager”).

Collection: When we see a large object during GC (i.e. a block with BF_LARGE flag set) we remove the object from its generation’s large_objects list¹, add it to the GC’s todo_large_objects list. todo_large_objects list is later scanned by scavenge_large, which adds large objects to their next generation’s scavenged_large_objects lists. Finally, after the GC is done, scavenged_large_objects lists are appended to large_objects lists of their generations.

Effectively we move large objects that we found during the usual copying GC to their next generations without copying.

2. Pinned objects

Pinned objects are similar to large objects; they’re also not moved by the GC. However, unlike large objects, they don’t have a minimum size. The RTS maintains capability-local pinned block lists, and allocates pinned objects in these blocks. Currently the only pinned object type is the MutableByteArray#, which is allocated via newPinnedByteArray#.

Allocation: Allocation is done via the RTS function allocatePinned. If we have enough space in the capability-local pinned object block we allocate there, otherwise we allocate a new block and start using it as the new pinned object block. The old block is added to the capability-local pinned_object_blocks list, which will be later moved to the first generation’s large_objects list for collection.

Pinned object allocation only requires synchronization (via sm_mutex) when the current capability’s pinned object block does not have enough space.

Collection: When allocating pinned objects we cheat a little bit, and mark all pinned blocks as BF_LARGE. This makes the GC collect pinned blocks the same way that it collects large blocks. collect_pinned_object_blocks moves all capabilities’ pinned_object_blocks to the first generation’s large_objects list.

One another difference between a pinned block and a large block is that a pinned block may have many objects, while a large block is just one object. However, this does not cause problems when collecting a pinned block as if it was a large block, because the primop for pinned object allocation returns a mutable byte array, which does not contain any pointers and does not provide an API for adding arbitrary heap objects to the array. This also means unlike large objects pinned objects are not scavenged.

3. Compact objects

Compact objects are similar to pinned and large objects in that they’re not moved. Unlike pinned and large objects, they can have multiple blocks linked together (whereas pinned and large objects are contiguous block groups). As far as GC is concerned a compact object is just one object with no outgoing pointers, so the fact that they can have multiple linked block groups is not important: we only worry about liveness of the object as a whole, and there is no need to scavenge it.

See the paper for some example uses of compact objects.

Allocation: Allocation is done via compactNew RTS function. compactNew adds the compact block to the first generation’s compact list. compactAdd copies an object (with everything referenced by it) to a compact by allocating in the compact’s existing blocks, allocating new blocks if necessary (code).

Compact object blocks are marked as BF_COMPACT. Compact object allocation requires synchronization via sm_lock.

Collection: When we see an object that lives in a block with BF_COMPACT we get the head of the block (remember that blocks for a compact object are linked together) and evacuate the head block by removing it from its current compact list adding it to the next generation’s live compact objects list (code). After GC is done any compact objects left in compact lists are collected and live compact objects are moved to compact lists.

4. Weak pointers

A weak pointer (or weak object) is essentially a record with key, value, and finalizer fields. While all of these fields are ordinary Haskell objects, they’re not marked as pointer fields in the weak object info table²³, so a reachable weak object does not make these fields reachable.

As to why this is useful, see the paper and System.Mem.Weak module documentation.

Allocation: Weak pointers are allocated via mkWeak and mkWeakPtr. These high-level functions use the mkWeak# primop. mkWeak# allocates a heap object for the actual Weak value, and adds it to the current capability’s weak pointer list.

Collection: As already noted, because fields of weak objects are not marked as pointers, we do not copy its fields. Instead we do this:

1. Right before starting evacuating the roots, move Capability-local weak pointers to the first generation’s weak pointer list. (code)

2. After evacuating the roots but before scavenging, move weak pointer lists of collected generations to old_weak_ptr_lists. (code)

3. During scavenging, traverse old_weak_ptr_lists of collected generations, and for each weak pointer check if the key is alive (code) (keys in uncollected generations are considered alive). If it is then evacuate other fields of the weak object, and promote it to next generation’s weak_ptr_list. Otherwise just skip it (do not detach it from the list!).

If in this step we evacuated anything (i.e. found an alive key) we signal the scavenging code to continue scavenging, because we have to copy any heap objects reachable from the weak object’s fields.

If we traverse all of the weak pointer lists without evacuating anything then we’re done. We append all old_weak_ptr_lists to the global dead_weak_ptr_list while also evacuating their finalizer fields. dead_weak_ptr_list is later used to schedule threads to run finalizers.

This effectively implements our special GC strategy for weak objects: a weak object does not make its key or value reachable, but if its key is reachable (even if the weak itself is not reachable) then the value is also reachable. When the key becomes unreachable we schedule finalizers.

5. Threads

A GHC thread is a heap object like any other. However, when a thread becomes unreachable we sometimes want to raise an async exception in the thread instead of collecting it, effectively resurrecting the thread.

What does it mean for a thread to become unreachable? The reachability rules for threads are:

1. If ThreadId for a thread is reachable, then the thread is also reachable ⁴.

2. If a thread has work to do and not blocked then it’s reachable. This is because threads with work to do are in capabilities’ run queues, which are roots for GC.

3. If a thread is in a blocking queue (e.g. when blocked by an MVar operation), and the object that owns the blocking queue is reachable, then the thread is also reachable.

Now suppose that a thread was blocked in an MVar operation, and its ThreadId is unreachable. In this case we want to raise a BlockedIndefinitelyOnMVar exception in the thread. This suggests that we have to somehow know about threads that become unreachable. So we maintain a list of threads. Before moving on to the details, here’s a simple program that demonstrates the reachability rules:

{-# LANGUAGE ScopedTypeVariables #-}

module Main where

import Control.Concurrent
import Control.Exception
import System.Mem

main :: IO ()
main = do
    var :: MVar Int <- newEmptyMVar

    thr <-
      forkIO $
        catch (takeMVar var >>= print)
              (\(e :: BlockedIndefinitelyOnMVar) ->
                   putStrLn "Blocked")

    performMajorGC
    yield
    performMajorGC
    threadDelay 1000000

This version should print a single Blocked line. This is because both the MVar and the thread become unreachable during the first GC and the thread is resurrected⁵.

Now, add seq var (return ()) or seq thr (return ()) at the end. In both cases we don’t get an exception in the thread because it’s still reachable, and thus not resurrected.

Now, the details.

Allocation: A thread is allocated with forkIO, which calls fork# primop, which in turn calls createThread RTS function. createThread allocates the thread in the nursery, and adds the thread to the first generation’s threads list⁶. Thread allocation requires synchronization via sched_mutex.

At this point we have a thread but it’s not scheduled yet. For this the primop calls scheduleThread RTS function with the return value of createThread. scheduleThread adds the thread to the current capability’s run queue. At this point the thread becomes a GC root.

Collection: Collection works similarly with weak object collection. Before starting the GC, for collected generations, we move the threads lists to old_threads lists. Any threads that will be in the old_threads lists will need resurrection if they’re blocked (otherwise they will be collected).

During scavenging, we traverse old_threads lists, moving any alive threads to their next generation’s threads lists (code). Note that this process interleaved with step (3) of weak object collection, because a weak object with alive key may make a thread reachable (by referencing to it in its value).

When we don’t find any more weaks with live keys we “resurrect” threads in the old_threads lists if they were blocked in an operation (rather than being killed or finished). This happens in resurrectUnreachableThreads. Because resurrecting makes some unreachable objects reachable again (by adding threads to run queues) we continue with scavenging after this process.

---

Aside: The way blocked threads are resurrected causes somewhat counter-intuitive behavior when multiple threads are blocked but resurrecting one thread unblocks others. Apparently this behavior is discovered by users and reported as a bug from time to time (see e.g. #10241). The code from #10241 demonstrates the issue (slightly simplified):

module Main where

import Control.Concurrent
import Control.Concurrent.MVar
import Control.Exception

main :: IO ()
main = do
    mvar1 <- newEmptyMVar :: IO (MVar ())
    mvar2 <- newEmptyMVar :: IO (MVar ())

    forkIO $ do
        takeMVar mvar1 `catch` errorHandler1
        putStrLn "after error catch"
        threadDelay 1000000
        putMVar mvar2 ()
        putStrLn "after putMVar"

    readMVar mvar2 `catch` errorHandler2
    putStrLn "after readMVar"
    threadDelay 5000000
  where
    errorHandler1 :: BlockedIndefinitelyOnMVar -> IO ()
    errorHandler1 e = putStrLn ("errorHandler1: " ++ show e)

    errorHandler2 :: BlockedIndefinitelyOnMVar -> IO ()
    errorHandler2 e = putStrLn ("errorHandler2: " ++ show e)

The idea is that while both threads are blocked, resurrecting one of them unblocks the other, so we should see only one “errorHandler…” line in the output. However, because all dead threads are resurrected once, both threads end up getting a BlockedIndefinitelyOnMVar exception.

There’s a simple fix that I explained in the ticket and implemented, but it’s rejected because it’s non-deterministic in which thread to resurrect.

Personally I think this non-determinism is OK because current behavior is worse, and scheduling (and thus GC and BlockedIndefinitelyOnMVar exceptions) are already non-deterministic, so I doubt anyone relies on determinism in such programs.

---

6. Stable pointers

A stable pointer is simply a reference to a Haskell object. However, they’re never collected, and after every GC stable pointers are updated to point to new locations of the Haskell objects that they were pointing to before the GC. This is useful when storing references to Haskell objects in foreign code.

Allocation: Done via getStablePtr RTS function. Stable pointers are held in an array of spEntry (which is just typedef for a pointer). New pointers are simply added at the end of the array, and array is resized (capacity is doubled) when it’s out of room.

Collection: The stable pointer table is never collected. However, it’s contents are evacuated as GC roots, and after every GC addresses of objects in the table is updated.

GHC itself uses stable pointers in an interesting way: some closures are used by the RTS, but not by generated code. Because these closures are not referenced by the generated code the GC is free to collect them. To prevent this the RTS adds them to the stable pointer table, effectively making them roots. This way they’re never collected and the RTS can use them.

7. Stable names

A stable name just some abstract object unique to a Haskell object. They come with a fast Eq instance and a hash function, and when you generate stable name for an object multiple times you get the same stable name back. This means stable names can be used for implementing something similar to pointer equality.

Allocation: Done via makeStableName# primop. Stable names are held in an array similar to stable pointers, however to enable collection the entry type is more complex. I updated comments of this type while writing this post so give it a read for details.

Collection: Because we keep a list of all stable names, and stable names know addresses of their StableName objects (sn_obj field), after a GC we can check if a stable name is still alive. If not then we free its entry in the table. Otherwise we evacaute the pointed object. This happens in gcStableTables.

Note that stable names, unlike stable pointers, are not roots. gcStableTables is called after GC is done.

8. Static objects

Top-level definitions are allocated as static objects. The allocation happens in compile time, outside of the heap.

Allocation: Allocation happens in compile time. It’s not possible to allocate a static object in runtime.

Collection: The space allocated for static objects is never really reclaimed. When the GC encounters a static object⁷ it adds the static object to the GC-thread-local static objects list. This list later used by scavenge to evacuate any objects referenced by these static objects.

To avoid collecting a static object multiple times, evacuated static objects are tagged with a flag. Before a major GC the flag is swapped so that evacuate_static can distinguish static objects flagged in the current GC from those flagged in the previous GC.

Static objects are only collected in major GC.

Conclusion

Most of these objects require a combination of global data structures (like stable name and pointer tables), capability-local lists (large objects, pinned objects, weak pointers, threads) and generation-local lists (large objects, pinned objects, weak pointers, compact objects, threads). Among these objects, most of the complexity is caused by weak pointers and threads, because of the special reachability rules. When these are added the runtime becomes quite complex but also useful.

---

1. This is a doubly-linked list so this operation is efficient.↩

2. The info table is defined here. The 1 for one pointer field for C finalizer list, 4 is for four non-pointer fields for the key, value, Haskell finalizer, and a field to make an intrusive linked lists from weak objects.↩

3. The C finalizers field is used by addCFinalizerToWeak# primop. I don’t know what high-level functions use this. C finalizers are like Haskell finalizers, but they’re more reliable in that they’re always called eventually when key of a weak objects becomes unreachable (in the worst case when the Haskell process terminates).↩

4. This is actually a “misfeature”. Ideally a ThreadId would only keep the thread alive when it still has work to do.↩

5. Why do we need two performMajorGCs and a yield in between? I don’t understand this yet, but I can see in gdb that the thread is definitely resurrected during the first GC and added to the run queue. The reason why we need the other stuff is probably related with the scheduler.↩

6. The name choice here is terrible because it’s making searching for uses impossible. For this reason I have a commit that renames this to thread_list which I cherry-pick to my work branches.↩

7. This is done via HEAP_ALLOCED macro, which checks if the object is outside of heap.↩

by omer at May 15, 2018 05:35 AM

Guide to matrix.org and riot.im

NOTE: This guide is essentially me taking notes while I learn about the matrix.org/riot.im projects. Some of it is almost certainly wrong. And I'm trying to take notes on how an end user uninterested in the technical underpinnings work. There is clearly much more to these projects than I imply here. If you have suggestions for improvements, please send a PR.

As anyone on the internet or a cell phone knows, there are very, very many different and competing messenger applications out there. I recently started using Matrix and Riot. I didn't find a good "getting started" guide to these systems, and so decided to write down my findings here in such a setup.

I'm not going to belabor this point too much, but I want to at least acknowledge the question: why should I start using a new system when so many other, more popular options exist? And especially one that apparently requires a guide to use correctly! Here is my quick list of reasons why I started using these systems:

• Fully open source tooling and open protocols: no lock in at all
• Potential to use alternative, lighter-weight clients if desired
• Encryption
• Full decentralization

If these reasons don't seem important to you, you may want to stick with more mainstream tooling. I'm particularly interested in these options for open source project communication, which is also why I'm writing this blog post (to help others onboard more easily). More on that topic in a separate blog post.

Matrix.org vs Riot.im

Matrix, hosted at matrix.org, is "An open network for secure, decentralized communication." It is a protocol people use to communicate with each other. There is a concrete server at matrix.org that speaks this protocol, but you're free to run your own server on your own machine. That's the "decentralized" aspect of things.

Riot is the "default" application for talking with Matrix. It's a web app, a Desktop app (via Electron), and a mobile app. Just like the server, the client has alternatives as well, including text-based interfaces.

Since I'm going for simple overview of the common use case here, I'm going to assume you're using the matrix.org server and the Riot.im client.

Identifiers/entities

As you'd expect, there are users on Matrix. You can create an account with Riot and get a username. I did this myself, and created my standard username: snoyberg. If Matrix was a more standard system, you may think you could find me as @snoyberg. However, that's not the case. Remember, there are different servers in the network, and matrix.org is just one of them. Therefore, we need to state which server I'm a part of. Therefore, my identifier is @snoyberg:matrix.org.

There's a convenient site, matrix.to, which will allow you to create URLs linking to specific entities. When you visit these pages, you'll see links to communicate with those entities. If you enter @snoyberg:matrix.org on matrix.to, you'll get the URL https://matrix.to/#/@snoyberg:matrix.org.

Besides users, there are two other entities you can create and interact with:

• Chat rooms, which begin with #
• Communities (aka teams and groups), which begin with +

As two concrete examples:

• https://matrix.to/#/@commercialhaskell:matrix.org
• https://matrix.to/#/+commercialhaskell:matrix.org

Summary You can use https://matrix.to to create links to entities. Entities must include the server they are a part of, which will usually be :matrix.org at the end. The @ prefix is for users, # is for channels, and + is for communitites.

Rooms

Rooms are places where multiple people can have a conversation. You can create a new room with the icon with a + sign in the bottom-left corner of Riot. You can give each room a name when creating it. Once you're in the room, you can invite people via the "Invite" icon in the bottom right.

You can invite via email address. If they aren't already on Matrix, they'll get an invitation email to sign up. You can also invite via ID. Remember, if you wanted to invite me, don't just use snoyberg; you need to use @snoyberg:matrix.org.

You can click on the gear icon in the top-middle of the screen to open a bunch of settings for a room. Changing the name and topic of the room are fairly self-explanatory. To me, the most interesting settings are around privacy.

You can change who has access to a room. By default, each person must be invited to the room. You can also allow people to join via a link. In order to do this, you need to create an address for a room. This would be something like #myroomid:matrix.org. For example, I created a room @commercialhaskell:matrix.org.

You can also choose whether a room will be listed in the Matrix directory.

Communities

Communities seem to be a relatively new feature, and not all clients support them yet. It seems to me that they are adding two nice things:

• Create a description for a community
• Add a bunch of related rooms

I'm still exploring this feature, but I think it will fill the exact niche I need for my open source project maintenance. If you're interested, you can check out the Commercial Haskell community I created.

Bridging

This seems to be a "killer feature" for Matrix. There are lots of apps available for it to bridge with other systems, including IRC and Slack. For example, #haskell:matrix.org is a bridge to the #haskell channel on Freenode (IRC).

For open source work, I'm hoping that this kind of bridging will allow people who prefer IRC to interact with those looking for clients with a different interface.

UPDATE May 15, 2018 I found a great guide that demonstrates how to get tighter integration with IRC: https://opensource.com/article/17/5/introducing-riot-IRC.

May 14, 2018 01:28 PM

The end of Bake

Summary: I no longer develop Bake, my continuous integration tool.

In 2014 I started a new project of a continuous integration system, named Bake. The selling point of Bake was that it provided always-correct master development, but didn't require running all tests on all patches, allowing the development to scale much faster than the test resources. Over time I refined the model and figured out exactly how to optimise throughput. The experiments were promising, but I'm no longer working on Bake, because:

• I wrote Bake with an eye to a particular set of challenges for my employer. I then changed jobs, and the challenges have changed. I don't have a strong need for Bake, and I don't think a project like Bake can be successful without dogfooding.
• I have plenty of other projects that are fighting for my attention. While I think Bake is cool, it's certainly at the early stages, I think it needs a lot of work to have any meaningful impact.
• Bake has a clever algorithm (I <3 algorithms!), and now needs a ton of evangalism, polish and web UI work (I was a webdev in a previous life, but it's not something I want to spend my spare time on).
• The problem space that Bake targets is a bit weird. Open-source projects with a small contributor base (less than 5 people full time) are well served by Travis/Appveyor etc, which I happily use for all my open-source projects. Big tech companies (e.g. Google and Facebook) can aford to throw hardware at the problem and have custom solutions. That leaves Bake with the niche of 5-500 commerical programmer teams, which isn't such a natural fit for open-source software.

What I didn't find is any design flaw in the approach. I still think the ideas behind Bake are valuable, so would love to see them go somewhere, but leave it to others. The code remains on GitHub with a stack.yaml and shell.nix that should (in theory) let people play with it indefinitely, but I won't be accepting any patches - other than to point at forks.

by Neil Mitchell (noreply@blogger.com) at May 13, 2018 09:02 PM

Practical Property Testing in Haskell

We aired our second webinar in our ongoing series on Wednesday, May 9th. The topic was "Practical Property Testing in Haskell." This webinar is one in our continuing series covering topics in Haskell Programming, DevOps, Cloud Computing, Cryptocurrencies, FinTech, Medical Device Software, DataOps, and all the other great things we do. If you want to be notified of future webinars, we highly recommend you subscribe to our blog post by providing your email and clicking  the   button  on the top right of this page .

by Robert Bobbett (robert@fpcomplete.com) at May 10, 2018 06:53 PM

Practical Property Testing in Haskell

We aired our second webinar in our ongoing series on Wednesday, May 9th. The topic was "Practical Property Testing in Haskell." This webinar is one in our continuing series covering topics in Haskell Programming, DevOps, Cloud Computing, Cryptocurrencies, FinTech, Medical Device Software, DataOps, and all the other great things we do. If you want to be notified of future webinars, we highly recommend you subscribe to our blog post by providing your email and clicking  the   button  on the top right of this page .

by Robert Bobbett (robert@fpcomplete.com) at May 10, 2018 06:53 PM

Journal of Financial Technology

I've just been appointed to the editorial board of the newly formed Journal of Financial Technology. Please submit! Our second issue will be a special issue devoted to formal methods.

by Philip Wadler (noreply@blogger.com) at May 09, 2018 11:35 PM

Pinpointing deadlocks in Haskell

Concurrent programming is hard! I still remember the moment of my introduction to multi-threaded programming at the University of New Mexico, our professor grabbed his head and said: “Here be demons!”. There are all sorts of issues that arise in a concurrent setup, such as race conditions, starvation, deadlocks, data corruption, you name it. All of these are also applicable to Haskell, and in this post, I would like to introduce a simple yet very effective way to track down deadlocks.

by Alexey Kuleshevich (alexey@fpcomplete.com) at May 09, 2018 08:32 PM

Apply to attend the Oregon Programming Languages Summer School!

Although the official deadline has passed, I hear there are still a few spots left for the Oregon Programming Languages Summer School (OPLSS), hosted at the University of Oregon in Eugene. This is a really fantastic opportunity to take a deep dive in programming languages and type theory. I attended as a graduate student and although it was overwhelming at times—like drinking from a fire hose!—it was a wonderful experience. I made some great friends and learned a ton (I still occasionally refer back to my notes!). Eugene is also beautiful in the summer (I have fond memories of going geocaching in a nearby park).

The main summer school (July 9–21) has a focus on parallelism and concurrency, but for those with less background, there is also a one-week introduction on the foundations of programming languages (July 3–8). If you want, you can actually choose to attend only the July 3–8 session (or both, or just July 9–21 of course). Attending just the introductory session could be a great option for someone who knows some functional programming but wants a more solid grounding in the underlying theory.

If you’re a member of the Haskell/FP community who is thinking of applying, and I’m familiar with you or your work, I would be happy to write you a recommendation if you need one.

by Brent at May 09, 2018 02:21 AM

[mmpffczs] Generating Keccak round constants

We investigate the round constants for the Keccak hash function (of which SHA-3 is a subset).  We work mostly from the officially published SHA-3 standard which was a little bit easier to understand than the reference specification.

These round constants are used in Keccak's iota step-mapping function.  The internal function rc(t) is a linear-feedback shift register (LFSR) with 8 bits of state and a period of 255.  Its period is 255 if its state is seeded with a nonzero value, which it is, namely the value 1.  Here is its full period, grouped in chunks of 7 for reasons which will be made clear shortly.  We write the 0 bit as period "." and the 1 bit as "1" to be able to easily distinguish them: 1...... .1.11.. .1111.1 ....111 11111.. 1....1. 1..1111 1.1.1.1 .111... ..11... 1.1.11. .11..1. 111111. 1111..1 1.111.1 11..1.1 .1..1.1 ...1..1 .11.1.. .11..11 1..1111 ...11.1 1....1. ..1.111 .1.1111 .11.111 11....1 1.1..11 .1.11.1 1.1.1.. ...1..1 11.11.. 1..1..1 1...... 111.1.. 1...111 ...

The Keccak round constants are easiest to understand in binary.  We write binary constants below with the least significant bit on the left (little-endian), opposite the standard convention of writing numbers.

Round
0	1...............................................................
1	.1.....1.......1................................................
2	.1.1...1.......1...............................................1
3	...............1...............1...............................1
4	11.1...1.......1................................................
5	1..............................1................................
6	1......1.......1...............1...............................1
7	1..1...........1...............................................1
8	.1.1...1........................................................
9	...1...1........................................................
10	1..1...........1...............1................................
11	.1.1...........................1................................
12	11.1...1.......1...............1................................
13	11.1...1.......................................................1
14	1..1...1.......1...............................................1
15	11.............1...............................................1
16	.1.............1...............................................1
17	.......1.......................................................1
18	.1.1...........1................................................
19	.1.1...........................1...............................1
20	1......1.......1...............1...............................1
21	.......1.......1...............................................1
22	1..............................1................................
23	...1...........1...............1...............................1

Of the 64 bit positions for each 64-bit constant, only 7 can ever be set, seen in the rough columns of 1s at bit positions 2^j-1 above.  Whether a position is set or not is taken from the output of the LFSR defined above (which is why we grouped the output in chunks of 7).  It is curious that Keccak uses such sparse binary round constants; the best explanation I can imagine is that it reduces the gate count in unrolled hardware implementations.  It's nice that Keccak is secure despite such weak round constants which barely modify values each round and differ so little between rounds.

The last round (of 64-bit Keccak, i.e., w=64) always uses the round constant with index 23 above.  If you wish to do Keccak with fewer than 24 rounds, then start somewhere in the middle, ending at round 23.  If you wish to do Keccak with more than 24 rounds, then start at a negative round index.  This is kind of bizarre, but I think the reason is something along the lines of being able to reuse cryptanalytic results from reduced-round variants.  Incidentally, negative round indices means that the rc(t) function must be able to handle negative t, so your (mod 255) operation must give a proper positive result for negative input.  Because 255 (the period of the LFSR) and 7 (the number of bits consumed per round constant) are relatively prime, the round constants cycle with a period of 255.  The period could have been less if the number of LFSR bits consumed per round constant shared factors with 255=3*5*17.  Here is the full list of round constants (in big-endian hexadecimal) for as many rounds of Keccak you care to do:

RC[-231] = 0x8000000080008082
RC[-230] = 0x800000008000800a
RC[-229] = 0x8000000000000003
RC[-228] = 0x8000000080000009
RC[-227] = 0x8000000000008082
RC[-226] = 0x0000000000008009
RC[-225] = 0x8000000000000080
RC[-224] = 0x0000000000008083
RC[-223] = 0x8000000000000081
RC[-222] = 0x0000000000000001
RC[-221] = 0x000000000000800b
RC[-220] = 0x8000000080008001
RC[-219] = 0x0000000000000080
RC[-218] = 0x8000000000008000
RC[-217] = 0x8000000080008001
RC[-216] = 0x0000000000000009
RC[-215] = 0x800000008000808b
RC[-214] = 0x0000000000000081
RC[-213] = 0x8000000000000082
RC[-212] = 0x000000008000008b
RC[-211] = 0x8000000080008009
RC[-210] = 0x8000000080000000
RC[-209] = 0x0000000080000080
RC[-208] = 0x0000000080008003
RC[-207] = 0x8000000080008082
RC[-206] = 0x8000000080008083
RC[-205] = 0x8000000080000088
RC[-204] = 0x0000000000008089
RC[-203] = 0x0000000000008009
RC[-202] = 0x8000000000000009
RC[-201] = 0x0000000080008008
RC[-200] = 0x0000000080008001
RC[-199] = 0x800000000000008a
RC[-198] = 0x800000000000000b
RC[-197] = 0x0000000000000089
RC[-196] = 0x0000000080000002
RC[-195] = 0x800000000000800b
RC[-194] = 0x000000008000800b
RC[-193] = 0x000000000000808b
RC[-192] = 0x0000000080000088
RC[-191] = 0x800000000000800a
RC[-190] = 0x0000000080000089
RC[-189] = 0x8000000000000001
RC[-188] = 0x8000000000008088
RC[-187] = 0x8000000000000081
RC[-186] = 0x0000000000000088
RC[-185] = 0x0000000080008080
RC[-184] = 0x0000000000000081
RC[-183] = 0x800000000000000b
RC[-182] = 0x0000000000000000
RC[-181] = 0x0000000000000089
RC[-180] = 0x000000008000008b
RC[-179] = 0x8000000080008080
RC[-178] = 0x800000000000008b
RC[-177] = 0x8000000000008000
RC[-176] = 0x8000000080008088
RC[-175] = 0x0000000080000082
RC[-174] = 0x000000000000000b
RC[-173] = 0x800000000000000a
RC[-172] = 0x0000000000008082
RC[-171] = 0x8000000000008003
RC[-170] = 0x800000000000808b
RC[-169] = 0x800000008000000b
RC[-168] = 0x800000008000008a
RC[-167] = 0x0000000080000081
RC[-166] = 0x0000000080000081
RC[-165] = 0x0000000080000008
RC[-164] = 0x0000000000000083
RC[-163] = 0x8000000080008003
RC[-162] = 0x0000000080008088
RC[-161] = 0x8000000080000088
RC[-160] = 0x0000000000008000
RC[-159] = 0x0000000080008082
RC[-158] = 0x0000000080008089
RC[-157] = 0x8000000080008083
RC[-156] = 0x8000000080000001
RC[-155] = 0x0000000080008002
RC[-154] = 0x8000000080000089
RC[-153] = 0x0000000000000082
RC[-152] = 0x8000000080000008
RC[-151] = 0x8000000000000089
RC[-150] = 0x8000000080000008
RC[-149] = 0x8000000000000000
RC[-148] = 0x8000000000000083
RC[-147] = 0x0000000080008080
RC[-146] = 0x0000000000000008
RC[-145] = 0x8000000080000080
RC[-144] = 0x8000000080008080
RC[-143] = 0x8000000000000002
RC[-142] = 0x800000008000808b
RC[-141] = 0x0000000000000008
RC[-140] = 0x8000000080000009
RC[-139] = 0x800000000000800b
RC[-138] = 0x0000000080008082
RC[-137] = 0x0000000080008000
RC[-136] = 0x8000000000008008
RC[-135] = 0x0000000000008081
RC[-134] = 0x8000000080008089
RC[-133] = 0x0000000080008089
RC[-132] = 0x800000008000800a
RC[-131] = 0x800000000000008a
RC[-130] = 0x8000000000000082
RC[-129] = 0x0000000080000002
RC[-128] = 0x8000000000008082
RC[-127] = 0x0000000000008080
RC[-126] = 0x800000008000000b
RC[-125] = 0x8000000080000003
RC[-124] = 0x000000000000000a
RC[-123] = 0x8000000000008001
RC[-122] = 0x8000000080000083
RC[-121] = 0x8000000000008083
RC[-120] = 0x000000000000008b
RC[-119] = 0x000000000000800a
RC[-118] = 0x8000000080000083
RC[-117] = 0x800000000000800a
RC[-116] = 0x0000000080000000
RC[-115] = 0x800000008000008a
RC[-114] = 0x0000000080000008
RC[-113] = 0x000000000000000a
RC[-112] = 0x8000000000008088
RC[-111] = 0x8000000000000008
RC[-110] = 0x0000000080000003
RC[-109] = 0x8000000000000000
RC[-108] = 0x800000000000000a
RC[-107] = 0x000000000000800b
RC[-106] = 0x8000000080008088
RC[-105] = 0x000000008000000b
RC[-104] = 0x0000000080000080
RC[-103] = 0x000000008000808a
RC[-102] = 0x8000000000008009
RC[-101] = 0x0000000000000003
RC[-100] = 0x0000000080000003
RC[-99] = 0x8000000000000089
RC[-98] = 0x8000000080000081
RC[-97] = 0x800000008000008b
RC[-96] = 0x0000000080008003
RC[-95] = 0x800000008000800b
RC[-94] = 0x8000000000008008
RC[-93] = 0x0000000000008008
RC[-92] = 0x8000000000008002
RC[-91] = 0x8000000000000009
RC[-90] = 0x0000000080008081
RC[-89] = 0x000000000000808a
RC[-88] = 0x000000008000800a
RC[-87] = 0x0000000000000080
RC[-86] = 0x8000000000008089
RC[-85] = 0x800000000000808a
RC[-84] = 0x8000000080008089
RC[-83] = 0x0000000080008000
RC[-82] = 0x8000000000008081
RC[-81] = 0x000000008000800a
RC[-80] = 0x0000000000000009
RC[-79] = 0x8000000080008002
RC[-78] = 0x000000008000000a
RC[-77] = 0x0000000080008002
RC[-76] = 0x8000000080000000
RC[-75] = 0x0000000080000009
RC[-74] = 0x0000000000008088
RC[-73] = 0x0000000000000002
RC[-72] = 0x0000000080008008
RC[-71] = 0x0000000080008088
RC[-70] = 0x8000000080000001
RC[-69] = 0x000000008000808b
RC[-68] = 0x8000000000000002
RC[-67] = 0x8000000080008002
RC[-66] = 0x0000000080000083
RC[-65] = 0x0000000000008089
RC[-64] = 0x0000000000008080
RC[-63] = 0x8000000080000082
RC[-62] = 0x8000000000000088
RC[-61] = 0x800000008000808a
RC[-60] = 0x000000000000808a
RC[-59] = 0x0000000080008083
RC[-58] = 0x000000008000000b
RC[-57] = 0x0000000080000009
RC[-56] = 0x0000000000008001
RC[-55] = 0x0000000080000089
RC[-54] = 0x8000000000000088
RC[-53] = 0x8000000080008003
RC[-52] = 0x0000000080008001
RC[-51] = 0x8000000000000003
RC[-50] = 0x8000000080000080
RC[-49] = 0x8000000080008009
RC[-48] = 0x8000000080000089
RC[-47] = 0x000000000000000b
RC[-46] = 0x8000000000000083
RC[-45] = 0x0000000080008009
RC[-44] = 0x0000000080000083
RC[-43] = 0x0000000000008000
RC[-42] = 0x000000008000800b
RC[-41] = 0x0000000000008002
RC[-40] = 0x0000000000000003
RC[-39] = 0x000000008000008a
RC[-38] = 0x8000000080000002
RC[-37] = 0x0000000000008001
RC[-36] = 0x0000000080000000
RC[-35] = 0x8000000080000003
RC[-34] = 0x0000000000000083
RC[-33] = 0x800000008000808a
RC[-32] = 0x0000000000008003
RC[-31] = 0x0000000000008008
RC[-30] = 0x800000000000808b
RC[-29] = 0x8000000080000082
RC[-28] = 0x8000000000000001
RC[-27] = 0x8000000000008001
RC[-26] = 0x800000008000000a
RC[-25] = 0x8000000080008008
RC[-24] = 0x800000008000800b
RC[-23] = 0x8000000000008081
RC[-22] = 0x0000000080008083
RC[-21] = 0x0000000080000082
RC[-20] = 0x0000000000000082
RC[-19] = 0x8000000080000081
RC[-18] = 0x8000000080000002
RC[-17] = 0x0000000000008088
RC[-16] = 0x000000000000008b
RC[-15] = 0x0000000000008083
RC[-14] = 0x8000000000000008
RC[-13] = 0x000000008000008a
RC[-12] = 0x800000008000008b
RC[-11] = 0x000000008000808a
RC[-10] = 0x8000000000008080
RC[-9] = 0x0000000080000088
RC[-8] = 0x8000000000008083
RC[-7] = 0x0000000000000002
RC[-6] = 0x0000000080008081
RC[-5] = 0x0000000000008003
RC[-4] = 0x0000000000008081
RC[-3] = 0x8000000080008000
RC[-2] = 0x0000000000008002
RC[-1] = 0x000000000000008a
RC[0] = 0x0000000000000001
RC[1] = 0x0000000000008082
RC[2] = 0x800000000000808a
RC[3] = 0x8000000080008000
RC[4] = 0x000000000000808b
RC[5] = 0x0000000080000001
RC[6] = 0x8000000080008081
RC[7] = 0x8000000000008009
RC[8] = 0x000000000000008a
RC[9] = 0x0000000000000088
RC[10] = 0x0000000080008009
RC[11] = 0x000000008000000a
RC[12] = 0x000000008000808b
RC[13] = 0x800000000000008b
RC[14] = 0x8000000000008089
RC[15] = 0x8000000000008003
RC[16] = 0x8000000000008002
RC[17] = 0x8000000000000080
RC[18] = 0x000000000000800a
RC[19] = 0x800000008000000a
RC[20] = 0x8000000080008081
RC[21] = 0x8000000000008080
RC[22] = 0x0000000080000001
RC[23] = 0x8000000080008008

The final 24 constants agree with those published at Team Keccak.  If you need more than 255 rounds, RC[-232] loops back to RC[23] and so forth.

Observations: In 24-round normal Keccak, rounds 5 and 22 use the same round constant, as do rounds 6 and 20.  Keccak with 25 rounds or more additionally sees the same round constant on rounds -1 and 8.  27 rounds or more sees duplication at rounds -3 and 3.  At 255 rounds (full period), there are 128 unique round constants, with every constant repeated twice except the zero constant which only occurs at round -182.

32-bit Keccak (w=32) uses the lower 32 bits of the round constants above.  7 bits of the LFSR are still consumed for each constant; 1/7 of the bits are thrown away.  There are by default 22 rounds total with last round having round index 21.  Duplicated pairs are rounds (6,20) and (11,19).  Doing more rounds causes more repeated round constants: doing 6 additional rounds (22 + 6 = 28 total) sees triplication of constants in rounds -6, 6, and 20.  16-bit Keccak has 20 rounds, duplication at (0,5), (4,12), (7,10), and (11,19) and first triplication with 6 extra rounds (-6,-4,6).  8-bit Keccak (18 rounds) sees repeated constants in rounds (0,5), (2,8), (4,12,13), and (7,10).

If we wish to extend Keccak to 128-bit lane width (w) or more, we would want to consume more than 7 LFSR bits per round, maybe also use a longer-period LFSR.  This should be safe, as these round constants are Nothing-Up-My-Sleeve numbers, so other numbers should also be safe to use.  A deeper Keccak will probably want other modifications also, for example the rho step-mapping function.  Its 25 triangular numbers, representing rotation amounts, grow only up to 300, but we would like larger rotations for better diffusion if the lane width is significantly longer than 300.

Here is an implementation in Haskell of the generation of these Keccak round constants.  We represented bit strings as lists of Bool.

by Ken (noreply@blogger.com) at May 08, 2018 04:46 AM

Katara constructs finite projective planes

This weekend I got a very exciting text message from Katara:

I have a math question for you

Oh boy! I hope it's one I can answer.

Okay

there's this game called spot it where you have cards with 8 symbols on them like so

<figure> </figure>

and the goal is to find the one matching symbol on your card and the one in the middle

how is it possible that given any pair of cards, there is exactly one matching symbol

Well, whatever my failings as a dad, this is one problem I can solve. I went a little of overboard in my reply:

You need a particular kind of structure called a projective plane.

They only exist for certain numbers of symbols

A simpler example has 7 cards with 3 symbols each.

One thing that's cool about it is that the symbols and the cards are "dual": say you give each round card a name. Then make up a new deck of square cards. There's one square card for each symbol. So there's a square"Ladybug" card. The Ladybug card has on it the names of the round cards that have the Ladybug. Now you can play Spot with the square cards instead of the round ones: each two square cards have exactly one name in common.

In a geometric plane any two points lie on exactly one common line and any two lines intersect in exactly one common point. This is a sort of finite model of that, with cards playing the role of lines and symbols playing the role of points. Or vice versa, it doesn't matter.

More than you wanted to know 😂

ah thank you, I'm pretty sure I understand, sorry for not responding, my phone was charging

I still couldn't shut up about the finite projective planes:

No problem! No response necessary.

It is known that all finite projective planes have n²+n+1 points for some n. So I guess the Spot deck has either 31, 57, or 73 cards and the same number of symbols. Is 57 correct?

Must be 57 because I see from your picture that each card has 8 symbols.

Katara was very patient:

I guess, I would like to talk about this some more when i get home if that's okay

Any time.

(The game costs $13.)

Anyway this evening I cut up some index cards, and found a bunch of stickers in a drawer, and made Katara a projective plane of order 3. This has 13 cards, each with 4 different stickers, and again, every two cards share exactly one sticker. She was very pleased and wanted to know how to make them herself.

Each set of cards has an order, which is a non-negative integer. Then there must be cards, each with stickers or symbols. When is a prime power, you can use field theory to construct a set of cards from the structure of the (unique) field of order .

Fields to projective planes

Order 2

I'll describe the procedure using the plane of order , which is unusually simple. There will be cards, each with of the symbols.

Here is the finite field of order 2, called :

+ 0 1 0 0 1 1 1 0

× 0 1 0 0 0 1 0 1

• The stickers correspond to ordered triples of elements of , except that is always omitted. So they are:

  $$\require{cancel}\begin{array}{cc} \cancel{\langle 0,0,0\rangle} & \langle 1,0,0\rangle \\ \langle 0,0,1\rangle & \langle 1,0,1\rangle \\ \langle 0,1,0\rangle & \langle 1,1,0\rangle \\ \langle 0,1,1\rangle & \langle 1,1,1\rangle \\ \end{array} $$

  Of course, you probably do not want to use these symbols exactly. You might decide that is a sticker with a picture of a fish, and is a sticker with a ladybug.

• Each card will have stickers. To generate a card, pick any two stickers that haven't appeared together before and put them on the card. Say these stickers correspond to the triples and . To find the triple for the third sticker on the card, just add the first two triples componentwise, obtaining . Remember that the addition must be done according to the addition table above! So for example if a card has and , its third triple will be

  $$\begin{align} \langle 1,0,1 \rangle + \langle 0,1,1 \rangle & = \\ \langle 1+0,0+1,1+1 \rangle & = \\ \langle 1,1,0 \rangle \end{align} $$

  Observe that it doesn't matter which two triples you add; you always get the third one!

Okay, well, that was simple.

Larger order

After Katara did the order 2 case, which has 7 cards, each with 3 of the 7 kinds of stickers, she was ready to move on to something bigger. I had already done the order 3 deck so she decided to do order 4. This has cards each with 5 of the 21 kinds of stickers. The arithmetic is more complicated too; it's instead of :

+ 0 1 2 3 0 0 1 2 3 1 1 0 3 2 2 2 3 0 1 3 3 2 1 0

× 0 1 2 3 0 0 0 0 0 1 0 1 2 3 2 0 2 3 1 3 0 3 1 2

When the order is larger than 2, there is another wrinkle. There are possible triples, and we are throwing away as usual, so we have 63. But we need , not .

Each sticker is represented not by one triple, but by three. The triples and must be understood to represent the same sticker, all the multiplications being done according to the table above. Then each group of three triples corresponds to a sticker, and we have 21 as we wanted.

Each triple must have a leftmost non-zero entry, and in each group of three similar triples, there will be one where this leftmost non-zero entry is a ; we will take this as the canonical representative of its class, and it can wear a costume or a disguise that makes it appear to begin with a or a .

We might assign stickers to triples like this:

$$ \begin{array}{rl} \cancel{\langle 0,0,0\rangle} & \\ \langle 0,0,1 \rangle & \text{apple} \\ \hline \langle 0,1,0 \rangle & \text{bicycle} \\ \langle 0,1,1 \rangle & \text{carrot} \\ \langle 0,1,2 \rangle & \text{dice} \\ \langle 0,1,3 \rangle & \text{elephant} \\ \hline \langle 1,0,0 \rangle & \text{frog} \\ \langle 1,0,1 \rangle & \text{goat} \\ \langle 1,0,2 \rangle & \text{hat} \\ \langle 1,0,3 \rangle & \text{igloo} \\ \langle 1,1,0 \rangle & \text{jellyfish} \\ \langle 1,1,1 \rangle & \text{kite} \\ \langle 1,1,2 \rangle & \text{ladybug} \\ \langle 1,1,3 \rangle & \text{mermaid} \\ \langle 1,2,0 \rangle & \text{nose} \\ \langle 1,2,1 \rangle & \text{octopus} \\ \langle 1,2,2 \rangle & \text{piano} \\ \langle 1,2,3 \rangle & \text{queen} \\ \langle 1,3,0 \rangle & \text{rainbow} \\ \langle 1,3,1 \rangle & \text{shoe} \\ \langle 1,3,2 \rangle & \text{trombone} \\ \langle 1,3,3 \rangle & \text{umbrella} \\ \end{array} $$

We can stop there, because everything after begins with a or a , and so is some other triple in disguise. For example what sticker goes with ? That's actually in disguise, it's , which is “dice”. Okay, how about ? That's the same as , which is “ladybug”. There are , as we wanted. Note that the naturally breaks down as , depending on how many zeroes are at the beginning; that's where that comes from.

Now, just like before, to make a card, we pick two triples that have not yet gone together, say and . We start adding these together as before, obtaining . But we must also add together the disguised versions of these triples, and for the first, and and for the second. This gets us two additional sums, , which is in disguise, and , which is in disguise.

It might seem like it also gets us and , but these are just again, in disguise. Since there are three disguises for and three for , we have nine possible sums, but it turns out the the nine sums are only three different triples, each in three different disguises. So our nine sums get us three additional triples, and, including the two we started with, that makes five, which is exactly how many we need for the first card. The first card gets the stickers for triples and which are apple, bicycle, carrot, dice, and elephant.

That was anticlimactic. Let's do one more. We don't have a card yet with ladybug and trombone. These are and , and we must add them together, and also the disguised versions:

$$\begin{array}{c|ccc} & \langle 1,1,2 \rangle & \langle 2,2,3 \rangle & \langle 3,3,1 \rangle \\ \hline \langle 1,3,2 \rangle & \langle 0,2,0 \rangle & \langle 3,1,1 \rangle & \langle 2,0,3 \rangle \\ \langle 2,1,3 \rangle & \langle 3,0,1 \rangle & \langle 0,3,0 \rangle & \langle 1,2,2 \rangle \\ \langle 3,2,1 \rangle & \langle 2,3,3 \rangle & \langle 1,0,2 \rangle & \langle 0,1,0 \rangle \\ \end{array}$$

These nine results do indeed pick out three triples in three disguises each, and it's easy to select the three of these that are canonical: they have a 1 in the leftmost nonzero position, so the three sums are and , which are bicycle, hat, and piano. So the one card that has a ladybug and a trombone also has a bicycle, a hat, and a piano, which should not seem obvious. Note that this card does have the required single overlap with the other card we constructed: both have bicycles.

Well, that was fun. Katara did hers with colored dots instead of stickers:

<figure> </figure>

The ABCDE card is in the upper left; the bicycle-hat-ladybug-piano-trombone one is the second row from the bottom, second column from the left. The colors look bad in this picture; the light is too yellow and so all the blues and purples look black.x

After I took this picture, we checked these cards and found a couple of calculation errors, which we corrected. A correct set of cards is:

$$ \begin{array}{ccc} \text{abcde} & \text{bhlpt} & \text{dgmpr} \\ \text{afghi} & \text{bimqu} & \text{dhjou} \\ \text{ajklm} & \text{cfkpu} & \text{diknt} \\ \text{anopq} & \text{cgjqt} & \text{efmot} \\ \text{arstu} & \text{chmns} & \text{eglnu} \\ \text{bfjnr} & \text{cilor} & \text{ehkqr} \\ \text{bgkos} & \text{dflqs} & \text{eijps} \\ \end{array} $$

Fun facts about finite projective planes:

• This construction always turns a finite field of order into a finite projective plane of order .

• A finite field of order exists exactly when is a prime power and then there is exactly one finite field. So this construction gives us finite projective planes of orders , but not of orders . Do finite projective planes of those latter orders exist?

  • 6: No, proven by R.C. Bose in 1938
  • 10: No, proven by Clement Lam in 1991 with a very large computer search
  • 12, 15: Nobody knows.
  • 14: No, by the Bruck-Ryser theorem (1949).

• Is this method the only way to construct a finite projective plane? Yes, when . But there are four non-isomorphic projective planes of order , and this only constructs one of them.

  What about for ? Nobody knows.

by Mark Dominus (mjd@plover.com) at May 07, 2018 05:21 PM

Conversations with a six-year-old on functional programming

My six-year-old son walked up to me yesterday. “What are you reading?”

At the time, I was reading part of Janis Voigtländer’s habilitation thesis. Unsure where to even start, I decided to just answer straightforwardly: “I’m reading a very long story about free theorems.”

He persisted. “What are free theorems?”

Never one to shrink from a pedagogical challenge, I thought for a moment, then began: “Do you know what a function is?” He didn’t. “A function is like a machine where you put something in one end and something comes out the other end. For example, maybe you put a number in, and the number that is one bigger comes out. So if you put in three, four comes out, or if you put in six, seven comes out.” This clearly made sense to him, so I continued, “The type of a function machine tells you what kinds of things you put in and what kinds of things come out. So maybe you put a number in and get a number out. Or maybe you put in a list of numbers and get a number out.” He interrupted excitedly, “Or maybe you could put words in??” “Yes, exactly! Maybe you can put words in and get words out. Or maybe there is a function machine where you put other function machines in and get function machines out!” He gasped in astonishment at the idea of putting function machines into function machines.

“So,” I concluded, “a free theorem is when you can say something that is always true about a function machine if you only know its type, but you don’t know anything about what it does on the inside.” This seemed a bit beyond him (and to be fair, free theorems are only interesting when polymorphism is involved which I definitely didn’t want to go into). But the whole conversation had given me a different idea.

“Hey, I have a good idea for a game,” I said. “It’s called the function machine game. I will think of a function machine. You tell me things to put into the function machine, and I will tell you what comes out. Then you have to guess what the function machine does.” He immediately liked this game and it has been a huge hit; he wants to play it all the time. We played it while driving to a party yesterday, and we played it this morning while I was in the shower. So far, he has correctly guessed:

• 
• 
• 
• 
• 
• 
• 

I tried but that was a bit tough for him. I realized that in some cases he may understand intuitively what the function does but have trouble expressing it in words (this was also a problem with ), so we started using the obvious variant where once the guesser thinks they know what the function does, the players switch roles and the person who came up with function specifies some inputs in order to test whether the guesser is able to produce the correct outputs.

was also surprisingly difficult for him to guess (though he did get it right eventually). I think he was just stuck on the idea of the function doing something arithmetical to the input, and was having trouble coming up with some sort of arithmetic procedure which would result in no matter what you put in! It simply hadn’t occurred to him that the machine might not care about the input. (Interestingly, many students in my functional programming class this semester were also confused by constant functions when we were learning about the lambda calculus; they really wanted to substitute the input somewhere and were upset/confused by the fact that the bound variable did not occur in the body at all!)

After a few rounds of guessing my functions, he wanted to come up with his own functions for me to guess (as I knew he would). Sometimes his functions are great and sometimes they don’t make sense (usually because his idea of what the function does changes over time, which of course he, in all sincerity, denies), but it’s fun either way. And after he finally understood , he came up with his own function which was something like

inspired, I think, by his kindergarten class where they were learning about pairs of numbers that added up to .

Definitely one of my better parenting days.

by Brent at May 06, 2018 07:19 PM

Shitpost roundup, 2018-04

Last month I regretted making only 22 posts but I promised:

April will be better; I'm on pace to break the previous volume record, and I've also been doing a good job of promoting better posts to the major leagues.

I blew it! I tied the previous volume record. But I also think I did do a decent job promoting the better posts. Usually I look over the previous month's posts and pick out two or three that seem to be of more interest than the others. Not this month! They are all shit, except the one ghostwritten by Anette Gordon-Reed. If this keeps up, I will stop doing these monthly roundup posts.

• Hotel classification jargon
• I'm missing !!Con this year
• Camptown
• Sigils in Perl and PILOT
• Birthday greetings from my stalker
• Yuca frita
• Intriguing trending hashtags
• On the preferred numbers of the One God
• Chitin
• History of the Unicode “byte order mark”; addendum
• 'Abd al-Karim
• One of everything in the universe
• Ruby improvement
• My hero Kurt Schwitters
• The hardest question ever asked on Math StackExchange
• Friday the 13th
• September 12 activities
• The National Day of Catalonia
• Melilla
• Beware…
• The joy of Dada [1] [2]
• FGSFDS
• Why we itch
• Why we have little hairs on our arms
• Minoxidil
• Ulcers
• Things English fails to distinguish
• Today I learned… [2] [3] [4] [5]
• Xiangtan
• Mealworm frass
• Free-range organically fed flies
• Not the worst job in the world
• Bug squeamishness
• Gordon-Reed on Andrew Johnson
• People suck
• Plagiarism, plagiarism, baked beans, and plagiarism
• I learned a new word!
• Phagocytization
• Lipogrammatic Math Stackexchange posts
• Hegel and the Seven Planets
• Philosophical duh
• Headline of the Month
• Why do people hate?
• Software sucks
• Comment of the day

by Mark Dominus (mjd@plover.com) at May 06, 2018 06:33 AM

April 2018 1HaskellADay Problems and Solutions

• April 25th, 2018: For Wednesday's #haskell problem we prove, definitively, @fermatslibrary n^5 is n ... for very small n. For Wednesday's #haskell solution we learn that number theory is so cool! 
  
• April 24th, 2018: For Tuesday's #haskell problem we look for a fix-point of simplifying HTML. Good thing it's not NP-hard! ... no ... wait. Tuesday's #haskell solution is the fix-point for HTML. Just like the fix-point for factorial. Structurally, maybe, but otherwise, kinda not. 
• April 23rd, 2018: What happens when things go wrong? We start to look at debugging for Monday's #haskell problem. For Monday's #haskell solution: the error is not here; the error is in another castle. 
  
• April 20th, 2018: Friday's #haskell problem is to decode HTML entities from titles of articles. Friday's #haskell solution: deHTMLification: get 
• April 18th, 2018: Hey! Let's store the raw JSON as a fall-back should our ETL process fail for Wednesday's #haskell problem. Wednesday's #Haskell solution: storing raw JSON in a SQL data store BECAUSE WE CAN! 
  
• April 17th, 2018: For Tuesday's #haskell problem we upload articles from a different publisher of a compressed JSON archive with a different format. We find adding a differently-structured set of articles to IxArt store is simple for Tuesday's #haskell solution. 
• April 16th, 2018: For Monday's #haskell problem, we take articles-as-json from various sources and put them into a common SQL data store. For Monday's #haskell solution we upload articles from different publications to a common SQL data store, both compressed and uncompressed archives. 
  
• April 13th, 2018: Friday's #haskell problem is to grab packets of articles from a REST endpoint for later processing. Friday's #haskell solution: Those are some rather large packets downloaded from the REST endpoint! 
• April 12th, 2018: Thursday's #haskell problem: auditing and logs. Thursday's #haskell solution is to wrap packet extraction and insertion in an ETL process. 
  
• April 11th, 2018: Wednesday's #haskell problem: when we download packets of articles, let's record that event. Wednesday's #haskell solution: we're inserting packets into our new database. 
  
• April 10th, 2018: Tuesday's #haskell problem: 🎵 "Does anybody know what time it is?" 🎶 (bonus: name that tune) Tuesday's #haskell solution: "Hey, Mister! You got the time?" 
• April 9th, 2018: Monday's #haskell problem is to extract article tags from JSON then store them in a PostgreSQL lookup table. Monday's #haskell solution: Inserting tags for articles into a PostgreSQL database is a breeze! 
  
• April 6th, 2018: Friday's #haskell problem is to parse categories-as-JSON, strip it down to its essentials, and store in a PostgreSQL data table. Friday's #haskell solution uploaded categories to a PostgreSQL databse after 'removing the stupid.' That's a technical term. 
  
  
• April 5th, 2018: Thursday's #haskell problem is revising the database connector now that we're managing multiple databasen. Thursday #haskell solution is making connections to SQL databases configurable. Whoa. Edgy, tweeps! I'm really pressing the bleeding edge of technological advancement here with configurations and database connections. 
• April 4th, 2018: Wednesday's #haskell problem is storing authors in a PostgreSQL table. Wednesday's #haskell solution shows that transferring authors from articles to a SQL database is as easy as 1, 2, 3! 
  
  
• April 3rd, 2018: Tuesday's #haskell exercise: AUTHOR! AUTHOR! Is there an author in the house? Tuesday's #haskell solution: extracting author information from very unstructured data. 
• April 2nd, 2018: Monday's #haskell problem is to explore JSON to find the structure in the data. Monday's #haskell solution: oooh! Pritteh JSON! But what's this weirdness with the author-identifier? 
  

by geophf (noreply@blogger.com) at May 03, 2018 08:28 PM

Follow the Denotation

Your scientists were so preoccupied with whether or not they could, they didn't stop to think if they should.

Ian, Jurassic Park

Overview

Designing an abstraction or library often feels wonderfully unconstrained; it is the task of the engineer (or logician) to create something from nothing. With experience and training, we begin to be able to consider and make trade-offs: efficiency vs simplicity-of-implementation vs ease-of-use vs preventing our users from doing the wrong thing, among many other considerations. Undeniably, however, there seems to be a strong element of "taste" that goes into design as well; two engineers with the same background, task, and sensibilities will still come up with two different interfaces to the same abstraction.

The tool of denotational design aims to help us nail down exactly what is this "taste" thing. Denotational design gives us the ability to look at designs and ask ourselves whether or not they are correct.

However, it's important to recognize that having a tool to help us design doesn't need to take the fun out of the endeavor. Like any instrument, it's up to the craftsman to know when and how to apply it.

This essay closely works through Conal Elliott's fantastic paper Denotational design with type class morphisms.

Example: Maps

Consider the example of Data.Map.Map. At it's essence, the interface is given by the following "core" pieces of functionality:

empty  :: Map k v
insert :: k -> v -> Map k v -> Map k v
lookup :: k -> Map k v -> Maybe v
union  :: Map k v -> Map k v -> Map k v

With the laws:

-- get back what you put in
lookup k   (insert k v m) = Just v

-- keys replace one another
insert k b (insert k a m) = insert k b m

-- empty is an identity for union
union empty m = m
union m empty = m

-- union is just repeated inserts
insert k v m = union (insert k v empty) m

These laws correspond with our intuitions behind what a Map is, and furthermore, capture exactly the semantics we'd like. Although it might seem silly to explicitly write out such "obvious" laws, it is the laws that give your abstraction meaning.

Consider instead the example:

empathy :: r -> f -> X r f -> X r f
fear    :: e -> X e m -> Either () m
taste   :: X o i -> X o i -> X o i
zoo     :: X z x

It might take you some time to notice that this X thing is just the result of me randomly renaming identifiers in Map. The names are valuable to us only because they suggest meanings to us. Despite this, performing the same substitutions on the Map laws would still capture the semantics we want. The implication is clear: names are helpful, but laws are invaluable.

Meanings

Our quick investigation into the value of laws has shown us one example of how to assert meaning on our abstractions. We will now take a more in-depth look at another way of doing so.

Let us consider the concept of a "meaning functor." We can think of the term μ(Map k v) as "the meaning of Map k v." μ(Map k v) asks not how is Map k v implemented, but instead, how should we think about it? What metaphor should we use to think about a Map? The μ(⋅) operator, like any functor, will map types to types, and functions to functions.

We can encode this mapping as a function, and the partiality with Maybe:

μ(Map k v) = k -> Maybe v

With the meaning of our type nailed down, we can now also provide meanings for our primitive operations on Maps:

  μ(empty) = \k -> Nothing

An empty map is one which assigns Nothing to everything.

  μ(lookup k m) = μ(m) k

Looking up a key in the map is just giving back the value at that key.

  μ(insert k' v m) = \k ->
    if k == k'
      then Just v
      else μ(m) k

If the key we ask for is the one we inserted, give back the value associated with it.

  μ(union m1 m2) = \k ->
    case μ(m1) k of
      Just v  -> Just v
      Nothing -> μ(m2) k

Attempt a lookup in a union by looking in the left map first.

Looking at these definitions of meaning, it's clear to see that they capture an intuitive (if perhaps, naive) meaning and implementation of a Map. Regardless of our eventual implementation of Map, μ(⋅) is a functor that transforms it into the same "structure" (whatever that means) over functions.

Herein lies the core principle of denotational design: for any type X designed in this way, X must be isomorphic to μ(X); literally no observational (ie. you're not allowed to run a profiler on the executed code) test should be able to differentiate one from the other.

This is not to say that it's necessary that X = μ(X). Performance or other engineering concerns may dissuade us from equating the two -- after all, it would be insane if Map were actually implemented as a big chain of nested if-blocks. All we're saying is that nothing in the implementation is allowed to break our suspension of believe that we are actually working with μ(Map). Believe it or not, this is a desirable property; we all have a lot more familiarity with functions and other fundamental types than we do with the rest of the (possibly weird corners of) ecosystem.

The condition that X ≅ μ(X) is much more constraining than it might seem at first glance. For example, it means that all instances of our type-classes must agree between X and μ(X) -- otherwise we'd be able to differentiate the two.

Our Map has some obvious primitives for building a Monoid, so let's do that:

instance Monoid (Map k v) where
  mempty  = empty
  mappend = union

While this is indeed a Monoid, it looks like we're already in trouble. The Monoid instance definition for μ(Map), after specializing to our types, instead looks like this:

instance Monoid v => Monoid (k -> Maybe v) where

There's absolutely no way that these two instances could be the same. Darn. Something's gone wrong along the way; suggesting that μ(Map) isn't in fact a denotation of Map. Don't panic; this kind of thing happens. We're left with an intriguing question; is it our meaning functor that's wrong, or the original API itself?

Homomorphisms

Our instances of Monoid Map and Monoid μ(Map) do not agree, leading us to the conclusion that μ(Map) cannot be the denotation for Map. We are left with the uneasy knowledge that at least one of them is incorrect, but without further information, we are unable to do better.

A property of denotations is that their instances of typeclasses are always homomorphisms, which is to say that they are structure preserving. Even if you are not necessarily familiar with the word, you will recognize the concept when you see it. It's a pattern that often comes up when writing instances over polymorphic datastructures.

For example, let's look at the Functor instance for a pair of type (a, b):

instance Functor ((,) a) where
  fmap f (a, b) = (a, f b)

This is a common pattern; unwrap your datatype, apply what you've got anywhere you can, and package it all up again in the same shape. It's this "same shape" part that makes the thing structure preserving.

The principle to which we must adhere can be expressed with a pithy phrase: the meaning of the instance is the instance of the meaning. This is true for any meaning functor which is truly a denotation. What this means, for our hypothetical type μ(X), is that all of our instances must be of this form:

instance Functor μ(X) where
  μ(fmap f x) = fmap f μ(x)

instance Applicative μ(X) where
  μ(pure x)  = pure x
  μ(f <*> x) = μ(f) <*> μ(x)

and so on.

Having such a principle gives us an easy test for whether or not our meaning functor is correct; if any of our instances do not reduce down to this form, we know our meaning must be incorrect. Let's take a look at our implementation of mempty:

μ(mempty) = \k -> Nothing
          = \k -> mempty
          = const mempty
          = mempty  -- (1)

At (1), we can collapse our const mempty with mempty because that is the definition of the Monoid ((->) a) instance. So far, our meaning is looking like a true denotation. Let's also look at mappend:

μ(mappend m1 m2) = \k ->
  case μ(m1) k of
    Just v  -> Just v
    Nothing -> μ(m2) k

It's not immediately clear how to wrestle this into a homomorphism, so let's work backwards and see if we can go backwards:

mappend μ(m1) μ(m2)
    = mappend (\k -> v1) (\k -> v2)
    = \k -> mappend v1 v2
    = \k ->
        case v1 of   -- (2)
          z@(Just a) ->
            case v2 of
              Just b  -> Just $ mappend a b
              Nothing -> z
          Nothing -> v2

At (2) we inline the definition of mappend for Maybe.

That's as far as we can go, and, thankfully, that's far enough to see that our instances do not line up. While mappend for μ(Map) is left-biased, the one for our denotation may not be.

We're left with the conclusion that our meaning functor μ(⋅) must be wrong; either the representation of μ(Map) is incorrect, or our meaning μ(mappend) is. Fortunately, we are free to change either in order to make them agree. Because we're sure that the left-bias in mappend is indeed the semantics we want, we must change the representation.

Fortunately, this is an easy fix; Data.Monoid provides the First newtype wrapper, which provides the left-biased monoid instance we want. Substituting it in gives us:

μ(Map k v) = k -> First v

Subsequent analysis of this revised definition of μ(Map) reveals that indeed it satisfies the homomorphism requirement. This is left as an exercise to the reader.

(De)composition of Functors

We have now derived a denotation behind Map, one with a sensible Monoid instance. This gives rise to a further question---which other instances should we provide for Map?

Map is obviously a Functor, but is it an Applicative? There are certainly implementations for Applicative (Map k), but it's unclear which is the one we should provide. To make the discussion concrete, what should be the semantics behind pure 17? Your intuition probably suggests we should get a singleton Map with a value of 17, but what should it's key be? There's no obvious choice, unless we ensure k is a Monoid.

Another alternative is that we return a Map in which every key maps to 17. This is implementation suggested by the Applicative homomorphism of μ(Map), but it doesn't agree with our intuition. Alternatively, we could follow in the footsteps of Data.Map.Map, whose solution to this predicament is to sit on the fence, and not provide any Applicative instance whatsoever.

Sitting on the fence is not a very satisfying solution, however. Applicative is a particularly useful class, and having access to it would greatly leverage the Haskell ecosystem in terms of what we can do with our Map. As a general rule of thumb, any type which can be an instance of the standard classes should be, even if it requires a little finagling in order to make happen.

We find ourselves at an impasse, and so we can instead turn to other tweaks in our meaning functor, crossing our fingers that they will elicit inspiration.

Given the Compose type from Data.Functor.Compose, we can re-evaluate our choices once more (as we will see, this is a common theme in denotational design.)

data Compose f g a = Compose
  { getCompose :: f (g a)
  }

Compose is a fantastic tool when building new types that are composites of others. For example, consider the meaning of μ(Map k v) = \k -> First v. If we'd like to fmap over the v here, we'll need to perform two of them:

             f  ::         v  ->         w
  fmap (fmap f) :: μ(Map k v) -> μ(Map k w)

Although it seems minor, this is in fact quite a large inconvenience. Not only does it require us two fmap through two layers of functors, more egregiously, it allows us to use a single fmap to break the abstraction. Consider the case of fmap (const 5) -- this will transform a μ(Map k v) into a k -> 5, which is obviously not a functor. Yikes.

We instead can re-redefine μ(Map k v):

`μ(Map k v) = Compose ((->) k) First v`

Presented in this form, we are exposed to another interpretation of what our type means. μ(Map) is a composition of some sort of mapping-ness ((->) k) and of partiality (First). The mapping-ness is obviously crucial to the underlying concept, but it's harder to justify the partiality. One interpretation is that we use the Nothing value to indicate there was no corresponding key, but another is that we use Nothing as a default value.

When viewed as a default, a few minutes' pondering on this thought reveals that a partial map (k -> Maybe v) is just a special case of a total map (k -> v) where the value itself is partial. Maybe---if you'll excuse the pun---partiality is completely orthogonal to the semantics we want to express.

As our final (and ultimately correct) attempt, we define

μ(Map k v) = \k -> v

From here, the problem of "what typeclasses should this thing have" becomes quite trivial---we should provide equivalent instances for all of those of k -> v. The question about what should our Applicative instance do is resolved: the same thing arrows do.

A point worth stressing here is that just because the meaning of Map k v is k -> v, it doesn't mean our representation must be. For example, we could conceive implementing Map as the following:

data Map k v = Map
  { mapDefVal :: v
  , mapTree   :: BalancedTree k v
  }

lookup :: Ord k => Map k v -> k -> v
lookup m = fromMaybe (mapDefVal m) . treeLookup (mapTree m)

Such an implementation gives us all of the asymptotics of a tree-based map, but the denotations of (and therefore the intuitions behind) functions.

Hopefully this worked example has given you some insight into how the process of denotational design works. Guess at a denotation and then ruthlessly refine it until you get something that captures the real essence of what you're trying to model. It's an spectacularly rewarding experience to find an elegant solution to a half-baked idea, and your users will thank you to boot.

May 03, 2018 03:11 PM

GHC-style note snippet for Vim

I am a big fan of GHC-style notes. Notes are a convention for long, in-depth comments that do not interrupt the flow of the code.

A note is a comment that is formatted to be easily searchable and recognizable:

{- Note [Extra args in rule matching]
   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   If we find a matching rule, we return (Just (rule, rhs)),
   but the rule firing has only consumed as many of the input args
   as the ruleArity says.  It's up to the caller to keep track
   of any left-over args.  E.g. if you call
       lookupRule ... f [e1, e2, e3]
   and it returns Just (r, rhs), where r has ruleArity 2
   then the real rewrite is
       f e1 e2 e3 ==> rhs e3
-}

A note can be referenced in the code like this:

lookupRule :: (Activation -> Bool) -> InScopeSet
        -> Id -> [CoreExpr]
        -> [CoreRule] -> Maybe (CoreRule, CoreExpr)
-- See Note [Extra args in rule matching]
lookupRule is_active in_scope fn args rules
  = case go [] rules of
    []     -> Nothing
    (m:ms) -> Just (findBest (fn,args) m ms)

This convention for notes was originally developed for GHC, but it can be used in absolutely any project and in any programming language. You can read more about notes in the GHC commentary and in The Architecture of Open Source Applications.

The only issue I used to have with notes was that I could never remember how to format them properly, so every time I wanted to insert one, I would find and copy-paste one either from my own code or from the GHC source.

This motivated me to create a SnipMate snippet for Vim that automates the process.

Here are the steps:

1. Install SnipMate

2. Make sure it uses the new snippet parser. Put

   let g:snipMate = { 'snippet_version': 1 }

   in your ~/.vimrc.

3. Run

   base64 -d >> ~/.vim/snippets/haskell.snippets <<EOF
   c25pcHBldCBOb3RlCgktLSBTZWUgTm90ZSBbJHsxOnRpdGxlfV0KCXstIE5vdGUgWyQxXQoJICAg
   fn5+fn5+fiR7MS8uL34vZ30KCSAgICR7Mjp0ZXh0fQoJLX0K
   EOF

   (The reason for base64 is to preserve the relevant tab characters.)

   This will install the following snippet:

   snippet Note
     -- See Note [${1:title}]
     {- Note [$1]
        ~~~~~~~${1/./~/g}
        ${2:text}
     -}

Now you are ready to insert a note. Open a Haskell file in Vim and type

Note<Tab>

This will expand into a template

-- See Note [title]
{- Note [title]
   ~~~~~~~~~~~~
   text
-}

Just start typing the title of the note, and it will replace both occurrences of title at the same time. Then press <Tab>, and start typing in the text of the note.

The snippet consists of two part: the note itself, and the reference to the note. You leave one in place and cut-and-paste the other one to where you want it to be.

<figure> <video controls="controls" muted="muted" preload="preload" src="/img/vim-note-screencast.mp4"> </video> </figure>

May 02, 2018 08:00 PM

Addenda to recent articles 201804

• Andrew Rodland and Adam Vartanian explained ramp metering. Here's M. Rodland's explanation:

  ramp metering is the practice of installing signals on freeway onramps that only allow one car every few seconds, so that cars enter the freeway at evenly-spaced intervals instead of in bunches and don't cause as many problems merging.

  He added that it was widely used in California. McCain is headquartered in California, and mentions frequently on their web site that their equipment conforms to Caltrans standards.

• M. Vartanian and Richard Soderberg also suggested an explanation for why the traffic control system might also control sprinklers and pumps. M. Soderberg says:

  DOTs in California and presumably elsewhere often have a need for erosion control on the steep inclines of earth surrounding their highway ramps. So any time you see a 45-degree incline covered in greenery, chances are it has a sprinkler system attached and carefully maintained by the DOT. Those same sprinklers are often within a few feet of the ramp's metering lights…

  That makes perfect sense! I had been imagining fire sprinklers, and then I was puzzled: why would you need fire sprinklers at an intersection?

• Several readers suggested explanations for why soldier fly larvae are more expensive than pork chops. I rejected several explanations:

  • Hogs are kept in poor and inhumane conditions (often true, but their accommodations must still be much more expensive than the flies’)

  • Hog farmers are exempted from paying for the negative externalities of their occupation such as environmental degradation and antibiotic resistance (often true, but the fly farmers cannot be paying that much to offset externalities)

  • Slaughterhouse waste and rotten fruit are more expensive than the corn and soy on which hogs are fed (I think slaughterhouse waste and waste fruit are available essentially free to anyone who wants to haul them away)

  • The drying process is difficult and expensive (but the listed price for undried maggots is twice as high)

  But I find Marcel Fourné's suggestion much more plausible: the pork price is artificially depressed by enormous government subsidies.

  I started looking into the numbers on this, and got completely sidetracked on something only peripherally related:

  According to the USDA Census of Agriculture for 2012, in 2012 U.S. farms reported an inventory of 66 million pigs and hogs, and sales of 193 million pigs and hogs. (Table 20, page 22.)

  When I first saw this, I thought I must be misunderstanding the numbers. I said to myself:

  , so the inventory must be turning over three times a year. But that means that the average hog goes to market when it is four months old. That can't be right.

  Of course it isn't right, it isn't even close, it's complete nonsense. I wrote up my mistake but did not publish it, and while I was doing that I forgot to finish working on the subsidy numbers.

• James Kushner directed my attention to the MUTCD news feed and in particular this amusing item:

  the FHWA issued Official Interpretation 4(09)-64 to clarify that the flash rate for traffic control signals and beacons is a single repetitive flash rate of approximately once per second, and that a combination of faster and slower flash rates that result in 50 to 60 flashes per minute is not compliant…

  James writes:

  I imagined a beacon that flashed once every ten seconds; after five such iterations, there was one iteration where the beacon would flash fifty times in a second. "But it flashes 55 times every minute, so, you know, it, uh, conforms to the standard..."

  But the Official Interpretation also says

  You asked whether the FHWA would be willing to consider experimentation with alternative flash rates for warning beacons. Any requests for experimentation would be evaluated on their merits and would be addressed separately from this official ruling.

  so there is still hope for James’ scheme.

• Two readers suggested musical jokes. Jordan Fultz asks:

  Q: How does Lady Gaga like her steak?
  A: Raw, raw, raw-raw-raw!

  (This is Bad Romance)

  And betaveros asks:

  Q. What kind of overalls does Mario wear?
  A. Denim denim denim.

  (This is the Super Mario Bros. Underworld Theme)

  I feel like we might be hitting the bottom of the barrel.

Thanks to all readers who wrote to me, and also to all readers who did not write to me.

by Mark Dominus (mjd@plover.com) at May 02, 2018 05:48 AM

A new Haskell library for talking to ODBC databases

I'm pleased to announce the release of a Haskell library for connecting to SQL Server databases via ODBC.

by Chris Done (chrisdone@fpcomplete.com) at May 01, 2018 11:14 PM

Avoid the dilemma of the trailing comma

The Haskell syntax uses comma-separated lists in various places and does, in contrast to other programming language, not allow a trailing comma. If everything goes on one line you write

  (foo, bar, baz)

and everything is nice.

Lining up

But if you want to have one entry on each line, then the obvious plan

  (foo,
   bar,
   baz
  )

is aesthetically unpleasing and moreover, extending the list by one to

  (foo,
   bar,
   baz,
   quux
  )

modifies two lines, which produces less pretty diffs.

Because it is much more common to append to lists rather than to prepend, Haskellers have developed the idiom of leading comma:

  ( foo
  , bar
  , baz
  , quux
  )

which looks strange until you are used to it, but solves the problem of appending to a list. And we see this idiom in many places:

• In Cabal files:

    build-depends: base >= 4.3 && < 5
                 , array
                 , deepseq >= 1.2 && < 1.5

• In module headers:

  {-# LANGUAGE DefaultSignatures
             , EmptyCase
             , ExistentialQuantification
             , FlexibleContexts
             , FlexibleInstances
             , GADTs
             , InstanceSigs
             , KindSignatures
             , RankNTypes
             , ScopedTypeVariables
             , TemplateHaskell
             , TypeFamilies
             , TypeInType
             , TypeOperators
             , UndecidableInstances #-}

Think outside the list!

I started to avoid this pattern where possible. And it is possible everywhere instead of having a declaration with a list, you can just have multiple declarations. I.e.:

• In Cabal files:

    build-depends: base >= 4.3 && < 5
    build-depends: array
    build-depends: deepseq >= 1.2 && < 1.5

• In module headers:

  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE EmptyCase #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeInType #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}

It is a bit heavier, but it has a number of advantages:

1. Both appending and prepending works without touching other lines.
2. It is visually more homogeneous, making it – despite the extra words – easier to spot mistakes visually.
3. You can easily sort the declarations alphabetically with your editor.
4. Especially in Cabal files: If you have syntax error in your dependency specification (which I always have, writing << instead of < due to my Debian background), cabal will actually give you a helpful error location – it always only tells you which build-depends stanza was wrong, so if you have only one, then that’s not helpful.

What when it does not work?

Unfortunately, not every list in Haskell can have that treatment, and that’s why the recent GHC proposal on ExtraCommas wants to lift the restriction. In particular, it wants to allow trailing commas in subexport lists:

module Foo
    ( Foo(
        A,
	B,
      ),
      fromFoo,
    )

(Weirdly, export lists already allow trailing commas). An alternative here might be to write

module Foo
    ( Foo(A),
      Foo(B),
      fromFoo,
    )

and teach the compiler to not warn about the duplicate export of the Foo type.

For plain lists, this idiom can be useful:

list :: [Int]
list = let (>>) = (++) in do
   [ 1 ]
   [ 2 ]
   [ 3 ]
   [ 4 ]

It requires RebindableSyntax, so I do not recommend it for regular code, but it can be useful in a module that is dedicated to hold some generated data or configuration. And of course it works with any binary operator, not just (++)

by Joachim Breitner (mail@joachim-breitner.de) at May 01, 2018 02:19 AM

Don't Fear the Monad - T-shirts

Summary: I made some t-shirts.

For Christmas my brother-in-law got me the classic "Don't Fear the Monads" t-shirt, which comes complete with the Monad functions printed on it. Of course, while one adult geeky t-shirt is awesome, a child geeky t-shirt is even better, and a whole family full of them is best. I made some SVG designs for "Don't Fear the Functor" (for my son) and "Don't Fear the Applicative" (for my wife), available here (I followed the style of the Monad one, even if I disagree with some of the technical choices in the original). You can turn these into real t-shirts with the Cafe Press design your own feature. The result is pictured below.

by Neil Mitchell (noreply@blogger.com) at April 30, 2018 09:17 PM

#deleteFacebook

2018-04-23 update

Not that I was in any doubt, but Facebook’s response to GDPR completely confirms that I have made the right decision. “Think you can protect your citizens’ data, European Union? Fuck you, we’ll just move it all to a different jurisdiction.” I expect the EU to challenge this in the courts, but it demonstrates yet again the fundamental arrogance of the company.

Original article

I’m going to be deleting my Facebook account.

This is moderately annoying, as it is quite a handy way to stay in touch with various friends and family. But the ongoing revelations about the simply appalling way they have handled personal data mean I can’t in all conscience keep my account open.

Facebook friends have received a message with lots of other ways to get in contact with me. If you think you should have these, drop me an email.

• If you like my crummy jokes, links to interesting web content, and random (short) opinions, https://twitter.com/toby1851
• If you want to get in touch, try email toby@paccrat.org

If you feel inspired to join the #deleteFacebook campaign, you might find these links helpful:

https://motherboard.vice.com/en_us/article/a3yz9k/how-to-delete-your-facebook-permanently

https://eand.co/why-facebook-shows-us-just-how-badly-broken-the-economy-is-e98cc8485650

https://jonworth.eu/everyday-tech-ethics/

https://www.theguardian.com/commentisfree/2018/mar/27/pioneer-delete-facebook-addiction-social-life

If you plan to keep using Facebook, I do strongly recommend that you do so in a web browser. If you install the apps (Facebook itself, Messenger, WhatsApp, Instagram) you are opening yourself up to them filching all sorts of data from your phone.

Google - I realise it’s a bit perverse to give more data to Google. Their business model is essentially indistinguishable from Facebook, and they’re bigger. (So far, they do seem to have behaved a bit more like grownups.) I do avoid some of Google’s more obvious snares: I don’t use their search engine, I use https://duckduckgo.com/ - I have a gmail address, but all my real email goes to a system that I run myself - I use Firefox rather than Chrome for my web browser.

April 26, 2018 12:16 PM

Debian chroot on Android

2018-04-26 update

I now use and recommend termux. It is an apt-based Linux system for Android (and ChromeOS apparently). This works much more smoothly than a simple Debian chroot because it interacts properly with the Android permission system.

---

Original article

Sometimes, a simple idea — so simple it can be distilled down to 4 words — can be truly astounding.

Why?

For quite a while, I've been considering the best way to ensure the resilience, security, and accessibility of various pieces of personal data. There are several different categories, and no solution will be optimal for all of them. My music collection, for example, is large, non-secret, and largely replaceable (although the thought of dragging that enormous box of CDs out of the garage and reripping them all is pretty daunting!) The music lives on a server in my home, with my own backups. I upload medium bitrate versions to a cloud music service, and I have a low bitrate copy on my laptop and phone. So that's pretty well covered.

A similar scheme covers my photos and videos. They are much less replaceable than music, but fortunately much smaller, so there are a few extra copies kicking about.

Then, I have a few tiny things that I want to keep in sync across various devices. For example, today's todo list, my "blue skies ideas" list, and my password store. I've looked at syncthing, which is an awesome project, and I'm sure I'm going to find a good use for it someday.

But for these things, git is really the obvious solution. Most of them are already git repos, including my password-store, the only missing piece is a git client on my phone. So I was searching for recommendations for Android git clients, and these words jumped out at me:

create a debian image, mount it in your android device and chroot to it

My flabber was well and truly gasted.

How?

It's very straightforward. From some debian instance on which you have root, run:

debootstrap --foreign --arch=armhf jessie jessie

Tar up the resulting tree in jessie, copy it to android, unpack it (ah, but where?), chroot, and then run:

debootstrap --second-stage

Which?

Here are some things I've used: ssh, rsync, dash, bash, the rc shell (which I happen to maintain). All the usual userland tools, mv, chmod, etc. These (of course) are the proper full GNU versions, so you don't keep being bitten by the little discrepancies in, for instance, the busybox versions.

Package management with apt-get and dpkg. And perl, git, nano, vim, update-alternatives (so I never have to see nano again), less, man.

I started installing the pass package, but that pulls in gtk, pango and a whole bunch of other things I'm not going to use. So I downloaded password-store and installed it myself.

The ps command (you need to mount /proc in the chroot of course), top, strace, lsof. You can even strace android processes, it all Just Works. (OK, lsof gets upset because it's inside a chroot and it can't see all the mount points that /proc/mounts says exist. But still.)

I thought it might be fun to run mosh. It installed fine, but then bombed out with a weird error. I went on a bit of a wild goose chase, and concluded (it was late at night) that I needed a fix from the development version. So I cloned the mosh repo on github, installed a whole heap of build tools, compilers, libraries, and built mosh. On my phone!

In fact, the problem was simpler than that, and easily solved by using the stty command to declare my terminal size. And then I had to open up some ports in android's firewall... with iptables of course.

I could go on, but you're getting the idea. In summary, this is not something pretending to be a GNU/Linux system. It's the real deal.

Of course, there are some missing pieces, of which the most serious is the lack of daemons. I've installed etckeeper, but there will be no daily autocommit.

Ping doesn't work, because even a root shell is not allowed to use raw sockets. You can create a user, but it's not able to do much... I'll look at this some more when I have time, but I'm just running everything as root at the moment. Android's systems for users, permissions, and capabilities are entirely unfamiliar to me, although I'm trying to learn.

Where?

I made and remade my chroot several times before I was happy with it. Hopefully these notes will make things quicker for you.

First of all, Debian wants a “real” filesystem, which is to say, anything except FAT. Of the existing partitions, an obvious choice would be /data, which on my phone is ext4. Unfortunately, the major major drawback of my phone is that its /data is tiddly, just 1GB, and perennially full. (I did try the chroot on /data, before realising the fatal flaw. One curiosity is that /data is mounted with nodev, so populating /dev fails till you remount without nodev. You might think it would be better to bind mount the real /dev into the chroot anyway, and you might well be right. But I've been running with the /dev made by debootstrap with no problems.)

So it's time to repartition my 32GB SD card. Android apparently doesn't support GPT which is only a minor nuisance. I do hate all that primary / extended / logical nonsense though, it's so 1980s.

Much, much more seriously, it complains bitterly if it finds an SD card without a FAT partition. This is infuriating. The kernel supports ext3 just fine (and ext4 too, at least for partitions on fixed internal storage, although apparently not for the SD card, which makes no sense to me). So, if I insert a card that happens to have an ext3 partition on it, why not just mount it? Or if there's some scenario I'm not aware of that might not work quite right, notify a dialogue that explains and offers to mount the partition anyway. What actually happens is a notification that tells you the SD card is “damaged”, and offers to format it. Arrggh!

(I have reason to believe that the latest versions of Android will countenance SD cards with real file systems, although I need to research this further.)

My next try was a 50MB FAT partition, and the remainder ext3. This largely worked, but it didn't leave anywhere for android to move those apps which are prepared to live on SD card, absolutely vital to squeeze some extra apps onto my old phone.

The final iteration was a 4GB FAT partition, and the rest ext3. Of course, I don't need 28GB for the chroot itself: it starts off well under 1G, and even after installing loads of stuff I'm still under 2G. But I realised that I'd be able to put my music collection on the ext3 partition, which would save the tedious step of renaming everything to comply with FAT restrictions (mainly the prohibition on : in file names). Of course, I can now rsync-over-ssh the music from my laptop, which seems to go quicker than via USB.

Another annoyance is that the ext3 partition on the SD card isn't automatically mounted. I've spent some time in the past trying to find a boot time hook I can use, but with no luck. So I have to do this from the android shell every time my phone reboots, using a helper script cunningly located under the mount point:

root@android:/ # cat /data/ext3/m
#!/system/bin/sh
mount -t ext3 /dev/block/mmcblk1p5 /data/ext3

What?

Far and away the nicest way to communicate with the chroot is to plug into a laptop or desktop and use adb shell from the Android SDK. At that point, it's scarcely different from sshing to a remote server.

Of course, the whole point of the phone is that it's portable. On the move, I'm using Jack Palevich's Terminal Emulator for Android and Klaus Weidner's Hacker's Keyboard. The keyboard has all the keys you need — Esc, Tab, Ctrl etc — so it's ideal for non-trivial tasks (such as vim!). But the tiny keys are very fiddly on my phone, especially in portrait, so I sometimes stick to my usual keyboard.

I've got a trivial helper script to start my favourite shell under ssh-agent:

root@android:/ # cat /data/ext3/ch
#!/system/bin/sh
exec chroot /data/ext3/jessie /usr/bin/ssh-agent /usr/bin/rc -l

Whither?

So I have a fantastic solution to my document and password management problems. And a great ssh client. And a whole new architecture to build my projects on, most of which aren't the sort of thing that it makes much sense to run on a phone, but building in different places is always good for portability.

I'd heard that Android uses a "modified Linux" kernel, so I wasn't really expecting any of this stuff to work properly, let alone tools like strace and lsof. Apparently, though, the changes were folded back into the mainline kernel at the 3.3 release. My (3 year old) phone runs 3.4.5, so presumably this a fairly vanilla kernel.

This is awesome. Google has its faults, but their commitment to free software easily earns them the “least evil” prize among the current Internet quintumvirate. (That's Google, Apple, Facebook, Amazon, and Microsoft, for anyone who's been asleep the last few years.)

Realising that, yes, that computer in my pocket is a pukka Linux box has endeared me even further to Android. I'd love to write some apps for it... except I've already got more than enough projects to fill my “copious spare time”!

Update November 2016

A couple of new things I've discovered since writing this article.

First, the debootstrap command is available on Fedora, from the system repository! So you don't need a Debian box to build the initial system image. (Having debootstrap around is also handy for making a Debian container on my desktop.)

Secondly, I think the reason Android won't automatically mount an ext2/3/4 partition is that it has no idea how to map UIDs and GIDs on the filesystem. Any obvious trivial solution, such as “only UID 0 can read or write”, would make it inaccessible to Android processes. Remember, you're not supposed to root your Android device! I've just ordered my next phone, which is supported by CyanogenMod, so it's likely that I'll end up with an OS that is rather more enlightened about users having full control of their devices. Having said that, I don't believe it has an SD slot, so the issue of real FS support won't arise.

April 26, 2018 12:15 PM

Machine learning, drones, and whales: A great combination!

Last June, a simple question changed my life: “Hey Bryn, what do you know about whales?” Of course like most people, my answer was “Not much,” but that marked the beginning of an important project to help track the health of whale populations by using machine learning to analyze video from drones. Parley for the Oceans introduced me and my colleagues Ted Willke and Javier Turek to Dr. Iain Kerr of Ocean Alliance, and we started talking about how machine learning could help make marine biologists’ lives easier and help protect the whales, using the video from Dr. Kerr’s SnotBot drones.

SnotBot drone with Petri dishes, courtesy of Christian Miller

SnotBot

Dr. Kerr started the SnotBot program because in the not-so-distant past, when people wanted to understand the health of a whale, or get its DNA, the only way to do this was to shoot it with a crossbow with a specially prepared bolt with a string on it, that would only go a couple of inches into the (remember, bus-size) body. The bolt would then be reeled in and the sample could be extracted from it. Iain realized there was a better way, that didn’t involve crossbows or Zodiac inflatable rafts: put a Petri dish on a drone, and fly the drone through the blow that whales exhale when they come to the surface. It turns out there are all kinds of interesting things in that exhaled breath condensate (i.e. snot), like DNA, hormones, and microbiomes. Much less stress on the whale, and easier on the humans, too.

Drones and Cameras

These days, drones are equipped with some pretty amazing cameras, and the ones that are built for camera work are very steady in the air, using GPS to hold their position steady, and have camera gimbals that compensate for any tilting of the aircraft. As a result, you can get some excellent video of whales. With cameras that good in the air, we realized we could do two important things using machine learning: we could identify individual whales, and we could do health assessments based on body condition.

Whale Research in Alaska

The good folks at Alaska Whale Foundation shared their database of known humpback whales that they had been studying in the Alaskan waters for years, and Ocean Alliance shared a lot of the video they had collected over the years with drones, and we got to work. In a few short weeks, we built some software prototypes, and then we set off to Alaska with Ocean Alliance, Parley, and the Alaska Whale Foundation, to test the software out.

To get to the whales, we needed to take a plane, like you’d expect. In Alaska, the planes are a little different.

The seaplane

And of course, we had lodgings, that were also different from what you’d expect on a normal business trip…

The Glacier Seal, the boat we lived on for a week. Photo courtesy of Christian Miller

Plus the rental car…

Rental car

It was an amazing experience on many levels.

Image obtained under NMFS #18686

Identification

Identifying individual whales is important for many reasons. In the case of humpback whales in Alaska, there are two populations: one that migrates to Hawaii in the winter, and one that migrates to Mexico in the winter. The Mexico population is much more endangered, so NOAA asks that researchers avoid interacting with the Mexico population if possible. But how is a researcher to know the whale in front of them is from Mexico or from Hawaii? Only if he or she can identify the individual.

We built a program that could compare a snapshot of a humpback whale’s tail flukes against a database of known whales, using the shape of the ragged trailing edge and the amount of grey or white spotting on the tail, and we were able to identify several whales in Alaska while the drone was still in the air over them, which opens up lots of possibilities. Before this, researchers would usually identify the whales days or months after the fact, if at all.

A discovery

While we were out on the water, listening to a hydrophone, we heard a whale feeding call. It was very distinctive, and Dr. Fred Sharpe from Alaska Whale Foundation said he thought it sounded familiar. He checked his archival database on his laptop, and found a similar call from 20 years earlier, from a whale

named Trumpeter. A few minutes later, a whale surfaced, and then we got a picture of its flukes when it dove. We ran it through our software, and we got a match! Sure enough, it was Trumpeter! So we learned something nobody else has known for sure - humpback whale feeding calls remain stable in adults over decades. It wasn’t a question we set out to answer, but it fell into our laps, purely because we were able to identify the whale swimming in front of us.

“Live” flukes under NMFS #18636, “Database” under NMFS #14599

Health Assessment

There are lots of things we don’t know about whales. They’re hard to study because they go underwater and they move around a lot. So even a little bit of knowledge about how they’re doing is hard to come by. We built a program that can analyze video data from a drone camera to evaluate how healthy a humpback whale is based on its length and width. Just like other animals, a really thin whale is probably a sick whale, so this simple observational technique alone is already a pretty important indicator of health.

The hard part of this, for a computer, is actually identifying the whale in a video frame. We trained a specialized convolutional neural network to identify whales in difficult conditions like the waters of Alaska, where the color of the whale isn’t much different from the color of the water, and the water tends to be murky.

Once the whale pixels are identified, we calculate the area of the whale that’s used to store energy (basically, everything but the head and the flukes), that’s identified in pink in the picture above.

The technique worked pretty well, though it requires considerable input from an expert user in its present form (e.g. what was the altitude of the drone, what is the sex the whale, what day of the season is it, and in the case of a mother, how long has it been since the calf was born). We’ll be working to make it easier to use, since this kind of health assessment is an important first step before any kind of interaction with a whale. In fact, I’m supervising an intern, Kelly Cates of the University of Alaska at Fairbanks, to help extend the tool.

We presented a poster about this work at the Society for Marine Mammology in October 2017, and just a couple of months later, Iain and I presented together at the Consumer Electronics Show in Las Vegas, which was quite an experience as well.

Photo by Christina Caputo

I just received news that the video that was made about our collaboration was nominated for a Webby award! You can see it here.

I also went down to Mexico back in February with Parley and Ocean Alliance to capture images of blue whales and grey whales, to see about expanding the health assessment tool to those species as well. Unfortunately, there were very few of either compared to the numbers that were seen even last year. One hesitates to draw conclusions, but it does underscore the urgency of getting a better understanding of the overall population health of whales, who are so important to our ecosystem, our oceans, and our own survival.

Important Note: Flying drones is an activity that is heavily regulated in many parts of the world, and you should check your local regulations before flying any drone. It is especially important to understand that in the United States, it is illegal to fly a drone anywhere near a whale without a very special permit from the National Oceanic and Atmospheric Administration.

by Bryn Keller at April 26, 2018 12:00 AM

Why I don’t believe in the Second Amendment (and neither do you or the Supreme Court)

The second amendment says:

A well regulated Militia, being necessary to the security of a free State, the right of the people to keep and bear Arms, shall not be infringed.

This consists of two parts, the preamble “A well regulated Militia, being necessary to the security of a free State”and the effective part “the right of the people to keep and bear Arms, shall not be infringed”.
The meaningof the effective part is very straightforward: “arms” means any kind of weapon. A bowie knife is “arms”, and during the Cold War the superpowers engaged in “Strategic Arms Limitations Talks” (SALT). Although military technology has changed beyond all recognition, the useof the word “arms” to mean any kind of weaponhas not changed since 1791 when the Bill of Rights was ratified. Had James Madison and the otherframers of the constitution been shown the modern world they would have had no hesitation in agreeing that any form of modern weaponry from a bowie knife to a nukewas included in the definition.

So it would seem that anyone in the United States of America has the constitutionalright to purchase, say, a shoulder launched surface to air missile, and to bear that armament anywhere they wish, such as near the end of a runway where large passenger jets are taking off. That would not be a good idea. If military weapons were widely available then they would be used for mass murder of unarmed civilian targets. Stephen Paddock, the Las Vegas shooter, seems to have set out to kill as many people as possible, and he managed to kill 58. AnAirbus A-380 typically has a maximum capacity of 525 plus crew, and if one were bought down over the right bit of city then the body count could go into the thousands. Given the opportunityPaddockwould surelyhave done so, and he is not unique.

The Courts

Today the original intentof the Second Amendment is dead as a matter of established law. It is not legal for anyone within the United States to make or buy heavy weapons except under the most stringent and careful of controls.

This would have surprised and disappointed the framers. They had just fought a war in which ordinary armed citizens had beaten off the professional British army. The framers saw this as an important lesson; the liberty of their new nation would be assured by having an armed citizenry who could be relied upon to form a militia and fight against any future tyrant, foreign or domestic. This is what the preamble part of the Second Amendment is about.

I haven’t been able to find any case in which the constitutionality of this banon heavy weapons has ever been truly tested. However the courts have found that bans on semi-automatic rifles and the carrying of handguns in public are constitutional, and the Supreme Court has declined to review these decisions.

In the case of the Maryland ban on assault rifles, the 4^thCircuit Court of Appeals decided 10-4 that the ban was constitutional. The judgement explains this with “Put simply, we have no power to extend Second Amendment protections to weapons of war”. The framers of the constitution would have found that bizzare; to them the Second Amendment wasprecisely about weapons of war.

On the other hand back in 1939 in the Miller case the Supreme Court decided that a sawn-off shotgun was not protected by the Second Amendment because it was not potentially a military weapon, and this is still a valid precedent (they may have been wrong about the military use of sawn-off shotguns in particular, but the principle still stands). So the 4^thCircuit has decided that military weapons are unprotected, and the Supreme Court has decided that non-military weapons are unprotected. According to these precedents it would seem that Americans have the constitutional right to keep and bear arms, except for military weapons and non-military weapons.

Self Defense

The most recent case on the Second Amendment that reachedthe Supreme Court was District of Columbia v Hellerin 2008, which was about the constitutionality of a ban on handguns and a requirement that larger guns be kept unloaded and locked. The Court found 5-4 that this ban violated the Second Amendment.

The Heller case was about restrictions on small arms rather than heavy weapons, and the decision is rightly focussed on that. So the question of whether it is constitutional to own heavy weapons was not directly considered. However if the Court had found that small arms are protected by the plain meaning of the Second Amendment, then someone would have used this to challenge laws banning heavy weapons on the grounds that they are equally protected by the Second Amendment. So to overturn the handgun ban the Court had to do two things. First, they had to ignore the plain meaning of the words they were analysing, and second they had to find some other right to keep small arms.
They managed the first partby finding that the Second Amendment is not an unlimited right. They dispose of this in one brief paragraph:

Like most rights, the Second Amendment right is not unlimited. It is not a right to keep and carry any weapon whatsoever in any manner whatsoever and for whatever purpose: For example, concealed weapons prohibitions have been upheld under the Amendment or state analogues. The Court’s opinion should not be taken to cast doubt on longstanding prohibitions on the possession of firearms by felons and the mentally ill, or laws forbidding the carrying of firearms in sensitive places such as schools and government buildings, or laws imposing conditions and qualifications on the commercial sale of arms. Miller’s holding that the sorts of weapons protected are those “in common use at the time” finds support in the historical tradition of prohibiting the carrying of dangerous and unusual weapons.

It is true that, as with other parts of the Bill of Rights, the government can restrict the scope of a right where it has a pressing need to do so. Thus, for instance the First Amendment has at various times been limited to exclude the publication of libel, copyright infringement, certain secrets,and various kinds ofpornography. However the scope of First Amendment restrictions has only rarely been allowed to extend beyond those areas. The only significant case in modern times was the Sedition Act of 1918, which the Supreme Court found constitutional the following year. However this is now considered to be a mistake; today the heart of the First Amendment is seen as political speech and any speech touching on politics enjoys the highest level of constitutional protection. The framers of the Constitution would surely agree that this is the proper state of affairs.

However the restrictions on the right to keep and bear armsare not so limited. The Second Amendment is primarily about military weapons, but under federal lawtoday only weapons of little military use may be legally held by civilians. Imagine if the First Amendment were restricted to stating opinions that are in "common use", with citizens only allowed to comment on local politics and speechon state and national affairs being restricted to those government officials employed to do so. That would not be freedom of speech as it is understood in most of the world; indeed it would resemblemany dicatorships.

So having found that the Second Amendment does not in fact protect the right to keep and bear most arms, the Supreme Court in 2008 had to find a right that protected handguns. Theyfound this in the right to self defense.

Unlike the right to keep and bear arms, the right to self defense is not enumerated in the Bill of Rights. This is not a problem because the Ninth Amendmentspecifically says that this “shall not be construed to deny or disparage others retained by the people”. Anyone being attacked has the right to defend themselves with whatever means may be at hand; if you are faced with an attacker then you may pick up a golf club and swing at their head, or try to stab them with a kitchen knife, or just use your fists. The question in such cases is not whether the weapon islegal but whether itisused in a legitimate act of self defense. The same argument applies to guns; if you are forced to defend yourself then using a gun is as reasonable as using a knife, even if that gun was not one you were legally permitted to have.

However in Heller the Supreme Court, after exhaustive analysis of the history of self defense law in both the United States and the United Kingdom, concluded that the right to self defense included the right to keep a hand gun in your housefor that purpose.

As an aside, I should say that some state constitutions provide a right to bear arms in self defense. Obviously in those states the situation is different, but this post is about the US constitution.

I’m not going to go any further into this question of personal self defense because this essay is not about that; its about the Second Amendment. Heller is not about the general right to keep and bear arms, its about the right to keep a hand gun as self defense against home invasions. The fact that the Supreme Court found it necessary to invoke a different right to protect hand guns shows that they don’t believe in the Second Amendment either; they actually upheld something different.

The NRA Version of the Second Amendment

The original purpose of the Second Amendment was not individual defense against home invasion, it was collective defense against tyranny. Despite a long consideration of the “well regulated militia” the Heller decision is silent on this question.

Supporters of the NRA are not silent on this question; when asked to justify the right to keep and bear small arms they claim that their guns are a bulwark against government over-reach. Somego so far as to claim that overturning the Second Amendment is the first step in a deep and dark plot to overthrow the rest of the Bill of Rights and institute a socialist tyranny.

However the historical facts do not support the NRA rhetoric on this. Since 1776 the US government has been responsible for a long and sad list of human rights violations, but civilian firearms have never prevented any of them. The lastcentury alone sawthe following:

• The Sedition Act of 1918, which directly violated the First Amendment by restricting political speech.
• The internment of Japanese Americans in World War II, in violoation of pretty much every constitutional right they had.
• The “Jim Crow” laws of the southern states, finally abolished in 1964. Not only were these laws themselves an infringement on the constitutional rights of many citizens, but they went alongside a grossly biased justice system that somehow never got around to prosecuting white perpetrators of violence against blacks.
• The Chicago “machine” rigging elections and protecting corrupt politicians.
• The FBI investigating and undermining lawful civil rights movements under J. Edgar Hoover
• Guantanamo Bay.
• Civil forfeiture used to seize property under mere suspicion.
  
• Pretextual traffic stops and “parallel construction” used to cover violations of the Fourth Amendment.
  
• A national security apparatus that routinely scans the email and other private communications of many American citizens without any effective oversight.
  

In all of this list civilian gunswere never used to defend the rights of anyone. In the few cases where civilian guns appeared, such as Jim Crow lynch mobs, they were on the wrong side.

Has there ever been a case whereguns held by civilians were effective in preventing a violation of constituional rights? I doubt it. The fact is that if the American government decides to actin violation of the constitution then there is nothing that a small band of gun owners can do to stop them. The government can always bring in bigger guns and more of them. Various small bands have tried to defy the government; it always ends badly. Today the only ways to change the way the American government behaves are the ballot box, the courts, and bribery making political donations. Pointing guns at government employees will simply get you shot.

Edit:  This Stack Exchange question  points to the Wounded Knee incident in 1973, which was indeed a case where civilians with guns prevented the infringement of constitutional rights by the government. Another answer to the same question also cited the Bundy standoff of 2014 and the related Malheur occupation of 2016, but they are not good examples. The Bundy standoff seems to have been driven by Cliven Bundy's fringe beliefs about federal land ownership rather than a real infringement of constitutional rights, and the Malheur occupation ended with the shooting of one participant and the arrest of everyone else.

The Second Amendment Today

The Bill of Rights was written at a time when there was little difference between military and civilian firearms, military ships were in civilian hands (“privateers”), and the fastest means of communication was a rider on horseback. Firearms were mostly muzzle-loading flintlocks; a skilled gunman might get off two or three rounds per minute and for an individual they were effectively single-shot weapons. They were also not very accurate. Effective use of such weapons required collective action to keep the enemy at bay while you reloaded. The only thing bigger than a rifle was a cannon, which was also muzzle loading and inaccurate.

Today the scope of military weapons has expanded along with the rest of our technology. If the Second Amendment were taken at face value today then many high explosive ranged weapons capable of major destruction would be within the financial reach of much of the population. I opened this essay by inviting you to consider a shoulder launched surface to air missile. I’d like to close by inviting you to consider a school shooter with a bazooka firing a white phosphorus munition.

Most of the Bill of Rights has fared surprisingly well with time; the First Amendment right to free speech now applies to film, television, web sites and computer software, but the basic principle is still the same. This is equally true of Amendments 3 to 10. The Second stands out as a product of its time, overtaken by changes in technology and society.

If you truly believe in the Second Amendment then you believe that any military weapon held by the armed forces of the United States should also be legally available to most civilians. I think the number of people who really believe that is very small. Even the National Rifle Association only believes in the right to keep rifles. There is no National Bazooka Association (actually that’s not true, but it seems to be only one person and may just be a joke).



<style type="text/css">h1 { margin-bottom: 0.08in; }h1.western { font-family: "Liberation Sans", sans-serif; font-size: 18pt; }h1.cjk { font-family: "Source Han Sans CN Regular"; font-size: 18pt; }h1.ctl { font-family: "Lohit Devanagari"; font-size: 18pt; }p { margin-bottom: 0.1in; line-height: 120%; }</style>

by Paul Johnson (noreply@blogger.com) at April 25, 2018 02:41 PM

[ljdyledo] Sort of UTF-6

We present an encoding of Unicode code points to printable ASCII characters while keeping English text still vaguely readable.  It accomplishes a similar purpose as Quoted-Printable.  This design is modeled after UTF-8.  We use 6-bit bytes instead of UTF-8's 8-bit bytes.  We also do not encode the number of continuation bytes in the first byte; instead, the most significant bit (high bit) signifies whether a byte is followed by further continuation bytes.  The last byte of a sequence does not have its high bit set, signifying it is the last byte of a sequence representing one Unicode character.  The binary bits of the Unicode code point numbers of various magnitudes are encoded big-endian into the x's as follows:

• 0xxxxx
• 1xxxxx 0xxxxx
• 1xxxxx 1xxxxx 0xxxxx
• 1xxxxx 1xxxxx 1xxxxx 0xxxxx
• ...

This encoding can encode values of arbitrary size, in contrast to the 36-bit limit of UTF-8 extended in the obvious way.  But this is a moot point (for now) as Unicode was originally limited to 31 bits, and later (including currently) limited further to 21 bits.

Here, in order, are the 64 printing characters used to encode a 6-bit byte.  It is modeled after ASCII, but some common punctuation namely ;,-.? has been moved so that it remains unchanged when encoded.  (The moved punctuation was moved only up or down a column of the 16-wide ASCII table, preserving low-order bits out of tradition).  The second row, beginning with @, are characters that will only be used in multibyte sequences.  The first row, beginning with space, represents characters which will be unchanged when encoded but can also occur as the last byte of a multibyte sequence.

 abcdefghijklmnopqrstuvwxyz;,-.?
@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_

The following is how Unicode code points 0 through 127 are encoded.  Here is a 16-wide ASCII table to see the corresponding original characters.

B

Ba

Bb

Bc

Bd

Be

Bf

Bg

Bh

Bi

Bj

Bk

Bl

Bm

Bn

Bo

Bp

Bq

Br

Bs

Bt

Bu

Bv

Bw

Bx

By

Bz

B;

B,

B-

B.

B?

Cq

Cr

Cs

Ct

Cu

Cv

Cw

Cx

Cy

Cz

C;

,

-

.

C?

C

Ca

Cb

Cc

Cd

Ce

Cf

Cg

Ch

Ci

Cj

;

Cl

Cm

Cn

?

A

Aa

Ab

Ac

Ad

Ae

Af

Ag

Ah

Ai

Aj

Ak

Al

Am

An

Ao

Ap

Aq

Ar

As

At

Au

Av

Aw

Ax

Ay

Az

A;

A,

A-

A.

A?

Cp

a

b

c

d

e

f

g

h

i

j

k

l

m

n

o

p

q

r

s

t

u

v

w

x

y

z

Ck

C,

C-

C.

Co

The fact that some multibyte sequences are terminated by space (e.g., code points 48 and 64, corresponding to the digit zero and the at-sign respectively) is a little unfortunate.

Here is some more text containing higher Unicode code points, followed by its vaguely readable encoding:

lowercase Capitalized camelCase UPPERCASE numbers 0123456789 common punctuation ;,-.? at-sign @ bob@example.com http://example.com exclamation ! (parentheses) time 12:01 tilde ~ ‘single curly quotes’ “double curly quotes” yen ¥ euro € en–dash em—dash ellipsis … y-umlaut ÿ eng ŋ tent emoji ⛺ fire kanji 火 canoe emoji 🛶 newline

lowercase Acapitalized camelAcase AuApApAeArAcAaAsAe numbers C CaCbCcCdCeCfCgChCi common punctuation ;,-.? at-sign A  bobA example.com httpCjC?C?example.com exclamation Cq CxparenthesesCy time CaCbCjC Ca tilde C. H@xsingle curly quotesH@y H@,double curly quotesH@- yen Ee euro HEl enH@sdash emH@tdash ellipsis HAf y-umlaut G? eng Jk tent emoji IWz fire kanji \Ck canoe emoji C]Wv newlineBj

We implemented an encoder and decoder in Haskell (after first trying in Perl but finding it to be the wrong tool).  Some code excerpts:

We represented bytes as lists of Bool, sometimes little-endian sometimes big-endian depending on where we were in the conversion.  This is highly space-inefficient, but does allow some elegant code.  Given a list of big-endian bytes, splitting off the initial bytes that all have their high (first) bit set is elegantly span head.  This is used in decoding.

type Bstring=[Bool];
myspan :: [Bstring] -> ([Bstring],[Bstring]);
myspan = span head; -- takeWhile (\l -> head l == True)

Conversion to binary is an unfold.  Output is little-endian.

to_binary :: Integer -> [Bool];
to_binary = unfoldr (\n -> if n==0 then Nothing else Just (case divMod n 2 of {(q,r) -> (r==1,q)}));

Conversion from big-endian binary to an integer is a fold.

from_binary :: [Bool] -> Integer;
from_binary = foldl' (\accum b -> 2*accum+(if b then 1 else 0)) 0;

A few times we relied on the fact that mod x y with x negative and y positive yields a positive result.  This is in contrast to rem x y which would return a negative result.

by Ken (noreply@blogger.com) at April 24, 2018 02:03 AM

Workshop on Numerical Programming in Functional Languages (NPFL)

I’m the chair this year for the first(!) ACM SIGPLAN International
Workshop on Numerical Programming in Functional Languages (NPFL),
which will be co-located with ICFP this September in St. Louis,
Missouri, USA.

Please consider submitting something! All you have to do is submit
between half a page and a page describing your talk. There will be no
proceedings so all you need do is prepare your slides or demo. We do
plan to video the talks for the benefit of the wider world.

We have Eva Darulova giving the keynote.

The submission deadline is Friday 13th July but I and the Committee
would love to see your proposals earlier.

See here for more information. Please contact me if you have any
questions!

by Dominic Steinitz at April 23, 2018 03:54 PM

Call for submissions: FARM 2018

I’m the general chair this year for the ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design (better known as FARM), which will be colocated with ICFP this September in St. Louis, Missouri, USA. The goal of the workshop is to “gather together people who are harnessing functional techniques in the pursuit of creativity and expression”. For me (and I think for many others as well), FARM, including the associated performance evening, is always one of the highlights of ICFP.

Please consider submitting something! As in previous years, we are accepting a wide range of types of submissions. Paper and demo submissions are due by June 28: you can submit original research, a technology tutorial, a call for collaboration, or propose some sort of live demo. In addition, we also solicit performances to be given during the associated performance evening—performance proposals are due by July 8.

See the website for more info, and let me know if you have any questions!

by Brent at April 23, 2018 12:35 PM

Verifying local definitions in Coq

TL;DR: We can give top-level names to local definitions, so that we can state and prove stuff about them without having to rewrite the programs.

When a Haskeller writes Coq

Imagine you teach Coq to a Haskell programmer, and give them the task of pairing each element in a list with its index. The Haskell programmer might have

addIndex :: [a] -> [(Integer, a)]
addIndex xs = go 0 xs
  where go n [] = []
        go n (x:xs) = (n,x) : go (n+1) xs

in mind and write this Gallina function (Gallina is the programming language of Coq):

Require Import Coq.Lists.List.
Import ListNotations.

Definition addIndex {a} (xs : list a) : list (nat * a) :=
  let fix go n xs := match xs with
                     | []    => []
                     | x::xs => (n, x) :: go (S n) xs
                     end
  in go 0 xs.

Alternatively, imagine you are using hs-to-coq to mechanically convert the Haskell definition into Coq.

When a Coq user tries to verify that

Now your task is to prove something about this function, for example

Theorem addIndex_spec:
  forall {a} n (xs : list a),
  nth n (map fst (addIndex xs)) n = n.

If you just have learned Coq, you will think “I can do this, this surely holds by induction on xs.” But if you have a bit more experience, you will already see a problem with this (if you do not see the problem yet, I encourage you to stop reading, copy the few lines above, and try to prove it).

The problem is that – as so often – you have to generalize the statement for the induction to go through. The theorem as stated says something about addIndex or, in other words, about go 0. But in the inductive case, you will need some information about go 1. In fact, you need a lemma like this:

Lemma go_spec:
  forall {a} n m k (xs : list a), k = n + m ->
  nth n (map fst (go m xs)) k = k.

But go is not a (top-level) function! How can we fix that?

• We can try to awkwardly work-around not having a name for go in our proofs, and essentially prove go_spec inside the proof of addIndex_spec. Might work in this small case, but does not scale up to larger proofs.
• We can ask the programmer to avoid using local functions, and first define go as a top-level fixed point. But maybe we don’t want to bother them because of that. (Or, more likely, we are using hs-to-coq and that tool stubbornly tries to make the output as similar to the given Haskell code as possible.)
• We can copy’n’paste the definition of go and make a separate, after-the-fact top-level definition. But this is not nice from a maintenance point of view: If the code changes, we have to update this copy.
• Or we apply this one weird trick...

The weird trick

We can define go after-the-fact, but instead of copy’n’pasting the definition, we can use Coq’s tactics to define it. Here it goes:

Definition go {a} := ltac:(
  let e := eval cbv beta delta [addIndex] in (@addIndex a []) in
  (* idtac e; *)
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

Let us take it apart:

1. We define go, and give the parameters that go depends upon. Note that of the two parameters of addIndex, the definition of go only depends on (“captures”) a, but not xs.
2. We do not give a type to go. We could, but that would again just be copying information that is already there.
3. We define go via an ltac expression: Instead of a term we give a tactic that calculates the term.
4. This tactic first binds e to the body of addIndex. To do so, it needs to pass enough arguments to addIndex. The concrete value of the list argument does not matter, so we pass []. The term @addIndex a [] is now evaluated with the evaluation flags eval cbv beta delta [addIndex], which says “unfold addIndex and do beta reduction, but nothing else”. In particularly, we do not do zeta reduction, which would reduce the let go := … definition. (The user manual very briefly describes these flags.)
5. The idtac e line can be used to peek at e, for example when the next tactic fails. We can use this to check that e really is of the form let fix go := … in ….
6. The lazymatch line matches e against the pattern let x := ?def in _, and binds the definition of go to the name def.
7. And the exact def tactic tells Coq to use def as the definition of go.

We now have defined go, of type go : forall {a}, nat -> list a -> list (nat * a), and can state and prove the auxiliary lemma:

Lemma go_spec:
  forall {a} n m k (xs : list a), k = n + m ->
  nth n (map fst (go m xs)) k = k.
Proof.
  intros ?????.
  revert n m k.
  induction xs; intros; destruct n; subst; simpl.
  1-3:reflexivity.
  apply IHxs; lia.
Qed.

When we come to the theorem about addIndex, we can play a little trick with fold to make the proof goal pretty:

Theorem addIndex_spec:
  forall {a} n (xs : list a),
  nth n (map fst (addIndex xs)) n = n.
Proof.
  intros.
  unfold addIndex.
  fold (@go a).
  (* goal here: nth n (map fst (go 0 xs)) n = n *)
  apply go_spec; lia.
Qed.

Multiple local definitions

The trick extends to multiple local definitions, but needs some extra considerations to ensure that terms are closed. A bit contrived, but let us assume that we have this function definition:

Definition addIndex' {a} (xs : list a) : list (nat * a) :=
  let inc := length xs in
  let fix go n xs := match xs with
                     | []    => []
                     | x::xs => (n, x) :: go (inc + n) xs
                     end in
  go 0 xs.

We now want to give names to inc and to go. I like to use a section to collect the common parameters, but that is not essential here. The trick above works flawlessly for `inc':

Section addIndex'.
Context {a} (xs : list a).

Definition inc := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

But if we try it for go', like such:

Definition go' := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := _ in let y := ?def in _ =>
    exact def
  end).

we get “Ltac variable def depends on pattern variable name x which is not bound in current context”. To fix this, we use higher-order pattern matchin (@?def) to substitute “our” inc for the local inc:

Definition go' := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := _ in let y := @?def x in _ =>
    let def' := eval cbv beta in (def inc) in
    exact def'
  end).

instead. We have now defined both inc and go' and can use them in proofs about addIndex':

Theorem addIndex_spec':
  forall n, nth n (map fst (addIndex' xs)) n = n * length xs.
Proof.
  intros.
  unfold addIndex'.
  fold inc go'. (* order matters! *)
  (* goal here: nth n (map fst (go' 0 xs)) n = n * inc *)

Reaching into a match

This trick also works when the local definition we care about is inside a match statement. Consider:

Definition addIndex_weird {a} (oxs : option (list a))
  := match oxs with
     | None => []
     | Some xs =>
       let fix go n xs := match xs with
                          | []    => []
                          | x::xs => (n, x) :: go (S n) xs
                          end in
       go 0 xs
     end.

Definition go_weird {a} := ltac:(
  let e := eval cbv beta match delta [addIndex_weird]
           in (@addIndex_weird a (Some [])) in
  idtac e;
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

Note the addition of match to the list of evaluation flags passed to cbv.

Conclusion

While local definitions are idiomatic in Haskell (in particular thanks to the where syntax), they are usually avoided in Coq, because they get in the way of verification. If, for some reason, one is stuck with such definitions, then this trick presents a reasonable way out.

by Joachim Breitner (mail@joachim-breitner.de) at April 22, 2018 09:47 PM

Ghcid with colors

Summary: I've just released ghcid-0.7, which provides a much better user experience, including colors.

Ghcid is now over three years old, with 28 versions, but I'm particularly pleased with the improvements in the latest version. The focus has been on better defaults and a more polished user experience, some things you might spot:

Color output: GHC 8.2 added colored output, with important information highlighted. Previously Ghcid would explicitly disable that color. Now Ghcid embraces that color, turning the flag on for GHC versions that support it and ensuring any output munging is aware of the colors. It also enables colors in Hspec and colors the "All good" message green.

Color defaults: While enabling more color, it also provides --color=never to disable colors, and auto-detects when colors are likely to work well.

Error spans: Ghcid has always recommended that people turn on the -ferror-spans flag, but now it does it for you. For people using the VS Code addin that will provide a smoother experience out of the box.

Parallel compilation: Ghcid now passes -j to ghci, which I find speeds up compilation by about one third. Not a huge speedup, but still useful.

Tracking files: Ghcid now tracks both the .ghcid file (which you can use to specify the command line you want to use with ghcid) and .ghci file (which configures ghci). If either change it will cause Ghcid to restart, picking up the changes.

Absolute paths: The internals of Ghcid have been rewritten to always use absolute file paths, rather than relative paths. If your ghci wrapper changes directory (as I believe multi-project cabal new-repl does) Ghcid will continue to work.

Enabling IDE improvements: I have improved the integration features for editor plugins - you can now output a .json file with the parsed messages, including start/end position, and escape codes. There is a new --setup flag for sending initial messages to the underlying ghci. I haven't modified any of the IDE plugins to take advantage of these new features, but that's phase 2.

Ctrl-C and cleaning up processes: Ghcid is a continual fight to deal properly with Ctrl-C and close down all appropriate processes at the right time. In this release I've fought the battle in a few more corners, seemingly with some level of success.

Crazy extensions: GHC 8.4 is now able to deal with both RebindableSyntax and OverloadedStrings and still start ghci. I've modified Ghcid so it can also deal with this composition.

Together these changes make for a much more pleasant user experience.

by Neil Mitchell (noreply@blogger.com) at April 18, 2018 06:36 PM

A very long Haskell type

For GUI programming I've migrated from the gtk2hs library to the gi-gtk library. This uses overloaded labels to access the properties of GTK3 objects.

I wanted a function which would set the background and foreground colours of a widget. Rather than simply have it modify the object I decided to have it return a list of property setters. It looks like this (the function "contrastText" just returns either white or black):

setColour c = do
      bg <- colourToRGBA c
      fg <- colourToRGBA $ contrastText c
      return [#backgroundRgba := bg, #foregroundRgba := fg]

However when I couldn't get it to type-check I asked ghci what the type should be. Here is the reply!

> :type setColour
setColour
  :: (Data.GI.Base.Attributes.AttrOpIsAllowed
        tag
        (Data.GI.Base.Attributes.AttrAllowedOps
           (Data.GI.Base.Overloading.FindElement
              "foregroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        (Data.GI.Base.Attributes.AttrLabel
           (Data.GI.Base.Overloading.FindElement
              "foregroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        (Data.GI.Base.Attributes.AttrOrigin
           (Data.GI.Base.Overloading.FindElement
              "foregroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        obj
      ~
      'Data.GI.Base.Attributes.OpIsAllowed,
      Data.GI.Base.Attributes.AttrOpIsAllowed
        tag
        (Data.GI.Base.Attributes.AttrAllowedOps
           (Data.GI.Base.Overloading.FindElement
              "backgroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        (Data.GI.Base.Attributes.AttrLabel
           (Data.GI.Base.Overloading.FindElement
              "backgroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        (Data.GI.Base.Attributes.AttrOrigin
           (Data.GI.Base.Overloading.FindElement
              "backgroundRgba"
              (Data.GI.Base.Overloading.AttributeList obj)
              (((('GHC.TypeLits.Text "Unknown attribute \8216"
                  'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
                 'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
                'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")))
        obj
      ~
      'Data.GI.Base.Attributes.OpIsAllowed,
      Data.GI.Base.Attributes.AttrInfo
        (Data.GI.Base.Overloading.FindElement
           "foregroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")),
      Data.GI.Base.Attributes.AttrInfo
        (Data.GI.Base.Overloading.FindElement
           "backgroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217.")),
      Control.Monad.IO.Class.MonadIO m,
      Data.GI.Base.Overloading.HasAttributeList obj,
      Data.GI.Base.Attributes.AttrBaseTypeConstraint
        (Data.GI.Base.Overloading.FindElement
           "backgroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217."))
        obj,
      Data.GI.Base.Attributes.AttrSetTypeConstraint
        (Data.GI.Base.Overloading.FindElement
           "backgroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "backgroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217."))
        GI.Gdk.Structs.RGBA.RGBA,
      Data.GI.Base.Attributes.AttrBaseTypeConstraint
        (Data.GI.Base.Overloading.FindElement
           "foregroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217."))
        obj,
      Data.GI.Base.Attributes.AttrSetTypeConstraint
        (Data.GI.Base.Overloading.FindElement
           "foregroundRgba"
           (Data.GI.Base.Overloading.AttributeList obj)
           (((('GHC.TypeLits.Text "Unknown attribute \8216"
               'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "foregroundRgba")
              'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217 for object \8216")
             'GHC.TypeLits.:<>: 'GHC.TypeLits.ShowType obj)
            'GHC.TypeLits.:<>: 'GHC.TypeLits.Text "\8217."))
        GI.Gdk.Structs.RGBA.RGBA) =>
     Reactive.Banana.Common.Colour
     -> m [Data.GI.Base.Attributes.AttrOp obj tag]

by Paul Johnson (noreply@blogger.com) at April 18, 2018 07:23 AM

Applied Functional Programming Summer School in Utrecht

If you like to get a thorough introduction to functional programming in Haskell, check out the Applied Functional Programming Summer School, which is 27-31 August in Utrecht, Netherlands. It is part of Utrecht University’s summer school program and will have Koen Classen, Gabriele Keller, and myself as guest lecturers.

April 17, 2018 07:46 AM

Algorithmically Scrapping Your Typeclasses

I've been working on a simple Haskell98 compiler over the last few days, partly as an excuse to learn how it works, and partly to have a test-bed for trying out some potential language extensions. More on that in a future blog post.

As of yesterday, I have typeclass resolution working. The algorithm to desugar constraints into dictionaries hasn't been discussed much. Since it's rather involved, and quite interesting, I thought it might make a good topic for a blog post.

Our journey begins having just implemented Algorithm W aka Hindley-Milner. This is pretty well described in the literature, and there exist several implementations of it in Haskell, so we will not dally here. Algorithm W cashes out in a function of the type:

infer :: SymTable VName Type -> Exp VName -> TI Type

where SymTable VName is a mapping from identifiers in scope to their types, Exp VName is an expression we want to infer, and TI is our type-inference monad. As a monad, TI gives us the ability to generate fresh type variables, and to unify types as we go. Type represents an unqualified type, which is to say it can be used to describe the types a, and Int, but not Eq a => a. We will be implementing qualified types in this blog post.

infer is implemented as a catamorphism, which generates a fresh type variable for every node in the expression tree, looks up free variables in the SymTable and attempts to unify as it goes.

The most obvious thing we need to do in order to introduce constraints to our typechecker is to be able to represent them, so we two types:

infixr 0 :=>
data Qual t = (:=>)
  { qualPreds  :: [Pred]
  , unqualType :: t
  } deriving (Eq, Ord, Functor, Traversable, Foldable)

data Pred = IsInst
  { predCName :: TName
  , predInst  :: Type
  } deriving (Eq, Ord)

Cool. A Qual Type is now a qualified type, and we can represent Eq a => a via [IsInst "Eq" "a"] :=> "a" (assuming OverloadedStrings is turned on.) With this out of the way, we'll update the type of infer so its symbol table is over Qual Types, and make it return a list of Preds:

infer :: SymTable VName (Qual Type) -> Exp VName -> TI ([Pred], Type)

We update the algebra behind our infer catamorphism so that adds any Preds necessary when instantiating types:

infer sym (V a) =
  case lookupSym a sym of
    Nothing -> throwE $ "unbound variable: '" <> show a <> "'"
    Just sigma -> do
      (ps :=> t) <- instantiate a sigma
      pure (ps, t)

and can patch any other cases which might generate Preds. At the end of our cata, we'll have a big list of constraints necessary for the expression to typecheck.

As a first step, we'll just write the type-checking part necessary to implement this feature. Which is to say, we'll need a system for discharging constraints at the type-level, without necessarily doing any work towards code generation.

Without the discharging step, for example, our algorithm will typecheck (==) (1 :: Int) as Eq Int => Int -> Bool, rather than Int -> Bool (since it knows Eq Int.)

Discharging is a pretty easy algorithm. For each Pred, see if it matches the instance head of any instances you have in scope; if so, recursively discharge all of the instance's context. If you are unable to find any matching instances, just keep the Pred. For example, given the instances:

instance Eq Int
instance (Eq a, Eq b) => Eq (a, b)

and a IsInst "Eq" ("Int", "c"), our discharge algorithm will look like this:

discharging: Eq (Int, c)
  try: Eq Int    --> does not match
  try: Eq (a, b) --> matches
    remove `Eq (Int, c)` pred
    match types:
      a ~ c
      b ~ Int
    discharge: Eq Int
    discharge: Eq c

discharging: Eq Int
  try: Eq Int  --> matches
  remove `Eq Int` pred

discharging: Eq c
  try: Eq Int    --> does not match
  try: Eq (a, b) --> does not match
  keep `Eq c` pred

We can implement this in Haskell as:

match    :: Pred -> Pred -> TI (Maybe Subst)
getInsts :: ClassEnv -> [Qual Pred]

discharge :: ClassEnv -> Pred -> TI (Subst, [Pred])
discharge cenv p = do
  -- find matching instances and return their contexts
  matchingInstances <-
    for (getInsts cenv) $ \(qs :=> t) -> do
      -- the alternative here is to prevent emitting kind
      -- errors if we compare this 'Pred' against a
      -- differently-kinded instance.
      res <- (fmap (qs,) <$> match t p) <|> pure Nothing
      pure $ First res

  case getFirst $ mconcat matchingInstances of
    Just (qs, subst) ->
      -- match types in context
      let qs' = sub subst qs
      -- discharge context
      fmap mconcat $ traverse (discharge cenv) qs'

    Nothing ->
      -- unable to discharge
      pure (mempty, pure p)

Great! This works as expected, and if we want to only write a type-checker, this is sufficient. However, we don't want to only write a type-checker, we also want to generate code capable of using these instances too!

We can start by walking through the transformation in Haskell, and then generalizing from there into an actual algorithm. Starting from a class definition:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

we will generate a dictionary type for this class:

data @Functor f = @Functor
  { @fmap :: (a -> b) -> f a -> f b
  }

(I'm using the @ signs here because these things are essentially type applications. That being said, there will be no type applications in this post, so the @ should always be understood to be machinery generated by the compiler for dictionary support.)

Such a definition will give us the following terms:

@Functor :: ((a -> b) -> f a -> f b) -> @Functor f
@fmap    :: @Functor f -> (a -> b) -> f a -> f b

Notice that @fmap is just fmap but with an explicit dictionary (@Functor f) being passed in place of the Functor f constraint.

From here, in order to actually construct one of these dictionaries, we can simply inline an instances method:

instance Functor Maybe where
  fmap = \f m -> case m of { Just x -> Just (f x); Nothing -> Nothing }

-- becomes

@Functor@Maybe :: @Functor Maybe
@Functor@Maybe =
  @Functor
  { @fmap = \f m -> case m of { Just x -> Just (f x); Nothing -> Nothing }
  }

Now we need to look at how these dictionaries actually get used. It's clear that every fmap in our expression tree should be replaced with @fmap d for some d. If the type of d is monomorphic, we can simply substitute the dictionary we have:

x :: Maybe Int
x = fmap (+5) (Just 10)

-- becomes

x :: Maybe Int
x = @fmap @Functor@Maybe (+5) (Just 10)

but what happens if the type f is polymorphic? There's no dictionary we can reference statically, so we'll need to take it as a parameter:

y :: Functor f => f Int -> f Int
y = \z -> fmap (+5) z

-- becomes

y :: @Functor f -> f Int -> f Int
y = \d -> \z -> @fmap d (+5) z

A reasonable question is when should we insert these lambdas to bind the dictionaries? This stumped me for a while, but the answer is whenever you get to a binding group; which is to say whenever your expression is bound by a let, or whenever you finish processing a top-level definition.

One potential gotcha is what should happen in the case of instances with their own contexts? For example, instance (Eq a, Eq b) => Eq (a, b)? Well, the same rules apply; since a and b are polymorphic constraints, we'll need to parameterize our @Eq@(,) dictionary by the dictionaries witnessing Eq a and Eq b:

instance (Eq a, Eq b) => Eq (a, b) where
  (==) = \ab1 ab2 -> (==) (fst ab1) (fst ab2)
                  && (==) (snd ab1) (snd ab2)

-- becomes

@Eq@(,) :: @Eq a -> @Eq b -> @Eq (a, b)
@Eq@(,) = \d1 -> \d2 ->
  @Eq
  { (@==) = \ab1 ab2 -> (@==) d1 (fst ab1) (fst ab2)
                     && (@==) d2 (snd ab1) (snd ab2)
  }

Super-class constraints behave similarly.

So with all of the theory under our belts, how do we actually go about implementing this? The path forward isn't as straight-forward as we might like; while we're type-checking we need to desugar terms with constraints on them, but the result of that desugaring depends on the eventual type these terms receive.

For example, if we see (==) in our expression tree, we want to replace it with (@==) d where d might be @Eq@Int, or it might be @Eq@(,) d1 d2, or it might just stay as d! And the only way we'll know what's what is after we've performed the dischargement of our constraints.

As usual, the solution is to slap more monads into the mix:

infer
    :: SymTable VName (Qual Type)
    -> Exp VName
    -> TI ( [Pred]
          , Type
          , Reader (Pred -> Exp VName)
                   (Exp VName)
          )

Our infer catamorphism now returns an additional Reader (Pred -> Exp VName) (Exp VName), which is to say an expression that has access to which expressions it should substitute for each of its Preds. We will use this mapping to assign dictionaries to Preds, allowing us to fill in the dictionary terms once we've figured them out.

We're in the home stretch; now all we need to do is to have discharge build that map from Preds into their dictionaries and we're good to go.

getDictTerm        :: Pred -> Exp VName
getDictTypeForPred :: Pred -> Type

-- DSL-level function application
(:@) :: Exp VName -> Exp VName -> Exp VName


discharge
    :: ClassEnv
    -> Pred
    -> TI ( Subst
          , [Pred]
          , Map Pred (Exp VName)
          , [Assump Type]
          , [Exp VName]
          )
discharge cenv p = do
  matchingInstances <-
    for (getInsts cenv) $ \(qs :=> t) -> do
      res <- (fmap (qs, t, ) <$> match t p) <|> pure Nothing
      pure $ First res

  case getFirst $ mconcat matchingInstances of
    Just (qs, t, subst) ->
      -- discharge all constraints on this instance
      (subst', qs', mapPreds, assumps, subDicts)
        <- fmap mconcat
         . traverse (discharge cenv)
         $ sub subst qs

      let dictTerm = getDictTerm t
          myDict = foldl (:@) dictTerm subDicts
      pure ( subst'
           , qs'
           , mapPreds <> M.singleton p myDict
           , assumps
           -- this is just in a list so we can use 'mconcat' to
           -- collapse our traversal
           , [myDict]
           )

    Nothing ->
      -- unable to discharge, so assume the existence of a new
      -- variable with the correct type
      param <- newVName "d"
      pure ( mempty
           , [p]
           , M.singleton p param
           , [MkAssump param $ getDictTypeForPred p]
           , [param]
           )

The logic of discharge is largely the same, except we have a little more logic being driven by its new type. We now, in addition to our previous substitution and new predicates, also return a map expanding dictionaries, a list of Assumps (more on this in a second), and the resulting dictionary witnessing this discharged Pred.

If we were successful in finding a matching instance, we discharge each of its constraints, and fold the resulting dictionaries into ours. The more interesting logic is what happens if we are unable to discharge a constraint. In that case, we create a new variable of the necessary type, give that as our resulting dictionary, and emit it as an Assump. Assumps are used to denote the creation of a new variable in scope (they are also used for binding pattern matches).

The result of our new discharge function is that we have a map from every Pred we saw to the resulting dictionary for that instance, along with a list of generated variables. We can build our final expression tree via running the Reader (Pred -> Exp VName) by looking up the Preds in our dictionary map. Finally, for every assumption we were left with, we fold our resulting term in a lambda which binds that assumption.

Very cool! If you're interested in more of the nitty-gritty details behind compiling Haskell98, feel free to SMASH THAT STAR BUTTON on Github.

April 16, 2018 01:47 PM

February 2018 1 Liner 1HaskellADay Problems and Solutions

• February 8th, 2018: We have maybe :: b -> (a -> b) -> Maybe a -> b. But we don't have list? Or do we? Define list:
  list :: b -> ([a] -> b) -> [a] -> b
  list nullanswer flist lst = undefined
• BONUS: Both Maybe a and [a] are binary types, ... so is MonadPlus:
  
  Maybe a = Nothing | Just a
  List a = Cons a (List a) | Nil
  MonadPlus m => mzero | m a `mplus` m a
  
  Is there some generalization that maybe and list are functions of? What is that generalization?
• February 6th, 2018:
  You have f :: a -> [b] -> [c]
  But instead of just one a you have [a]
  Define g :: [a] -> [b] -> [c]
  in terms of f
• Daniel @leptonyu g as bs = foldl (\xs a -> f a bs ++ xs) [] as
• ptdr_bot @m0rth0n g as bs = flip f bs =<< as
• Victoria C @ToriconPrime g as bs = concat $ fmap ($ bs) (fmap f as)
• matt @themattchan g = flip $ concatMap . flip f
• Nicoλas @BeRewt g = flip (flip (>>=) . flip f) Or: g as bs = as >>= flip f bs
• Sangeet Kar @sangeet_kar g = foldMap f

by geophf (noreply@blogger.com) at April 13, 2018 02:49 PM

Software Engineer / Developer at ITProTV (Full-time)

ITPro.TV is a fast-growing digital media business that focuses on continuing education in technical domains. We are seeking software developers to help us build out and scale our next-generation of internal services and customer-facing knowledge and entertainment products.

We are currently accepting applications for full-stack software professionals to join our small but talented multidisciplinary team. The ideal candidates would demonstrate the following: • Strong familiarity with Amazon Web Services APIs • Strong familiarity with Docker • 1+ years professional experience on http-based services • Personal initiative in learning new technologies • Strong collaborative instincts (willingness to pair) • Comfort with functional programming and/or robust type systems

Technologies in play at ITPro.TV today include: • Haskell • Elm • golang • Javascript • NodeJS • Angular • Terraform • AWS

This is not at present a remote position - we are looking for full-time employees at our beautiful new Gainesville, Florida video facilities.

If you are interested in joining our team, please submit your resume and we will contact you for a quick phone interview. Successful applicants will be asked to produce a small coding exercise as part of the review process.

Get information on how to apply for this position.

April 11, 2018 02:13 PM

DDC renamed to the Disco Discus Compiler

A few weeks ago we renamed DDC to the Disco Discus Compiler (was the Disciplined Disciple Compiler). Discus is the name of the language. Disco is another word that was added because all the best compilers have three words in their name.

The system we have now is quite different to the old "Disciple" language. Discus uses capabilities instead of latent effects in its type system, and the latter was one of the main features of Disciple. The implementation of DDC has also been completely rewritten. Not a single line of code exists in the compiler that was part of the first DDC / Disciple release.

The reasons for choosing "Disco Discus" are the following:

1. A Discus fish makes a nice, friendly logo.
   
2. The logo is eminently "plushable", meaning that one can imagine manufacturing a plush toy (stuffed soft toy) with the same theme. Stickers are also an option, as are t-shirts.
3. "Disco" partly recalls a quote of Simon Peyton Jones in his paper Tackling the Awkward Squad: "In the programming-language world one rule of survival is simple: dance or die."
4. The pattern of the "Blue Discus" fish variety featured in the logo looks a bit like a mirror ball.
5. Both "Disco" and "Discus" start with a "D" so we can keep the acronym DDC.

Let it be known that Amos Robinson was the first to mention "Disco" as a viable name. The language itself was almost called "Disco", but "Discus" was chosen as the primary label due to its higher plushability.

Another option was to have called the language Tetra, as that word was already used to label an intermediate language in the compiler. "Tetra" recalled the four base kinds in the language: Data, Region, Effect, and Capability. We went so far as to try to register tetra-lang.org, but it was already taken by another fine language called Tetra. This is for the better.

We have now completed renaming all the web assets to reflect the new name. Check out the website at http://discus-lang.org/

by Ben Lippmeier (noreply@blogger.com) at April 08, 2018 11:47 AM

A compile-time debugger that helps you write tensor shape checks

A run-time debugger allows you to see concrete values in a program, make changes to them, and continue running your program. A compile-time debugger allows you to see symbolic values in a program, reason about them, and write the rest of your program, e.g. filling in missing tensor size checks, for example.

Here's an example of a compiler-time debugger in action.

Let's suppose you are writing a simple program to read a pair of tensors from two files and do a matrix multiply on them. "Easy," you think, while writing the following program:

main() {
  x = load("tensor1.t")
  y = load("tensor2.t")
  return matmul(x, y)
}

However, there is a twist: this matrix multiply is an unchecked matrix multiply. If you pass it tensors which cannot be validly multiplied together, this is undefined behavior. Your compiler has cottoned up to this fact and is refusing to compile your program. You fire up your compile-time debugger, and it drops you to the point of your program right before the error:

# Ahoy there Edward!  I stopped your program, because I could not
# prove that execution of this line was definitely safe:

   main() {
     x = load("tensor1.t")
     y = load("tensor2.t")
->   return matmul(x, y)
   }

# Here's what's in scope:

  _x_size : List(Nat)  # erases to x.size()
  _y_size : List(Nat)  # erases to y.size()
  x : Tensor(_x_size)
  y : Tensor(_y_size)

# I don't know anything else about these values

Let's take a careful look at the variables in scope. Our compile-time debugger tells us the type of a variable x by writing x : t, meaning that x has type t. We have all sorts of ordinary types like natural numbers (Nat) and lists of natural numbers (List(Nat)). More interestingly, a tensor is parametrized by a list of natural numbers, which specify their sizes at each dimension. (For simplicity, the underlying field of the tensor is assumed to be fixed.)

Our debugger has a command line, so we can ask it questions about the types of things in our program (:t is for type):

> :t 1
# Here's the type of 1, which you requested:
Nat

> :t [1, 2, 0]
# Here's the type of [1, 2, 0], which you requested:
List(Nat)

> :t matmul
# Here's the type of matmul, which you requested:
forall (a, b, c : Nat). (Tensor([a, b]), Tensor([b, c])) -> Tensor([a, c])

The type of matrix multiplication should make sense. We say a matrix multiply takes two 2-D tensors of sizes AxB and BxC, and produces a tensor of size AxC. An equivalent way of phrasing, as was done in the type above, is to say, “for any natural numbers A, B and C, matrix multiply will take a tensor of size AxB and a tensor of BxC, and give you a tensor of size AxC”.

It is also instructive to see what the type of load is:

> :t load
# Here's the type of load, which you requested:
String ~> exists (size : List(Nat)). Tensor(size)

We do not know what the dimensions of a tensor loaded from a file are; all we can say is that there exists some size (list of natural numbers), which describes the tensor in question. Our compile-time debugger has helpfully given us names for the sizes of our tensors in scope, _x_size and _y_size, and has also told us how to compute them at runtime (x.size() and y.size()).

Enough of this. Let's remind ourselves why our program has failed to typecheck:

> matmul(x, y)

# I'm sorry!  I was trying to find values of a, b and c which
# would make the following equations true:
#
#     [a, b] = _x_size
#     [b, c] = _y_size
#
# But I don't know anything about _x_size or _y_size (they are skolem
# variables), so I couldn't do it.  Cowardly bailing out!

The compiler is absolutely right. We don't know anything about the size of x or y; they could be 2D, or they could be 100D, or not have matching dimensions.

As an aside: sometimes, it's OK not to know anything about the sizes. Consider the case of adding a tensor to itself:

> add
# Here's the type of add, which you requested!
add : forall (size : List(Nat)). Tensor(size) -> Tensor(size) -> Tensor(size)

> add(x, x)
Tensor(_x_size)

# This type-checked OK!  I set size = _x_size and all of the arguments
# checked out.  You're good to go.

We don't know anything about _x_size, but add doesn't care; it'll take any List(Nat), and _x_size is certainly one of those.

Back to business. We are going to insert dynamic checks will will refine our knowledge of x and y, until it is obvious that matrix multiply will succeed.

What is a dynamic check? Operationally, a dynamic check tests whether or not some condition is true, and aborts if it is not. If we successfully run the dynamic check, we now have new information about the symbolic types in our scope. So for example, after adding a runtime test that two numbers are equal, we can subsequently assume at compile time that the numbers are equal:

> :t assert_eq_nat!
(x : Nat) -> (y : Nat) ~> x = y

First things first, we'd like to assert that our tensors are 2D tensors:

> assert_eq_nat!(len(_x_size), 2)

# OK!  I added assert_eq_nat!(len(x.size()), 2) to your program, and
# here's what I know now:

  _x_size : List(Nat)
  _y_size : List(Nat)
  x : Tensor(_x_size)
  y : Tensor(_y_size)
  len(_x_size) = 2

# By the way, I can profitably destruct _x_size into its constituent
# parts; would you like to do this? (Y/n)

> Y

# OK, your new context is this:

  _x0, _x1 : Nat
  _y_size : List(Nat)
  x : Tensor([_x0, _x1])
  y : Tensor(_y_size)

# I don't know anything about the new variables _x0 and _x1, but I
# learned enough about _x_size that I was able to eliminate it from
# the context (_x_size = [_x0, _x1])

List length is a very helpful property to test against, since it greatly specifies the shape of the list in question. We can do the same for _y_size:

> assert_eq_nat!(len(_y_size), 2)

# OK!  I added assert_eq_nat!(len(y.size()), 2) to your program, and
# here's what I know now:

  _x0, _x1 : Nat  # erases to x.size(0), x.size(1)
  _y_size : List(Nat)
  x : Tensor([_x0, _x1])
  y : Tensor(_y_size)
  len(_y_size) = 2

# By the way, I can profitably destruct _y_size into its constituent
# parts; would you like to do this? (Y/n)

> Y

# OK, your new context is this:

  _x0, _x1 : Nat  # erases to x.size(0), x.size(1)
  _y0, _y1 : Nat  # erases to y.size(0), y.size(1)
  x : Tensor([_x0, _x1])
  y : Tensor([_y0, _y1])

# I don't know anything about the new variables _y0 and _y1, but I
# learned enough about _y_size  that I was able to eliminate it from
# the context (_y_size = [_y0, _y1])

We're very close now. All we need to do is assert that the inner dimensions are equal:

> assert_eq_nat!(_x1, _y0)

# OK!  I added assert_eq_nat!(x.size(1), y.size(0)) to your program.
# After doing this, I learned _x1 = _y0, so I replaced all occurrences
# of _y0 with _x1. Now the context looks like this.

  _x0, _x1 : Nat  # erases to x.size(0), x.size(1)
  _y1 : Nat  # erases to y1.size(1)
  x : Tensor([_x0, _x1])
  y : Tensor([_x1, _y1])

Victory!

> matmul(x, y)

# This type-checked OK!  I set a = _x0, b = _x1, c = _y1 and all of the
# arguments checked out.  You're good to go.

Extracting the contents of this session back into our code, we now have:

  main() {
    x = load("tensor1.t")
    y = load("tensor2.t")
    assert_eq_nat!(x.size(), 2)
    assert_eq_nat!(y.size(), 2)
    assert_eq_nat!(x.size(1), y.size(0))
    matmul(x, y)
}

---

At this point, I must come clean: the compile time debugger I've described above doesn't actually exist. But it is not all that different from the proof modes of interactive proof assistants the automated theorem proving community works with today. But unlike theorem proving, we have a secret weapon: when the going gets tough, the tough turns into a runtime check. Conventional wisdom says that automated theorem proving requires too idealized a setting to be useful in writing software today. Conventional wisdom is wrong.

by Edward Z. Yang at April 07, 2018 03:49 AM

Exam advice

Part of my job is to give advice to my undergraduate students about exam technique and preparing for exams. I was always quite a nervous about exams “back in the day”, and I put a lot of effort into revising and planning. In retrospect, I think I enjoyed these times: I have many happy memories of long days and evenings studying with my friends (whose presence and encouragement made it a lot more palatable).

Anyway, I decided to serialise my advice and put it online in case it can be of any help or inspiration to others either taking exams, or giving exam advice. I’m sure I can and will probably think of more, so I made it a GitHub “gist” so I can revise it whenever more advice pops into my head.

<script src="https://gist.github.com/dorchard/f7b9b95fe93c118fd1880197bcdfe196.js"></script>

by dorchard at April 04, 2018 09:28 PM

Darcs 2.14.0 released

The Darcs team is pleased to announce the release of Darcs 2.14.0!

Darcs is a free, open source revision control system. It is:

• Distributed: Every user has access to the full command set, removing boundaries between server and client or committer and non-committers.
• Interactive: Darcs is easy to learn and efficient to use because it asks you questions in response to simple commands, giving you choices in your work flow. You can choose to record one change in a file, while ignoring another. As you update from upstream, you can review each patch name, even the full "diff" for interesting patches.
• Smart: Originally developed by physicist David Roundy, darcs isbased on a unique algebra of patches.

Learn more about Darcs on http://darcs.net .

Supported GHC and Cabal versions

Darcs 2.14 can be compiled with GHC 8.0, 8.2 and 8.4, and
supports Cabal versions from 1.24.

Windows issues

Darcs 2.14 received many updates in its support of encoding.
However, it may still contain bugs, especially under Windows,
a platform for which we have fewer known users. Please let us
know if you encounter weird behaviour under Windows.

What's new

User Interface:

•  fix encoding business, make DARCS_DONT_ESCAPE_8BIT=1 default (Ben Franksen, Ganesh Sittampalam)
• show explicit dependencies in `darcs log -s` (Gian Piero Carrubba)
• improve bash/zsh completion (Ben, Gian Piero)
• no longer print an error message when ctrlc'ing pager (Guillaume Hoffmann)
• darcs help markdown` mentions all files in `_darcs/prefs/` (Guillaume)
• add patch index status to `show repo` command (Ben)

New features:

• per-file conflict marking (Ben)
• make it possible to use DARCS_SCP=rsync (Ben)
• add --not-in-remote option to unrecord command (Ben)

Performance:

• plug memory leak and improve efficiency in annotate (Ben)
• save unneeded FL/RL reverses in SelectChanges module (Ben)
• optimize token replace code and --look-for-replaces (Ben)
• no longer show conflicting files on `whatsnew -s`, will reintrodue this
• feature when it is done efficiently (Guillaume)

Developer-related:

• separate display and storage of patches (Ben)
• support GHC 8.2 and GHC 8.4 (Ganesh)
• many refactorings in Darcs.Repository modules and API (Ben, Guillaume)
• no longer track build dependencies in Setup.hs, nor use alpha, beta, rc names (Guillaume)
• refactor `pull --reorder-patches` (Ben)
• refactor SelectChanges (Ben)
• remove Patchy typeclass and redundant constaints where possible (Guillaume)
• fix build with cabal new-build (Francesco Ariis)
• unit and quickcheck tests for inventories (Ben)
• throw out all access to bytestring internals from Darcs.Util.ByteString (Ben)
• refactor, simplify, and document hunk application (Ben)
• drop support of old cache location and SHA1-hashed repos (Guillaume)
• rely on GHC's own stack traces for bug reporting (Guillaume)

Issues resolved in Darcs 2.14:

• fix mail encoding with '.' or '=' as last character (Timo von Holtz)
• issue2526: whatsnew -l --boring should list boring files (Ben)
• issue2208: replace detects existing force hunks in working (Ben)
• issue2512: author name is written to repository after multiple-choice  prompt (Stephan-A. Posselt)
• issue2359: convert --export mishandles Unicode filenames (Ben)
• issue2545: prevent argument smuggling in SSH repository URLs (Gian Piero)
• issue2581: fix rebase pull --reorder (Ben)
• issue2575: fix unrevert with rebase (Ben)
• issue2579: allow darcs send to work even if no MTA is installed
• issue2555: include explicit dependencies in the output of `log -v` (Gian Piero)
• issue2569: decoding multibyte characters (Ben)
• issue2563: create remote repo in correct format in ssh tests (Ben)
• issue2565: create _darcs dir after searching for an existing one (Ben)
• issue2567: darcs whatsnew --unified (Ben)
• issue2566: avoid renaming across file systems (Ben)
• issue2564: delete wrong and irrelevant propConcatPS (Guillaume)
• issue2559: remove trailing empty lines in patch header edition (Guillaume)
• issue2536: mask out internal matchers in `show files` routing logic (Gian Piero)

by guillaume (noreply@blogger.com) at April 04, 2018 03:04 PM

HKD: Less Terrible than You Might Expect

I thought I'd take some time to respond to some of the concerns raised about my recent Higher-Kinded Data and Free Lenses for Higher-Kinded Data posts.

Deriving Instances for HKD

One of the biggest concerns over the HKD technique was that it breaks automated deriving of instances. This is not entirely true, it just requires turning on {-# LANGUAGE StandaloneDeriving #-} and then using one of two approaches.

The simplest method is that we can simply derive all of our instances only for the types we expect to use:

deriving instance Eq (Person' Identity)
deriving instance Eq (Person' Maybe)
deriving instance Ord (Person' Identity)
deriving instance Ord (Person' Maybe)

Admittedly it's kind of a shit solution, but technically it does work.

An alternative approach is to automatically lift these instances from f a over the HKD f a type family. The construction is a little more involved than I want to get into today, but thankfully it's available as library code from the spiffy one-liner package.

After adding one-liner as a dependency, we can lift our instances over a polymorphic f using the Constraints type-synonym:

deriving instance (Constraints (Person' f) Eq) => Eq (Person' f)

Easy!

Runtime Performance

The other big concern was over whether we pay performance costs for getting so many cool things for free.

For the most part, if you mark all of your generic type-class methods as INLINE and turn on -O2, most of the time you're not going to pay any runtime cost for using the HKD technique.

Don't believe me? I can prove it, at least for our free lenses.

Let's fire up the inspection-testing package, which allows us to write core-level equalities that we'd like the compiler to prove for us. The equality we want to show is that the core generated for using our free lenses is exactly what would be generated by using hand-written lenses.

We can do this by adding some front-matter to our module:

{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}

import Test.Inspection

This installs the inspection-testing compiler plugin, which is responsible for doing the work for us. Next, we'll define our lenses:

freeName :: Lens' (Person' Identity) String
Person (LensFor freeName) _ = getLenses

handName :: Lens' (Person' Identity) String
handName a2fb s = a2fb (pName s) <&> \b -> s { pName = b }

and finally, we can write the equalities we'd like GHC to prove for us. This is done in two steps -- writing top-level left- and right- handed sides of the equality, and then writing a TemplateHaskell splice to generate the proof.

viewLhs, viewRhs :: Person' Identity -> String
viewLhs = view freeName
viewRhs = view handName

inspect $ 'viewLhs === 'viewRhs

Compiling this dumps some new information into our terminal:

src/Main.hs:34:1: viewLhs === viewRhs passed.
inspection testing successful
      expected successes: 1

We can write an analogy equality to ensure that the generated setter code is equivalent:

setLhs, setRhs :: String -> Person' Identity -> Person' Identity
setLhs y = freeName .~ y
setRhs y = handName .~ y

inspect $ 'setLhs === 'setRhs

And upon compiling this:

src/Main.hs:34:1: viewLhs === viewRhs passed.
src/Main.hs:35:1: setLhs === setRhs passed.
inspection testing successful
      expected successes: 2

Cool! Just to satisfy your curiosity, the actual lenses themselves aren't equivalent:

inspect $ 'freeName === 'handName

results in a big core dump showing that freeName is a gross disgusting chain of fmaps and that handName is pretty and elegant. And the module fails to compile, which is neat -- it means we can write these proofs inline and the compiler will keep us honest if we ever break them.

But what's cool here is that even though our lenses do not result in equivalent code, actually using them does -- which means that under most circumstances, we won't be paying to use them.

April 04, 2018 02:15 PM

HsQML 0.3.5.1 released: Cabal Armageddon

For some years now, HsQML* has been accumulating an increasingly complex pile of Template Haskell in its Setup script in order to accommodate all the API changes since Cabal 1.14. It couldn't last forever and indeed Cabal 2.0 has finally delivered a blow to what must have at least been a contender for the title of "world's most arcane Setup.hs". Not a fatal blow mind you, but let's say that it's less complicated than it used to be.

Last September, I very quietly released version 0.3.5.0 of HsQML which, among
other things, used the new setup-depends feature to try and stem the tide and force building the Setup script against Cabal 1.24. However, the even newer 0.3.5.1 release made last week finally adopts the Cabal 2.0 API and does away with Template Haskell. Hurray!

There are a number of other minor fixes in these two releases, mostly adjusting for newer versions of Haskell tools and libraries.

* For the uninitiated, HsQML is a Haskell binding to the Qt Quick user interface toolkit.

release-0.3.5.1 - 2018.03.28

 * Fixed building with Semigroup/Monoid changes in base 4.11 (GHC 8.4.1).
 * Fixed crash if setDebugLogLevel called before other functions.
 * Fixed GHCi cbits library install location.
 * Changed Setup script to use Cabal 2 API only.
 * Relaxed Cabal constraint on 'QuickCheck'.

release-0.3.5.0 - 2017.09.08

 * Added facility for setting Qt application flags.
 * Fixed building GHCi objects with Cabal 1.24.
 * Relaxed Cabal constraint on 'QuickCheck' and fixed test suite.
 * Relaxed Cabal constraint on 'directory'.

by Robin KAY (noreply@blogger.com) at April 03, 2018 10:55 PM

Frontend Engineer at Trivium Real Estate (Full-time)

TriviumRE is an investor-backed, data-mining startup for the commercial real estate industry; we're making data entry jobs less painful. Our MVP is moments away from launching and customers are queuing to take it for a spin. As such, we're growing our team to tackle the challenges ahead.

What about the team? We have a high emphasis on continual learning. If you're not learning something new on the job its time for a new one. Our tech stack reflects this; Haskell and Elm are the main languages. We don't mind if its your first exposure to either. We're not afraid of experimenting or making mistakes. The most important quality of anyone on our team is their ability to learn and teach.

Since we're still young, working with us means you have a lot of influence in shaping the culture and direction of the company. You'll also a chance to grow your skill set faster than somewhere else.

The product We're building a data mining tool that can explicitly learn a relational data model based on sample inputs. It's radically improves data entry and data cleaning for financial analysts. Customers have loved our demos and we're understandably coy in our public descriptions.

Front-End Engineer

This is for someone who:

• is comfortable in functional programming, especially Elm; and
• is experienced shipping front-end software to production; and
• has empathy for users and loves friendly UX; and
• has an eagerness to learn and willingness to share knowledge.

Benefits

• £50-70k DOE. + Equity.
• Highly intelligent, supportive team.
• 20+ holidays per year.
• Support for conferences & other tech related education.

A Typical Day

• Start off writing a feature that requires elm-ports. These can be tricky, so you pair with another developer who has shipped such code before.

• After lunch you're requested to review a Pull Request that fixes a bug you accidentally introduced a couple weeks back. There's no blame, instead some discussion about how our tests and review process could have caught this earlier.

• The afternoon is spent with the Product guys around a whiteboard. You're helping them sketch out a realistic wire-frame for a feature we plan to deliver in a couple of weeks.

Some Tech we like:

We're more interested in a willingness and ability to learn than what you currently know. But in case you're interested in the stack we're using:

• Haskell
• Elm
• PostgreSQL
• Javascript
• Python / scikit-learn
• Tensorflow / Deep learning
• AWS
• CircleCI
• Automated Testing

Get information on how to apply for this position.

April 03, 2018 12:35 PM

March 2018 1HaskellADay problems and solutions

• March 14th, 2018: Wednesday #haskell problem I am thinking about sumaSumasCuadradosDivisores from the Haskell community via @Jose_A_Alonso 
• March 12th, 2018: Monday's #haskell problem is Improving Tarski's logic language with curried functions. 
• March 8th, 2018: For Thursday's #haskell problem, thanks to @wtfunctional, we'll play with Other People's Code! ... and Mandelbrot sets. 
  
• March 6th, 2018: Tuesday's #haskell exercise asks the eternal question: "Are you my mom?"... and also looks at curried functions in a logic framework... which is nice. Last Tuesday's #haskell solution ended in pathos: I know 'momOf', but I cannot answer, 'are you my mom?' Can you not feel the sads? 
• March 5th, 2018: Monday's #haskell problem is a little "Introduction to Logic" by Tarski to start our week of right. I went a little 'forall' in the #haskell solution today. Sorry. #notsorry 
  

by geophf (noreply@blogger.com) at April 02, 2018 02:31 PM

Stop breaking compatibility

To get things started correctly, I'd like to define backwards compatibility as the following:

Maintaining the invariant that, amongst successive versions of a library or tool, software using that library or tool continues to build and execute with matching semantics (though perhaps different performance characteristics).

There is some wiggle room for defining if a change is properly backwards compatible. If we introduce a new identifier which conflicts with an old one, this may break a build, but most people accept this as "backwards compatible enough." Also, fixing a bug in an implementation may, in some cases, break something. But let's ignore the subtle cases, and instead just focus on the big picture: I released some new library, and it changed the type signature of a function, tweaked a data type, or significantly altered runtime behavior.

Let's just cut to the chase: every single time you break backwards compatibility should be considered a software crime. I'm going to demonstrate why.

It wastes time

Let's face it: changelogs are a total waste of time. No one ever reads them. Ever. And the only reason you're writing them is to notify people of backwards incompatible changes. So now you've wasted the time of two groups of people:

• The library maintainer has to write a changelog that no one is going to read
• Users of a library have to spend time reading the changelog that they're never going to read anyway

Instead, try this one simple trick: never break the API in any way. It takes literally no time to not break things. So save yourself and your users some time, and:

• Don't write useless changelogs
• Don't break APIs

Freedom is Slavery

The freedom to break an API is a false freedom. In fact, you are now a slave. You're a slave to perfection. You will never be satisfied with your API. You'll always want to improve it. You'll want to make it safer, easier to use, or provide more efficient functions. If you go down this route, you'll never be free!

Instead, embrace the true freedom: your API will never be perfect. People will limp along with it as is. But this is far better than ever making a user change their code.

Follow Java's example

Java avoids backwards incompatible changes. And there has literally never been a downside to this approach. Code from 20 years ago works perfectly on modern JVMs without any form of modification, and it is a pleasure to write against Java APIs. After all: who minds a little cruft if you don't have to learn new APIs ever?

Some people are concerned that new users of the language may have trouble understanding accumulated cruft. But seriously, just keep some log of things that have changed over time, which every new user must read, and you'll be golden. Worried about scaring off new people? Don't be. If they're not willing to invest in learning the history of your language or library, you don't want them anyway.

Use prefixes and suffixes

Let's say you've written a function theThing. And now you've realized that the function needs to take some extra parameter. You're tempted to change the signature. But that's pure evil! Instead, follow one of these time-tested techniques:

• Call the new function, of course, newTheThing. The naming pattern is clear here: newerTheThing, newNewerTheThing, newerNewerTheThing, etc. It's totally obvious, easy to remember, and helpers users understand the work you've put in on your library over the years
• If for some reason you don't like that, you can go with the less elegant _v2, _v3, etc suffix: newThing_v2, newThing_v3, etc

After all, it's not like there's any other place where you could increment a number to indicate that there have been changes in your library.

Compile time checking

This approach may unironically be necessary for dynamically typed languages (cough, Python 3, cough). But pretend like all languages are actually good, and have nice type systems and compile-time checking.

You may think that we're going through too much work here with maintaining backwards compatibility. After all, users will just have to build their project with the new release and then fix up compiler errors.

But let's be honest here. No one uses CI. And no one pins versions of their dependencies. If you break backwards compat, you're guaranteed to have dozens of production services just stop working tomorrow when the code fails to compile. There is literally nothing to do to stop this. Do you want to be responsible for taking down the worlds' banks just because you wanted to clean up an API? I didn't think so.

Do the moral thing, and don't break APIs!

Conclusion

I think I've made my point more than well enough. There is never a justification to break an API. Ever. At all. If you do it, you are an evil, immoral, selfish person. Stop thinking of beauty. Stop thinking of elegance. Stop thinking of an easy to use API. Let the cruft accumulate, embrace the cruft, live in the cruft, and the world will be a better place.

April 01, 2018 12:00 AM

Free Lenses for Higher-Kinded Data

In the previous blog post, we discussed higher-kinded data (HKD), the technique of parameterizing your data types by something of kind * -> *, and subsequently wrapping each of its fields by this parameter. The example we used previously was transforming this type:

data Person = Person
  { pName :: String
  , pAge  :: Int
  } deriving (Generic)

into its HKD representation:

data Person' f = Person
  { pName :: HKD f String
  , pAge  :: HKD f Int
  } deriving (Generic)

Recall that HKD is a type family given by

type family HKD f a where
  HKD Identity a = a
  HKD f        a = f a

which is responsible for stripping out an Identity wrapper. This means we can recreate our original Person type via type Person = Person' Identity, and use it in all the same places we used to be able to.

Our previous exploration of the topic unearthed some rather trivial applications of this approach; we generated a function validate :: f Maybe -> Maybe (f Identity) which can roughly be described as a "type-level sequence." In fact, in the comments, Syrak pointed out we can implement this function in a less-round-about way via gtraverse id.

So, how about we do something a little more interesting today? Let's generate lenses for arbitrary product types.

In my opinion, one of the biggest advantages of the HKD approach is it answers the question "where can we put this stuff we've generated?" Generating lenses generically is pretty trivial (once you have wrapped your head around the mind-boggling types), but the harder part is where to put it. The lens package uses TemplateHaskell to generate new top-level bindings so it has somewhere to put the lenses. But we have HKD.

Recall, our Person' type:

data Person' f = Person
  { pName :: HKD f String
  , pAge  :: HKD f Int
  } deriving (Generic)

By substituting f ~ Lens' (Person' Identity), we'll have pName :: Lens' (Person' Identity) String, which is exactly the type we need. All of a sudden it looks like we have an answer to "where should we put it": inside our original structure itself. If we can generate a record of type Person' (Lens' (Person' Identity), destructuring such a thing will give us the lenses we want, allowing us to name them when we do the destructuring. Cool!

Unfortunately, we're unable to partially apply type-synonyms, so we'll need to introduce a new type constructor that we can partially apply. Enter LensesFor:

data LensFor s a = LensFor
  { getLensFor :: Lens' s a
  }

The next step is to think really hard about what our lens-providing type-class should look like. At the risk of sounding like a scratched CD in a walkman, I consider the design of the typeclass to be by far the hardest part of this approach. So we'll work through the derivation together:

I always begin with my "template" generic-deriving class:

class GLenses i o where
  glenses :: i p -> o p

where p is a mysterious existentialized type parameter "reserved for future use" by the GHC.Generics interface. Recall that i is the incoming type for the transformation (not the original Person' type), and o is correspondingly the output type of the transformation.

Since lenses don't depend on a particular "input" record -- they should be able to be generated ex nihilo -- we can drop the i p parameter from glenses. Furthermore, since eventually our lenses are going to depend on our "original" type (the Person' in our desired LensesFor (Person' Identity)), we'll need another parameter in our typeclass to track that. Let's call it z.

class GLenses z i o where
  glenses :: o p

As far as methods go, glenses is pretty unsatisfactory right now; it leaves most of its type parameters ambiguous. No good. We can resolve this issue by realizing that we're going to need to actually provide lenses at the end of the day, and because GHC.Generics doesn't give us any such functionality, we'll need to write it ourselves. Which implies we're going to need to do structural induction as we traverse our generic Representation.

The trick here is that in order to provide a lens, we're going to need to have a lens to give. So we'll add a Lens' to our glenses signature -- but what type should it have? At the end of the day, we want to provide a Lens' (z Identity) a where a is the type of the field we're trying to get. Since we always want a lens starting from z Identity, that pins down one side of our lens parameter.

class GLenses z i o where
  glenses :: Lens' (z Identity) _ -> o p

We still have the notion of an input to our glenses, which we want to transform into our output. And that's what tears it; if we have a lens from our original type where we currently are in our Generic traversal, we can transform that into a Generic structure which contains the lenses we want.

class GLenses z i o where
  glenses :: Lens' (z Identity) (i p) -> o p

Don't worry if you're not entirely sure about the reasoning here; I wasn't either until I worked through the actual implementation. It took a few iterations to get right. Like I said, figuring out what this method should look like is by far the hardest part. Hopefully going through the rest of the exercise will help convince us that we got our interface correct.

With our typeclass pinned down, we're ready to begin our implementation. We start, as always, with the base case, which here is "what should happen if we have a K1 type?" Recall a K1 corresponds to the end of our generic structural induction, which is to say, this is a type that isn't ours. It's the HKD f String in pName :: HKD f String from our example.

So, if we have an a wrapped in a K1, we want to instead produce a LensFor (z Identity) a wrapped in the same.

instance GLenses z (K1 _x a)
                   (K1 _x (LensFor (z Identity) a)) where
  glenses l = K1                            -- [3]
            $ LensFor                       -- [2]
            $ \f -> l $ fmap K1 . f . unK1  -- [1]
  {-# INLINE glenses #-}

Egads there's a lot going on here. Let's work through it together. In [1], we transform the lens we were given (l) so that it will burrow through a K1 constructor -- essentially turning it from a Lens' (z Identity) (K1 _x a) into a Lens' (z Identity) a. At [2], we wrap our generated lens in the LensFor constructor, and then in [3] we wrap our generated lens back in the GHC.Generics machinery so we can transform it back into our HKD representation later.

And now for our induction. The general idea here is that we're going to need to transform the lens we got into a new lens that focuses down through our generic structure as we traverse it. We can look at the M1 case because it's babby's first instance when compared to K1:

instance (GLenses z i o)
    => GLenses z (M1 _a _b i) (M1 _a _b o) where
  glenses l = M1 $ glenses $ \f -> l $ fmap M1 . f . unM1
  {-# INLINE glenses #-}

Here we're saying we can lift a GLenses z i o over an M1 constructor by calling glenses with an updated lens that will burrow through the M1-ness. This transformation is completely analogous to the one we did for K1. Once we have our generated lenses, we need to re-wrap the structure in an M1 constructor so we can transform it back into our HKD representation.

The product case looks a little trickier, but it's only because GHC.Generics doesn't provide us with any useful un/wrapping combinators for the (:*:) constructor.

instance (GLenses z i o, GLenses z i' o')
    => GLenses z (i :*: i') (o :*: o') where
  glenses l = glenses (\f -> l (\(a :*: b) -> fmap (:*: b) $ f a))
          :*: glenses (\f -> l (\(a :*: b) -> fmap (a :*:) $ f b))
  {-# INLINE glenses #-}

We finish it off with the trivial instances for V1 and U1:

instance GLenses z V1 V1 where
  glenses l = undefined

instance GLenses z U1 U1 where
  glenses l = U1

And voila! Our induction is complete. Notice that we did not write an instance for (:+:) (coproducts), because lenses are not defined for coproduct types. This is fine for our Person' case, which has no coproducts, but types that do will simply be unable to find a GLenses instance, and will fail to compile. No harm, no foul.

With this out of the way, we need to write our final interface that will use all of the generic machinery and provide nice access to all of this machinery. We're going to need to call glenses (obviously), and pass in a Lens' (z Identity) (Rep (z Identity)) in order to get the whole thing running. Then, once everything is build, we'll need to call to to turn our generic representation back into the HKD representation.

But how can we get a Lens'(z Identity) (Rep (z Identity))? Well, we know that GHC.Generics gives us an isomorphism between a type and its Rep, as witnessed by to and from. We further know that every Iso is indeed a Lens, and so the lens we want is just iso from to. Our function, then, is "simply":

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

getLenses
    :: forall z
     . ( Generic (z Identity)
       , Generic (z (LensFor (z Identity)))
       , GLenses z (Rep (z Identity))
                   (Rep (z (LensFor (z Identity))))
       )
    => z (LensFor (z Identity))
getLenses = to $ glenses @z $ iso from to

where I just wrote the z (LensFor (z Identity)) part of the type signature, and copy-pasted constraints from the error messages until the compiler was happy.

OK, so let's take it for a spin, shall we? We can get our lenses thusly:

Person (LensFor lName) (LensFor lAge) = getLenses

Yay! Finally we can ask GHCi for their types, which is a surprisingly satisfying experience:

> :t lName
lName :: Lens' (Person' Identity) String

Pretty sweet, ne? Now that getLenses has been implemented generically, it can become library code that will work for any product-type we can throw at it. Which means free lenses without TemplateHaskell for any types we define in the HKD form.

This HKD pattern is useful enough that I've begun implement literally all of my "data" (as opposed to "control") types as higher-kinded data. With an extra type synonym type X = X' Identity, and {-# LANGUAGE TypeSynonymInstances #-}, nobody will ever know the difference, except that it affords me the ability to use all of this stuff in the future should I want to.

As Conal says, all of this stuff might not necessarily be "for free" but at the very least, it's "already paid for."

---

More shoutouts to Travis Athougies, whose sweet library beam uses this approach to generate lenses for working with SQL tables. I consulted the beam source more than a couple times in writing this post. Thanks again, Travis!

March 31, 2018 12:42 PM

LambdaConf Haskell Hackathon 2018

On June 6, 2018, I'll be running a Haskell Hackathon as a Mini-Conf after LambdaConf. I've started a Github repo for preparing for this hackathon, and I'd like to ask for people to contribute, whether or not you'll be attending the hackathon.

My goal with this repository is to provide a way for people maintaining open source projects to submit work items that they would like help with, and which they believe could be tackled by a new contributor within the course of a day (or less!). Note that these don't necessarily need to be beginner-level tasks, but the issue tracker does ask you to indicate the skill level you think is needed.

If you have such a task, please submit it as an issue.

And of course: if you're going to be at LambdaConf, or otherwise will be in or around Boulder on that date, you're warmly welcome to attend and participate in this hackathon. It will be a great opportunity to dive in to the open source Haskell ecosystem, meet other Haskellers, get some guidance, and/or mentor others. If anyone has questions, please feel free to reach out in the comments below or elsewhere. Hope to see you there!

March 28, 2018 10:12 AM

Haskell development job with Well-Typed

tl;dr If you’d like a job with us, send your application as soon as possible.

We are looking for a Haskell expert to join our team at Well-Typed. This is a great opportunity for someone who is passionate about Haskell and who is keen to improve and promote Haskell in a professional context.

About Well-Typed

We are a team of top notch Haskell experts. Founded in 2008, we were the first company dedicated to promoting the mainstream commercial use of Haskell. To achieve this aim, we help companies that are using or moving to Haskell by providing a range of services including consulting, development, training, and support and improvement of the Haskell development tools. We work with a wide range of clients, from tiny startups to well-known multinationals. We have established a track record of technical excellence and satisfied customers.

Our company has a strong engineering culture. All our managers and decision makers are themselves Haskell developers. Most of us have an academic background and we are not afraid to apply proper computer science to customers’ problems, particularly the fruits of FP and PL research.

We are a self-funded company so we are not beholden to external investors and can concentrate on the interests of our clients, our staff and the Haskell community.

About the job

The role is not tied to a single specific project or task, and allows remote work.

In general, work for Well-Typed could cover any of the projects and activities that we are involved in as a company. The work may involve:

• working on GHC, libraries and tools;

• Haskell application development;

• working directly with clients to solve their problems;

• teaching Haskell and developing training materials.

We try wherever possible to arrange tasks within our team to suit peoples’ preferences and to rotate to provide variety and interest.

Well-Typed has a variety of clients. For some we do proprietary Haskell development and consulting. For others, much of the work involves open-source development and cooperating with the rest of the Haskell community: the commercial, open-source and academic users.

Our ideal candidate has excellent knowledge of Haskell, whether from industry, academia or personal interest. Familiarity with other languages, low-level programming and good software engineering practices are also useful. Good organisation and ability to manage your own time and reliably meet deadlines is important. You should also have good communication skills.

You are likely to have a bachelor’s degree or higher in computer science or a related field, although this isn’t a requirement.

Further (optional) bonus skills:

• experience in teaching Haskell or other technical topics,

• experience of consulting or running a business,

• knowledge of and experience in applying formal methods,

• familiarity with (E)DSL design,

• knowledge of concurrency and/or systems programming,

• experience with working on GHC,

• experience with web programming (in particular front-end),

• … (you tell us!)

Offer details

The offer is initially for one year full time, with the intention of a long term arrangement. Living in England is not required. We may be able to offer either employment or sub-contracting, depending on the jurisdiction in which you live.

If you are interested, please apply via info@well-typed.com. Tell us why you are interested and why you would be a good fit for Well-Typed, and attach your CV. Please indicate how soon you might be able to start.

We are more than happy to answer informal enquiries. Contact Andres Löh (andres@well-typed.com, kosmikus on freenode IRC) for further information.

We will consider applications as soon as we receive them. In any case, please try to get your application to us by 27 April 2018.

by andres, duncan, adam at March 27, 2018 08:55 PM

This is the video of the Sydney instance of my YOW! Night tour...

<iframe allow="autoplay; encrypted-media" allowfullscreen="allowfullscreen" frameborder="0" height="225" id="youtube_iframe" src="https://www.youtube.com/embed/2CWEg64qZnY?feature=oembed&amp;enablejsapi=1&amp;origin=http://safe.txmblr.com&amp;wmode=opaque" width="400"></iframe>

This is the video of the Sydney instance of my YOW! Night tour this month, talking about “Demystifying functional programming and what that means for learning & teaching” — i.e., teaching FP to the early majority of adopters (slides).

March 26, 2018 03:44 AM

Reservoir sampling with few random bits

Assume you are Nisus, the “one cross each” guy in Monty Python’s “Life of Brian” movie. Condemned prisoners file past you one by one, on their way to crucifixion. Now it happens that this particular day, feel both both benevolent and very indecisive. Because you feel benevolent, you want to liberate one of the condemned. But because you feel indecisive, you don’t want to pick the lucky one yourself, so you have to leave it to chance. And you don’t want anybody to have grounds to to complain, so you want to give each prisoner exactly the same chance.

This would be a relatively simple task if you knew the number of prisoners, n, ahead of time: Pick a random number k ∈ {1, …, n}, count while you hand our the crosses, and tell the kth prisoner to get lost.

But alas, the Romans judiciary system is big and effective, and you have no idea how many prisoners will emerge from the dungeons today. So you might plan to just let them all wait next to you while you count them (to figure out what n is), but that won’t work either: There is not enough space to have them waiting, and some might try to escape in the confusion before you are done counting. So in fact, you can only have one prisoner waiting at a time. As soon as the next one comes, you have to send one of them towards execution.

This is still a solvable problem, and the solution is Reservoir sampling: You let the first prisoner wait. When the second one comes, you pick one of them with probability ½, and let him wait. When the third one comes, with probability ⅔ you send him on, and with probability ⅓ to let him wait. The fourth is sent forth with probability ¼ and kept waiting with probability ¼. And so on. When finally the dungeon master tells you that all prisoners have emerged, whoever is waiting next to you is the lucky guy.

Before you do that, you should convince yourself that this is fair: The kth prisoner is the lucky one if you let him wait and from then on, all other prisoners are sent forth. The probability of this happening is ¹ ⁄ ₖ ⋅ ᵏ ⁄ ₖ₊₁ ⋅ ᵏ⁺¹ ⁄ ₖ₊₂ ⋅ ⋯ ⋅ ⁿ⁻¹ ⁄ ₙ which, after a number of cancellations, resolves to ¹ ⁄ ₙ. Because k does no longer show up in this calculation, the probability is the same for everybody, and hence fair.

How to not make a decision

A fair RNG

So far so good. But the story misses an important point: Where do you get your randomness from? Just picking randomly is hardly random. Luckily, you just have been given your guerdon, and you have a Roman coin in your pocket. Let us assume the coin is perfectly fair: With probability ½ it shows the head of Libertas, and with probability ½ a bunch of horses. It is easy to use this coin to distinguish between the first and second prisoners, but when the third comes out, things get hairy.

You can try to throw the coin many times; say, 10 times. This has 2¹⁰ = 1024 outcomes, which we can interpret as a number between 1 and 1024. If you give the third prisoner his freedom when this number is between 1 and 341, and you give him a cross if the number is between 342 and 1024, then you made pretty fair call. Not yet fully satisfying, but let’s go with it for now.

There is, however, another problem with this: You have to throw the coin a lot of times: For each prisoner, you toss it 10 times! This is too slow, and the plebs will get impatient. And it clearly is wasteful. The great philosopher Shannonus taught you that throwing the coin ten times gives you 10 bits of entropy, but you actually need only −(⅓ ⋅ log(⅓)+⅔⋅log(⅔)) = 0.918… bits to make this ⅓-⅔ decision. We should use those left-over 9.81 bits! How do we do that?

Unreal real randomness

To come up with a better (and maybe even optimal) plan, imagine for a moment that you had a source of randomness that gives you a real real number in the range (0, 1), uniformly. Clearly, that would solve your problem, because when prisoner k emerges, you can draw a random number r and let this prisoner wait if r < ¹ ⁄ ₖ.

But you don’t actually have to draw a random number more than once: It suffices to pick a single r ∈ (0, 1) at the very beginning. You just have to be a bit cleverer when deciding whether to keep the kths prisoner next to you. Let’s go through it step by step:

• When Augustus, the first prisoner, comes out, you simply keep him.
• When Brutus, the second prisoner, comes out, you keep him with probability ½. You do that if r < ½. You also start some bookkeeping, by remembering the range of r that has led to this outcome; in this case, the range is (0, ½). If you picked Augustus, the range is (½,1).

• Now Claudius comes out, and you want to keep him with probability ⅓. If the range that you remembered is (0, ½), you keep him if r < ⅙. Similarly, if the range is (½,1) you keep him if r < ½ + ⅙ = ⁴ ⁄ ₆.

  The currently remembered range is now (⁴⁄₆,1) if Augustus is waiting, (⅙,½) if Brutus is waiting and either (0, ⅙) or (½,⁴⁄₆) if Claudius is waiting. Notice that the ranges are not all of the same size, but if you add the lengths of each prisoner’s range, you have ⅓, which means that every prisoner has the same chance to be waiting so far.

• Finally, Decimus shows up. You repeat this procedure: Look at the current interval; if r is in the left quarter of it, Decimus stays, otherwise he leaves.

I tried to visualize this, and came up with this. Pick r, locate the right spot on the x axis, and you can read off, by going down, who is waiting next you.

A table for Nisus

Back to using coins

With this strategy in mind, we can go back to using a coin. Now, a single coin flip does not give us r. 1000 coin flips don’t either. If we could flip the coin an infinite number of times, yes, then we could get r out of this: The first coin flip decides the first bit after the decimal binary point: Head is 0, horses are 1. The second the second bit. And so on.

But note that you don’t need to know precisely r. To decide whether Augustus or Brutus stay, you only need to know if r is in the left or the right half -- and you know that after the first coin flip. You can also tell whether Claudius stays as soon as you threw the coin often enough to determine if r < ⅙. This might already be the case after a single coin throw (if it shows horses), or after a few more. The likelihood that you can’t decide with certainty whether r < ⅓ goes down exponentially, so with probability 1, you will come to a conclusion eventually.

And the good thing is: If you were unlucky and had to throw the coin very often, then you learned a lot about r, and you can decide the next few prisoners without throwing a coin at all! In this sense, we managed to use “left-over entropy”.

And the other good thing is: There are no rounding errors any more. Every prisoner has the same chance to be freed.

A visualization

I tried to visualize the whole story, using CodeWorld. In this not very pretty animation, you see the prisoners (so far just simple numbers) coming from the left. Nisus (not shown) either lets them wait in the slot in the top, or sends them to the right. Sometimes he needs to toss a coin. Below you can see, in numbers and in a bar, what ranges of r are interesting: In green, the range which indicates that the current prisoner can stay, in red the range where he has to go, and in blue the range that r is known so far.

Nisus (not shown) at work

Probably, by the time you have read this until now, the animation is not at the beginning any more. Move the mouse over it, and you will see controls in the lower left corner; the first button resets the animation. You can also check out the source code.

Open questions

So Nisus is happy, because with few coin tosses, he can fairly pick a random prisoner to free. I am not fully satisfied yet, because of two option questions:

• Is this algorithm optimal? (And what does it mean to be optimal?)
• What is the expected number of coin throws for n prisoners? Does this number converge to log(n), which is the entropy of the result?

If you know the anwers, let me know!

Related ideas

Brent Yorgey pointed me to a sequence of blog posts by Jeremy Gibbons, on “Arithmetic Coding”, which use a similar structure of dividing the unit intervals.

by Joachim Breitner (mail@joachim-breitner.de) at March 25, 2018 08:31 PM