Planet Haskell

August 28, 2018

Mark Jason Dominus

Yogi Bear and Ranger Smith

Yogi, accompanied by his constant companion Boo-Boo Bear, would often try to steal picnic baskets from campers in the park, much to the displeasure of Park Ranger Smith.

by Mark Dominus (mjd@plover.com) at August 28, 2018 08:25 PM

How quickly did dentists start trying to use X-rays?

I had dental x-rays today and I wondered how much time elapsed between the discovery of x-rays and their use by dentists.

About two weeks, it turns out. Roentgen's original publication was in late 1895. Dr. Otto Walkhoff made the first x-ray picture of teeth 14 days later. The exposure took 25 minutes.

Despite the long exposure time, dentists had already begun using x-rays in their practices in the next two years. Dr. William J. Morton presented the new technology to the New York Odontological Society in April 1896, and his dental radiography, depicting a molar with an artificial crown clearly visible, was published in a dental journal later that year.

Morton's subject had been a dried skull. The first dental x-ray of a living human in the United States was made by Charles Edmund Kells in April or May of 1896. In July at the annual meeting of the Southern Dental Association he presented a dental clinic in which he demonstrated the use of his x-ray equipment on live patients. The practice seems to have rapidly become routine.

The following story about Morton is not dental-related but I didn't want to leave it out:

In March 1896, strongman Eugene Sandow, considered the father of modern bodybuilding, turned to Morton in an effort to locate the source of a frustrating pain he was experiencing in his foot. Apparently Sandow had stepped on some broken glass, but even his personal physician could not specify the location of the glass in his foot. The potential for the x-ray must have seemed obvious, and Sandow reached out specifically to Morton to see if he could be of help. Morton was eager to oblige. He turned the x-rays on Sandow’s foot and located the shard of glass disturbing Sandow’s equanimity. A surgeon subsequently operated and removed the glass, and the story made national news.

(Daniel S. Goldberg, “The Early Days of the X-Ray”)

The first dental x-ray machine was manufactured in 1923 by Victor X-ray Company, which later became part of General Electric.

In preparing this article I was fortunate to have access to B. Martinez, In a New Light: Early X-Ray Technology in Dentistry, 1890–1955, Arizona State University, 2013.

by Mark Dominus (mjd@plover.com) at August 28, 2018 06:56 PM

Michael Snoyman

Kids Coding, Part 3
Eliezer asked me a few questions about programming yesterday, and I ended up demonstrating a little bit about pattern matching. He then had a lot of fun showing a friend of his how programming works. I may end up giving some lessons to some of my kids’ friends in the next few weeks, which should be interesting.

Kids IDE

I’ve started using a minimalistic “kids IDE” I threw together for teaching the kids. It’s helped us not worry about details like filepaths, saving, and running in a terminal. It’s not a great tool, but good enough. I’ve included links to better tools in the README, though this fits my needs for the moment.

https://github.com/snoyberg/kids-haskell-ide#readme

I’ve set up AppVeyor to upload Windows executables to S3:

https://s3.amazonaws.com/www.snoyman.com/kids-ide/bin/kids-ide.exe

You’ll also need to install Stack.

Pattern matching strings

This morning, Eliezer and Gavriella both had their next “official” lesson. I started over with that pattern matching demonstration. First, I showed them this example:
main = do
  sayNickname "Eliezer"
  sayNickname "Gavriella"
  sayNickname "Yakov"
  sayNickname "Lavi"

sayNickname realname =
  putStrLn (nickname realname)

nickname "Eliezer" = "Elie Belly"
nickname "Gavriella" = "Galla Galla"
nickname "Lavi" = "Fat baby"
nickname "Yakov" = "Koko"
They got the basic idea of this. (And I ended up introducing putStrLn around here as well, which they were fine with.) However, as I had them typing out some of this on their own, they ended up with a lot of trouble around capitalization, which was a good introduction to Haskell’s rules around that. We’ll see how in a bit.

Pattern matching ints

After establishing that we could pattern match on strings, I switched the code to this:
main = do
  sayNickname 1
  sayNickname 2
  sayNickname 3
  sayNickname 4

sayNickname realname =
  putStrLn (nickname realname)

nickname 1 = "Elie Belly"
nickname "Gavriella" = "Galla Galla"
nickname "Lavi" = "Fat baby"
nickname "Yakov" = "Koko"
And gave them the challenge to rewrite nickname so that the code worked, which wasn’t too much of a problem. The misordering of Lavi and Yakov between main and nickname did cause some confusion, and then helped them understand better how pattern matching works. (I didn’t intentionally put that in, it somehow slipped in while the kids were working on rewriting things.)

Type signatures

I asked them what the type of nickname was, and they said function (yay!). And then explained to them that you can tell Haskell explicitly what a thing’s type is, and typed this in:
nickname :: ? -> ?
The funny syntax didn’t give them too much trouble, and then we got to fill in the question marks. I asked them what the output of the function was, pointing at the string. I was surprised: they said the type was “nickname” or “name.” They accepted that it was a string, but they didn’t like that. (New theory: humans’ brains are naturally strongly typed.)

I then asked what the input was, and they said “number.” I hadn’t taught them about Int yet, and didn’t know about integers from math, so I told them that integer is a kind of number, and that in Haskell we call it Int. Filling in the type signature was fine.

I pointed out that some things (like Int and String) were upper case, and some were lower case. I pointed out that concrete things that “actually exist” (maybe not the best terminology) are capitalized. We know what an Int is, for example. Variables are things we don’t know yet, and those are lowercase. And finally, you can put whatever you want inside a string, but it has to match exactly. That seemed to click fairly well for them.

Enums

I pointed out that referring to the kids as numbers isn’t good. (He responded that I actually do call them 1, 2, 4, and 8 sometimes…) Anyway, I said that a better type for the nickname function would be to take a Child as input. He said “can we say Child = Int,” which was a great insight. I showed up that, yes, we can do type Child = Int, but that there’s a better way.

I introduced the idea that data defines a new datatype, and then showed them:
data Child
  = Eliezer
  | Gavriella
  | Yakov
  | Lavi
Gavriella asked “what are those lines?” and I explained they mean “or.” Therefore, a child is Eliezer, or Gavriella, or Yakov, or Lavi. They got this.

Exercise: fix the following program, uncommenting the lines in main.
main = do
  sayNickname Eliezer
  --sayNickname Gavriella
  --sayNickname Yakov
  --sayNickname Lavi

sayNickname realname =
  putStrLn (nickname realname)

data Child
  = Eliezer
  | Gavriella
  | Yakov
  | Lavi

nickname :: Child -> String
nickname Eliezer = "Elie Belly"
--nickname 2 = "Galla Galla"
--nickname 3 = "Fat baby"
--nickname 4 = "Koko"
Some caveats where they got stuck:

Using lower case lavi instead of Lavi. I got to explain how pattern matching a variable works, and “wildcards.” They got this, though still needed to be coached on it.

I’d been on the fence about including syntax highlighting in the kids IDE, but it turns out that the different colors of Eliezer and lavi helped Gavriella realize her mistake. Syntax highlighting is a good thing here.

I did ultimately have to give her a hint: “Lavi is BIG but you made him small.”

I started to try and define data Person = Kid Child | Adult Parent, but realized quickly it was too complicated for now and aborted.

Recursion

I did not teach this well, the children did not get the concepts correctly. However, they did understand the code as I wrote it.
main = print total

total = addUp 10

addUp 10 = 10 + addUp 9
addUp 9 = 9 + addUp 8
addUp 8 = 8 + addUp 7
addUp 7 = 7 + addUp 6
addUp 6 = 6 + addUp 5
addUp 5 = 5 + addUp 4
addUp 4 = 4 + addUp 3
addUp 3 = 3 + addUp 2
addUp 2 = 2 + addUp 1
addUp 1 = 1 + addUp 0
addUp 0 = 0
They really hated how repetitive typing that out was, which was exactly the goal. It was easy to convince them that this was stupid. I then changed total to addUp 11 and it broke. They understood why, and so we started working on something better.
main = print total

total = addUp 10

addUp 0 = 0
addUp x = x + addUp (x - 1)
I stepped through the executable of this, complete with pattern matching. Doing this a few times in the future is probably a good idea.

Eliezer asked what happens if we remove the addUp 0 = 0 case. We discussed it, he said it wouldn’t work, and said it would “keep going.” I told him it was called an infinite loop, and we got a stack overflow. Good insight.

Gavriella asked how long it took me to learn this stuff. I told her 12 years; after all, I only started learning Haskell in my twenties. It made them feel pretty good that they were learning this stuff earlier than I did.

I gave them an exercise to implement multTo instead of addUp. They didn’t understand this, or recursion, and I had to help them through the whole thing. Mea culpa completely.

Gavriella asked for another exercise:
main = do
  sayAge Eliezer
  sayAge Gavriella
  sayAge Yakov
  sayAge Lavi

data Child = ...

sayAge child = print (age child)

age ? = ?
She typed something like:
age ? = ?
Eliezer=10
I showed her that she needed:
age Eliezer = 10
And then she got the rest just fine, though with a few capitalization mistakes.
August 28, 2018 12:12 PM

August 27, 2018

Mark Jason Dominus

Linear mappings of projective space

[ Epistemic status: uninformed musings; anything and everything in here might be wrong or ill-conceived. ]

Suppose $V$ is some vector space, and let $V_n$ be the family of all $n$ -dimensional subspaces of $V$ . In particular $V_1$ is the family of all one-dimensional subspaces of $V$ . When $V$ is euclidean space, $V_1$ is the corresponding projective space.

if $L$ is a nonsingular linear mapping $V\to V$ , then $L$ induces a mapping $L_n$ from $V_n\to V_n$ . (It does not make sense to ask at this point if the induced mapping is linear because we do not have any obvious linear structure on the projective space. Or maybe there is but I have not heard of it.)

The eigenspaces of $V$ are precisely the fixed points of $L_n$ .

(Wrong! Any subspace generated by an $n$ -set of eigenvectors is a fixed point of $L_n$ . But such a subspace is not in general an eigenspace. (Note this includes the entire space as a special case.) The converse, however, does hold, since any eigenspace is generated by a subset of eigenvectors.)

Now it is an interesting and useful fact that for typical mappings, say from $\Bbb R\to\Bbb R$ , fixed points tend to be attractors or repellers. (For example, see this earlier article.) This is true of $L_1$ also. One-dimensional eigenspaces whose eigenvalues are larger than $1$ are attractors of $L_1$ , and those whose eigenvalues are smaller than $1$ are repellers, and this is one reason why the eigenspaces are important: if $L$ represents the evolution of state space, then vectors in $V$ will tend to evolve toward being eigenvectors.

So consider, say, the projective plane $\Bbb P^2$ , under the induced mapping of some linear operator on $\Bbb R^3$ . There will be (typically) three special points in $\Bbb P^2$ and other points will typically tend to gravitate towards one or more of these. Isn't this interesting? Is the three-dimensional situation more interesting than the two-dimensional one? What if a point attracts in one dimension and repels in the other? What can the orbits look like?

Or consider the Grassmanian space $Gr(2, \Bbb R^3)$ of all planes in $\Bbb R^3$ . Does a linear operator on $\Bbb R^3$ tend to drive points in $Gr(2, \Bbb R^3)$ toward three fixed points? (In general, I suppose $Gr(k, \Bbb R^n)$ will have $n\choose k$ fixed points, some of which might attract and some repel.) Is there any geometric intuition for this?

I have been wanting to think about Grassmanian spaces more for a long time now.

by Mark Dominus (mjd@plover.com) at August 27, 2018 02:23 PM

August 26, 2018

Sean Seefried

Gabriel Gonzalez's notes on Stack, Cabal and Nixpkgs

Gabriel Gonzalez recently tweeted about the history of Stack which I thought were worth recording for posterity here.

When stack was first introduced the killer features were:

declarative dependency specification (i.e. stack.yaml)

isolated project builds

cabal new-build was when cabal-install began to support the above two features (cabal.project being analogous to stack.yaml)Gabriel Gonzalez added,

Also, once Nixpkgs added Haskell support that also offered a third approach for isolated builds with declarative dependencies

The combination of cabal new-build + Nix’s Haskell integration is what caused stack to lose its competitive advantage on that front

A small advantage of stack was built-in support for using Stackage resolvers to select a working package set en masse

However, you could reuse that within a Cabal project by saving https://www.stackage.org/lts/cabal.config to your project

This compatibility was an intentional goal of @snoyberg

Stackage was probably the single best outcome of the stack project because it benefited all three of stack, cabal-install and Nixpkgs (which closely tracks the latest Stackage resolver, too)

Before Stackage getting a working build of, say, lens or yesod was a nightmare

by Sean Seefried at August 26, 2018 12:00 AM

August 25, 2018

Mark Jason Dominus

A software archaeology screwup
This week I switched from using the konsole terminal program to using gnome-terminal, because the former gets all sorts of font widths and heights wrong for high-bit characters like ⇒ and ③, making it very difficult to edit such text, and the latter, I discovered doesn't. Here's how it displays the text ☆☆★★★ “Good” as I move the cursor rightwards through it:

Uggggggh. Why did I put up with this bullshit for so long?

(I know, someone is going to write in and say the problem isn't in konsole, it's in the settings for the KooKooFont 3.7.1 package, and I can easily fix this by adding, removing, or adjusting the appropriate directives in /usr/share/config/fontk/config/fontulator-compat.d/04-spatulation, and… I don't care, gnome-terminal works and konsole doesn't.)

So I switched terminals, but this introduced a new problem: konsole would detect when a shell command had been run, and automatically retitle the tab it was run in, until the command exited. I didn't realize until this feature went away how much I had been depending on it to tell the tabs apart. Under gnome-terminal all the tabs just said Terminal.

Reaching back into my memory, to a time even before there were tabs, I recalled that there used to be a simple utility I could run on the command line to set a terminal title. I did remember xsetname, which sets the X window title, but I didn't want that in this case. I looked around through the manual and my bin directory and didn't find it, so I decided to write it fresh.

It's not hard. There's an escape sequence which, if received by the terminal, should cause it to retitle itself. If the terminal receives
    ESC ] 0 ; pyrzqxgl \cG
it will change its title to pyrzqxgl. (Spaces in the display above are for clarity only and should be ignored.)

It didn't take long to write the program:
#!/usr/bin/python3

from sys import argv, stderr

if len(argv) != 2:
    print("Usage: title 'new title'", file=stderr)
    exit(-2)

print("\033]0;{}\a".format(argv[1]), end="")
The only important part here is the last line. I named the program title, installed it in ~/bin, and began using it immediately.

A few minutes later I was looking for the tab that had an SSH session to the machine plover.com, and since the title was still Terminal, once I found it, I ran title plover, which worked. Then I stopped and frowned. I had not yet copied the program to Plover. What just happened?

Plover already had a ~/bin/title that I wrote no less than 14½ years ago:
   -rwxr-xr-x 1 mjd mjd 138 Feb 11  2004 /home/mjd/bin/title
Here it is:
#!/usr/bin/perl

my $title = join " ", @ARGV;
$title = qx{hostname -s || hostname} if $title eq "";
chomp $title;
print "\e]0;$title\cG";
Why didn't I find that before I wrote the other one?

The old program is better-written too. Instead of wasting code to print a usage message if I didn't use it right, I had spent that code in having it do something useful instead.

This is not the first time I have done something like this.

Oh well, at least I can reacquire the better UI now that I know about it.
by Mark Dominus (mjd@plover.com) at August 25, 2018 01:15 PM

August 24, 2018

Michael Snoyman

Kids Coding, Part 2
I didn’t expect to be writing the second blog post only 12 hours after the first. But when the kids came downstairs this morning, they were unbelievably excited to do more coding. So here we are!

Eliezer and I discussed using more visual tooling (like Code World or Jupiter) for doing the learning, and I showed him what it looked like. It seems he’s got quite a bit of his father’s preferences, and wanted to stick to plain text for now. We’ll probably circle back to that kind of stuff after they get the basics. It will also give me a chance to get more comfortable with those offerings. (Thanks all for the recommendations on Reddit.)

One final note. I’m extremely happy that we went with Haskell after today’s lessons. Concepts like variable replacement which are natural in Haskell were great teaching tools. I obviously don’t have enough data to prove this yet, but I’m more strongly believing the long-held theory that Haskell is easier for brand new programmers than those familiar with imperative programming.

Coding environment

I moved us over to VSCode, with only syntax highlighting set up. Previously, I’d used my emacs setup with intero, and the red squiggles let them know they’d messed up too early. I used the docked terminal at the bottom, taught them to save, and showed them to press “up enter” in the terminal to rerun stack runghc foo.hs. Perhaps not the ideal setup, but definitely good enough.

Variables
Started with main = print "hello world"

Explained that main is defined as other thing
Expanded to
main = print hello
hello = "hello world"
They were not surprised at all that this just worked

hello = 5 + 6, both got confused about whether it would print 11 or 5 + 6, reminded them of strings

How about hello = five + six?

Both agreed it wouldn’t work. I typed in five = 5, and ask if it would work. They agree that it won’t, and I show them GHC’s error message.

“Variable not in scope.” Computers talk funny, just means “I don’t know what six is.” Instilled that they’ll eventually be able to understand those massive error messages, but not to worry about it yet.

Exercise: five the program. Both of them got it no problem.

I was about to demonstrate five = 4, and then Gavriella figured it out for herself! They understand that, again, “computers are dumb.” Names are just there for our benefit, computer doesn’t care.

We do five + six * seven (with appropriate variable definitions), they get that answer, and then (five + six) * seven, they get that too.

Now I define fivePlusSix = five + six, and change to hello = (fivePlusSix) * seven (direct replacement). They’re fine with this. Yay replacement.

Point out that the parens are now unneeded and remove them. Again, no problem.

Parens just tell us “do this first”, not needed for one thing
Functions

Type in hello = 5 * 2, no problem.

How about hello = double 5? They figured out that it won’t work cuz computers be dumb

How do we define double? Eliezer guessed * 2, which is really close, but we’re not ready for sections, and I want to teach standard function stuff first.

Show them double x = x * 2, that x is a variable, and a function argument. They don’t know algebra yet, but got this fairly quickly.

hello = addFive (double 5)

Exercise: fix the program!

Eliezer did this one, defined addFive, and he started spacing things like me without any prompting. Cool.

Exercise: Gavriella, write minusTwo

Got it first time, ran it, answer’s still 15. Why?

We stepped through how the program is evaluated. “Let’s look at main, oh, I got an action! I need to print hello, what’s that? Oh, it’s addFive .... That means I gotta figure out .... What’s double 5? Oh, it’s 10. So that’s 15. And minusTwo was never (terminology break, I taught them that it wasn’t used).

Exercise: make the answer 13. They’re struggling to figure out where to use it. They’re stumped, time to jump in.

Stepped through all of the types involved. “double is a function that takes a number and gives you back a number” blah blah blah

minusTwo is also a function. It needs one number. Let’s try something wrong: minusTwo addFive (double 5). That’s wrong: it means “apply minusTwo to two values” but it only needs one number.

We need to turn addFive (double 5) into one thing. Ask them what we can use. They played with idea of double quotes, and then they figured out the parens! Awesome!

One final exercise: make the answer 16 with plus3

Eliezer did that typing, so I gave Gavriella one real final one: make the answer 6 with minusTen. She did it.

Realizing now: learning to type and navigate an editor is possibly harder for them than the coding itself

Bonus

Gavriella kept playing with the code (wow, she’s focused on this). She decided she wanted to do division. That was more complicated, but she persevered. I taught her about div being a function that takes 2 arguments. She didn’t know anything about remainders, and was confused that div 15 2 worked at all. I taught her about divMod, and she did great.
August 24, 2018 06:04 AM

August 23, 2018

FP Complete

Haskell Development Workflows (4 ways)

One fantastic aspect of Haskell is that it offers various tools that allow different development workflows. In this blog post, we are going to focus on four different workflows to develop Haskell. These are techniques that the FP Complete team themselves use regularly and we wanted to share them with our readers.

by Roman Gonzalez (roman@fpcomplete.com) at August 23, 2018 07:45 PM

Michael Snoyman

Kids Coding, Part 1
Kids Coding, Part 1

I’ve been wanting to give my eldest child (Eliezer, now 10) a chance to learn to code for about a year now, with little success. My second child (Gavriella, now 8) is also ready to start learning some coding. “Ready” to me means “they have a decent enough grasp of written English.” (Yakov, my 6 year old, also wants in, but unfortunately is going to have to wait a bit.)

I know how I learned to code: sitting at a DOS prompt since the age of 2 and reading a massive “Teach Yourself QBasic in 21 Days” book. For various reasons, this doesn’t seem to apply to the next generation. I’ve looked into other modern approaches, including the graphical programming environments. My kids enjoyed some of this, but this week told me that “it’s fun, but we’re not learning anything.”

Previously, I tried teaching Eliezer some Haskell by writing up lessons for him. Whether because of my writing or his interest, it didn’t work at the time. I decided to not go down this path again, and an hour ago sat down with Eliezer and Gavriella for their first lesson. I’m winging this completely, but here’s the approach I’m taking:

Keep the computer in front of me and show them things

See what confuses them, what interests them, and follow that

Give them one or two exercises at the end to reinforce the ideas

Keep the lessons short to keep their interest

Write up a blog post right afterward to record what happened, so I can learn for the future. After all, Yakov and Lavi (the baby, aka #YoungestHaskeller) need to learn too

This is the first of these summary blog posts. Caveats:

This will likely be incomplete

The material is very much geared towards my kids and probably won’t generalize

I have no idea how long or frequently I’ll be doing this.

I considered making these private notes for myself instead, but thought some others may be interested, so I’m posting publicly.

Without further ado!

Python portion

Previous experience with Haskell made Eliezer think it was too hard for him, so we decided to learn Python instead. He has some experience with that from Code Combat.

I started at the REPL and demonstrated printing strings. We made some typical jokes (yes, they were fart jokes) in text form, which made the kids giggle. Upshot: they learned about strings, and stayed interested.

I demonstrated that basic arithmetic works at the REPL.

I opened up a hello-world.py file and demonstrated you could write the same stuff from the REPL in a file.

This was the point where Eliezer commented that it looked a lot like the Haskell he’d seen. I’m not sure what it was, but somehow it clicked with him that whatever scared him off of Haskell previously wasn’t a real issue. We decided together to switch over to learning Haskell instead, which I’m quite happy about (more because I know the language better than anything else).

Haskell portion

Did the same print, string, and arithmetic stuff at the GHCi prompt and in a file

Asked them what 2 + 3 + 4 was, they got that

Asked them what 2 * 3 + 4 was, they got that too

Then 2 + 3 * 4, and I was surprised to find out that they knew about order of operations already. Yay school system.

They mentioned parentheses, and I told them that would be the same way to do things in programming, and showed them (2 + 3) * 4.

Next we talked about print 2 + 3. They had some inkling that this wouldn’t work, but couldn’t be sure of why.

I then branched into the next topics…

Types

Types are really important in Haskell programming

Everything has a “type” (this raised confusion and interest, as expected)

Explained that 2 is a number, that’s its type (yes, it’s a bit of a lie, Int, and defaulting to Integer, and Num a => a, blah blah blah, this is fine for first lesson)

Is 2 a string? No. Is 2 a dog? (giggles) No. Is 2 a missile? (Eliezer got to explain that concept to Gavriella.)

print 2 + 3 because of order of operations (just like math) really is (print 2) + 3, what does that mean?

What’s the type of print? Confusion

We’ve discussed functions a lot before, so pointed out that print is a function that takes a number (here) and returns something else. What is that something else?

I introduce the idea of actions. Eliezer got this, Gavriella was more confused. So more humor to explain this.

fart = print "Sorry, I farted" lots of giggling. What is the type of fart? Is it a number? No. Is it a dog? No. It’s something that you do, or the computer does. That’s what an action is. (Gavriella translated some words into Hebrew at that point, and the ideas clicked. Got to remember: they’re learning both programming languages and how to learn things in English at the same time.)

OK, you can add two numbers together. Does it make sense to add an action and a number together? No. So print 2 + 3 doesn’t make sense!

Now, what’s print? It’s a function that takes a number and gives you back an action. And that’s how you use functions in Haskell: just stick things next to each other.

They figured out really quickly at this point that they needed parens to fix the program, and ended up with print (2 + 3).

Today’s excercise

Note: Somewhere above, I briefly showed them that you could use do notation and put multiple print calls on different lines. No confusion from this at all. Relevant to the exercise:

Write a program that print “2 + 3 + 4”, first as a string, and then as a number.

I started them off with:
main = do
  | -- prompt started here
They both got the answer, one of them with a bit of help:
main = do
  print "2+3+4"
  print (2+3+4)
Things to note:

They naturally left off the spaces, despite me using the spaces throughout my typing.

They never questioned why print "Hello World" resulted in output that kept the double quotes. I’ll have to explain at some point about putStrLn, but that can come much, much later.

To figure out

How much shell do I teach them?

What editor will I set them up with?

Next lesson

I don’t want to plan out what to cover next time too intricately, because I want to experiment with them and bounce things around. I’m thinking about showing them how to create their own functions, maybe with lambda syntax, not sure.
August 23, 2018 05:55 PM

August 22, 2018

Philip Wadler

I'll be speaking at Lambdup 2018 in Prague

I'm looking forward to LambdUp, Prague, 13 September 2018. The programme is up! My keynote will be the talk below.
Categories for the Working Hacker
The talk will explain why category theory is of interest for developers, taking examples from Java and Haskell, and referencing the new blockchain scripting languages Simplicity, Michelson, and Plutus. The principle of Propositions as Types describes a correspondence between, on the one hand, propositions and proofs in logic, and, on the other, types and programs in computing. And, on the third hand, we have category theory! Assuming only high school maths, the talk will explain how categories model three basic data types: products (logical and), sums (logical or), and functions (logical implication). And it explains why you already learned the most important stuff in high school.

by Philip Wadler (noreply@blogger.com) at August 22, 2018 09:23 AM

August 20, 2018

Functional Jobs

Senior Software Engineer at Habito (Full-time)

Launched in 2016, Habito is transforming the mortgage industry through innovation and cutting-edge technology. We are the UK's free online mortgage broker backed by Atomico, Ribbit Capital and Mosaic Ventures, with angel investors including Transferwise CEO Taavet Hinrikus, Funding Circle’s founder Samir Desai and Yuri Milner, influential tech investor.

We are building a great brand synonymous with great customer service, ease and transparency. Simple, fast and honest, coupled with no fees, and no misinformation.

Our team is super-smart, ambitious, collaborative and friendly. We work hard, play hard and learn fast. This is a great opportunity to help steer, shape and mould our business.

Are you excited? Come and make your home at Habito!

The Role

We are looking for a full-time senior software engineer to join our team of full-stack engineers. Our core development values are strong, static typing and correctness, rigorous automation (in both testing and infrastructure) and everyone having a say.

The stack: On the back end we have an HTTP API written in Haskell (and built using stack) with PostgreSQL serving as the persistence layer. All of our data is event sourced thanks to PostgreSQL's great support for relational and blob data (e.g. jsonb) and some in-house libraries for handling ES/CQRS in a type-safe (or what we believe to be, as far as possible) manner. We lean heavily on GHC and its extensions and are also using some of the bigger power-to-weight-ratio players like lens and conduit.

The front end is written in PureScript on top of React and Redux (the bindings to which are our own but are both quite thin and based on the design of purescript-react and later pux).

Infrastructure wise we are sitting atop AWS and using Docker to manage containment. Jenkins manages continuous integration and deployment using a combination of AWS' Java SDK and some management code written in Scala

While we're a technology company first and foremost, initially we're trying to make the UK mortgage brokering market a better place. This means building and maintaining our website, but it also involves a slurry of behind-the-scenes work integrating lenders, insurers, conveyancers and all the other players in the space as we seek to introduce robust automation into what is currently so many manual processes. Slack bots, job queues, working around the fact that some actors don't have APIs -- you'll get to handle it all!

Work on our back-end software, written in Haskell and our front-end web applications, written in PureScript, HTML and CSS.

Help maintain and extend our infrastructure, hosted in AWS using technologies such as Docker and Kubernetes.

Use tools such as QuickCheck, Tasty and HUnit to produce reliable, well-tested software.

Work with our product and design teams to produce customer-centric experiences that excite and delight.

The Candidate

A passionate developer who cares about clean code and code quality; a full-stack polyglot

An experienced engineer familiar with automated testing and deployment

Experienced with functional programming and domain-driven design or simply interested and capable of learning on the job

Someone who cares about UX and UI; you have a fundamental aversion to ugliness in product

And Finally......

Competitive salary & share options

Career development, coaching & training

Free catered lunches, snacks & team bonding

Bupa Healthcare & Life Assurance

Contributory pension scheme

Bi-weekly massages with Urban Massage

Unlimited Holiday

Cycle to Work Scheme

Childcare Vouchers

Get information on how to apply for this position.

August 20, 2018 05:32 PM

August 19, 2018

Philip Wadler

Deacti-Day

I'm a bit late, but I find the arguments in this article compelling. Bye Twitter! I've enjoyed the people, but not the time wasted.

by Philip Wadler (noreply@blogger.com) at August 19, 2018 04:08 PM

Is the staggeringly profitable business of scientific publishing bad for science?

A long read in the Guardian by Stephen Buranyi.
It is an industry like no other, with profit margins to rival Google – and it was created by one of Britain’s most notorious tycoons: Robert Maxwell.
Spotted by Ross Anderson.

by Philip Wadler (noreply@blogger.com) at August 19, 2018 03:39 PM

August 18, 2018

Manuel M T Chakravarty

Learning Dutch

About six weeks ago, I moved from Sydney, Australia, to Utrecht in the Netherlands. Naturally, I started to learn Dutch.(*)

This post is mainly a summary of the things I found helpful so far. Apparently, the Netherlands is becoming an increasingly popular expat destination (cough Brexit cough), so this might be useful to some.

I quickly discovered that, even after living in an English-speaking country for many years, as a German native speaker, learning Dutch from the perspective of German is much easier than going via English (although, fluency in English obviously also helps). The first obstacle here is that it is a lot easier to find a good Dutch-English (electronic) dictionary than a Dutch-German one — for instance, my macOS and iOS devices already come with a Dutch-English dictionary that I can hook into the system look-up service with a click (or tap). The best Dutch-German dictionary that I could find so far is uitmuntend — thanks to Chris Eidhof for that very useful recommendation. Its creator also runs the super informative buurtaal forum.

As a starting point, I found the mondly app quite useful. It encourages a daily routine and quickly builds up a basic vocabulary and set of common expressions. It’s not cheap, but light years ahead of other iOS apps I checked out.

The next step for me was to make a habit out of trying to decipher Dutch websites and to refrain from clicking on the English language option. Whether that is the daily whether forecast, a news item, or the instructions for opening a bank account, it is a slow process, but there is no substitute for constant practice.

As a stepping stone, comic books (especially those for kids) are of course a great choice. (I would have never learnt Japanese without a huge stack of manga.)

To practice listening comprehsion and to get into more complex vocabulary and casual language, I really like to watch Zondag met Lubach — thanks to Gabi who got me to watch the show with her. The show is very entertaining, focused around one topic with recurring vocabluary, and you can get all past shows online. (On YouTube, to get started, you can also get English subtitles for many episodes and Dutch subtitles when you start to get the hang of it and to more easily look up words.)

And then, there is speaking. Unfortunately, I know of no better way than to repeatedly and publicly embarrass yourself to make progress here. People won’t understand you, you will say silly things, and you will fail to understand their response. Over and over again.

But it is all worth it for the moments of success. For instance, when you leave a shop for the first time without the Dutch shop assistant having felt the need to switch to English. Tot ziens!

(*) Everybody here switches to fluent English in a heartbeat when they realise that you don’t understand them, but to me, assuming residency in a country obliges me to learn the local language. (I have never been able to relate to that expat lifestyle, where you stay in that bubble of like-minded foreigners.)

August 18, 2018 11:18 PM

August 17, 2018

Gabriel Gonzalez

NixOS in production
<html lang="" xml:lang="" xmlns="http://www.w3.org/1999/xhtml"><head> <meta charset="utf-8"/> <meta content="pandoc" name="generator"/> <meta content="width=device-width, initial-scale=1.0, user-scalable=yes" name="viewport"/> nixos.prod <style type="text/css"> code{white-space: pre-wrap;} span.smallcaps{font-variant: small-caps;} span.underline{text-decoration: underline;} div.column{display: inline-block; vertical-align: top; width: 50%;} </style> <style type="text/css">a.sourceLine { display: inline-block; line-height: 1.25; } a.sourceLine { pointer-events: none; color: inherit; text-decoration: inherit; } a.sourceLine:empty { height: 1.2em; position: absolute; } .sourceCode { overflow: visible; } code.sourceCode { white-space: pre; position: relative; } div.sourceCode { margin: 1em 0; } pre.sourceCode { margin: 0; } @media screen { div.sourceCode { overflow: auto; } } @media print { code.sourceCode { white-space: pre-wrap; } a.sourceLine { text-indent: -1em; padding-left: 1em; } } pre.numberSource a.sourceLine { position: relative; } pre.numberSource a.sourceLine:empty { position: absolute; } pre.numberSource a.sourceLine::before { content: attr(data-line-number); position: absolute; left: -5em; text-align: right; vertical-align: baseline; border: none; pointer-events: all; -webkit-touch-callout: none; -webkit-user-select: none; -khtml-user-select: none; -moz-user-select: none; -ms-user-select: none; user-select: none; padding: 0 4px; width: 4em; color: #aaaaaa; } pre.numberSource { margin-left: 3em; border-left: 1px solid #aaaaaa; padding-left: 4px; } div.sourceCode { } @media screen { a.sourceLine::before { text-decoration: underline; } } code span.al { color: #ff0000; font-weight: bold; } /* Alert */ code span.an { color: #60a0b0; font-weight: bold; font-style: italic; } /* Annotation */ code span.at { color: #7d9029; } /* Attribute */ code span.bn { color: #40a070; } /* BaseN */ code span.bu { } /* BuiltIn */ code span.cf { color: #007020; font-weight: bold; } /* ControlFlow */ code span.ch { color: #4070a0; } /* Char */ code span.cn { color: #880000; } /* Constant */ code span.co { color: #60a0b0; font-style: italic; } /* Comment */ code span.cv { color: #60a0b0; font-weight: bold; font-style: italic; } /* CommentVar */ code span.do { color: #ba2121; font-style: italic; } /* Documentation */ code span.dt { color: #902000; } /* DataType */ code span.dv { color: #40a070; } /* DecVal */ code span.er { color: #ff0000; font-weight: bold; } /* Error */ code span.ex { } /* Extension */ code span.fl { color: #40a070; } /* Float */ code span.fu { color: #06287e; } /* Function */ code span.im { } /* Import */ code span.in { color: #60a0b0; font-weight: bold; font-style: italic; } /* Information */ code span.kw { color: #007020; font-weight: bold; } /* Keyword */ code span.op { color: #666666; } /* Operator */ code span.ot { color: #007020; } /* Other */ code span.pp { color: #bc7a00; } /* Preprocessor */ code span.sc { color: #4070a0; } /* SpecialChar */ code span.ss { color: #bb6688; } /* SpecialString */ code span.st { color: #4070a0; } /* String */ code span.va { color: #19177c; } /* Variable */ code span.vs { color: #4070a0; } /* VerbatimString */ code span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */ </style> </head><body>
This is a short post summarizing what I wish I had known when I first started using NixOS in production. Hopefully other people will find this helpful to avoid the pitfalls that I ran into.
The main issue with NixOS is that the manual recommends a workflow that is not suitable for deployment to production. Specifically, the manual encourages you to:
keep Nix source code on the destination machine
i.e. /etc/nixos/{hardware-,}configuration.nix
build on the destination machine
use Nix’s channel system to obtain nixpkgs code
This post will describe how you can instead:
build a source-free binary closure on a build machine
transfer and deploy that binary closure to a separate destination machine
This guide overlaps substantially with what the NixOps tool does and you can think of this guide as a way to transplant a limited subset of what NixOps does to work with other provisioning tools (such as Terraform).
You might also find this guide useful even when using NixOS as a desktop operating system for handling more exotic scenarios not covered by the nixos-rebuild command-line tool.
Building the closure
We’ll build up to the final solution by slowly changing the workflow recommended in the NixOS manual.
Suppose that you already have an /etc/nixos/configuration.nix file and you use nixos-rebuild switch to deploy your system. You can wean yourself off of nixos-rebuild by building the binary closure for the system yourself. In other words, you can reimplement the nixos-rebuild build command from scratch.
To do so, create the following file anywhere on your system:
# ./nixos.nix

import <nixpkgs/nixos> {
 system = "x86_64-linux";

 configuration = {
 imports = [
 /etc/nixos/configuration.nix
 ];
 };
}
Then run:
$ nix-build --attr system ./nixos.nix
Congratulations, you’ve just built a binary closure for your system!
Deploying the closure
nix-build deposits a result symlink in the current directory pointing to the built binary closure. To deploy the current system to match the built closure, run:
$ sudo ./result/bin/switch-to-configuration switch
Congratulations, you’ve just done the equivalent of nixos-rebuild switch!
As the above command suggests, the closure contains a ./bin/switch-to-configuration which understands a subset of the commands that the nixos-rebuild command does. In particular, the switch-to-configuration script accepts these commands:
$ ./result/bin/switch-to-configuration --help
Usage: ../../result/bin/switch-to-configuration [switch|boot|test]

switch: make the configuration the boot default and activate now
boot: make the configuration the boot default
test: activate the configuration, but don't make it the boot default
dry-activate: show what would be done if this configuration were activated
Adding a profile
The nixos-rebuild command actually does one more thing in addition to buiding the binary closure and deploying the system. The nixos-rebuild command also creates a symlink pointing to the current system configuration so that you can roll back to that configuration later. The symlink also acts like a garbage collection root, preventing the system from being garbage collected until you remove the symlink (either directly using rm or a higher-level utility such as nix-collect-garbage)
You can record the system configuration in the same way as nixos-rebuild using the nix-env command:
$ nix-env --profile /nix/var/nix/profiles/system --set ./result
Querying system options
You can use the same nixos.nix file to query what options you’ve set for your system, just like the nixos-option utility. For example, if you want to compute the final value of the networking.firewall.allowedTCPPorts option then you run this command:
$ nix-instantiate --eval --strict --attr config.networking.firewall.allowedTCPPorts nixos.nix
[ 22 ]
Pinning nixpkgs
Now that you’ve taken control of the build you can do fancier things like pin nixpkgs to a specific revision of nixpkgs so that you don’t need to use a channels or the NIX_PATH any longer:
let
 nixpkgs = builtins.fetchTarball {
 url = "https://github.com/NixOS/nixpkgs/archive/b74b1cdb2fecc31ff7a127c5bc89771f887c93bb.tar.gz";
 sha256 = "0ncr4g29220amqm4riaa1xf4jz55v2nmh9fi16f1gzhww1gplk8h";
 };

in
 import "${nixpkgs}/nixos" {
 configuration = {
 imports = [
 /etc/nixos/configuration.nix
 ];
 };

 system = "x86_64-linux";
 }
In fact, this makes your build completely insensitive to the NIX_PATH, eliminating a potential source of non-determinism from the build.
Building remotely
Now that you’ve removed nixos-rebuild from the equation you can build the binary closure on a separate machine from the one that you deploy to. You can check your nixos.nix, configuration.nix and hardware-configuration.nix files into version control and nix-build the system on any machine that can check out your version controlled Nix configuration. All you have to do is change the import path to be a relative path to the configuration.nix file within the same repository instead of an absolute path:
# ./nixos.nix

let
 nixpkgs = builtins.fetchTarball {
 url = "https://github.com/NixOS/nixpkgs/archive/b74b1cdb2fecc31ff7a127c5bc89771f887c93bb.tar.gz";
 sha256 = "0ncr4g29220amqm4riaa1xf4jz55v2nmh9fi16f1gzhww1gplk8h";
 };

in
 import "${nixpkgs}/nixos" {
 configuration = {
 imports = [
 ./relative/path/to/configuration.nix
 ];
 };

 system = "x86_64-linux";
 }
Then all your build machine has to do is:
$ git clone "git@github.com:${OWNER}/${REPOSITORY}.git"
$ nix-build --attr system "./${REPOSITORY}/path/to/nixos.nix"
To deploy the built binary closure to another machine, use nix copy. If you have SSH access to the destination machine then you can nix copy directly to that machine:
$ nix copy --to "${USER}@${MACHINE}" ./result
If you do not have SSH access to the destination machine you can instead use nix-copy to create a binary archive file containing the binary closure of your system:
$ # On the build machine
$ nix copy --to 'file:///tmp/system' ./result
… and upload the binary archive located at /tmp/system to the destination machine using your upload method of choice. Then import the binary archive into the /nix/store on the destination machine using nix copy:
$ # On the destination machine
$ nix copy --from 'file:///tmp/system' ./result
Once the binary closure is on the machine, you install the closure the same way as before:
$ sudo /nix/store/.../bin/switch-to-configuration switch
… replacing /nix/store/... with the /nix/store path of your closure (since there is no result symlink on the destination machine).
Conclusion
That’s it! Now you should be able to store your NixOS configuration in version control, build a binary closure as part of continuous integration, and deploy that binary closure to a separate destination machine. You can also now pin your build to a specific revision of Nixpkgs so that your build is more deterministic.
I wanted to credit my teammate Parnell Springmeyer who taught me the ./result/bin/switch-to-configuration trick for deploying a NixOS system and who codified the trick into the nix-deploy command-line tool. I also wanted to credit Remy Goldschmidt who interned on our team over the previous summer and taught me how to reliably pin Nixpkgs.
</body></html>
by Gabriel Gonzalez (noreply@blogger.com) at August 17, 2018 02:01 AM

August 15, 2018

Functional Jobs

Haskell : Backend & Web App Developer at Tripshot (Full-time)

Hello,

I'm Wayne Lewis, Director of Engineering at Tripshot. Let me introduce you to our company and engineering team.

Tripshot was formed in 2014 with a mission to "optimize the commute". After observing the challenges large employers face getting their employees to and from work in crowded metro areas, we asked ourselves how we can help. With our backgrounds covering software product development, large-scale SAAS deployments, and selling and supporting large enterprises, we set upon our present course to deliver the best solution to this problem.

Coming off recent sales wins, we're excited to announce that we're expanding the engineering team.

But before diving into what we're looking for, its fair to explain what our team is all about. Tripshot engineering culture emphasizes:

Meritocracy. Good ideas come from everywhere, and we encourage healthy discussion and debate on the team.

Focus on the important stuff. No bikeshedding. Differentiate the business by tackling the difficult problems. Transportation is ripe with meaty problems in need of well engineered solutions.

Ownership. Find people with the skills, experience, and maturity to own a problem but know when they need to ask for help - then let them loose. Tripshot is a fully distributed company, and since everyone works from home we rely on people who can own problems, and deliver solutions.

Not all tech is created equal. We love static typing, and our tech stack reflects that fact. Backend services are all written in Haskell. Writing Haskell is sheer joy and highly productive. All web applications are developed in GWT, in our opinion the most mature of the "static language to javascript" compilers.

The next addition to the Tripshot engineering team will help with both the backend and web apps. Most of our new features require changes to both in roughly 75/25 proportion, but varies depending on the task.

Requirements:

Haskell experience is an absolute requirement. Personal projects are fine if they can be shared with us.

Java experience preferred. Its not necessary to have worked with GWT before, but that would be a bonus.

Highly motivated individual with excellent personal time management skills. You will be working from home.

Excellent analytical skills. Our roadmap is full of interesting problems requiring non-trivial algorithm design.

Must be eligible to work in the US.

Tripshot is committed to equal employment opportunity without regard for race, color, national origin, ethnicity, gender, protected veteran status, disability, sexual orientation, gender identity, or religion.

Get information on how to apply for this position.

August 15, 2018 08:43 PM

August 14, 2018

Jeremy Gibbons

Folds on lists

The previous post turned out to be rather complicated. In this one, I return to much simpler matters: ${\mathit{foldr}}$ and ${\mathit{foldl}}$ on lists, and list homomorphisms with an associative binary operator. For simplicity, I’m only going to be discussing finite lists.

Fold right

Recall that ${\mathit{foldr}}$ is defined as follows:

$\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldr} :: (\alpha \rightarrow \beta \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldr}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldr}\;(\oplus)\;e\;(a:x) & = a \oplus \mathit{foldr}\;(\oplus)\;e\;x \end{array}$

It satisfies the following universal property, which gives necessary and sufficient conditions for a function ${h}$ to be expressible as a ${\mathit{foldr}}$ :

$\displaystyle \begin{array}{@{}l} h = \mathit{foldr}\;(\oplus)\;e \quad\Longleftrightarrow\quad h\;[\,] = e \;\land\; h\;(a:x) = a \oplus (h\;x) \end{array}$

As one consequence of the universal property, we get a fusion theorem, which states sufficient conditions for fusing a following function ${g}$ into a ${\mathit{foldr}}$ :

$\displaystyle \begin{array}{@{}l} g \cdot \mathit{foldr}\;(\oplus)\;e = \mathit{foldr}\; (\otimes)\;e' \quad \Longleftarrow\quad g\;e = e' \;\land\; g\;(a \oplus b) = a \otimes g\;b \end{array}$

(on finite lists—infinite lists require an additional strictness condition). Fusion is an equivalence if ${\mathit{foldr}\;(\oplus)\;e}$ is surjective. If ${\mathit{foldr}\;(\oplus)\;e}$ is not surjective, it’s an equivalence on the range of that fold: the left-hand side implies

$\displaystyle g\;(a \oplus b) = a \otimes g\;b$

only for ${b}$ of the form ${\mathit{foldr}\;(\oplus)\;e\;x}$ for some ${x}$ , not for all ${b}$ .

As a second consequence of the universal property (or alternatively, as a consequence of the free theorem of the type of ${\mathit{foldr}}$ ), we have map–fold fusion:

$\displaystyle \mathit{foldr}\;(\oplus)\;e \cdot \mathit{map}\;g = \mathit{foldr}\;((\oplus) \cdot g)\;e$

The code golf “ ${((\oplus) \cdot g)}$ ” is a concise if opaque way of writing the binary operator pointfree: ${((\oplus) \cdot g)\;a\;b = g\;a \oplus b}$ .

Fold left

Similarly, ${\mathit{foldl}}$ is defined as follows:

$\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{foldl} :: (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{foldl}\;(\oplus)\;e\;[\,] & = e \\ \mathit{foldl}\;(\oplus)\;e\;(a:x) & = \mathit{foldl}\;(\oplus)\;(e \oplus a)\;x \end{array}$

( ${\mathit{foldl}}$ is tail recursive, so it is unproductive on an infinite list.)

${\mathit{foldl}}$ also enjoys a universal property, although it’s not so well known as that for ${\mathit{foldr}}$ . Because of the varying accumulating parameter ${e}$ , the universal property entails abstracting that argument on the left in favour of a universal quantification on the right:

$\displaystyle \begin{array}{@{}l} h = \mathit{foldl}\;(\oplus) \quad\Longleftrightarrow\quad \forall b \;.\; h\;b\;[\,] = b \;\land\; h\;b\;(a:x) = h\;(b \oplus a)\;x \end{array}$

(For the proof, see Exercise 16 in my paper with Richard Bird on arithmetic coding.)

From the universal property, it is straightforward to prove a map– ${\mathit{foldl}}$ fusion theorem:

$\displaystyle \mathit{foldl}\;(\oplus)\;e \cdot \mathit{map}\;f = \mathit{foldl}\;((\cdot f) \cdot (\oplus))\;e$

Note that ${((\cdot f) \cdot (\oplus))\;b\;a = b \oplus f\;a}$ . There is also a fusion theorem:

$\displaystyle (\forall e \;.\; f \cdot \mathit{foldl}\;(\oplus)\;e = \mathit{foldl}\;(\otimes)\;(f\;e)) \quad\Longleftarrow\quad f\;(b \oplus a) = f\;b \otimes a$

This is easy to prove by induction. (I would expect it also to be a consequence of the universal property, but I don’t see how to make that go through.)

Duality theorems

Of course, ${\mathit{foldr}}$ and ${\mathit{foldl}}$ are closely related. §3.5.1 of Bird and Wadler’s classic text presents a First Duality Theorem:

$\displaystyle \mathit{foldr}\;(\oplus)\;e\;x = \mathit{foldl}\;(\oplus)\;e\;x$

when ${\oplus}$ is associative with neutral element ${e}$ ; a more general Second Duality Theorem:

$\displaystyle \mathit{foldr}\;(\oplus)\;e\;x = \mathit{foldl}\;(\otimes)\;e\;x$

when ${\oplus}$ associates with ${\otimes}$ (that is, ${a \oplus (b \otimes c) = (a \oplus b) \otimes c}$ ) and ${a \oplus e = e \otimes a}$ (for all ${a,b,c}$ , but fixed ${e}$ ); and a Third Duality Theorem:

$\displaystyle \mathit{foldr}\;(\oplus)\;e\;x = \mathit{foldl}\;(\mathit{flip}\;f)\;e\;(\mathit{reverse}\;x)$

(again, all three only for finite ${x}$ ).

The First Duality Theorem is a specialization of the Second, when ${{\oplus} = {\otimes}}$ (but curiously, also a slight strengthening: apparently all we require is that ${a \oplus e = e \oplus a}$ , not that both equal ${a}$ ; for example, we still have ${\mathit{foldr}\;(+)\;1 = \mathit{foldl}\;(+)\;1}$ , even though ${1}$ is not the neutral element for ${+}$ ).

Characterization

“When is a function a fold?” Evidently, if function ${h}$ on lists is injective, then it can be written as a ${\mathit{foldr}}$ : in that case (at least, classically speaking), ${h}$ has a post-inverse—a function ${g}$ such that ${g \cdot h = \mathit{id}}$ —so:

$\displaystyle \begin{array}{@{}ll} & h\;(a:x) \\ = & \qquad \{ g \cdot h = \mathit{id} \} \\ & h\;(a : g\;(h\;x)) \\ = & \qquad \{ \mbox{let } a \oplus b = h\;(a : g\;b) \} \\ & a \oplus h\;x \end{array}$

and so, letting ${e = h\;[\,]}$ , we have

$\displaystyle h = \mathit{foldr}\;(\oplus)\;e$

But also evidently, injectivity is not necessary for a function to be a fold; after all, ${\mathit{sum}}$ is a fold, but not the least bit injective. Is there a simple condition that is both sufficient and necessary for a function to be a fold? There is! The condition is that lists equivalent under ${h}$ remain equivalent when extended by an element:

$\displaystyle h\;x = h\;x' \quad\Longrightarrow\quad h\;(a:x) = h\;(a:x')$

We say that ${h}$ is leftwards. (The kernel ${\mathrm{ker}\;h}$ of a function ${h}$ is a relation on its domain, namely the set of pairs ${(x,x')}$ such that ${h\;x = h\;x'}$ ; this condition is equivalent to ${\mathrm{ker}\;h \subseteq \mathrm{ker}\;(h \cdot (a:))}$ for every ${a}$ .) Clearly, leftwardsness is necessary: if ${h = \mathit{foldr}\;(\oplus)\;e}$ and ${h\;x = h\;x'}$ , then

$\displaystyle \begin{array}{@{}ll} & h\;(a:x) \\ = & \qquad \{ h \mbox{ as } \mathit{foldr} \} \\ & a \oplus h\;x \\ = & \qquad \{ \mbox{assumption} \} \\ & a \oplus h\;x' \\ = & \qquad \{ h \mbox{ as } \mathit{foldr} \mbox{ again} \} \\ & h\;(a:x') \end{array}$

Moreover, leftwardsness is sufficient. For, suppose that ${h}$ is leftwards; then pick a function ${g}$ such that, when ${b}$ is in the range of ${h}$ , we get ${g\;b = x}$ for some ${x}$ such that ${h\;x = b}$ (and it doesn’t matter what value ${g}$ returns for ${b}$ outside the range of ${h}$ ), and then define

$\displaystyle a \oplus b = h\;(a : g\;b)$

This is a proper definition of ${\oplus}$ , on account of leftwardsness, in the sense that it doesn’t matter which value ${x}$ we pick for ${g\;b}$ , as long as indeed ${h\;x = b}$ : any other value ${x'}$ that also satisfies ${h\;x' = b}$ entails the same outcome ${h\;(a:x') = h\;(a:x)}$ for ${a \oplus b}$ . Intuitively, it is not necessary to completely invert ${h}$ (as we did in the injective case), provided that ${h}$ preserves enough distinctions. For example, for ${h = \mathit{sum}}$ (for which indeed ${\mathit{sum}\;x = \mathit{sum}\;x'}$ implies ${\mathit{sum}\;(a:x) = \mathit{sum}\;(a:x')}$ ), we could pick ${g\;b = [b]}$ . In particular, ${h\;x}$ is obviously in the range of ${h}$ ; then ${g\;(h\;x)}$ is chosen to be some ${x'}$ such that ${h\;x' = h\;x}$ , and so by construction ${h\;(g\;(h\;x)) = h\;x}$ —in other words, ${g}$ acts as a kind of partial inverse of ${h}$ . So we get:

$\displaystyle \begin{array}{@{}ll} & a \oplus h\;x \\ = & \qquad \{ \mbox{definition of } \oplus \mbox{; let } x' = g\;(h\;x) \} \\ & h\;(a : x') \\ = & \qquad \{ h\;x' = h\;x \mbox{; assumption} \} \\ & h\;(a:x) \\ \end{array}$

and therefore ${h = \mathit{foldr}\;(\oplus)\;e}$ where ${e = h\;[\,]}$ .

Monoids and list homomorphisms

A list homomorphism is a fold after a map in a monoid. That is, define

$\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{hom} :: (\beta\rightarrow\beta\rightarrow\beta) \rightarrow (\alpha\rightarrow\beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow \beta} \\ \mathit{hom}\;(\odot)\;f\;e\;[\,] & = e \\ \mathit{hom}\;(\odot)\;f\;e\;[a] & = f\;a \\ \mathit{hom}\;(\odot)\;f\;e\;(x \mathbin{{+}\!\!\!{+}} y) & = \mathit{hom}\;(\odot)\;f\;e\;x \;\odot\; \mathit{hom}\;(\odot)\;f\;e\;y \end{array}$

provided that ${\odot}$ and ${e}$ form a monoid. (One may verify that this condition is sufficient for the equations to completely define the function; moreover, they are almost necessary— ${\odot}$ and ${e}$ should form a monoid on the range of ${\mathit{hom}\;(\odot)\;f\;e}$ .) The Haskell library ${\mathit{Data.Foldable}}$ defines an analogous method, whose list instance is

$\displaystyle \mathit{foldMap} :: \mathit{Monoid}\;\beta \Rightarrow (\alpha \rightarrow \beta) \rightarrow [\alpha] \rightarrow \beta$

—the binary operator ${\odot}$ and initial value ${e}$ are determined implicitly by the ${\mathit{Monoid}}$ instance rather than being passed explicitly.

Richard Bird’s Introduction to the Theory of Lists states implicitly what might be called the First Homomorphism Theorem, that any homomorphism consists of a reduction after a map (in fact, a consequence of the free theorem of the type of ${\mathit{hom}}$ ):

$\displaystyle \mathit{hom}\;(\odot)\;f\;e = \mathit{hom}\;(\odot)\;\mathit{id}\;e \cdot \mathit{map}\;f$

Explicitly as Lemma 4 (“Specialization”) the same paper states a Second Homomorphism Theorem, that any homomorphism can be evaluated right-to-left or left-to-right, among other orders:

$\displaystyle \mathit{hom}\;(\odot)\;f\;e = \mathit{foldr}\;(\lambda\;a\;b \;.\; f\;a \odot b)\;e = \mathit{foldl}\;(\lambda\;b\;a \;.\; b \odot f\;a)\;e$

I wrote up the Third Homomorphism Theorem, which is the converse of the Second Homomorphism Theorem: any function that can be written both as a ${\mathit{foldr}}$ and as a ${\mathit{foldl}}$ is a homomorphism. I learned this theorem from David Skillicorn, but it was conjectured earlier by Richard Bird and proved by Lambert Meertens during a train journey in the Netherlands—as the story goes, Lambert returned from a bathroom break with the idea for the proof. Formally, for given ${h}$ , if there exists ${\oplus, \otimes, e}$ such that

$\displaystyle h = \mathit{foldr}\;(\oplus)\;e = \mathit{foldl}\;(\otimes)\;e$

then there also exists ${f}$ and associative ${\odot}$ such that

$\displaystyle h = \mathit{hom}\;(\odot)\;f\;e$

Recall that ${h}$ is “leftwards” if

$\displaystyle h\;x = h\;x' \Longrightarrow h\;(a:x) = h\;(a:x')$

and that the leftwards functions are precisely the ${\mathit{foldr}}$ s. Dually, ${h}$ is rightwards if

$\displaystyle h\;x = h\;x' \Longrightarrow h\;(x \mathbin{{+}\!\!\!{+}} [a]) = h\;(x' \mathbin{{+}\!\!\!{+}} [a])$

and (as one can show) the rightwards functions are precisely the ${\mathit{foldl}}$ s. So the Specialization Theorem states that every homomorphism is both leftwards and rightwards, and the Third Homomorphism Theorem states that every function that is both leftwards and rightwards is necessarily a homomorphism. To prove the latter, suppose that ${h}$ is both leftwards and rightwards; then pick a function ${g}$ such that, for ${b}$ in the range of ${h}$ , we get ${g\;b = x}$ for some ${x}$ such that ${h\;x = b}$ , and then define

$\displaystyle b \odot c = h\;(g\;b \mathbin{{+}\!\!\!{+}} g\;c)$

As before, this is a proper definition of ${\odot}$ : assuming leftwardsness and rightwardsness, the result does not depend on the representatives chosen for ${g}$ . By construction, ${g}$ again satisfies ${h\;(g\;(h\;x)) = h\;x}$ for any ${x}$ , and so we have:

$\displaystyle \begin{array}{@{}ll} & h\;x \odot h\;y \\ = & \qquad \{ \mbox{definition of } \odot \} \\ & h\;(g\;(h\;x) \mathbin{{+}\!\!\!{+}} g\;(h\;y)) \\ = & \qquad \{ h \mbox{ is rightwards; } h\;(g\;(h\;x)) = h\;x \} \\ & h\;(x \mathbin{{+}\!\!\!{+}} g\;(h\;y)) \\ = & \qquad \{ h \mbox{ is leftwards; } h\;(g\;(h\;y)) = h\;y \} \\ & h\;(x \mathbin{{+}\!\!\!{+}} y) \end{array}$

Moreover, one can show that ${\odot}$ is associative, and ${e}$ its neutral element (at least on the range of ${h}$ ).

For example, sorting a list can obviously be done as a ${\mathit{foldr}}$ , using insertion sort; by the Third Duality Theorem, it can therefore also be done as a ${\mathit{foldl}}$ on the reverse of the list; and because the order of the input is irrelevant, the reverse can be omitted. The Third Homomorphism Theorem then implies that there exists an associative binary operator ${\odot}$ such that ${\mathit{sort}\;(x \mathbin{{+}\!\!\!{+}} y) = \mathit{sort}\;x \odot \mathit{sort}\;y}$ . It also gives a specification of ${\odot}$ , given a suitable partial inverse ${g}$ of ${\mathit{sort}}$ —in this case, ${g = \mathit{id}}$ suffices, because ${\mathit{sort}}$ is idempotent. The only characterization of ${\odot}$ arising directly from the proof involves repeatedly inserting the elements of one argument into the other, which does not exploit sortedness of the first argument. But from this inefficient characterization, one may derive the more efficient implementation that merges two sorted sequences, and hence obtain merge sort overall.

The Trick

Here is another relationship between the directed folds ( ${\mathit{foldr}}$ and ${\mathit{foldl}}$ ) and list homomorphisms—any directed fold can be implemented as a homomorphism, followed by a final function application to a starting value:

$\displaystyle \mathit{foldr}\;(\oplus)\;e\;x = \mathit{hom}\;(\cdot)\;(\oplus)\;\mathit{id}\;x\;e$

Roughly speaking, this is because application and composition are related:

$\displaystyle a \oplus (b \oplus (c \oplus e)) = (a\oplus) \mathbin{\$} (b\oplus) \mathbin{\$} (c\oplus) \mathbin{\$} e = ((a\oplus) \cdot (b\oplus) \cdot (c\oplus))\;e$

(here, ${\$ }$ is right-associating, loose-binding function application). To be more precise:

$\displaystyle \begin{array}{@{}ll} & \mathit{foldr}\;(\oplus)\;e \\ = & \qquad \{ \mbox{map-fold fusion: } (\$)\;(a\oplus)\;b = a \oplus b \} \\ & \mathit{foldr}\;(\$)\;e \cdot \mathit{map}\;(\oplus) \\ = & \qquad \{ \mbox{fusion: } (\$ e)\;\mathit{id} = e \mbox{ and } (\$ e)\;((\oplus) \cdot f) = (\oplus)\;(f\;e) = (\$)\;(\oplus)\;((\$ e)\;f) \} \\ & (\$ e) \cdot \mathit{foldr}\;(\cdot)\;\mathit{id} \cdot \mathit{map}\;(\oplus) \\ = & \qquad \{ (\cdot) \mbox{ and } \mathit{id} \mbox{ form a monoid} \} \\ & (\$ e) \cdot \mathit{hom}\;(\cdot)\;(\oplus)\;\mathit{id} \end{array}$

This result has many applications. For example, it’s the essence of parallel recognizers for regular languages. Language recognition looks at first like an inherently sequential process; a recognizer over an alphabet ${\Sigma}$ can be represented as a finite state machine over states ${S}$ , with a state transition function of type ${S \times \Sigma \rightarrow S}$ , and such a function is clearly not associative. But by mapping this function over the sequence of symbols, we get a sequence of ${S \rightarrow S}$ functions, which should be subject to composition. Composition is of course associative, so can be computed in parallel, in ${\mathrm{log}\;n}$ steps on ${n}$ processors. Better yet, each such ${S \rightarrow S}$ function can be represented as an array (since ${S}$ is finite), and the composition of any number of such functions takes a fixed amount of space to represent, and a fixed amount of time to apply, so the ${\mathrm{log}\;n}$ steps take ${\mathrm{log}\;n}$ time.

Similarly for carry-lookahead addition circuits. Binary addition of two ${n}$ -bit numbers with an initial carry-in proceeds from right to left, adding bit by bit and taking care of carries, producing an ${n}$ -bit result and a carry-out; this too appears inherently sequential. But there aren’t many options for the pair of input bits at a particular position: two ${1}$ s will always generate an outgoing carry, two ${0}$ s will always kill an incoming carry, and a ${1}$ and ${0}$ in either order will propagate an incoming carry to an outgoing one. Whether there is a carry-in at a particular bit position is computed by a ${\mathit{foldr}}$ of the bits to the right of that position, zipped together, starting from the initial carry-in, using the binary operator ${\oplus}$ defined by

$\displaystyle \begin{array}{@{}ll} (1,1) \oplus b & = 1 \\ (0,0) \oplus b & = 0 \\ (x,y) \oplus b & = b \end{array}$

Again, applying ${\oplus}$ to a bit-pair makes a bit-to-bit function; these functions are to be composed, and function composition is associative. Better, such functions have small finite representations as arrays (indeed, we need a domain of only three elements, ${G, K, P}$ ; ${G}$ and ${K}$ are both left zeroes of composition, and ${P}$ is neutral). Better still, we can compute the carry-in at all positions using a ${\mathit{scanr}}$ , which for an associative binary operator can also be performed in parallel in ${\mathrm{log}\;n}$ steps on ${n}$ processors.

The Trick seems to be related to Cayley’s Theorem, on monoids rather than groups: any monoid is equivalent to a monoid of endomorphisms. That is, corresponding to every monoid ${(M,{\oplus},e)}$ , with ${M}$ a set, and ${(\oplus) :: M \rightarrow M \rightarrow M}$ an associative binary operator with neutral element ${e :: M}$ , there is another monoid ${(N,(\cdot),\mathit{id})}$ on the carrier ${N = \{ (x\oplus) \mid x \in M \}}$ of endomorphisms of the form ${(x\oplus)}$ ; the mappings ${(\oplus) :: M \rightarrow N}$ and ${(\$ e) :: N \rightarrow M}$ are both monoid homomorphisms, and are each other’s inverse. (Cayley’s Theorem is what happens to the Yoneda Embedding when specialized to the one-object category representing a monoid.) So any list homomorphism corresponds to a list homomorphism with endomorphisms as the carrier, followed by a single final function application:

$\displaystyle \begin{array}{@{}ll} & \mathit{hom}\;(\oplus)\;f\;e \\ = & \qquad \{ \mbox{Second Homomorphism Theorem} \} \\ & \mathit{foldr}\;((\oplus) \cdot f)\;e \\ = & \qquad \{ \mbox{The Trick} \} \\ & (\$ e) \cdot \mathit{hom}\;(\cdot)\;((\oplus) \cdot f)\;\mathit{id} \end{array}$

Note that ${(\oplus) \cdot f}$ takes a list element ${a}$ the endomorphism ${(f\,a\, \oplus)}$ . The change of representation from ${M}$ to ${N}$ is the same as in The Trick, and is also what underlies Hughes’s novel representation of lists; but I can’t quite put my finger on what these both have to do with Cayley and Yoneda.

by jeremygibbons at August 14, 2018 03:05 PM

August 13, 2018

mightybyte

Setting Up A Private Nix Cache
I recently went through the process of setting up a private Nix binary cache. It was not obvious to me how to go about it at first, so I thought I would document what I did here. There are a few different ways of going about this that might be appropriate in one situation or another, but I’ll just describe the one I ended up using. I need to serve a cache for proprietary code, so I ended up using a cache served via SSH.

Setting up the server

For my cache server I’m using an Amazon EC2 instance with NixOS. It’s pretty easy to create these using the public NixOS 18.03 AMI. I ended up using a t2.medium with 1 TB of storage, but the jury is still out on the ideal tradeoff of specs and cost for our purposes. YMMV.

The NixOS AMI puts the SSH credentials in the root user, so log in like this:
ssh -i /path/to/your/key.pem root@nixcache.example.com
To get your new NixOS machine working as an SSH binary cache there are two things you need to do: generate a signing key and turn on cache serving.

Generate a signing key

You can generate a public/private key pair simply by running the following command:
nix-store --generate-binary-cache-key nixcache.example.com-1 nix-cache-key.sec nix-cache-key.pub
Turn on SSH Nix store serving

NixOS ships out of the box with a config option for enabling this, so it’s pretty easy. Just edit /etc/nixos/configuraton.nix and add the following lines:
 nix = {
 extraOptions = ''
 secret-key-files = /root/nix-cache-key.sec
 '';

 sshServe = {
 enable = true;
 keys = [
 "ssh-rsa ..."
 "ssh-rsa ..."
 ...
 ];
 };
 };
The extraOptions section makes the system aware of your signing key. The sshServe section makes the local Nix store available via the nix-ssh user. You grant access to the cache by adding your users’ SSH public keys to the keys section.

Setting up the clients

Now you need to add this new cache to your users’ machines so they can get cached binaries instead of building things themselves. The following applies to multi-user Nix setups where there is a Nix daemon that runs as root. This is now the default when you install Nix on macOS. If you are using single-user Nix, then you may not need to do all of the following.

You need to have an SSH public/private key pair for your root user to use the Kadena Nix cache. This makes sense because everything in your local Nix store is world readable, so private cache access needs to be semantically controlled on a per-machine basis, not a per-user basis.

Generating a Root SSH Key

To generate an SSH key for your root user, run the following commands. After the ssh-keygen command hit enter three times to accept the defaults. It is important that you not set a password for this SSH key because the connection will be run automatically and you won’t be able to type a password. You’ll do the rest of the section as the root user, so start by entering a root shell and generating an SSH key pair.
sudo su -
ssh-keygen -b 4096
Next ssh to the cache server. This will tell you that the authenticity of the server can’t be established and ask if you want to continue. Answer ‘yes’. After it connects and prompts you for a password, just hit CTRL-c to cancel.
ssh nixcache.example.com
This has the effect of adding the server to your .ssh/known_hosts file. If you didn’t do this, SSH would ask you to verify the host authenticity. But SSH will be called automatically by the Nix daemon and it will fail.

Now cat the public key file.
cat ~/.ssh/id_rsa.pub
Copy the contents of this file and send your key to the administrator of the nix cache.

Telling Nix to use the cache

In your $NIX_CONF_DIR/nix.conf, add your cache to the substituters line and add the cache's public signing key (generated above with the nix-store command or given to you by your cache administrator) to the trusted-public-keys line. It might look something like this:
substituters = ssh://nix-ssh@nixcache.example.com https://cache.nixos.org/
trusted-public-keys = nixcache.example.com-1:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
Now you need to restart the nix daemon.

On mac:
sudo launchctl stop org.nixos.nix-daemon
sudo launchctl start org.nixos.nix-daemon
On linux:
sudo systemctl restart nix-daemon.service
Populating the Cache

To populate the Nix cache, use the nix-copy-closure command on any nix store path. For instance, the result symlink that is created by a nix-build.
nix-copy-closure -v --gzip --include-outputs --to root@nixcache.example.com <nix-store-path>
After you copy binaries to the cache, you need to sign them with the signing key you created with the nix-store command above. You can do that by running the following command on the cache server:
nix sign-paths -k nix-cache-key.sec --all
It’s also possible to sign packages on the machines that build them. This would require copying the private signing key around to other servers, so if you’re going to do that you should think carefully about key management.

Maintenance

At some point it is likely that your cache will run low on disk space. When this happens, the nix-collect-garbage command is your friend for cleaning things up in a gradual way that doesn't suddenly drop long builds on your users.
by mightybyte (noreply@blogger.com) at August 13, 2018 08:40 PM

Ken T Takusagawa

[byhnlnng] Commonly occurring substrings in pi

We calculate the most frequently occurring N-digit sequences in the first 10^N digits of pi past the decimal point.
N=1: The most frequently occurring single digit in the first 10^1=10 digits of pi past the decimal point is 5. It occurs 3 times: 1415926535.
N=2: The most frequently occurring 2-digit sequence in the first 10^2=100 digits of pi past the decimal point is 62. It occurs 4 times: 1415926535897932384626433832795028841971693993751058209749445923078164062862089986280348253421170679.
Below is a table extended up to 10-digit sequences in the first 10^10 digits of pi. When there are ties, all sequences are listed.
(N, number of occurrences, [the N-digit sequences that occur most frequently])
(1,3,[5])
(2,4,[62])
(3,5,[019,105,171,446,609])
(4,6,[2019,2916,7669])
(5,8,[17663,91465])
(6,9,[919441])
(7,9,[0123880,1296878,2009579,2399789,2572735,3707493,4515163,4900343,5707393,8730991,9219118,9435538])
(8,11,[12058610,77114204])
(9,12,[550527601])
(10,12,[2063323454,2612299524,2907884134,4880022211,5078602578,5421790974,7646964010,7711937174,8193684176,9522257435,9725290655])
We stopped at N=10 because, for a computation involving pi in base 10, stopping at 10^10 digits seemed appropriate.
It is curious that the middle column, number of occurrences, is non-decreasing. We don't expect this trend to always be true.
Assuming the digits of pi are random, we expect a typical N-digit sequence to occur once in 10^N digits. This isn't exactly correct because digit sequences overlap so are not independent. I don't know the probability distribution of the number of occurrences of the most common sequence.
Here is Haskell code used in the computation. We used strict state threads (Control.Monad.ST) to avoid lazy thunks from piling up, a frequent occurrence in long computationally intensive tasks which produce output only at the end. We used seq to get rid of one giant space leak at the end when finding the largest item (and its index) of the array discussed below.
We used the unboxed STUArray s Integer Word8 to compactly store the counts for each possible digit string. We furthermore packed 2 entries into each Word8, one in the upper 4 bits and one in the lower, at the cost of limiting maximum counts to 15 (which turned out to be enough: the maximum seen was 12). For N=10, we were therefore expecting 5 GB memory usage for the 10^10 digit run, but memory use was 9848268k maxresident (9.8 GB) according to /usr/bin/time, so there is still a space leak somewhere. CPU time was 6000 seconds.

by Ken (noreply@blogger.com) at August 13, 2018 06:11 AM

August 09, 2018

FP Complete

Haskell Library Audit Reports

Since December, FP Complete has been working with Cardano Foundation on an audit of the Cardano settlement layer. The audit work is ongoing, with the currently released reports available on Cardano's website.

by Michael Snoyman (michael@fpcomplete.com) at August 09, 2018 09:47 PM

August 07, 2018

Joachim Breitner

Swing Dancer Profile

During my two years in Philadelphia (I was a post-doc with Stephanie Weirich at the University of Pennsylvania) I danced a lot of Swing, in particular at the weekly social “Jazz Attack”.

They run a blog, that blog features dancers, and this week – just in time for my last dance – they featured me with a short interview.

by Joachim Breitner (mail@joachim-breitner.de) at August 07, 2018 04:16 PM

Jeremy Gibbons

Asymmetric Numeral Systems

The previous two posts discussed arithmetic coding (AC). In this post I’ll discuss a related but more recent entropy encoding technique called asymmetric numeral systems (ANS), introduced by Jarek Duda and explored in some detail in a series of 12 blog posts by Charles Bloom. ANS combines the effectiveness of AC (achieving approximately the theoretical optimum Shannon entropy) with the efficiency of Huffman coding. On the other hand, whereas AC acts in a first-in first-out manner, ANS acts last-in first-out, in the sense that the decoded text comes out in reverse; this is not a problem in a batched context, but it makes ANS unsuitable for encoding a communications channel, and also makes it difficult to employ adaptive text models.

Arithmetic coding, revisited

Here is a simplified version of arithmetic coding; compared to the previous posts, we use a fixed rather than adaptive model, and rather than ${\mathit{pick}}$ ing some arbitrary element of the final interval, we pick explicitly the lower bound of the interval (by ${\mathit{fst}}$ , when it is represented as a pair). We suppose a function

$\displaystyle \begin{array}{@{}l} \mathit{count} :: \mathit{Symbol} \rightarrow \mathit{Integer} \\ \end{array}$

that returns a positive count for every symbol, representing predicted frequencies of occurrence, from which it is straightforward to derive functions

$\displaystyle \begin{array}{@{}l} \mathit{encodeSym} :: \mathit{Symbol} \rightarrow \mathit{Interval} \\ \mathit{decodeSym} :: \mathit{Rational} \rightarrow \mathit{Symbol} \end{array}$

that work on a fixed global model, satisfying the central property

$\displaystyle \mathit{decodeSym}\;x = s \Leftrightarrow x \in \mathit{encodeSym}\;s$

For example, an alphabet of three symbols `a’, `b’, `c’, with counts 2, 3, and 5 respectively, could be encoded by the intervals ${(0,\frac{1}{5}), (\frac{1}{5},\frac{1}{2}),(\frac{1}{2},1)}$ . We have operations on intervals:

$\displaystyle \begin{array}{@{}ll} \mathit{weight}\;(l,r)\;x & = l + (r-l) \times x \\ \mathit{scale}\;(l,r)\;x & = (x-l)/(r-l) \\ \mathit{narrow}\;i\;(p,q) & = (\mathit{weight}\;i\;p, \mathit{weight}\;i\;q) \\ \end{array}$

that satisfy

$\displaystyle \begin{array}{@{}ll} \mathit{weight}\;i\;x \in i & \Leftrightarrow x \in \mathit{unit} \\ \mathit{weight}\;i\;x = y & \Leftrightarrow \mathit{scale}\;i\;y = x \\ \end{array}$

Then we have:

$\displaystyle \begin{array}{@{}l} \mathit{encode}_1 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_1 = \mathit{fst} \cdot \mathit{foldl}\;\mathit{estep}_1\;\mathit{unit} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_1 :: \mathit{Interval} \rightarrow \mathit{Symbol} \rightarrow \mathit{Interval} \\ \mathit{estep}_1\;i\;s = \mathit{narrow}\;i\;(\mathit{encodeSym}\;s) \medskip \end{array} \\ \mathit{decode}_1 :: \mathit{Rational} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_1 = \mathit{unfoldr}\;\mathit{dstep}_1 \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{dstep}_1 :: \mathit{Rational} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Rational}) \\ \mathit{dstep}_1\;x = \mathbf{let}\;s = \mathit{decodeSym}\;x\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{scale}\;(\mathit{encodeSym}\;s)\;x) \end{array} \end{array}$

For example, with the alphabet and intervals above, the input text “abc” gets encoded symbol by symbol, from left to right (because of the ${\mathit{foldl}}$ ), to the narrowing sequence of intervals ${(\frac{0}{1}, \frac{1}{1}), (\frac{0}{1}, \frac{1}{5}), (\frac{1}{25}, \frac{1}{10}), (\frac{7}{100}, \frac{1}{10})}$ from which we select the lower bound ${\frac{7}{100}}$ of the final interval. (This version doesn’t stream well, because of the decision to pick the lower bound of the final interval as the result. But it will suffice for our purposes.)

Note now that the symbol encoding can be “fissioned” out of ${\mathit{encode}_1}$ , using map fusion for ${\mathit{foldl}}$ backwards; moreover, ${\mathit{narrow}}$ is associative (and ${\mathit{unit}}$ its neutral element), so we can replace the ${\mathit{foldl}}$ with a ${\mathit{foldr}}$ ; and finally, now using fusion forwards, we can fuse the ${\mathit{fst}}$ with the ${\mathit{foldr}}$ . That is,

$\displaystyle \begin{array}{@{}cl} & \mathit{encode}_1 \\ = & \qquad \{ \mbox{definition} \} \\ & \mathit{fst} \cdot \mathit{foldl}\;\mathit{estep}_1\;\mathit{unit} \\ = & \qquad \{ \mbox{fusion for } \mathit{foldl} \mbox{, backwards} \} \\ & \mathit{fst} \cdot \mathit{foldl}\;\mathit{narrow}\;\mathit{unit} \cdot \mathit{map}\;\mathit{encodeSym} \\ = & \qquad \{ \mathit{narrow} \mbox{ is associative} \} \\ & \mathit{fst} \cdot \mathit{foldr}\;\mathit{narrow}\;\mathit{unit} \cdot \mathit{map}\;\mathit{encodeSym} \\ = & \qquad \{ \mbox{fusion for } \mathit{foldr} \} \\ & \mathit{foldr}\;\mathit{weight}\;0 \cdot \mathit{map}\;\mathit{encodeSym} \end{array}$

and we can fuse the ${\mathit{map}}$ back into the ${\mathit{foldr}}$ ; so we have ${\mathit{encode}_1 = \mathit{encode}_2}$ , where

$\displaystyle \begin{array}{@{}l} \mathit{encode}_2 :: [\mathit{Symbol}] \rightarrow \mathit{Rational} \\ \mathit{encode}_2 = \mathit{foldr}\;\mathit{estep}_2\;0 \qquad\mathbf{where} \\ \qquad \begin{array}[t]{@{}l} \mathit{estep}_2 :: \mathit{Symbol} \rightarrow \mathit{Rational} \rightarrow \mathit{Rational} \\ \mathit{estep}_2\;s\;x = \mathit{weight}\;(\mathit{encodeSym}\;s)\;x \end{array} \end{array}$

Now encoding is a simple ${\mathit{foldr}}$ and decoding a simple ${\mathit{unfoldr}}$ . This means that we can prove that decoding inverts encoding, using the “Unfoldr–Foldr Theorem” stated in the Haskell documentation for ${\mathit{unfoldr}}$ (in fact, the only property of ${\mathit{unfoldr}}$ stated there!). The theorem states that if

$\displaystyle \begin{array}{@{}ll} g\;(f\;x\;z) & = \mathit{Just}\;(x,z) \\ g\;e & = \mathit{Nothing} \end{array}$

for all ${x}$ and ${z}$ , then

$\displaystyle \mathit{unfoldr}\;g\;(\mathit{foldr}\;f\;e\;\mathit{xs}) = \mathit{xs}$

for all finite lists ${\mathit{xs}}$ . Actually, that’s too strong for us here, because our decoding always generates an infinite list; a weaker variation (hereby called the “Unfoldr–Foldr Theorem With Junk”) states that if

$\displaystyle \begin{array}{@{}ll} g\;(f\;x\;z) & = \mathit{Just}\;(x,z) \end{array}$

for all ${x}$ and ${z}$ , then

$\displaystyle \exists \mathit{ys}\,.\, \mathit{unfoldr}\;g\;(\mathit{foldr}\;f\;e\;\mathit{xs}) = \mathit{xs} \mathbin{{+}\!\!\!{+}} \mathit{ys}$

for all finite lists ${\mathit{xs}}$ —that is, the ${\mathit{unfoldr}}$ inverts the ${\mathit{foldr}}$ except for appending some junk ${\mathit{ys}}$ to the output. It’s a nice exercise to prove this weaker theorem, by induction.

We check the condition:

$\displaystyle \begin{array}{@{}cl} & \mathit{dstep}_1\;(\mathit{estep}_2\;s\;x) \\ = & \qquad \{ \mathit{estep}_2 \mbox{; let } x' = \mathit{weight}\;(\mathit{encodeSym}\;s)\;x \} \\ & \mathit{dstep}_1\;x' \\ = & \qquad \{ \mathit{dstep}_1 \mbox{; let } s' = \mathit{decodeSym}\;x' \} \\ & \mathit{Just}\;(s', \mathit{scale}\;(\mathit{encodeSym}\;s')\;x') \end{array}$

Now, we hope to recover the first symbol, ie we hope that ${s' = s}$ :

$\displaystyle \begin{array}{@{}cl} & \mathit{decodeSym}\;x' = s \\ \Leftrightarrow & \qquad \{ \mbox{central property} \} \\ & x' \in \mathit{encodeSym}\;s \\ \Leftrightarrow & \qquad \{ x' = \mathit{weight}\;(\mathit{encodeSym}\;s)\;x \mbox{; } \mathit{weight} \} \\ & x \in \mathit{unit} \end{array}$

Fortunately, it is an invariant of the encoding process that ${x}$ —the result of ${\mathit{encode}_2}$ —is in the unit interval, so indeed ${s' = s}$ . Continuing:

$\displaystyle \begin{array}{@{}cl} & \mathit{dstep}_1\;(\mathit{estep}_2\;s\;x) \\ = & \qquad \{ \mbox{above} \} \\ & \mathit{Just}\;(s, \mathit{scale}\;(\mathit{encodeSym}\;s)\;(\mathit{weight}\;(\mathit{encodeSym}\;s)\;x)) \\ = & \qquad \{ \mathit{scale}\;i \cdot \mathit{weight}\;i = \mathit{id} \} \\ & \mathit{Just}\;(s, x) \end{array}$

as required. Therefore decoding inverts encoding, apart from the fact that it continues to produce junk having decoded all the input; so

$\displaystyle \mathit{take}\;(\mathit{length}\;\mathit{xs})\;(\mathit{decode}_1\;(\mathit{encode}_2\;\mathit{xs})) = \mathit{xs}$

for all finite ${\mathit{xs}}$ .

From fractions to integers

Whereas AC encodes longer and longer messages as more and more precise fractions, ANS encodes them as larger and larger integers. Given the ${\mathit{count}}$ function on symbols, we can easily derive definitions

$\displaystyle \begin{array}{@{}ll} \mathit{cumul} & :: \mathit{Symbol} \rightarrow \mathit{Integer} \\ \mathit{total} & :: \mathit{Integer} \\ \mathit{find} & :: \mathit{Integer} \rightarrow \mathit{Symbol} \\ \end{array}$

such that ${\mathit{cumul}\;s}$ gives the cumulative counts of all symbols preceding ${s}$ (say, in alphabetical order), ${\mathit{total}}$ the total of all symbol counts, and ${\mathit{find}\;x}$ looks up an integer ${0 \le x < \mathit{total}}$ :

$\displaystyle \mathit{find}\;x = s \Leftrightarrow \mathit{cumul}\;s \le x < \mathit{cumul}\;s + \mathit{count}\;s$

(for example, we might tabulate the function ${\mathit{cumul}}$ using a scan).

We encode a text as an integer ${x}$ , containing ${\log x}$ bits of information (all logs in this blog are base 2). The next symbol ${s}$ to encode has probability ${p = \mathit{count}\;s / \mathit{total}}$ , and so requires an additional ${\log (1/p)}$ bits; in total, that’s ${\log x + \log (1/p) = \log (x/p) = \log (x \times \mathit{total}/\mathit{count}\;s)}$ bits. So entropy considerations tell us that, roughly speaking, to incorporate symbol ${s}$ into state ${x}$ we want to map ${x}$ to ${x' \simeq x \times \mathit{total} / \mathit{count}\;s}$ . Of course, in order to decode, we need to be able to invert this transformation, to extract ${s}$ and ${x}$ from ${x'}$ ; this suggests that we should do the division by ${\mathit{count}\;s}$ first:

$\displaystyle x' = (x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s) \times \mathit{total} \qquad \mbox{\textemdash{} not final}$

so that the multiplication by the known value ${\mathit{total}}$ can be undone first:

$\displaystyle x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s = x' \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}$

How do we reconstruct ${s}$ ? Well, there is enough headroom in ${x'}$ to add any non-negative value less than ${\mathit{total}}$ without affecting the division; in particular, we can add ${\mathit{cumul}\;s}$ to ${x'}$ , and then we can use ${\mathit{find}}$ on the remainder:

$\displaystyle \begin{array}{@{}l} x' = (x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s) \times \mathit{total} + \mathit{cumul}\;s \qquad \mbox{\textemdash{} also not final} \\ x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s = x' \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total} \\ \mathit{cumul}\;s = x' \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{total} \\ s = \mathit{find}\;(\mathit{cumul}\;s) = \mathit{find}\;(x' \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{total}) \end{array}$

But we have still lost some information from the lower end of ${x}$ through the division, namely ${x \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{count}\;s}$ ; so we can’t yet reconstruct ${x}$ . Happily, ${\mathit{find}\;(\mathit{cumul}\;s) = \mathit{find}\;(\mathit{cumul}\;s+r)}$ for any ${0 \le r < \mathit{count}\;s}$ , so there is still precisely enough headroom in ${x'}$ to add this lost information too without affecting the ${\mathit{find}}$ , allowing us also to reconstruct ${x}$ :

$\displaystyle \begin{array}{@{}l} x' = (x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s) \times \mathit{total} + \mathit{cumul}\;s + x \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{count}\;s \qquad \mbox{\textemdash{} final} \\ x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s = x' \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total} \\ \mathit{cumul}\;s + x \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{count}\;s = x' \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{total} \\ s = \mathit{find}\;(\mathit{cumul}\;s + x \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{count}\;s) = \mathit{find}\;(x' \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{total}) \\ x = \mathit{count}\;s \times (x \mathbin{\underline{\smash{\mathit{div}}}} \mathit{count}\;s) + x \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{count}\;s = \mathit{count}\;s \times (x' \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}) + x' \mathbin{\underline{\smash{\mathit{mod}}}} \mathit{total} - \mathit{cumul}\;s \end{array}$

We therefore define

$\displaystyle \begin{array}{@{}l} \mathit{encode}_3 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_3 = \mathit{foldr}\;\mathit{estep}_3\;0 \\ \mathit{estep}_3 :: \mathit{Symbol} \rightarrow \mathit{Integer} \rightarrow \mathit{Integer} \\ \mathit{estep}_3\;s\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s)\;\mathbf{in}\;q \times \mathit{total} + \mathit{cumul}\;s + r \medskip \\ \mathit{decode}_3 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_3 = \mathit{unfoldr}\;\mathit{dstep}_3 \\ \mathit{dstep}_3 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_3\;x = \mathbf{let}\;(q,r) = \mathit{divMod}\;x\;\mathit{total} ; s = \mathit{find}\;r\;\mathbf{in}\; \mathit{Just}\;(s, \mathit{count}\;s \times q + r - \mathit{cumul}\;s) \end{array}$

Using similar reasoning as for AC, it is straightforward to show that a decoding step inverts an encoding step:

$\displaystyle \begin{array}{@{}cl} & \mathit{dstep}_3\;(\mathit{estep}_3\;s\;x) \\ = & \qquad \{ \mathit{estep}_3 \mbox{; let } (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s), x' = q \times \mathit{total} + \mathit{cumul}\;s + r \} \\ & \mathit{dstep}_3\;x' \\ = & \qquad \{ \mathit{dstep}_3 \mbox{; let } (q',r') = \mathit{divMod}\;x'\;\mathit{total} ; s' = \mathit{find}\;r' \} \\ & \mathit{Just}\;(s', \mathit{count}\;s' \times q' + r' - \mathit{cumul}\;s') \\ = & \qquad \{ r' = \mathit{cumul}\;s + r, 0 \le r < \mathit{count}\;s, \mbox{ so } s'=\mathit{find}\;r'=s \} \\ & \mathit{Just}\;(s, \mathit{count}\;s \times q' + r' - \mathit{cumul}\;s) \\ = & \qquad \{ r' - \mathit{cumul}\;s = r, q' = x' \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total} = q \} \\ & \mathit{Just}\;(s, \mathit{count}\;s \times q + r) \\ = & \qquad \{ (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \} \\ & \mathit{Just}\;(s,x) \end{array}$

Therefore decoding inverts encoding, modulo final junk, by the Unfoldr–Foldr Theorem With Junk:

$\displaystyle \mathit{take}\;(\mathit{length}\;\mathit{xs})\;(\mathit{decode}_3\;(\mathit{encode}_3\;\mathit{xs})) = \mathit{xs}$

for all finite ${\mathit{xs}}$ . For example, with the same alphabet and symbol weights as before, encoding the text “abc” (now from right to left, because of the ${\mathit{foldr}}$ ) proceeds through the steps ${0, 5, 14, 70}$ , and the last element ${70}$ is the encoding.

In fact, the inversion property holds whatever value we use to start encoding with (since it isn’t used in the proof); in the next section, we start encoding with a certain lower bound ${l}$ rather than ${0}$ . Moreover, ${\mathit{estep}_3}$ is strictly increasing on states strictly greater than zero, and ${\mathit{dstep}_3}$ strictly decreasing; which means that the decoding process can stop when it returns to the lower bound. That is, if we pick some ${l > 0}$ and define

$\displaystyle \begin{array}{@{}l} \mathit{encode}_4 :: [\mathit{Symbol}] \rightarrow \mathit{Integer} \\ \mathit{encode}_4 = \mathit{foldr}\;\mathit{estep}_3\;l \medskip \\ \mathit{decode}_4 :: \mathit{Integer} \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_4 = \mathit{unfoldr}\;\mathit{dstep}_4 \\ \mathit{dstep}_4 :: \mathit{Integer} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Integer}) \\ \mathit{dstep}_4\;x = \mathbf{if}\; x==l \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; \mathit{dstep}_3\;x \end{array}$

then the stronger version of the Unfoldr–Foldr Theorem holds, and we have

$\displaystyle \mathit{decode}_4\;(\mathit{encode}_4\;\mathit{xs}) = \mathit{xs}$

for all finite ${\mathit{xs}}$ , without junk.

Bounded precision

The previous versions all used arbitrary-precision arithmetic, which is expensive. We now change the approach slightly to use only bounded-precision arithmetic. As usual, there is a trade-off between effectiveness (a bigger bound means more accurate approximations to ideal entropies) and efficiency (a smaller bound generally means faster operations). Fortunately, the reasoning does not depend on much about the actual bounds. We will represent the integer accumulator ${z}$ as a pair ${(x,\mathit{ys})}$ which we call a ${\mathit{Number}}$ :

$\displaystyle \mathbf{type}\; \mathit{Number} = (\mathit{Integer}, [\mathit{Integer}])$

such that ${\mathit{ys}}$ is a list of digits in a given base ${b}$ , and ${x}$ is an integer with ${l \le x < u}$ (where we define ${u = l \times b}$ for the upper bound of the range), under the abstraction relation

$\displaystyle z = \mathit{foldl}\;\mathit{inject}\;x\;\mathit{ys}$

where

$\displaystyle \begin{array}{@{}ll} \mathit{inject}\;x\;y & = x \times b + y \\ \mathit{extract}\;x & = \mathit{divMod}\;x\;b \end{array}$

We call ${x}$ the “window” and ${\mathit{ys}}$ the “remainder”. For example, with ${b=10}$ and ${l=100}$ , the pair ${(123,[4,5,6])}$ represents ${123456}$ ; and indeed, for any ${z \ge l}$ there is a unique representation satisfying the invariants. According to Duda, ${\mathit{total}}$ should divide into ${l}$ evenly. On a real implementation, ${b}$ and ${l}$ should be powers of two, such that arithmetic on values up to ${u}$ fits within a single machine word.

The encoding step acts on the window in the accumulator using ${\mathit{estep}_3}$ , which risks making it overflow the range; we therefore renormalize with ${\mathit{enorm}_5}$ by shifting digits from the window to the remainder until this overflow would no longer happen, before consuming the symbol.

$\displaystyle \begin{array}{@{}l} \mathit{econsume}_5 :: [\mathit{Symbol}] \rightarrow \mathit{Number} \\ \mathit{econsume}_5 = \mathit{foldr}\;\mathit{estep}_5\;(l,[\,]) \medskip \\ \mathit{estep}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{estep}_5\;s\;(x,\mathit{ys}) = \mathbf{let}\;(x',\mathit{ys}') = \mathit{enorm}_5\;s\;(x,\mathit{ys})\;\mathbf{in}\;(\mathit{estep}_3\;s\;x',\mathit{ys}') \medskip \\ \mathit{enorm}_5 :: \mathit{Symbol} \rightarrow \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{enorm}_5\;s\;(x,\mathit{ys}) = \begin{array}[t]{@{}l@{}} \mathbf{if}\;\mathit{estep}_3\;s\;x < u \;\mathbf{then}\; (x,\mathit{ys})\;\mathbf{else}\; \\ \mathbf{let}\;(q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{enorm}_5\;s\;(q,r:\mathit{ys}) \end{array} \end{array}$

Some calculation, using the fact that ${\mathit{total}}$ divides ${l}$ , allows us to rewrite the guard in ${\mathit{enorm}_5}$ :

$\displaystyle \mathit{estep}_3\;s\;x < u \Leftrightarrow x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}) \times \mathit{count}\;s$

For example, again encoding the text “abc”, again from right to left, with ${r=10}$ and ${l=100}$ , the accumulator starts with ${(100,[\,])}$ , and goes through the states ${(205,[\,])}$ and ${(683,[\,])}$ on consuming the `c’ then the `b’; directly consuming the `a’ would make the window overflow, so we renormalize to ${(68,[3])}$ ; then it is safe to consume the `a’, leading to the final state ${(340,[3])}$ .

Decoding is an unfold using the accumulator as state. We repeatedly output a symbol from the window; this may make the window underflow the range, in which case we renormalize if possible by injecting digits from the remainder (and if this is not possible, because there are no more digits to inject, it means that we have decoded the entire text).

$\displaystyle \begin{array}{@{}l} \mathit{dproduce}_5 :: \mathit{Number} \rightarrow [\mathit{Symbol}] \\ \mathit{dproduce}_5 = \mathit{unfoldr}\;\mathit{dstep}_5 \medskip \\ \mathit{dstep}_5 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Symbol}, \mathit{Number}) \\ \mathit{dstep}_5\;(x,\mathit{ys}) = \begin{array}[t]{@{}l} \mathbf{let}\; \mathit{Just}\;(s, x') = \mathit{dstep}_3\;x ; (x'',\mathit{ys}'') = \mathit{dnorm}_5\;(x',\mathit{ys}) \;\mathbf{in} \\ \mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing} \medskip \end{array} \\ \mathit{dnorm}_5 :: \mathit{Number} \rightarrow \mathit{Number} \\ \mathit{dnorm}_5\;(x,y:\mathit{ys}) = \mathbf{if}\; x < l \;\mathbf{then}\; \mathit{dnorm}_5\; (\mathit{inject}\;x\;y, \mathit{ys}) \;\mathbf{else}\; (x,y:\mathit{ys}) \\ \mathit{dnorm}_5\;(x,[\,]) = (x,[\,]) \end{array}$

Note that decoding is of course symmetric to encoding; in particular, when encoding we renormalize before consuming a symbol; therefore when decoding we renormalize after emitting a symbol. For example, decoding the final encoding ${(340,[3])}$ starts by computing ${\mathit{dstep}_3\;340 = \mathit{Just}\;(\mbox{\texttt{\char39{}a\char39}},68)}$ ; the window value 68 has underflowed, so renormalization consumes the remaining digit 3, leading to the accumulator ${(683,[\,])}$ ; then decoding proceeds to extract the `b’ and `c’ in turn, returning the accumulator to ${(100,[\,])}$ .

We can again prove that decoding inverts encoding, although we need to use yet another variation of the Unfoldr–Foldr Theorem, hereby called the “Unfoldr–Foldr Theorem With Invariant”. We say that predicate ${p}$ is an invariant of ${\mathit{foldr}\;f\;e}$ and ${\mathit{unfoldr}\;g}$ if

$\displaystyle \begin{array}{@{}lcl} p\;z &\Rightarrow& p\;(f\;x\;z) \\ p\;z \land g\;z = \mathit{Just}\;(x,z') &\Rightarrow& p\;z' \end{array}$

The theorem is that if ${p}$ is such an invariant, and the conditions

$\displaystyle \begin{array}{@{}ll} g\;(f\;x\;z) & = \mathit{Just}\;(x,z) \qquad \Leftarrow p\;z \\ g\;e & = \mathit{Nothing} \end{array}$

hold for all ${x}$ and ${z}$ , then

$\displaystyle \mathit{unfoldr}\;g\;(\mathit{foldr}\;f\;e\;\mathit{xs}) = \mathit{xs} \qquad \Leftarrow p\;e$

for all finite lists ${\mathit{xs}}$ , provided that the initial state ${e}$ satisfies the invariant ${p}$ . In our case, the invariant is that the window ${x}$ is in range ( ${l \le x < u}$ ), which is indeed maintained by ${\mathit{estep}_5}$ and ${\mathit{dstep}_5}$ . Then it is straightforward to verify that

$\displaystyle \mathit{dstep}_5\;(l,[\,]) = \mathit{Nothing}$

and

$\displaystyle \mathit{dstep}_5\;(\mathit{estep}_5\;s\;(x,\mathit{ys})) = \mathit{Just}\;(s,(x,\mathit{ys}))$

when ${x}$ is in range, making use of a lemma that

$\displaystyle \mathit{dnorm}_5\;(\mathit{enorm}_5\;(x,\mathit{ys})) = (x,\mathit{ys})$

when ${x}$ is in range. Therefore decoding inverts encoding:

$\displaystyle \mathit{dproduce}_5\;(\mathit{econsume}_5\;\mathit{xs}) = \mathit{xs}$

for all finite ${\mathit{xs}}$ .

Trading in sequences

The version of encoding in the previous section yields a ${\mathit{Number}}$ , that is, a pair consisting of an integer window and a digit sequence remainder. It would be more conventional for encoding to take a sequence of symbols to a sequence of digits alone, and decoding to take the sequence of digits back to a sequence of symbols. For encoding, we have to flush the remaining digits out of the window at the end of the process, reducing the window to zero:

$\displaystyle \begin{array}{@{}l} \mathit{eflush}_5 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_5\;(0,\mathit{ys}) = \mathit{ys} \\ \mathit{eflush}_5\;(x,\mathit{ys}) = \mathbf{let}\; (x',y) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{eflush}_5\;(x',y:\mathit{ys}) \end{array}$

For example, ${\mathit{eflush}_5\;(340,[3]) = [3,4,0,3]}$ . Then we can define

$\displaystyle \begin{array}{@{}l} \mathit{encode}_5 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_5 = \mathit{eflush}_5 \cdot \mathit{econsume}_5 \end{array}$

Correspondingly, decoding should start by populating an initially-zero window from the sequence of digits:

$\displaystyle \begin{array}{@{}l} \mathit{dstart}_5 :: [\mathit{Integer}] \rightarrow \mathit{Number} \\ \mathit{dstart}_5\;\mathit{ys} = \mathit{dnorm}_5\;(0,\mathit{ys}) \end{array}$

For example, ${\mathit{dstart}_5\;[3,4,0,3] = (340,[3])}$ . Then we can define

$\displaystyle \begin{array}{@{}l} \mathit{decode}_5 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_5 = \mathit{dproduce}_5 \cdot \mathit{dstart}_5 \end{array}$

One can show that

$\displaystyle \mathit{dstart}_5\;(\mathit{eflush}_5\;x) = x$

provided that ${x}$ is initially in range, and therefore again decoding inverts encoding:

$\displaystyle \begin{array}{@{}ll} & \mathit{decode}_5\;(\mathit{encode}_5\;\mathit{xs}) \\ = & \qquad \{ \mathit{decode}_5, \mathit{encode}_5 \} \\ & \mathit{dproduce}_5\;(\mathit{dstart}_5\;(\mathit{eflush}_5\;(\mathit{econsume}_5\;\mathit{xs}))) \\ = & \qquad \{ \mathit{econsume}_5 \mbox { yields an in-range window, on which } \mathit{dstart}_5 \mbox{ inverts } \mathit{eflush}_5 \} \\ & \mathit{dproduce}_5\;(\mathit{econsume}_5\;\mathit{xs}) \\ = & \qquad \{ \mathit{dproduce}_5 \mbox { inverts } \mathit{econsume}_5 \} \\ & \mathit{xs} \end{array}$

for all finite ${\mathit{xs}}$ .

Note that this is not just a data refinement—it is not the case that ${\mathit{encode}_5}$ yields the digits of the integer computed by ${\mathit{encode}_4}$ . For example, ${\mathit{encode}_4\;\mbox{\texttt{\char34{}abc\char34}} = 3411}$ , whereas ${\mathit{encode}_5\;\mbox{\texttt{\char34{}abc\char34}} = [3,4,0,3]}$ . We have really changed the effectiveness of the encoding in return for the increased efficiency.

Streaming encoding

We would now like to stream encoding and decoding as metamorphisms: encoding should start delivering digits before consuming all the symbols, and conversely decoding should start delivering symbols before consuming all the digits.

For encoding, we have

$\displaystyle \begin{array}{@{}l} \mathit{encode}_5 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_5 = \mathit{eflush}_5 \cdot \mathit{econsume}_5 \end{array}$

with ${\mathit{econsume}_5}$ a fold; can we turn ${\mathit{eflush}_5}$ into an unfold? Yes, we can! The remainder in the accumulator should act as a queue of digits: digits get enqueued at the most significant end, so we need to dequeue them from the least significant end. So we define

$\displaystyle \begin{array}{@{}l} \mathit{edeal}_6 :: [\alpha] \rightarrow [\alpha] \\ \mathit{edeal}_6 = \mathit{unfoldr}\;\mathit{unsnoc} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} \mathit{unsnoc}\;[\,] & = \mathit{Nothing} \\ \mathit{unsnoc}\;\mathit{ys} & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, \mathit{ys}') \end{array} \end{array}$

to “deal out” the elements of a list one by one, starting with the last. Of course, this reverses the list; so we have the slightly awkward

$\displaystyle \mathit{eflush}_5 = \mathit{reverse} \cdot \mathit{edeal}_6 \cdot \mathit{eflush}_5$

Now we can use unfold fusion to fuse ${\mathit{edeal}_6}$ and ${\mathit{eflush}_5}$ into a single unfold, deriving the coalgebra

$\displaystyle \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{efstep}_6 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Integer}, \mathit{Number})} \\ \mathit{efstep}_6\;(0,[\,]) & = \mathit{Nothing} \\ \mathit{efstep}_6\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ \mathit{efstep}_6\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \end{array}$

by considering each of the three cases, getting ${\mathit{eflush}_5 = \mathit{eflush}_6}$ where

$\displaystyle \begin{array}{@{}l} \mathit{eflush}_6 :: \mathit{Number} \rightarrow [\mathit{Integer}] \\ \mathit{eflush}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \end{array}$

As for the input part, we have a ${\mathit{foldr}}$ where we need a ${\mathit{foldl}}$ . Happily, that is easy to achieve, at the cost of an additional ${\mathit{reverse}}$ , since:

$\displaystyle \mathit{foldr}\;f\;e\;\mathit{xs} = \mathit{foldl}\;(\mathit{flip}\;f)\;e\;(\mathit{reverse}\;\mathit{xs})$

on finite ${\mathit{xs}}$ . So we have ${\mathit{encode}_5 = \mathit{encode}_6}$ , where

$\displaystyle \begin{array}{@{}l} \mathit{encode}_6 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_6 = \mathit{reverse} \cdot \mathit{unfoldr}\;\mathit{efstep}_6 \cdot \mathit{foldl}\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}$

It turns out that the streaming condition does not hold for ${\mathit{efstep}_6}$ and ${\mathit{flip}\;\mathit{estep}_5}$ —although we can stream digits out of the remainder:

$\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[4,5,6]) & = \mathit{Just}\;(6,(123,[4,5])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6]) & = (248,[4,5,6]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[4,5,6])) & = \mathit{Just}\;(6,(248,[4,5])) \end{array}$

we cannot stream the last few digits out of the window:

$\displaystyle \begin{array}{@{}ll} \mathit{efstep}_6\;(123,[\,]) & = \mathit{Just}\;(3,(12,[\,])) \\ \mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,]) & = (248,[\,]) \\ \mathit{efstep}_6\;(\mathit{estep}_5\;\mbox{\texttt{\char39{}c\char39}}\;(123,[\,])) & = \mathit{Just}\;(8,(24,[\,])) \end{array}$

We have to resort to flushing streaming, which starts from an apomorphism

$\displaystyle \mathit{apo} :: (\beta \rightarrow \mathsf{Maybe}\;(\gamma,\beta)) \rightarrow (\beta \rightarrow [\gamma]) \rightarrow \beta \rightarrow [\gamma]$

rather than an unfold. Of course, any unfold is trivially an apo, with the trivial flusher that always yields the empty list; but more interestingly, any unfold can be factored into a “cautious” phase (delivering elements only while a predicate ${p}$ holds) followed by a “reckless” phase (discarding the predicate, and delivering the elements anyway)

$\displaystyle \mathit{unfoldr}\;g = \mathit{apo}\;(\mathit{guard}\;p\; g)\;(\mathit{unfoldr}\;g)$

where

$\displaystyle \begin{array}{@{}l} \mathit{guard} :: (b \rightarrow \mathit{Bool}) \rightarrow (b \rightarrow \mathsf{Maybe}\;(c,b)) \rightarrow (b \rightarrow \mathsf{Maybe}\;(c,b)) \\ \mathit{guard}\;p\;g\;x = \mathbf{if}\; p\;x \;\mathbf{then}\; g\;x \;\mathbf{else}\; \mathit{Nothing} \end{array}$

In particular, the streaming condition may hold for the cautious coalgebra ${\mathit{guard}\;p\;g}$ when it doesn’t hold for the reckless coalgebra ${g}$ itself. We’ll use the cautious coalgebra

$\displaystyle \begin{array}{@{}l} \mathit{efstep}_7 :: \mathit{Number} \rightarrow \mathsf{Maybe}\;(\mathit{Integer}, \mathit{Number}) \\ \mathit{efstep}_7 = \mathit{guard}\;(\mathit{not} \cdot \mathit{null} \cdot \mathit{snd})\;\mathit{efstep}_6 \end{array}$

which carefully avoids the problematic case when the remainder is empty. It is now straightforward to verify that the streaming condition holds for ${\mathit{efstep}_7}$ and ${\mathit{flip}\;\mathit{estep}_5}$ , and therefore ${\mathit{encode}_6 = \mathit{encode}_7}$ , where

$\displaystyle \begin{array}{@{}l} \mathit{encode}_7 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_7 = \mathit{reverse} \cdot \mathit{fstream}\;\mathit{efstep}_7\;(\mathit{unfoldr}\;\mathit{efstep}_6)\;(\mathit{flip}\;\mathit{estep}_5)\;(l,[\,]) \cdot \mathit{reverse} \end{array}$

and where ${\mathit{encode}_7}$ streams its output. On the downside, this has to read the input text in reverse, and also write the output digit sequence in reverse.

Streaming decoding

Fortunately, decoding is rather easier to stream. We have

$\displaystyle \mathit{decode}_5 = \mathit{dproduce}_5 \cdot \mathit{dstart}_5$

with ${\mathit{dproduce}_5}$ an unfold; can we turn ${\mathit{dstart}_5}$ into a fold? Yes, we can! In fact, we have ${\mathit{dstart}_5 = \mathit{foldl}\;\mathit{dsstep}_8\;(0,[\,])}$ , where

$\displaystyle \begin{array}{@{}ll} \mathit{dsstep}_8\;(x,[\,])\;y & = \mathbf{if}\; x < l \;\mathbf{then}\; (\mathit{inject}\;x\;y, [\,]) \;\mathbf{else}\; (x, [y]) \\ \mathit{dsstep}_8\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array}$

That is, starting with ${0}$ for the accumulator, digits are injected one by one into the window until this is in range, and thereafter appended to the remainder.

Now we have decoding as an ${\mathit{unfoldr}}$ after a ${\mathit{foldl}}$ , and it is straightforward to verify that the streaming condition holds for ${\mathit{dstep}_5}$ and ${\mathit{dsstep}_8}$ . Therefore ${\mathit{decode}_5 = \mathit{decode}_8}$ on finite inputs, where

$\displaystyle \begin{array}{@{}l} \mathit{decode}_8 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_8 = \mathit{stream}\;\mathit{dstep}_5\;\mathit{dsstep}_8\;(0,[\,]) \end{array}$

and ${\mathit{decode}_8}$ streams. It is perhaps a little more symmetric to move the ${\mathit{reverse}}$ from the final step of encoding to the initial step of decoding—that is, to have the least significant digit first in the encoded text, rather than the most significant—and then to view both the encoding and the decoding process as reading their inputs from right to left.

Summing up

Inlining definitions and simplifying, we have ended up with encoding as a flushing stream:

$\displaystyle \begin{array}{@{}l} \mathit{encode}_9 :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode}_9 = \mathit{fstream}\;g'\;(\mathit{unfoldr}\;g)\;f\;(l,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} f\;(x,\mathit{ys})\;s & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} total) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; (q \times \mathit{total} + \mathit{cumul}\;s + r,\mathit{ys}) \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; f\;(q, r : \mathit{ys})\;s \end{array} \\ g\;(0,[\,]) & = \mathit{Nothing} \\ g\;(x,[\,]) & = \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; \mathit{Just}\;(r,(q,[\,])) \\ g\;(x,\mathit{ys}) & = \mathbf{let}\; (\mathit{ys}',y) = (\mathit{init}\;\mathit{ys}, \mathit{last}\;\mathit{ys}) \;\mathbf{in}\; \mathit{Just}\;(y, (x,\mathit{ys}')) \\ g'\;(x,\mathit{ys}) & = \mathbf{if}\; \mathit{null}\;\mathit{ys} \;\mathbf{then}\; \mathit{Nothing} \;\mathbf{else}\; g\;(x,\mathit{ys}) \end{array} \end{array}$

and decoding as an ordinary stream:

$\displaystyle \begin{array}{@{}l} \mathit{decode}_9 :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode}_9 = \mathit{stream}\;g\;f\;(0,[\,]) \cdot \mathit{reverse} \;\mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} g\;(x,\mathit{ys}) & = \begin{array}[t]{@{}lll} \mathbf{let} & (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ & s & = \mathit{find}\;r \\ & (x'',\mathit{ys}'') & = n\;(\mathit{count}\;s \times q + r - \mathit{cumul}\;s,\mathit{ys}) \\ \mathbf{in} & \multicolumn{2}{l}{\mathbf{if}\; x'' \ge l \;\mathbf{then}\; \mathit{Just}\;(s,(x'',\mathit{ys}'')) \;\mathbf{else}\; \mathit{Nothing}} \end{array} \\ n\;(x,\mathit{ys}) & = \begin{array}[t]{@{}l} \mathbf{if}\; x\ge l \lor \mathit{null}\;\mathit{ys} \;\mathbf{then}\; (x,\mathit{ys}) \;\mathbf{else} \\ \mathbf{let}\; (y:\mathit{ys}') = \mathit{ys} \;\mathbf{in}\; n\;(\mathit{inject}\;x\;y, \mathit{ys}') \end{array} \\ f\;(x,[\,]) y & = n\;(x,[y]) \\ f\;(x,\mathit{ys})\;y & = (x, \mathit{ys} \mathbin{{+}\!\!\!{+}} [y]) \end{array} \end{array}$

Note that the two occurrences of ${\mathit{reverse}}$ can be taken to mean that encoding and decoding both process their input from last to first. The remainder acts as a queue, with digits being added at one end and removed from the other, so should be represented to make that efficient. But in fact, the remainder can be eliminated altogether, yielding simply the window for the accumulator—for encoding:

$\displaystyle \begin{array}{@{}l} \mathit{encode} :: [\mathit{Symbol}] \rightarrow [\mathit{Integer}] \\ \mathit{encode} = h_1\;l \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}[t]{@{}ll} h_1\;x\;(s:\mathit{ss}') & = \begin{array}[t]{@{}ll} \mathbf{if} & x < b \times (l \mathbin{\underline{\smash{\mathit{div}}}} \mathit{total}) \times \mathit{count}\;s \\ \mathbf{then} & \mathbf{let}\; (q,r) = \mathit{divMod}\;x\;(\mathit{count}\;s) \;\mathbf{in}\; h_1\;(q \times total + \mathit{cumul}\;s + r)\;\mathit{ss}' \\ \mathbf{else} & \mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_1\;q\;(s:\mathit{ss}') \end{array} \\ h_1\;x\;[\,] & = h_2\;x \\ h_2\;x & = \mathbf{if}\; x==0 \;\mathbf{then}\; [\,] \;\mathbf{else}\;\mathbf{let}\; (q,r) = \mathit{extract}\;x \;\mathbf{in}\; r : h_2\;q \end{array} \end{array}$

and for decoding:

$\displaystyle \begin{array}{@{}l} \mathit{decode} :: [\mathit{Integer}] \rightarrow [\mathit{Symbol}] \\ \mathit{decode} = h_0\;0 \cdot \mathit{reverse} \qquad \mathbf{where} \\ \qquad \begin{array}{@{}lll} h_0\;x\;(y:\mathit{ys}) & \mid x < l & = h_0\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_0\;x\;\mathit{ys} && = h_1\;x\;\mathit{ys} \\ h_1\;x\;\mathit{ys} && = \begin{array}[t]{@{}ll} \mathbf{let} & \begin{array}[t]{@{}ll} (q,r) & = \mathit{divMod}\;x\;\mathit{total} \\ s & = \mathit{find}\;r \\ x' & = \mathit{count}\;s \times q + r - \mathit{cumul}\;s \end{array} \\ \mathbf{in} & h_2\;s\;x'\;\mathit{ys} \end{array} \\ h_2\;s\;x\;(y:\mathit{ys}) & \mid x < l & = h_2\;s\;(\mathit{inject}\;x\;y)\;\mathit{ys} \\ h_2\;s\;x\;\mathit{ys} & \mid x \ge l & = s : h_1\;x\;\mathit{ys} \\ h_2\;s\;x\;[\,] && = [\,] \end{array} \end{array}$

This gives rather simple programs, corresponding to those in Duda’s paper; however, the calculation of this last version from the previous steps currently eludes me.

by jeremygibbons at August 07, 2018 11:45 AM

August 06, 2018

apfelmus

HyperHaskell — Release of version 0.2.1.0

It is my pleasure to announce the release of

HyperHaskell
— the strongly hyped Haskell interpreter —
version 0.2.1.0

HyperHaskell is a graphical Haskell interpreter (REPL), not unlike GHCi, but hopefully more awesome. You use worksheets to enter expressions and evaluate them. Results are displayed using HTML.

HyperHaskell is intended to be easy to install. It is cross-platform and should run on Linux, Mac and Windows. That said, the binary distribution is currently only built for Mac. Help is appreciated!

HyperHaskell’s main attraction is a Display class that supersedes the good old Show class. The result looks like this:

Version 0.2.1.0 supports HTML output, binding variables, text cells and GHC language extensions.

For more on HyperHaskell, see its project page on Github.

(EDITED 07 Aug 2018): Related projects that I know of:

IHaskell — a Haskell kernel for Jupyter

Haskell for Mac

haskell.do

Unfortunately, IHaskell has a reputation for being difficult to install, since it depends on Jupyter. Also, I don’t think the integration of Jupyter with the local Desktop environment and file system is particularly great. Haskell for Mac is partially proprietary and Mac only. Hence this new effort.

August 06, 2018 04:07 PM

Lysxia's blog

Haskell with only one type family

by Lysxia at August 06, 2018 12:00 AM

August 04, 2018

Disciple/DDC

Binary interface files with Shimmer
Over the last couple of months I've merged three big changes that continue to move DDC in the direction of a real compiler rather than a research experiment:
Support for binary interface files via the shimmer project.
Reworked the type checker and compiler driver to only require interface files for directly imported modules, rather than all transitively imported modules.
Rewrote the LLVM code printer to write directly to file, instead of going via a pretty printer.
Shimmer:Shimmer is a scheme-like language intended as a shim between compiler stages and intermediate languages. It provides a s-expression syntax and untyped functional intermediate language in which higher level languages can be encoded. It also has a native binary format, as well as its own REPL for testing. Shimmer is available as a hackage package.

DDC interface files are now serialised as binary shimmer files, using the grammar described on the Discus homepage. These files can be dumped in human readable (sort-of) form using the shimmer CLI that comes with the hackage package. For example, once you've build the DDC base libraries you can do:
$ shimmer -load src/s2/base/Data/List.di
+m-name = %module-name "Data" "List";

+m-deps = %l (%module-name "Class" "Applicative") ...

...

@d-Applicative 
   = %d-alg (%module-name "Class" "Applicative") "Applicative" 
      (%l (%bn "f" (%ta %tkf %tkd %tkd))) 
      (%s (%l (%ctor #nat'0 (%module-name "Class" "Applicative") "Applicative" 
              (%tu "Functor" "f") 
              (%tl (%bn "a" %tkd) (%tf "a" (%ta "f" "a"))) 
              (%tl (%bn "a" %tkd) (%tl (%bn "b" %tkd) (%tf (%ta "f" (%tf "a" "b")) (%ta "f" "a") (%ta "f" "b")))) 
                                  (%tu "Applicative" "f"))));
...

@t-mapMaybe 
 = %tl (%bn "a" %tkd) (%tl (%bn "b" %tkd) 
         (%tf (%tf "a" (%tu "Maybe" "b")) (%tu "List" "a") (%tu "List" "b")));

@x-mapMaybe 
 = %xb (%mtn "a" %tkd) (%mtn "b" %tkd) 
       (%mxn "f"  (%tf "a" (%tu "Maybe" "b"))) 
       (%mxn "xx" (%tu "List" "a")) 
       (%xc "xx"  (%ab (%dcn %n %n (%dc "Nil"))  (%xa (%dcn %n %n (%dc "Nil")) (%rt "b"))) 
                  (%ab (%dcn %n %n (%dc "Cons")) (%bn "x" "a") (%bn "xs" (%tu "List" "a")) 
                  (%xc (%xa "f" "x") (%ab (%dcn %n %n (%dc "Nothing")) (%xa "mapMaybe" (%rt "a") (%rt "b") "f" "xs")) 
                                     (%ab (%dcn %n %n (%dc "Just")) (%bn "x'" "b") 
                                          (%xa (%dcn %n %n (%dc "Cons")) (%rt "b") "x'" 
                                          (%xa "mapMaybe" (%rt "a") (%rt "b") "f" "xs"))))));
This is a simple encoding of the AST of the DDC Core intermediate language. For example @d-Applicative gives the data type declaration for an Applicative type class dictionary. @t-mapMaybe encodes the type of the mapMaybe function, and @x-mapMaybe encodes the declaration. %tl means "forall", %xb is a lambda binder, %xc a case expression, %xa an application, and so on. See the grammar for the rest.

The binary format is a not-completely-horrible packed representation, where I've made an effort to avoid redundant encoding, but haven't done any compression or indexing yet. The main feature is that serialisation and deserialisation are implemented by simply peeking and poking from memory, so performance should be reasonable. The binary grammar is defined in the hackage package.

Q. Why the name Shimmer?
A. Planner, Conniver, Schemer, Shimmer.

Did you know that Scheme used to be called "Schemer", but that Guy Steele's computer at the time only supported 6 character file names? Shimmer is a Scheme-like language, but without the Scheme.

No more transitive imports: Previously, when type checking a module, DDC needed to load the textual interface files for all transitively reachable modules, which in most cases was the entire base library. This approach works fine for a toy language and a minimal base library, but implies that the more useful the base library becomes, the slower compilation gets. In the current version, when some module A re-exports declarations for module B, those declarations are also added to module A's interface file. In general this means that when compiling a given module we only need to load interface files for directly imported modules, not all modules that are transitively reachable. When doing this change I also added in-memory indexes for the various sorts of declarations (data types, type synonyms, value declarations etc) to speed up name resolution. This framework should also support the addition of on-disk database style indexes to shimmer files. We'll need this when the base library grows large enough that deserialisation of interface files becomes a problem again.

Direct write of LLVM code: Haskell programmers love their pretty printer libraries. I had been using wl-pprint to pretty print LLVM code before calling the LLVM compiler to convert them to binary object files. For small output files intended for human consumption, wl-pprint is great. However, if one just wants to dump some LLVM code to feed to the LLVM compiler, then the time to construct and then consume the intermediate Doc type, as well as the overhead of Haskell Strings becomes an unreasonable overhead. Today I rewrote the LLVM generator to just write directly to a file handle -- an "ugly-printer", if you will. Doing that yielded a ~10% reduction in overall compilation time.

These three changes reduced compile time for the ddc-demo tree to about 35% of what it was previously, or about a 2.5x speedup. There are more low hanging fruits, but I've got enough juice for now, so am planning to return to higher level concerns in the immediate future. The DDC reflection system is also starting to work, but that will be the topic of a subsequent blog post.
by Ben Lippmeier (noreply@blogger.com) at August 04, 2018 09:47 AM

Chris Smith 2

CodeWorld post-mortem: Shared project outage

Unfortunately, users of CodeWorld for the last two weeks experienced some problems with projects they had shared in the past. Projects that were shared too long in the past would fail to load without source code. However, the same projects continued to work when loaded and run with source code in the CodeWorld environment.
This post explains what happened, who was impacted, and what I’m doing to prevent the similar issues in the future.
Background
The problem was with shared projects in CodeWorld. When you create and run a project in CodeWorld, you can easily share it with others, by using the Share button at the bottom of the screen.
<figure><figcaption>The Share button, which shares a project by URL.</figcaption></figure>
You have two options for sharing a project. The default is to share with the code. When you choose to share with code, others following your URL can see both the running program and the code that you’ve written. The other choice is to share without the code. When you choose to share without code, your URL will point straight to the running program, but it cannot be used to view your code.
<figure></figure>
Sharing without code is mainly used in two situations. The first is where you really want to keep your code secret, such as if you are creating an assignment where you want to give your own students an example of what their program should do, but do not want them to have the code to copy. The second is when you are embedding your CodeWorld program into another page, like a blog post, gallery, or other web site. In this case, the full CodeWorld environment and code editor would just get in the way.
What happened
Two weeks ago, I partially broke shares without code. That is, while you could still share your program with code, removing the code no longer worked correctly. Even worse, in some ways, was the fact that it did appear to work, but the links that you shared would stop working at a later time.
The consequence of this was mainly that other resources that embed or link to CodeWorld programs would now show blank white pages where the programs were supposed to be. The most important thing I’m aware of that broke is the first few weeks of Joachim Breitner’s CIS 194 lecture notes at http://www.seas.upenn.edu/~cis194/fall16/, which embed a large number of CodeWorld programs into some of the pages. That looked something like this:
<figure><figcaption>CodeWorld embedded into CIS 194 notes</figcaption></figure>
As of the early morning of Friday, August 3rd, all links should be working again. Therefore, these resources were broken for about two weeks. During this period, there were approximately 8,000 attempts to view shared CodeWorld programs that failed to load.
The bug that tracked this as it was happening is here.
A red herring
Initially, I misdiagnosed the problem. Once I noticed the thousands of errors in the server logs, I picked one of the errors to reproduce, so I could watch it occur and find out what went wrong. Something odd happened!
All shared code is stored on the server in files based on a hash of the source code. I discovered that the program that had failed was stored in a different hash than the one computed from its source code! This was suspicious, and I set out immediately to figure out why it was happening.
This was a mistake. I still don’t know why the hash originally computed for that program is different from the one computed today. Maybe there was a bug in the hashing algorithm, in some older version of that library? Who knows, really! In any case, I now do know that this has nothing to do with the shared program outage. In fact, once the code is stored, it no longer matters at all how its file name was computed.
The bad news is that this cost me hours of debugging time. The good news, though, is that I now understand that changing a hash function is not a disaster for CodeWorld. This frees me up to move to a new hash function in the future, instead of the very sub-optimal choice of MD5 that I made seven years ago!
Why it really happened
When students write code in CodeWorld, it’s written in a dialect of Haskell. In order to run, it needs to be translated to JavaScript. In the past, CodeWorld would store the original Haskell and the translated JavaScript code in the same directory. When a new version of the CodeWorld library is released, part of the process is to delete all that translated JavaScript so that it will be re-translated when needed, using the new library.
As part of an effort to make CodeWorld more scalable for more students, I moved all data from one server’s local disk to a network filesystem (NFS) on July 20th. This made walking through all the directories of shared programs and deleting old translated JavaScript about a thousand times slower! That was too much. In order to make it faster, I moved the translated JavaScript code to a new directory, separate from the Haskell code, so that it can be deleted in one big operation.
<figure><figcaption>Unfortunately, the message wasn’t clear the file is being opened for output!</figcaption></figure>
When I made this change, though, I needed to make sure that before translating the Haskell to JavaScript, I’d created the directory where the JavaScript is supposed to go. Before, this hadn’t been necessary, because that was the same directory where the Haskell source code already lived. But I forgot one place where this needed to happen. As a result, CodeWorld shared programs would only work if they were first run using a method that created the right directories. Once this happened once, they would work fine; but only until the next time the CodeWorld library was updated.
How it was fixed, and lessons learned
The immediate fix was to modify the translation process to always create the output directories whenever they are needed, regardless of how it was run. That change got the site back into a working state again.
<figure><figcaption>The bug fix: create output directories before writing files there!</figcaption></figure>
The next task is to prevent something similar from happening again. This problem should have been easily detected, because the web server was giving errors every time someone attempted to view a shared program (8,000 times over two weeks). Unfortunately, the existing monitoring only checks one URL to ensure it’s working. It does not look at errors from actual users. I’ve filed a bug to track extending the monitoring of the web site to look at actual user requests, and page me if a substantial number of them are failing. I’ll work on that in the near future.
The big lesson here is that CodeWorld is becoming more of a widespread shared resource. Down time doesn’t just matter during school sessions. Rather, CodeWorld is a resource that is used for documentation, demos, games, blogs, and other bits and pieces by many people. We ran into some growing pains here. The kind of monitoring I need to add would already exist in any commercial business project. Time to step up that game!
Conclusions
I do want to apologize to anyone affected by this mistake, and thank the whole community for their good will and patience. If you made one or more of the 8,000 failed requests, I hope you will keep trying, and I can win back your trust!
Thanks to our great community.

by Chris Smith at August 04, 2018 06:51 AM

August 03, 2018

Douglas M. Auclair (geophf)

July 2018 1HaskellADay Problems and Solutions

July 31st, 2018: Tuesday's #haskell problem: let's start to build a #kakuro-solver! YES! (Image via http://www.menneske.no/kakuro)
July 30th, 2018: For Monday's #haskell problem we are looking at merging databases. Monday's #haskell solution is a Set.intersection, and we see the shared data tables of the two databases.
July 24th, 2018: For Tuesday's #haskell problem we are discovering a JSON dictionary structure and pruning away non-entries. A little JSON dictionary exploration with #haskell gets us to our solution today.
July 17th, 2018: For Tuesday's #haskell problem we parse bits o' data from more extensive JSON.
July 11th, 2018: Wednesday's #haskell problem is going from an 'iffy' JSON structure to PERFECT (well: less 'iffy') JSON structure.
July 10th, 2018: For Tuesday's #haskell problem we explore and structure illtempered JSON. When JSON looks normal, but it's not quite, you call ... AESON on wings of eagles for Tuesday's #haskell solution.
July 9th, 2018: In Monday's #haskell problem we discover structure in mondo JSON. Monday's #Haskell solution revealed itself in the first 300 characters of prettiness!
July 3rd, 2018: For Tuesday's #haskell problem we translate the graph-like JSON to a set of relations, viewable in a graph database. For Tuesday, #haskell's graph-solution using Relation values and, ooh! pretteh pictures!

by geophf (noreply@blogger.com) at August 03, 2018 04:16 AM

August 01, 2018

Roman Cheplyaka

Probability of a regex occurrence

Given a regular expression $R$ and a random string $L$ of length $n$, what is the probability that $R$ matches somewhere in $L$?

This seems like an intimidating problem at first, but I was surprised how easy it becomes after a couple of insights.

The first insight is to turn a regex into a DFA. This moves us from “how can I possibly know whether a regex matches?” to “feed the string to the automaton and see if it ends up in an accepting state”.

Still, the DFA can be anything at all — how do we know the probability of ending up in an accepting state? The second insight is to ascribe probabilities to the edges (transitions) of the DFA and observe that this turns it into a Markov chain¹.

Why is that helpful? Because a Markov chain can be represented by its transition matrix $P$, and the probability of getting from any state $a$ to any state $b$ can be computed in logarithmic time by computing $P^n_{ab}$, the $a,b$-th element of the $n$-th power of the matrix $P$.

So how do we assign the probabilities to DFA transitions? If all characters are equally likely, $P_{ab}$ is simply the number of characters that move the DFA from state $a$ to state $b$ divided by the number of all possible characters. More generally, if every letter $l$ has a fixed probability $p_l$, we compute \[ P_{ab}=\sum_{a\overset{l}{\rightarrow} b}p_l, \] where the summation is over all characters $l$ that lead from $a$ to $b$.

And to get the probability of the regex $R$ matching anywhere inside the string as opposed to matching the whole string, replace $R$ with ${.}{*}R{.}{*}$ before compiling it to a DFA. Then calculate

\[ \sum_{f\in F} P^n_{sf}, \] where $s$ is the start state of the DFA, and $F$ is the set of accepting states.

Here’s a simple implementation of this algorithm. (The library code supports full regular expressions over arbitrary finite alphabets, but the command line tool only accepts simple IUPAC patterns over the DNA alphabet.)

References

There is nothing new or original here — specialists know how to solve this and even more involved problems. For these more involved problems, generating functions are typically used. It’s nice, however, that for this specific case, simple matrix exponentiation suffices.

For example, Nicodème, Salvy and Flajolet (2002) show how to use generating functions to calculate the probability distribution of the number of occurrences of a regex, both overlapping and non-overlapping, as well as the mean and variance of that number. They also derive the asymptotics and handle (first-order) Markov dependencies between the consequtive positions in $L$. But for our task — the probability of a regex occurring at least once — their method essentially reduces to the one described here.

Régnier (2000) also uses generating functions but explicitly models possible overlaps between patterns, which allows her to analyze regular expressions more efficiently than Nicodème et al. (see page 20).

Filion 2017 is a very accessible introduction to the paradigm of transfer graphs, which are a bridge between DFAs, transition matrices, and generating functions.
<section class="footnotes">

Here I assume that different positions in $L$ are independent.↩

</section>

August 01, 2018 08:00 PM

Functional Jobs

Scala developer for NetLogo at Northwestern University (Full-time)

Job Summary

The CCL Lab at Northwestern University is looking for a full-time Scala/Java Software Developer to work on the NetLogo desktop application, a celebrated modeling environment used in both education and research.

This Software Developer position is based at Northwestern University's Center for Connected Learning and Computer-Based Modeling (CCL), working in a small collaborative development team in a university research group that also includes professors, postdocs, graduate students, and undergraduates, supporting the needs of multiple research projects. A major focus would be on development of NetLogo, an open-source modeling environment for both education and scientific research. CCL grants also involve development work on HubNet and other associated tools for NetLogo, including research and educational NSF grants involving building NetLogo-based science curricula for schools.

NetLogo is a programming language and agent-based modeling environment. The NetLogo language is a dialect of Logo/Lisp specialized for building agent-based simulations of natural and social phenomena. NetLogo has many tens of thousands of users ranging from grade school students to advanced researchers. A collaborative extension of NetLogo, called HubNet, enables groups of participants to run participatory simulation activities in classrooms and distributed participatory simulations in social science research. NetLogo can also be extended to interface with external software such as R, Mathematica and Python.

Application information:

The Northwestern campus is in Evanston, Illinois on the Lake Michigan shore, adjacent to Chicago and easily reachable by public transportation.

Specific Responsibilities:

Collaborates with the NetLogo development team in designing features for NetLogo and other related software;

Writes Scala/Java code independently, and in the context of a team of experienced software engineers and principal investigator;

Interacts with commercial and academic partners to help determine design and functional requirements for NetLogo and other related software;

Interacts with user community including responding to bug reports, questions, and suggestions, and interacting with open-source contributors;

Mentors undergraduate student workers and guide Google Summer of Code participants on contributions to the NetLogo codebase; assists graduate students with issues encountered during their work;

Performs data collection, organization, and summarization for projects; assists with coordination of team activities;

Participates in the design of web-based applications, including NetLogo Web.

Performs other duties as required or assigned.

Minimum Qualifications:

A bachelor's degree in computer science or a closely related field or the equivalent combination of education, training and experience from which comparable skills and abilities may be acquired;

Demonstrated experience and enthusiasm for writing clean, modular, well-tested code.

Preferred Qualifications:

Experience with working effectively as part of a small software development team, including close collaboration, distributed version control, and automated testing;

Experience with at least one JVM language, Scala strongly preferred;

Experience developing GUI applications, especially Java Swing-based applications;

Experience with programming language design and implementation, functional programming (especially Haskell or Lisp), and compilers;

Interest in and experience with computer-based modeling and simulation, especially agent-based simulation;

Interest in and experience with distributed, multiplayer, networked systems like HubNet;

Experience working on research projects in an academic environment;

Experience with open-source software development and supporting the growth of an open-source community;

Experience with Linux/Unix system administration;

Experience with building web-based applications, both server-side and client-side components, particularly with html5 and JavaScript and/or CoffeeScript;

Interest in education and an understanding of secondary school math and science content.

As per Northwestern University policy, this position requires a criminal background check. Successful applicants will need to submit to a criminal background check prior to employment.

Northwestern University is an Equal Opportunity, Affirmative Action Employer of all protected classes including veterans and individuals with disabilities.

Get information on how to apply for this position.

August 01, 2018 07:38 PM

FP Complete

Pantry, part 3: Specifying Dependencies

This is part three of a series of blog posts on Pantry, a new storage and download system for Haskell packages. You can see part 1 and part 2.

by Michael Snoyman (michael@fpcomplete.com) at August 01, 2018 05:28 PM

July 30, 2018

Joachim Breitner

The merits of a yellow-red phase

In my yesterday post on Continuity Lines in North America I mentioned in passing that I am big fan of German¹ traffic lights, which have a brief yellow-red phase between the red and and the green phase (3 to 5 seconds, depending on road speed). A German reader of my blog was surprised by this, said that he considers it pointless, and would like to hear my reasons. So where we go…

Life without Yellow-Red

Lights that switch directly from red to green cause more stress. Picture yourself at the first car waiting at a traffic light, with a bunch of cars behind you. Can you relax, maybe observe the cars passing in front of you, switch the radio station, or simply look somewhere else for a moment? Well, you can, but you risk missing how the light switches from red to green. When your look at the traffic light again and see it bright green, you have no idea how long it has been on green. Hyper-aware of all the cars behind you waiting to get going, you’ll rush to get started, and if you don’t do that really fast now, surely one of the people waiting behind you will have honked.

So at the next intersection, you better don’t take your eyes off the light – or, alternatively, you develop a screw-you-I-don’t-care-attitude towards the other cars, which might allow you to relax in this situation, but is in general not desirable.

Maybe this is less of a problem on the West Coast, where supposedly everybody is nice, relaxed, and patient, and you can take all the time you want to get rolling. But in the stereotypical East Coast traffic full of angry, impatient and antisocial drivers, you really don’t get away with that.

Life with Yellow-Red

The yellow-red phase solves this problem elegantly: As long as the light is red, you don’t have to watch the light constantly and with maximum attention. You can relax: it suffices to check it often enough to catch the red-yellow phase, once every two or three seconds. When you see it, you get ready to start; and when it actually turns green, you start on time.

I would expect that it is not only less stressful, it is also more efficient: Because every car in the lane has the heads-up warning “green in a moment”, the cars can start rolling in quicker succession. Without the warning, every car to account much more for the possible slower reaction of the car before.

PS: A friend of mine wonders whether the German Yellow-Red is needed because cars with manual transmissions are much more common in Germany than in the US, and you need more time to, well, get into gear with these cars.

Also Great Britain, Croatia, Latvia, Norway, Austria, Poland, Russia, Saudi-Arabia, Sweden, Switzerland, Hungary and others.↩

by Joachim Breitner (mail@joachim-breitner.de) at July 30, 2018 09:41 PM

FP Complete

Streaming UTF-8 in Haskell and Rust

Since I seem to be a one-trick pony, I decided to write yet again to compare streaming data in Haskell and Rust. This was inspired by a cool post I saw on Reddit about converting characters in the Latin alphabet into look-alikes in the Cyrilic alphabet.

by Michael Snoyman (michael@fpcomplete.com) at July 30, 2018 09:00 AM

Joachim Breitner

Continuity Lines

I am currently on a road trip going from Philly going North along the Atlantic Coast into Canada, and aiming for Nova Scotia. When I passed from the US into Canada, I made had an unexpected emotional response to the highways there: I felt more at home!

And I believe it has to do with the pavement markings on US vs. Canadian freeways.

Consider this image, taken from the Manual on Uniform Traffic Control Devices of the United States, an official document describing (among other things) how the pavement of a freeway ought to be paved:

Parallel Deceleration Lane for Exit Ramp

This is a typical exit ramp from the freeway. On ramps and cloverleaf ramps look similar. Note that the right-most lane goes somewhere else than the left and the middle lane, yet the lanes look completely identical. In particular, the lines between the lanes are shaped the same!

Now, for comparison, the corresponding image in a Canadian manual, namely the Manual of Standard Traffic Signs & Pavement Markings for British Columbia:

Canadian off-ramps

Here, there are different lines between the different lanes: normal lane lines left, but a so-called continuity line, with a distinctly different pattern, between the normal lanes and the exit lane. It’s like in Germany!

With this is mind I understand one reason¹ why driving in the US² noticeably more stressful: There is just always anxiety whether you are accidentally in an exit lane!

Update (2018-07-30): AS Paul Johnson pointed out (see comment below), I was looking at an old version of the MUTCD. The current version, from 2009, has these lines:

Current US off-ramps

They have published a (very long) document describing the changes in the new version of the manual , and Section 306 describes the rationale:

[..] the FHWA adopts language to clarify that dotted lane lines, rather than broken lane lines, are to be used for non-continuing lanes, including acceleration lanes, deceleration lanes, and auxiliary lanes. [..] a number of States and other jurisdictions currently follow this practice, which is also the standard practice in Europe and most other developed countries. The FHWA believes that the existing use of a normal broken lane line for these non- continuing lanes does not adequately inform road users of the lack of lane continuity ahead and that the standardized use of dotted lane lines for non-continuing lanes as adopted in this final rule will better serve this important purpose in enhancing safety and uniformity.

So all is well! But it means that either Pennsylvania was slower than allowed in implementing these changes (the deadline was December 2016), or it was something else alltogether that made me feel more at home on the Canadian freeway.

I say “one reason”, not “the reason”, because there are many more – “Rechtsfahrgebot”, no red-and-yellow-phase in the traffic light, Pennsylvanian road quality…↩

Supposedly, Pennsylvania is particularly bad with roads in general, but also with this particular problem, and California has exit lanes clearly separated. But, of course, because this is the US, not using the same patter as the others (Canada, Europe), but using spaced dots…↩

by Joachim Breitner (mail@joachim-breitner.de) at July 30, 2018 12:25 AM

July 28, 2018

Chris Smith 2

Novices and motivation when learning to code

<figure><figcaption>Motivated children learning to code (CSUF Photos)</figcaption></figure>
Experts in any field don’t just know more; they also use different schemata for categorizing concepts and tasks. For example, chess masters understand games in terms of important configurations of pieces, instead of individual moves. Children who are experts on dinosaurs look at more fundamental properties when asked to describe a new kind of dinosaur, while beginners looked for size and color. Experts in physics sort phenomena by scientific principles like inertia, entropy, and friction, but novices look at literal features like the type of object that is moving and its size or shape.
The same idea applies to computer science. Novice coders classify programs by their superficial characteristics, and not by their deeper structure. This yields both consequences and opportunities that we need to keep in mind when teaching beginners!
Novice categorization matters for motivation.
Suppose you assigned students in a beginning programming class to find the longest common substring of two strings. This is an interesting algorithm question — enough so that it has its own Wikipedia page. Your students might have to work very hard to accomplish this task, but when they finally did so, they would be proud to have accomplished something pretty impressive… right?
<figure><figcaption>Suffix tree for max substring (Joey-das-WBF, via Wikipedia)</figcaption></figure>
Probably not. In fact, to a novice programmer, the problem probably sounds pretty easy. For the examples they will think of, they don’t even need a computer at all. Your novice students won’t have the combinatorial intuition that suggests this problem is hard. In fact, part of the reason this problem made it to Wikipedia is that it doesn’t sound hard.
You may find your students feeling inadequate, because such an “easy” task was difficult for them. Perhaps you can assure them that it really was an impressive problem to solve. You could show them the Wikipedia page, and show them people whose Ph.D. or tenure was earned by making a breakthrough on this task. They might understand, but alas, they probably won’t feel it deep inside.
Novice categorization presents opportunities, as well.
One you’re aware of this phenomenon, you can also use it to improve your students’ experiences. There are all sorts of opportunities for students to get excited about what they are doing, if you can get over that expert voice in your head, warning you that this doesn’t matter.
When I teach programming in middle schools using CodeWorld, we start by drawing circles and rectangles. The screen is set up as a coordinate plane.
<figure><figcaption>A circle on the CodeWorld coordinate plane</figcaption></figure>
In every class, there is a student who now announces that they are going to make a circle with a radius of one million! In expert mode, I want to stop them, and tell them to try reasonable numbers. But they would then learn that I don’t want them to try ambitious things — because to the novice, this is being ambitious. But in novice mode, I can get excited with them, and encourage them to try it. Of course, they don’t see anything at all, because the circle is outside the screen.
The first time this happened, I expected disappointment; but that’s not what I saw. They think it’s awesome that they made a circle so big it doesn’t even fit on their screen. Then someone says “Oh! I’m doing 999999999999999!” They know they aren’t going to see anything either, but just being able to tell a computer to do these ridiculous things is empowering, and they love it.
This doesn’t end on the first day. Later we animate shapes moving or spinning at different speeds. You guessed it: they want to shapes to move really fast. A million! Again, the result is not interesting to the expert brain, which screams “It will be off the screen after one frame!” and “Spinning that much faster than the frame rate will just break the illusion of motion, which depends on continuity!” These things don’t matter. Kids still think it’s hilarious and amazing. These are their favorite moments.
What would it mean to teach for a novice mindset?
These are just a few moments. What would happen if we reviewed our entire experience teaching introductory programming, and optimized it to motivate novices, who don’t yet have an expert schema for classifying tasks? I don’t know the full answer, but I have a few ideas.
First, we’d skip the command line for a while. There’s a long tradition of teach programming from the command line (starting with the timeless “Hello, world!”). Up through the 1970s, that was just how you used computers. Now, the command line isn’t just unfamiliar to many of our children, buried in the System menu; it isn’t even available on the computers they use most — mobile phones and tablets. When they do learn to use it, well, it doesn’t blow them away.
The command line is a natural starting point for experts, not just because it’s a tool we use regularly, but also because it’s simple. I/O can be messy, so we take the easy way out of it, so we can focus on the interesting part: the logic, the control flow, the data structures, etc. But that’s only the interesting part in the expert schema! To a novice, the I/O is the interesting part. They have less appreciation for the control flow and data structures, but they do know that printing characters to standard output isn’t what they had in mind.
Second, we’d take advantage of simple pleasures to get students to slow down on the basics. I think everyone who has taught coding has the experience of students who declare they want to build a top-tier game… but they’ve only written a bit of HTML in the past and are struggling with basic assignments. Sometimes we try to scaffold these students to the point that they can approach their goals; but often, those scaffolds can never be removed, leaving students unable to work independently, but with expectations set too high to fill in their fundamental skill gaps.
The good news is that your students don’t need to build these advanced projects. They usually have goals too ambitious for their skills not because they are just arrogant, but because they don’t understand why their goals are so challenging. In my CodeWorld class, I spend the first month or two working on still drawings, then move on to animations. These are tasks that can be made easy enough for beginners, and whose progress is immediate and visual. Dr. Felienne reports that she found a huge number of Scratch projects that students proudly share are just animations. She argues convincingly that experts would tend to dismiss these as not “real” programs, but this robs students of a chance to learn the basics.
Third, we’d stop trying to teach by isolating skills, and instead try to pair steps in difficulty with steps in motivation. The learning cycle often looks like this: identify the next skill that students need, explain it in detail, then assign them practices that isolate that skill until they’ve mastered it. But if you don’t understand the point of these isolated skills, this can feel soul-crushing.
I recently made a change to my CodeWorld curriculum to correct a mistake of this type. We used to progress from drawings to animations, and then to simulations. Animations are stateless programs that simply assign a picture to each instant in time. Simulations, on the other hand, are stateful. To create one, you describe an initial state, and then give a rule for how the state changes over time — basically describing a dynamical system. You can do cool stuff like simulate a bouncing ball by writing functions for rules like inertia, gravity, and elasticity.
I knew that students often struggled and lost motivation at this point in the course, but it seemed that this was a necessary step toward building interactive games. After all, games must be stateful, right? Instead of introducing both events and state at the same time, I wanted to introduce just state, and then add events as a second step.
Well, I was wrong. It turned out that students weren’t very interested in this new “simulation” thing. It opened lots of doors for them to make things move in more complex and interesting ways; but to them, “make stuff move” was a goal they had already accomplished. As we explored the capabilities of simulations, I was pestered by questions like “do I have to use a simulation, or can I just write an animation?” The energy level plummeted, just as we were — in my mind — gearing up toward interactive games, which is the most exciting step of all.
After understanding the novice perspective, I’ve started to modify the curriculum to introduce events first, and build up the idea of state using event handlers instead of time steps. I even modified the API to deemphasize time when building stateful programs. I have not yet taught with the new sequence, but early testing on willing subjects indicates it will go much better.
Building toward an expert schema.
We must be a little cautious, though. Appreciating the novice mindset doesn’t mean we don’t need to teach more advanced concepts at all! Eventually, we might hope that our students can work successfully on algorithm problems, appreciate their challenge, and be proud of their success. In other words, keeping students within the bounds of easy-but-superficially-impressive projects is its own kind of scaffolding.
This also requires attention. Showing students how to appreciate these deeper challenges needs to be an explicit objective. As with many things, if you leave students to figure it out on their own, some of them will, but others will struggle and never quite get it. So pretty soon, new programmers should learn an appreciation for combinatorial phenomena, a selection of algorithms, data structures, and so on.
When designing a course, it’s useful to ask how much of a mindset shift is needed for the value of each topic to be appreciated. This sets additional learning objectives and ordering constraints on how the class is presented. The ideal is that, by the time you reach the point of teaching a deeper idea, your students will have had the experience of wanting this, and not knowing how to do it!

by Chris Smith at July 28, 2018 08:58 PM

Joachim Breitner

Build tool semantic aware build systems

I just had a lovely visit at Ben Gamari and Laura Dietz, and at the breakfast table we had an idea that I want to record here.

The problem

Laura and Ben talked about the struggles they had using build systems like make or Nix in data science applications. A build system like nix is designed around the idea that builds are relatively cheap, and that any change in a dependency ought to trigger a rebuild, just to be sure that all build outputs are up-to-date. This is a perfectly valid assumption when building software, where build times are usually minutes, or maybe hours. But when some of the data processing takes days, then you really really want to avoid any unnecessary builds.

One way of avoiding unnecessary rebuilds that is supported by build systems like shake and (I presume, maybe with some extra work) Nix, is to do output hashing: If one build stage has its input changed and need to be re-run, but its output is actually unchanged, then later build stages do not have to be re-run. Great!

But even with this feature in place, there one common problem remains: Build tools! Your multi-gigabyte data is going to be processed by some code you write. What if the code changes? Clearly, if you change the algorithm, or fix a bug in your code, you want the output to be re-run. But if you just change some strings in the --help flag, or update some libraries, or do something else that does not change the program in a way that is significant for the task at hand, wouldn’t you prefer to not pay for that by futile multi-day data processing step?

Existing approaches

There are various ways you can tackle this these days:

You bite the bullet, add the build tool as a dependency of the processing step. You get the assurance that your data always reflects the output of the latest version of your tool, but you get lots of rebuilds.

You don’t track the tool as part of your build system. It is now completely up to you to decide when the tool has changed in significant ways. When you think it has, you throw away all build artifacts and start from scratch. Very crude, and easy to get wrong.

You keep track of a “build tool version”, e.g. a text file with a number, that you depend on in lieu of the build tool itself. When you make a change that you think is significant, you bump that version number. This is similar to the previous approach, but more precise: Only the build outputs that used this particular tools will be invalidated, and it also scales better to working in a team. But of course, you can still easily get it wrong.

Build tool semantics

Why are all these approaches so unsatisfying? Because none allow you to express the intent, which is to say “this build step depends on the semantics (i.e. behaviour) of the build tool”. If we could somehow specify that, then all would be great: Build tool changes, but its semantics is unaffected? no rebuild. Build tool changes, semantics change? rebuild.

This ideal is not reachable (blah blah halting problem blah blah) – but I believe we can approximate it. At least if good practices were used and the tool has a test suite!

Assume for now that the tool is a simple patch-processing tool, i.e. takes some input and produces some output. Assume further that there is a test suite with a small but representative set of example inputs, or maybe some randomly generated inputs (using a fixed seed). If the test suite is good, then the (hash of) the output on the test suite example is an approximation of the programs semantic.

And the build system can use this “semantics hash”. If the build tool changes, the build system can re-run the test suite and compare the output with the previous run. If they change, then the tools seems to have changed in significant ways, and it needs to re-run the data processing. But if the test suite outputs are unchanged, then it can assume that the behaviour of the tool has not changed, re-use the existing data outputs.

That is the core idea! A few additional thoughts, though:

What if the test suite changes? If the above idea is implemented naively, then adding a test case to the test suite will change the semantics, and re-build everything. That would be horrible in terms of incentives! So instead, the build systems should keep the old version of the build tool around, re-calculate its semantics hash based on the new test suite, and then compare that. This way, extending the test suite does not cause recompilation.

Hash-and-store-based build systems like Nix should have no problem keeping the previous version of the build tool around as long there is output that depends on it.

A consequence of this approach is that if you find and fix a bug in your tool that is not covered by the existing test suite, then you absolutely have to add a test for that to your test suite, otherwise the bug fix will not actually make it to your data output. This might be the biggest downside of the approach, but at least it sets incentives right in that it makes you maintain a good regression test suite.

What if things go wrong, the test suite is incomplete and the build system re-uses build output because it wrongly assumes that two versions of the build tool have the same semantics?

If done right, this can be detected and fixed: The build system needs to record which tool version (and not just which “semantics hash”) was used to produce a particular output. So once the test suite uncovers the difference, the build systems will no longer consider the two versions equivalent and – after the fact – invalidate the re-used of the previous build output, and re-build what needs to be rebuild

I am curious to hear if anybody has played with these or similar ideas before? How did it go? Would it be possible to implement this in Nix? In Shake? Other systems? Tell me your thoughts!

by Joachim Breitner (mail@joachim-breitner.de) at July 28, 2018 03:03 PM

July 27, 2018

FP Complete

Guide to open source maintenance

This blog post is a cross post from a guide I wrote on the Commercial Haskell Github account. That URL is the authoritative location for this document. If you want to send any updates and recommendations, pull requests certainly welcome!

by Michael Snoyman (michael@fpcomplete.com) at July 27, 2018 05:47 AM

July 25, 2018

Holden Karau

Live Code Reviews & Live Coding on OSS Big Data tools (mostly Apache Spark & Beam)

Do you want to see how large open source projects like Apache Spark and Apache Beam are developed? Then join me in some of this & next month's upcoming live streams where I'll be covering everything from writing code, setting up a new contributor's machine, reviewing PRs, all the way to improving review tooling.

All times quoted in US Pacific timezone.

For the more "traditional" live coding and dev tool set up type work:

This morning Gris & I did a quick live stream of updating one of my Beam PRs based on review feedback (and created another PR during the process) - https://www.youtube.com/watch?v=4xDsY5QL2zM. This afternoon on July 25th @ 3pm I'll be working on more review tool set up (exploring a mention-bot fork) - https://www.twitch.tv/events/vNzcZ7DdSuGFNYURW_9WEQ / https://www.youtube.com/watch?v=6cTmC_fP9B0 .

On Monday July 30th @ 9:30am I'll be doing some more coding using PySpark for data processing - https://www.youtube.com/watch?v=tKFiWKRISdc

On Thursday August 1st @ 2pm pacific Gris & I will be setting up Beam on her new laptop together, so for any new users looking to see how to install Beam from source this one is for you (or for devs looking to see how painful set up is) - https://www.twitch.tv/events/YAYvNp3tT0COkcpNBxnp6A / https://www.youtube.com/watch?v=x8Wg7qCDA5k

At a few folks requests I'll do a more Scala focused live stream on Apache Spark (exact PR TBD we'll go through Jira together and find a topic that looks fun) on August 6th @ 10 am - https://www.youtube.com/watch?v=w4IAdU0aVwo and in the afternoon @ 2pm I'll do a Beam focused one - https://www.youtube.com/watch?v=awhQzPIdoaE

On the code review side:

I have a few code review sessions scheduled for July/August, the dates float around a little bit because of travel plans instead of every Friday like I hoped, but they will be on July 27th @ 10am ( https://www.youtube.com/watch?v=O4rRx-3PTiM ), August 10th at 9am ( https://www.youtube.com/watch?v=Ary8WD1v7QA ) , August 16th at 8am ( https://www.youtube.com/watch?v=eg7Lo8KSN2U ) and August 24th at 2pm ( https://www.youtube.com/watch?v=kolojT8nPCU )

I've also tried to create events for this month on YT and twitch - https://youtube.com/user/holdenkarau & https://www.twitch.tv/holdenkarau/events

I'll probably fit some more things in as my conference schedule settles down a bit.

P.S.

As always if you have any requests (for PRs reviewed or areas) just give me a shout :)

I also have 2 talks coming up this month, August 24th in New York https://conferences.oreilly.com/jupyter/jup-ny/public/schedule/speaker/128567 & August 30th in Vancouver - https://ossna18.sched.com/event/FAOJ/introducing-kubeflow-a-system-for-deploying-mlai-on-kubernetes-trevor-grant-ibm-holden-karau-google

by Holden Karau (noreply@blogger.com) at July 25, 2018 08:06 PM

July 22, 2018

Joachim Breitner

WebGL, Fragment Shader, GHCJS and reflex-dom
What a potpourri of topics... too long to read? Click here!

On the side and very slowly I am working on a little game that involves breeding spherical patterns… more on that later (maybe). I want to implement it in Haskell, but have it run in the browser, so I reached for GHCJS, the Haskell-to-Javascript compiler.

WebGL for 2D images

A crucial question was: How do I draw a generative pattern onto a HTML canvas element. My first attempt was to calculate the pixel data into a bit array and use putImageData() to push it onto the canvas, but it was prohibitively slow. I might have done something stupid along the way, and some optimization might have helped, but I figured that I should not myself calculate the colors of each pixel, but leave this to who is best at it: The browser and (ideally) the graphic card.

So I took this as an opportunity to learn about WebGL, in particular fragment shaders. The term shader is misleading, and should mentally be replaced with “program”, because it is no longer (just) about shading. WebGL is intended to do 3D graphics, and one sends a bunch of coordinates for triangles, a vertex shader and a fragment shader to the browser. The vertex shader can places the vertices, while the fragment shader colors each pixel on the visible triangles. This is a gross oversimplification, but that is fine: We only really care about the last step, and if our coordinates always just define a rectangle that fills the whole canvas, and the vertex shader does not do anything interesting, then what remains is a HTML canvas that takes a program (written in the GL shader language), which is run for each pixel and calculates the color to be shown at that pixel.

Perfect! Just what I need. Dynamically creating a program that renders the pattern I want to show is squarely within Haskell’s strengths.

A reflex-dom widget

As my game UI grows, I will at some point no longer want to deal with raw DOM access, events etc., and the abstraction that makes creating such user interfaces painless is Functional Reactive Programming (FRP). One of the main mature implementations is Ryan Trinkle's reflex-dom, and I want to use this project to get more hands-on experience with it.

Based on my description above, once I hide all the details of the WebGL canvas setup, what I really have is a widget that takes a text string (representing the fragment shader), and creates a DOM element for it. This would suggest a function with this type signature
fragmentShaderCanvas ::
    MonadWidget t m =>
    Dynamic t Text ->
    m ()
where the input text is dynamic, meaning it can change over time (and the canvas will be updated) accordingly. In fact, I also want to specify attributes for the canvas (especially width and height), and if the supplied fragment shader source is invalid and does not compile, I want to get my hands on error messages, as provided by the browser. So I ended up with this:
fragmentShaderCanvas ::
    MonadWidget t m =>
    Map Text Text ->
    Dynamic t Text ->
    m (Dynamic t (Maybe Text))
which very pleasingly hides all the complexity of setting up the WebGL context from the user. This is abstraction at excellence!

I published this widget in the hackage.haskell.org/package/reflex-dom-fragment-shader-canvas package on Hackage.

A Demo

And because reflex-dom make it so nice, I created a little demo program; it is essentially a fragment shader playground!

On https://nomeata.github.io/reflex-dom-fragment-shader-canvas/ you will find a text area where you can edit the fragment shader code. All your changes are immediately reflected in the canvas on the right, and in the list of warnings and errors below the text area. The code for this demo is pretty short.

A few things could be improved, of course: For example, the canvas element should have its resolution automatically adjusted to the actual size on screen, but it is somewhat tricky to find out when and if a DOM element has changed size. Also, the WebGL setup should be rewritten to be more defensively, and fail more gracefully if things go wrong.

BTW, if you need a proper shader playground, check out Shadertoy.

Development and automatic deployment

The reflex authors all use Nix as their development environment, and if you want to use reflex-dom, then using Nix is certainly the path of least resistance. But I would like to point out that it is not a necessity, and you can stay squarely in cabal land if you want:

You don’t actually need ghcjs to develop your web application: reflex-dom builds on jsaddle which has a mode where you build your program using normal GHC, and it runs a web server that your browser connects to. It works better with Chrome than with Firefox at the moment, but is totally adequate to develop a program.

If you do want to install ghcjs, then it is actually relatively easily: The README on the ghc-8.2 branch of GHCJS tells you how to build and install GHCJS with cabal new-build.

cabal itself supports ghcjs just like ghc! Just pass --ghcjs -w ghcjs to it.

Because few people use ghcjs and reflex with cabal some important packages (ghcjs-base, reflex, reflex-dom) are not on Hackage, or only with old versions. You can point cabal to local checkouts using a cabal.project file or even directly to the git repositories. But it is simpler to just use a Hackage overlay that I created with these three packages, until they are uploaded to Hackage.

If the application you create is a pure client-based program and could therefore be hosted on any static web host, wouldn’t it be nice if you could just have it appear somewhere in the internet whenever you push to your project? Even that is possible, as I describe in an example repository!

It uses Travis CI to build GHCJS and the dependencies, caches them, builds your program and – if successful – uploads the result to GitHub Pages. In fact, the demo linked above is produced using that. Just push, and 5 minutes later the changes available online!

I know about rumors that Herbert’s excellent multi-GHC PPA repository might provide .deb packages with GHCJS prebuilt soon. Once that happens, and maybe ghcjs-base and reflex get uploaded to Hackage, then the power of reflex-based web development will be conveniently available to all Haskell developers (even those who shunned Nix so far), and I am looking forward to many cool projects coming out of that.
by Joachim Breitner (mail@joachim-breitner.de) at July 22, 2018 02:41 PM

July 19, 2018

Luke Palmer

Playground Programming

Every now and then, I have a small idea about a development environment feature I’d like to see. At that point, I usually say to myself, “make a prototype to see if I like it and/or show the world by example”, and start putting pressure on myself to make it. But of course, there are so many ideas and so little time, and at the end of the day, instead of producing a prototype, I manage just to produce some guilt.

This time, I’m just going to share my idea without any self-obligation to make it.

I’m working on Chrome’s build system at Google. We are switching the build scripts to a new system which uses an ingenious testing system that I’ve never seen before (though it seems like the kind of thing that would be well-known). For each build script, we have a few test inputs to run it on. The tests run all of our scripts on all of their test inputs, but rather than running the commands, they simply record the commands that would have been run into “test expectation” files, which we then check into source control.

Checking in these auto-generated files is the ingenious part. Now, when we want to change or refactor anything about the system, we simply make the change, regenerate the expectations, and do a git diff. This will tell us what the effects of our change are. If it’s supposed to be a refactor, then there should be no expectation diffs. If it’s supposed to change something, we can look through the diffs and make sure that it changed exactly what it was supposed to. These expectation files are a form of specification, except they live at the opposite end of the development chain.

This fits in nicely with a Haskell development flow that I often use. The way it usually goes: I write a function, get it to compile cleanly, then I go to ghci and try it on a few conspicuous inputs. Does it work with an empty list? What about an infinite list (and I trim the output if the output is also infinite to sanity check). I give it enough examples that I have a pretty high confidence that it’s correct. Then I move on, assuming it’s correct, and do the same with the next function.

I really enjoy this way of working. It’s “hands on”.

What if my environment recorded my playground session, so that whenever I changed a function, I could see its impact? It would mark the specific cases that changed, so that I could make sure I’m not regressing. It’s almost the same as unit tests, but with a friendlier workflow and less overhead (reading rather than writing). Maybe a little less intentional and therefore a little more error-prone, but it would be less error-prone than the regression testing strategy I currently use for my small projects (read: none).

It’s bothersome to me that this is hard to make. It seems like such a simple idea. Maybe it is easy and I’m just missing something.

by Luke at July 19, 2018 01:46 AM

Chris Smith 2

Teaching Algebraic Expressions with Tracking Arithmetic
I’ll share a trick that I’ve found helpful in getting students over the hump. The idea is due to John Mason, and it can be found, for example, in his chapter of the book Algebra in the Early Grades, or in the more recent And the Rest is Just Algebra, and likely other sources, as well.
The idea is to take a student who can work out a specific instance of a problem, and coax them into writing a general expression, by first going through an example with weird enough numbers.
Here’s an example that comes from my CodeWorld curriculum. Suppose you want to draw a rectangle with rounded corners. Let’s look at how we might approach this task using tracking arithmetic.
<figure><figcaption>An 8 x 6 rectangle with rounded corners of radius 1</figcaption></figure>
Step 1: Solve an easy instance.
We’ll start with a simple example. Let’s draw a rectangle that’s 8 units wide, 6 units high, and its corners have a radius of curvature of 1. First, you might sketch the result on graph paper, as in the picture above. Using CodeWorld, you can now construct this out of eight parts:
4 line segments — one from (-3, 3) to (3, 3) for the top; one from (-3, -3) to (3, -3) for the bottom, one from (-4, 2) to (-4, -2) for the left side, and one from (4, 2) to (4, -2) for the right side.
Four arcs for the corners — one from 0° to 90° centered at (3, 2); one from 90° to 180° centered at (-3, 2); one from 180° to 270° centered at (-3, -2); and one from 270° to 360° centered at (3, -2). Each arc has a radius of 1 unit.
Here’s the key definition:
pic = polyline([(-3, 3), ( 3, 3)])
 & polyline([(-3, -3), ( 3, -3)])
 & polyline([(-4, -2), (-4, 2)])
 & polyline([( 4, -2), ( 4, 2)])
 & translated(arc( 0, 90, 1), 3, 2)
 & translated(arc( 90, 180, 1), -3, 2)
 & translated(arc(180, 270, 1), -3, -2)
 & translated(arc(270, 360, 1), 3, -2)
If they’ve had enough practice in basic drawing primitives, most students can perform this task by making observations of the picture drawn on graph paper. If they can’t, then it’s too early to take the next steps.
Step 2: Solve an instance with “weird” numbers.
The next step involves repeating the same process, but using weird enough numbers. Using our 8 x 6 rectangle, the same numbers often come up in multiple ways. For example, when (3, 3) is an endpoint of a line segment, one of those 3s came about because it’s half of 6; but the other came about because it’s one less than half of 8! Our goal is to choose numbers so that it’s unlikely the same number will appear for more than one reason.
This time, let’s make the rectangle 13 x 8 instead.
<figure></figure>
The code for this one uses distinct numbers each time they come up.
pic = polyline([(-5.5, 4), ( 5.5, 4)])
 & polyline([(-5.5, -4), ( 5.5, -4)])
 & polyline([(-6.5, -3), (-6.5, 3)])
 & polyline([( 6.5, -3), ( 6.5, 3)])
 & translated(arc( 0, 90, 1), 5.5, 3)
 & translated(arc( 90, 180, 1), -5.5, 3)
 & translated(arc(180, 270, 1), -5.5, -3)
 & translated(arc(270, 360, 1), 5.5, -3)
Now we’re ready for to start getting some symbolism in the answer.
Step 3: Solve the same problem without doing arithmetic.
The key in this step is to solve the same instance as before, but refuse to do any arithmetic. So instead of a single number, you end up accumulating an arithmetic expression. For example, instead of 6.5, they should write 13/2.
This is the key step, and students will still struggle. But you have a secret weapon: you can prove they know how to do it, because they’ve already solved the problem. You’re asking them to do less than they already did.
Teacher: 6.5 is the answer, but what math operation did you do to get it?
Student: I don’t know… it’s just 6.5.
Teacher: Well, where did you get the 6.5 from?
Student: I just looked at the graph paper, and that’s where the line was.
Teacher: You drew that on your graph paper. Why did you put it there?
Student: That’s where it needed be to make a width of 13.
Teacher: And why is that?
Student: Because it’s half of 13.
Even more interesting is the 5.5. Once you’ve established that 6.5 is 13/2, you can write 5.5 as 13/2 – 1. It will often take some practice for students to be comfortable building up expressions in this way, but it helps that they’ve had plenty of practice doing the same thing with picture expressions.
The code they’ve written now has a lot more arithmetic in it.
pic = polyline([(-13/2 + 1, 8/2 ), ( 13/2 - 1, 8/2 )])
 & polyline([(-13/2 + 1, -8/2 ), ( 13/2 - 1, -8/2 )])
 & polyline([(-13/2, -8/2 + 1), (-13/2, 8/2 - 1)])
 & polyline([( 13/2, -8/2 + 1), ( 13/2, 8/2 - 1)])
 & translated(arc( 0, 90, 1), 13/2 - 1, 8/2 - 1)
 & translated(arc( 90, 180, 1), -13/2 + 1, 8/2 - 1)
 & translated(arc(180, 270, 1), -13/2 + 1, -8/2 + 1)
 & translated(arc(270, 360, 1), 13/2 - 1, -8/2 + 1)
Step 4: Replace the special numbers with variables.
If they’ve done their job well, all the “special” numbers, like width, height, and radius of curvature, now appear in the code directly. They can be simply replaced with arguments or variables, to get a general expression!
Here’s the result:
roundedRect(w, h, r)
 = polyline([(-w/2 + r, h/2 ), ( w/2 - r, h/2 )])
 & polyline([(-w/2 + r, -h/2 ), ( w/2 - r, -h/2 )])
 & polyline([(-w/2, -h/2 + r), (-w/2, h/2 - r)])
 & polyline([( w/2, -h/2 + r), ( w/2, h/2 - r)])
 & translated(arc( 0, 90, r), w/2 - r, h/2 - r)
 & translated(arc( 90, 180, r), -w/2 + r, h/2 - r)
 & translated(arc(180, 270, r), -w/2 + r, -h/2 + r)
 & translated(arc(270, 360, r), w/2 - r, -h/2 + r)
And you can now play around with different specific rounded rectangles.
<figure><figcaption>A smorgasbord of rounded rectangles using a general formula.</figcaption></figure>
This process has been helpful for me in coaxing students to express what they already know using algebra. Of course, it’s just a starting point! To become experts, students need to recognize when their example is truly general, and when they’ve made decisions that aren’t always appropriate. What happens to a rounded rectangle, for example, if the radius is greater than half of the width or height?
Good luck!
by Chris Smith at July 19, 2018 12:03 AM

July 16, 2018

Ken T Takusagawa

[xjzqtjzg] Top-heavy perfect powers

Below are a list of perfect powers b^n (b<=n) in increasing order, up to a googol. There are 2413 values. The list omits bases which are perfect powers themselves, e.g., 4^n, 8^n, 9^n.
Here is Haskell source code to compute the list. We used functions from the data-ordlist package to merge an infinite list of ordered infinite lists into a single ordered list. This seems to be a nontrivial function to write, having written it a few times ((1) and (2)) before discovering Data.List.Ordered. (Incidentally, data-ordlist is not indexed by Hoogle version 4. It is indexed by the alpha version (Hoogle 5), but Hoogle 5 cannot search by type Ord a => [[a]] -> [a].) We also used Data.List.Ordered.minus to compute the set difference of two infinite lists.
The motivation was to investigate increasing the breadth of the Cunningham project, which currently factors integers b^n +/- 1 with b restricted to {2, 3, 5, 6, 7, 10, 11, 12}. Within the original Cunningham range up to about 2^1200, there are 4357 perfect powers in the restricted set, but there would be 19256 in our expanded set.
What is the growth rate of this sequence?
2^2 2^3 2^4 3^3 2^5 2^6 3^4 2^7 3^5 2^8 2^9 3^6 2^10 2^11 3^7 5^5 2^12 3^8 2^13 5^6 2^14 3^9 2^15 6^6 3^10 2^16 5^7 2^17 3^11 2^18 6^7 5^8 2^19 3^12 7^7 2^20 3^13 6^8 5^9 2^21 2^22 3^14 7^8 2^23 5^10 6^9 3^15 2^24 2^25 7^9 3^16 5^11 6^10 2^26 3^17 2^27 5^12 2^28 7^10 6^11 3^18 2^29 2^30 3^19 5^13 7^11 2^31 6^12 3^20 2^32 5^14 2^33 10^10 3^21 6^13 7^12 2^34 5^15 3^22 2^35 2^36 6^14 3^23 7^13 10^11 2^37 5^16 2^38 3^24 11^11 6^15 2^39 7^14 5^17 3^25 10^12 2^40 2^41 3^26 6^16 11^12 5^18 2^42 7^15 3^27 2^43 12^12 10^13 6^17 2^44 5^19 3^28 7^16 11^13 2^45 3^29 2^46 5^20 10^14 6^18 12^13 2^47 3^30 7^17 2^48 13^13 11^14 5^21 2^49 6^19 3^31 10^15 2^50 12^14 7^18 3^32 2^51 5^22 6^20 13^14 11^15 2^52 3^33 2^53 10^16 14^14 7^19 5^23 12^15 3^34 2^54 6^21 2^55 11^16 3^35 13^15 5^24 2^56 7^20 10^17 6^22 2^57 3^36 14^15 12^16 2^58 5^25 15^15 3^37 11^17 7^21 2^59 13^16 6^23 10^18 2^60 3^38 5^26 14^16 12^17 2^61 7^22 3^39 2^62 6^24 11^18 15^16 5^27 13^17 2^63 10^19 3^40 2^64 12^18 7^23 6^25 14^17 3^41 2^65 5^28 11^19 2^66 15^17 10^20 3^42 13^18 2^67 6^26 5^29 7^24 2^68 12^19 3^43 14^18 2^69 11^20 17^17 5^30 3^44 10^21 6^27 2^70 7^25 13^19 15^18 2^71 3^45 12^20 5^31 2^72 14^19 6^28 11^21 3^46 7^26 2^73 10^22 17^18 2^74 13^20 15^19 5^32 3^47 6^29 2^75 18^18 12^21 7^27 2^76 3^48 11^22 14^20 10^23 5^33 2^77 6^30 17^19 3^49 13^21 2^78 15^20 7^28 12^22 5^34 2^79 18^19 3^50 11^23 10^24 14^21 2^80 6^31 19^19 3^51 2^81 5^35 13^22 7^29 17^20 2^82 15^21 3^52 12^23 6^32 2^83 11^24 10^25 18^20 5^36 14^22 2^84 3^53 7^30 19^20 2^85 13^23 6^33 3^54 17^21 5^37 15^22 2^86 12^24 10^26 20^20 11^25 2^87 7^31 3^55 18^21 14^23 6^34 2^88 5^38 3^56 13^24 2^89 19^21 12^25 10^27 7^32 15^23 17^22 11^26 2^90 3^57 6^35 5^39 20^21 2^91 14^24 18^22 3^58 2^92 21^21 13^25 7^33 5^40 2^93 10^28 6^36 12^26 11^27 19^22 3^59 15^24 2^94 17^23 2^95 20^22 3^60 14^25 5^41 7^34 6^37 18^23 2^96 13^26 10^29 21^22 3^61 12^27 11^28 2^97 5^42 15^25 19^23 2^98 17^24 22^22 6^38 7^35 3^62 14^26 2^99 20^23 10^30 5^43 3^63 13^27 2^100 18^24 11^29 12^28 6^39 2^101 21^23 7^36 3^64 15^26 19^24 2^102 5^44 17^25 22^23 14^27 10^31 2^103 3^65 6^40 13^28 20^24 11^30 7^37 12^29 2^104 23^23 18^25 5^45 3^66 2^105 21^24 15^27 6^41 2^106 3^67 19^25 17^26 10^32 14^28 7^38 5^46 2^107 22^24 11^31 13^29 12^30 3^68 2^108 20^25 18^26 23^24 6^42 2^109 5^47 3^69 15^28 7^39 10^33 21^25 2^110 24^24 17^27 14^29 19^26 11^32 3^70 2^111 13^30 12^31 6^43 5^48 22^25 2^112 7^40 20^26 3^71 18^27 10^34 2^113 23^25 15^29 6^44 5^49 2^114 3^72 11^33 21^26 14^30 17^28 24^25 19^27 13^31 12^32 2^115 7^41 3^73 22^26 2^116 5^50 10^35 6^45 20^27 18^28 2^117 15^30 3^74 23^26 11^34 7^42 2^118 14^31 12^33 13^32 5^51 17^29 21^27 3^75 6^46 19^28 2^119 24^26 10^36 2^120 22^27 3^76 7^43 5^52 18^29 2^121 20^28 11^35 15^31 6^47 14^32 12^34 2^122 3^77 13^33 23^27 26^26 17^30 10^37 21^28 2^123 5^53 19^29 7^44 3^78 24^27 2^124 6^48 11^36 22^28 2^125 15^32 18^30 3^79 20^29 5^54 12^35 14^33 13^34 2^126 10^38 7^45 23^28 6^49 17^31 3^80 26^27 2^127 21^29 19^30 5^55 11^37 2^128 24^28 3^81 15^33 2^129 12^36 7^46 6^50 18^31 22^29 14^34 13^35 10^39 20^30 3^82 2^130 5^56 17^32 2^131 23^29 11^38 3^83 26^28 19^31 21^30 6^51 7^47 2^132 5^57 12^37 15^34 10^40 24^29 2^133 3^84 13^36 14^35 18^32 22^30 20^31 2^134 6^52 28^28 5^58 3^85 7^48 17^33 11^39 2^135 23^30 19^32 2^136 21^31 10^41 12^38 3^86 26^29 15^35 13^37 5^59 2^137 6^53 14^36 24^30 7^49 18^33 3^87 2^138 22^31 20^32 11^40 17^34 2^139 5^60 28^29 3^88 10^42 6^54 12^39 2^140 19^33 23^31 7^50 21^32 13^38 15^36 14^37 29^29 2^141 26^30 3^89 5^61 18^34 11^41 2^142 24^31 6^55 20^33 3^90 22^32 10^43 2^143 17^35 7^51 12^40 5^62 2^144 28^30 3^91 13^39 19^34 15^37 14^38 23^32 6^56 21^33 2^145 11^42 26^31 29^30 3^92 18^35 7^52 2^146 10^44 5^63 24^32 20^34 12^41 2^147 17^36 22^33 30^30 6^57 3^93 2^148 13^40 15^38 14^39 5^64 19^35 11^43 7^53 3^94 2^149 28^31 23^33 21^34 10^45 6^58 2^150 18^36 26^32 12^42 3^95 29^31 5^65 2^151 17^37 20^35 24^33 7^54 22^34 13^41 2^152 30^31 3^96 11^44 14^40 15^39 6^59 10^46 19^36 2^153 5^66 31^31 21^35 3^97 23^34 28^32 2^154 12^43 18^37 7^55 2^155 6^60 26^33 17^38 3^98 13^42 29^32 5^67 20^36 11^45 24^34 2^156 22^35 14^41 10^47 15^40 3^99 2^157 30^32 19^37 7^56 6^61 12^44 5^68 2^158 21^36 23^35 18^38 3^100 31^32 28^33 2^159 13^43 11^46 17^39 10^48 26^34 14^42 20^37 2^160 7^57 3^101 15^41 5^69 6^62 29^33 24^35 22^36 2^161 12^45 19^38 3^102 30^33 2^162 21^37 5^70 11^47 18^39 10^49 13^44 7^58 23^36 6^63 2^163 3^103 28^34 31^33 17^40 14^43 2^164 15^42 20^38 26^35 3^104 5^71 12^46 22^37 2^165 24^36 29^34 6^64 7^59 19^39 2^166 11^48 10^50 3^105 33^33 13^45 18^40 30^34 21^38 2^167 5^72 23^37 14^44 17^41 15^43 2^168 3^106 6^65 28^35 7^60 31^34 12^47 20^39 2^169 26^36 10^51 22^38 5^73 11^49 3^107 24^37 19^40 2^170 29^35 13^46 6^66 18^41 2^171 3^108 7^61 21^39 14^45 33^34 17^42 30^35 5^74 23^38 15^44 2^172 12^48 10^52 3^109 20^40 11^50 34^34 2^173 28^36 6^67 31^35 26^37 22^39 13^47 2^174 7^62 5^75 19^41 24^38 3^110 29^36 2^175 18^42 14^46 12^49 21^40 17^43 6^68 15^45 3^111 2^176 10^53 23^39 11^51 5^76 33^35 30^36 7^63 2^177 20^41 3^112 13^48 28^37 2^178 34^35 31^36 6^69 22^40 19^42 26^38 5^77 24^39 14^47 2^179 3^113 12^50 18^43 10^54 35^35 7^64 15^46 29^37 17^44 11^52 2^180 21^41 3^114 23^40 6^70 2^181 5^78 13^49 20^42 30^37 33^36 2^182 3^115 7^65 19^43 28^38 10^55 14^48 12^51 22^41 2^183 34^36 31^37 26^39 11^53 24^40 5^79 18^44 6^71 15^47 3^116 17^45 2^184 21^42 29^38 35^36 2^185 13^50 7^66 3^117 23^41 5^80 20^43 2^186 10^56 6^72 12^52 30^38 14^49 33^37 11^54 19^44 2^187 3^118 22^42 28^39 15^48 18^45 24^41 2^188 26^40 17^46 5^81 7^67 34^37 31^38 3^119 6^73 13^51 21^43 2^189 10^57 29^39 35^37 23^42 2^190 12^53 20^44 3^120 11^55 14^50 5^82 7^68 2^191 19^45 6^74 30^39 15^49 33^38 22^43 3^121 18^46 2^192 17^47 28^40 13^52 24^42 10^58 26^41 5^83 37^37 2^193 31^39 21^44 34^38 3^122 12^54 7^69 11^56 6^75 2^194 14^51 29^40 20^45 23^43 35^38 3^123 2^195 5^84 15^50 19^46 18^47 10^59 2^196 13^53 17^48 22^44 30^40 6^76 7^70 3^124 33^39 2^197 28^41 24^43 12^55 11^57 5^85 26^42 21^45 37^38 14^52 2^198 3^125 31^40 34^39 20^46 2^199 23^44 6^77 29^41 15^51 10^60 7^71 38^38 19^47 5^86 3^126 13^54 2^200 35^39 18^48 17^49 11^58 22^45 12^56 2^201 30^41 3^127 6^78 24^44 33^40 14^53 28^42 2^202 5^87 21^46 26^43 7^72 10^61 3^128 2^203 31^41 20^47 15^52 37^39 34^40 13^55 23^45 19^48 2^204 29^42 11^59 6^79 18^49 5^88 12^57 17^50 3^129 38^39 7^73 2^205 22^46 35^40 14^54 10^62 2^206 3^130 30^42 39^39 24^45 21^47 5^89 28^43 6^80 26^44 33^41 2^207 15^53 13^56 20^48 11^60 3^131 7^74 12^58 2^208 31^42 23^46 19^49 37^40 17^51 18^50 34^41 29^43 5^90 2^209 3^132 10^63 6^81 14^55 22^47 38^40 2^210 35^41 7^75 3^133 21^48 24^46 13^57 15^54 30^43 2^211 11^61 5^91 39^40 12^59 26^45 28^44 20^49 33^42 6^82 2^212 3^134 19^50 17^52 10^64 23^47 18^51 40^40 2^213 31^43 14^56 7^76 37^41 5^92 34^42 29^44 3^135 2^214 22^48 11^62 6^83 13^58 15^55 2^215 12^60 38^41 21^49 35^42 24^47 3^136 30^44 10^65 5^93 2^216 20^50 7^77 26^46 28^45 17^53 19^51 39^41 18^52 33^43 2^217 14^57 23^48 6^84 3^137 11^63 31^44 2^218 40^41 5^94 13^59 22^49 29^45 12^61 3^138 34^43 15^56 37^42 7^78 2^219 10^66 21^50 41^41 6^85 2^220 24^48 3^139 38^42 20^51 35^43 5^95 17^54 30^45 14^58 19^52 26^47 2^221 18^53 28^46 11^64 23^49 7^79 3^140 33^44 39^42 2^222 13^60 12^62 6^86 10^67 15^57 5^96 31^45 22^50 2^223 29^46 3^141 40^42 34^44 2^224 37^43 21^51 7^80 14^59 24^49 20^52 17^55 11^65 6^87 2^225 41^42 3^142 19^53 18^54 5^97 26^48 38^43 35^44 30^46 13^61 12^63 10^68 28^47 2^226 23^50 42^42 15^58 3^143 33^45 2^227 39^43 7^81 22^51 6^88 5^98 31^46 2^228 3^144 11^66 29^47 21^52 14^60 40^43 17^56 34^45 2^229 20^53 10^69 37^44 24^50 18^55 19^54 13^62 12^64 3^145 5^99 2^230 6^89 7^82 26^49 41^43 15^59 30^47 23^51 28^48 35^45 38^44 2^231 3^146 11^67 42^43 22^52 2^232 33^46 5^100 14^61 10^70 39^44 6^90 21^53 31^47 17^57 3^147 2^233 7^83 12^65 13^63 29^48 43^43 20^54 18^56 19^55 24^51 2^234 34^46 40^44 15^60 37^45 5^101 3^148 2^235 26^50 23^52 6^91 11^68 30^48 28^49 41^44 7^84 10^71 35^46 2^236 14^62 38^45 3^149 22^53 12^66 13^64 5^102 2^237 17^58 33^47 21^54 42^44 18^57 20^55 3^150 31^48 6^92 39^45 19^56 2^238 29^49 15^61 24^52 7^85 11^69 43^44 2^239 34^47 5^103 10^72 3^151 40^45 37^46 26^51 23^53 14^63 2^240 12^67 44^44 28^50 6^93 30^49 13^65 22^54 3^152 2^241 35^47 41^45 17^59 38^46 7^86 5^104 21^55 18^58 2^242 20^56 33^48 19^57 11^70 15^62 3^153 10^73 42^45 31^49 29^50 6^94 2^243 24^53 39^46 14^64 12^68 5^105 2^244 3^154 43^45 34^48 13^66 7^87 23^54 26^52 40^46 37^47 2^245 28^51 17^60 22^55 30^50 6^95 11^71 3^155 44^45 10^74 21^56 2^246 18^59 5^106 15^63 35^48 20^57 19^58 41^46 38^47 2^247 7^88 45^45 33^49 3^156 12^69 14^65 24^54 31^50 29^51 13^67 2^248 42^46 6^96 39^47 5^107 23^55 3^157 2^249 11^72 26^53 10^75 34^49 17^61 43^46 22^56 7^89 28^52 2^250 15^64 37^48 40^47 18^60 30^51 21^57 3^158 19^59 20^58 6^97 5^108 12^70 2^251 44^46 14^66 35^49 13^68 41^47 38^48 2^252 3^159 24^55 33^50 10^76 11^73 29^52 45^46 7^90 31^51 2^253 5^109 23^56 6^98 17^62 42^47 3^160 39^48 26^54 15^65 2^254 46^46 22^57 18^61 34^50 12^71 21^58 28^53 19^60 20^59 2^255 43^47 14^67 30^52 3^161 37^49 13^69 5^110 40^48 7^91 10^77 6^99 11^74 2^256 35^50 44^47 24^56 3^162 2^257 38^49 41^48 33^51 29^53 17^63 31^52 5^111 23^57 15^66 2^258 45^47 12^72 7^92 3^163 6^100 26^55 18^62 22^58 42^48 14^68 39^49 2^259 13^70 10^78 19^61 21^59 20^60 11^75 34^51 28^54 46^47 3^164 2^260 5^112 30^53 43^48 37^50 40^49 2^261 47^47 6^101 7^93 24^57 3^165 35^51 17^64 12^73 15^67 2^262 44^48 33^52 29^54 23^58 5^113 38^50 10^79 41^49 31^53 18^63 14^69 13^71 11^76 2^263 3^166 22^59 26^56 19^62 21^60 45^48 20^61 6^102 7^94 2^264 42^49 39^50 28^55 34^52 3^167 5^114 30^54 2^265 46^48 12^74 15^68 37^51 17^65 10^80 43^49 24^58 2^266 40^50 6^103 3^168 11^77 13^72 14^70 47^48 7^95 35^52 18^64 23^59 2^267 5^115 29^55 33^53 44^49 31^54 22^60 19^63 38^51 3^169 41^50 26^57 21^61 20^62 2^268 48^48 6^104 12^75 2^269 10^81 45^49 28^56 5^116 3^170 7^96 39^51 15^69 42^50 34^53 17^66 11^78 30^55 2^270 13^73 14^71 24^59 46^49 37^52 2^271 3^171 18^65 43^50 23^60 40^51 6^105 5^117 35^53 19^64 2^272 22^61 29^56 47^49 20^63 7^97 21^62 33^54 10^82 12^76 31^55 3^172 26^58 38^52 44^50 2^273 41^51 11^79 15^70 48^49 13^74 17^67 5^118 2^274 6^106 28^57 14^72 3^173 45^50 34^54 30^56 39^52 2^275 42^51 24^60 7^98 18^66 10^83 3^174 23^61 2^276 12^77 37^53 19^65 46^50 5^119 22^62 6^107 20^64 21^63 43^51 40^52 11^80 29^57 35^54 2^277 26^59 3^175 15^71 31^56 33^55 13^75 47^50 7^99 14^73 17^68 2^278 38^53 44^51 41^52 5^120 28^58 3^176 2^279 10^84 6^108 48^50 18^67 12^78 24^61 30^57 34^55 2^280 45^51 39^53 11^81 19^66 42^52 23^62 3^177 7^100 20^65 22^63 5^121 2^281 21^64 13^76 15^72 37^54 46^51 14^74 6^109 29^58 2^282 26^60 17^69 40^53 35^55 3^178 43^52 50^50 10^85 31^57 33^56 2^283 12^79 5^122 47^51 38^54 7^101 18^68 28^59 11^82 3^179 44^52 41^53 2^284 24^62 6^110 30^58 19^67 48^51 34^56 13^77 23^63 2^285 15^73 20^66 3^180 22^64 39^54 21^65 14^75 45^52 5^123 10^86 42^53 2^286 17^70 7^102 37^55 29^59 26^61 12^80 3^181 6^111 2^287 11^83 46^52 35^56 31^58 40^54 33^57 43^53 18^69 50^51 5^124 2^288 28^60 3^182 13^78 38^55 47^52 24^63 19^68 2^289 10^87 15^74 7^103 51^51 41^54 44^53 14^76 30^59 23^64 6^112 20^67 22^65 21^66 34^57 2^290 3^183 17^71 5^125 12^81 48^52 11^84 39^55 2^291 45^53 42^54 26^62 29^60 3^184 37^56 18^70 7^104 2^292 6^113 31^59 10^88 13^79 35^57 5^126 33^58 40^55 46^53 2^293 15^75 43^54 19^69 14^77 3^185 28^61 24^64 50^52 38^56 20^68 12^82 2^294 23^65 11^85 21^67 17^72 22^66 47^53 30^60 41^55 6^114 7^105 3^186 44^54 5^127 51^52 2^295 34^58 10^89 39^56 2^296 48^53 13^80 18^71 26^63 29^61 3^187 52^52 45^54 42^55 15^76 37^57 14^78 2^297 5^128 31^60 6^115 19^70 35^58 11^86 12^83 7^106 33^59 3^188 2^298 24^65 40^56 28^62 20^69 46^54 17^73 43^55 23^66 21^68 22^67 10^90 2^299 50^53 38^57 30^61 5^129 3^189 13^81 6^116 47^54 2^300 41^56 34^59 18^72 44^55 7^107 51^53 14^79 26^64 15^77 11^87 2^301 12^84 3^190 29^62 39^57 48^54 19^71 5^130 42^56 2^302 45^55 52^53 37^58 31^61 10^91 6^117 17^74 20^70 24^66 35^59 33^60 3^191 28^63 2^303 21^69 23^67 7^108 22^68 40^57 13^82 53^53 46^55 43^56 2^304 5^131 30^62 3^192 38^58 18^73 11^88 14^80 12^85 15^78 50^54 2^305 6^118 34^60 41^57 47^55 26^65 10^92 44^56 19^72 3^193 2^306 7^109 29^63 51^54 5^132 39^58 17^75 20^71 2^307 13^83 31^62 48^55 24^67 37^59 42^57 21^70 3^194 45^56 23^68 6^119 28^64 22^69 33^61 35^60 52^54 11^89 2^308 12^86 14^81 18^74 15^79 40^58 7^110 5^133 10^93 2^309 3^195 30^63 43^57 53^54 46^56 38^59 2^310 19^73 6^120 26^66 34^61 50^55 17^76 3^196 41^58 54^54 13^84 29^64 2^311 47^56 5^134 20^72 44^57 11^90 7^111 24^68 39^59 21^71 12^87 51^55 2^312 31^63 23^69 22^70 14^82 3^197 10^94 28^65 15^80 37^60 18^75 33^62 42^58 48^56 6^121 35^61 2^313 45^57 5^135 52^55 3^198 40^59 2^314 30^64 19^74 7^112 13^85 43^58 17^77 11^91 46^57 38^60 26^67 2^315 53^55 6^122 3^199 34^62 12^88 20^73 10^95 29^65 5^136 2^316 14^83 50^56 41^59 21^72 24^69 15^81 54^55 47^57 22^71 44^58 23^70 18^76 3^200 2^317 31^64 39^60 7^113 28^66 51^56 37^61 33^63 6^123 55^55 2^318 35^62 5^137 42^59 13^86 11^92 48^57 45^58 3^201 19^75 17^78 10^96 30^65 2^319 12^89 52^56 40^60 26^68 14^84 20^74 2^320 7^114 38^61 43^59 3^202 15^82 46^58 5^138 34^63 6^124 29^66 21^73 53^56 24^70 2^321 22^72 18^77 23^71 41^60 50^57 11^93 3^203 13^87 2^322 31^65 28^67 44^59 47^58 10^97 54^56 39^61 12^90 5^139 33^64 19^76 7^115 17^79 37^62 2^323 6^125 35^63 51^57 3^204 42^60 14^85 55^56 30^66 48^58 2^324 45^59 20^75 15^83 26^69 40^61 3^205 52^57 2^325 21^74 5^140 11^94 56^56 18^78 38^62 29^67 24^71 22^73 10^98 43^60 34^64 13^88 7^116 23^72 6^126 46^59 2^326 12^91 53^57 3^206 41^61 28^68 31^66 17^80 2^327 19^77 50^58 5^141 14^86 44^60 39^62 47^59 33^65 2^328 54^57 3^207 15^84 37^63 35^64 6^127 7^117 20^76 11^95 30^67 10^99 42^61 2^329 51^58 26^70 13^89 21^75 18^79 45^60 48^59 55^57 3^208 5^142 12^92 40^62 22^74 2^330 24^72 23^73 29^68 38^63 52^58 34^65 6^128 2^331 43^61 56^57 17^81 14^87 3^209 7^118 19^78 46^60 28^69 31^67 2^332 5^143 15^85 11^96 41^62 10^100

by Ken (noreply@blogger.com) at July 16, 2018 06:54 AM

Chris Smith 2

CodeWorld Update — July 14, 2018

Here’s some of the latest news with CodeWorld.
Classes and curriculum. I’m working on a whole slew of new CodeWorld learning opportunities for students and Haskell beginners. There’s also exciting news about resources for teaching.
I’ll be teaching at one or two schools in New York, with details still to be announced once scheduling is finalized. I’m very excited that it looks like I’ll be able to teach during the school day several times per week. I hope that fixes some of the logistic challenges of teaching an after-school activity once per week.
I’m also trying to set up some teaching in Atlanta on the weekends. It looks like this will include a class for adult Haskell beginners, using the Haskell dialect of CodeWorld. I’m looking forward to that one. If you’re in Atlanta and looking to get into Haskell in a gentle way, stay tuned.
There’s also ongoing work on cleaning up some of the resources I use for teaching. The main effort is winding down here, but I think the results will speak for themselves through the next school year, which will create some deadlines to clean up and release parts. I’m also looking forward to supporting more of the work Fernando Alegre and Juana Moreno and their colleagues are doing at LSU on high school computational thinking curriculum.
Platform. The gist of this is that we continue to make progress on making the development environment more powerful and easier to use, while being careful to keep it simple and intuitive. We’ve also been moving to slowly incorporate what we’ve all learned from our teaching experience, while minimizing the impact of changes on students.
I’ve started to formalized a deprecation process for CodeWorld. Instead of just removing things when it seems right, I’m now trying to avoid making breaking changes except in the summers (in the northern hemisphere), because this minimizes the impact on currently running classes. Deprecation warnings now include specific timelines for when things will be removed, so you can plan ahead.
Two big deprecation changes are now in progress. First, we’re committing to the migration from main to program as the name of the entry point in the CodeWorld dialect. This will affect 100% of programs, so it’s a big one! Second (and this affects both the CodeWorld and Haskell dialects), we’re moving away from simulations and interactions as concepts, and toward activities. The big change here is that the passage of time is modeled as an Event value, using the constructor TimePassing, instead of a separate function. This makes it easier to teach event handling before time steps, which is much better for maintaining energy and motivation in the learning process.
Another less major deprecation is the move from text to lettering. This is a simple rename, but it helps to address a common source of confusion by students: that it’s unclear when they have a value of type Text versus Picture.
Krystal Maughan has been doing some cool work with the development UI. The most visible is that she’s added a debug slider so you can change the speed at which animations and simulations run. Krystal is now working on a time-traveling debugger to go with it, so you can go back and review what went wrong in the past.
Also because of Krystal’s work, you can now resize a running program on the web site, by dragging the divider between your code and the program. This was a long-standing limitation that Krystal fixed in a night.
Robert Cook added a new local SQLite-based authentication system, which you can use if you want to run your own version of CodeWorld. This eliminates the dependency on Google accounts, but at the cost of doing your own account administration.
Branding. We have a new logo! After a lot of back-and-forth, we settled on this design a couple months ago.
<figure></figure>
Please share any other interesting stories and news in the comments.

by Chris Smith at July 16, 2018 05:12 AM

Chris Smith

I’m moving to medium for the future.

Thanks to everyone who has read my very inconsistent blog entries over the past 11 years. I am looking forward to communicating more often in the future, but it’s time to modernize my tools. I’m primarily switching to:

Twitter for status updates and short thoughts.

Medium for longer pieces.

Please feel free to follow these to stay up to date.

I still intend to leave this site here, to avoid breaking links. But at the same time, I’m looking for something to get the Medium started, so I will likely start to move some of my favorite older content to Medium as well.

by cdsmith at July 16, 2018 03:00 AM

July 15, 2018

Dominic Steinitz

Estimating Parameters in Chaotic Systems

Post available from my new site. Sadly WordPress doesn’t allow me to render the html exported by a Jupyter notebook.

by Dominic Steinitz at July 15, 2018 02:28 PM

Michael Snoyman

Post Fast Write-up

As I blogged about last week, last week I did a multiday fast. There was definitely interest in this topic on Twitter, and at least one request for a post-fast write-up. So here we go.

I fasted from about 8pm on Saturday, July 7 to 8am on Friday, July 13. This works out to 5.5 days, or 132 hours of fasting. Additionally, I had done a shorter 1.5 day fast the previous week (from Thursday, July 5 till Friday, July 6), which as you’ll see is relevant to the weight results.

That previous blog post shared some of my reasons for fasting. The short version is: there are lots of potential health benefits, but my goal right now was to try to lose some fat with minimal muscle loss.

Weight change

Since the primary goal of the fast was fat loss, let me share the numbers. I always weigh in first thing in the morning for consistency. I additionally record skinfold caliper and waist measurement approximations of body fat percentage, which should be taken with a large grain of salt. I’ll include them in the information below.

Unfortunately, I forgot to record my weight on Sunday, July 8. The most recent weigh-in I’d had before was Wednesday, July 4. I took measurements on Monday, Wednesday, and Friday (just before breaking the fast), and again Sunday morning (48 hours after breaking the fast).

Finally, for context, I am 175cm tall (5’9”).

Day Weight Body fat % (est) Fat mass (est) Lean mass (est)

July 4 81.8kg 21% 17.4kg 64.4kg

July 9 79.3kg 21% 16.9kg 62.4kg

July 11 77.7kg 20% 15.5kg 62.2kg

July 13 76.8kg 19% 14.3kg 62.5kg

July 15 78.5kg 20% 15.7kg 62.8kg

Again, take the numbers with a grain of salt: body fat measurements are not perfect. A secondary measurement I’ll get to in the next section is changes in lifting strength. Here are some takeaways:

There was a precipitous drop in weight right after starting the fast. This is expected as a loss of water weight.

Similarly, I put on almost 2kg of weight again in the 48 hours following the fast. This is again expected as I was regaining water weight. (I ended up eating around 100g of carbs over the course of Saturday.)

There was a relatively steady weight loss during the course of the fast.

To me, it looks like I lost between 2-3kg of fat from the fast, including the 1.5 days the previous week. This would come out to between 15,400 and 23,100 calories, which would mean between 2,369 and 3,554 calories per day. All of which sounds perfectly reasonable given my weight and activity level.

Strength during fast

There is a major confounding factor in measuring my strength: I’ve been recovering from a wrist injury which has affected all of my major lifts (squat, deadlift, and bench). That said: I had no major drop in strength measured by a 5 rep max during the fast. I did tire out more quickly on subsequent sets, however. I’ll have a better feel for whether I had any strength loss over the coming week.

Difficulty

This was by far the easiest fast I’ve ever tried. The second day was, as usual, the hardest day. But it wasn’t really that difficult. I had a high level of mental focus, had plenty of interesting (and some non-interesting) work tasks to perform, and plenty of phyiscal activity. In other words, I was able to distract myself from eating.

There were a few times during the week when the hunger was intense, but only for 1-2 hours at a time. There were a few times when I didn’t feel like I could focus on anything, but that seemed more to do with an overabundance of things grabbing my attention than the fast itself.

I had decided in advance that I would break my fast Friday morning. I was certainly excited to get back to eating, but when I woke up Friday morning, I did not feel ravenous, nauseous, or in any other way in need of breaking the fast. Had circumstances allowed it, I have no doubt that I could have easily kept going.

Hunger after fast

Usually after a fast it takes me a while to feel properly hungry again. I broke my fast on a (for me) relatively light meal of 2 scrambled eggs. Twenty minutes later, I added in some cheese, and then took the baby for a walk to visit my parents. That’s when the hunger really kicked in. I started snacking on anything I could get access to. I came home and fried up a pan full of tuna. I continued eating a lot throughout the day, finishing off with some large pieces of meat Miriam made for dinner.

Saturday felt much the same, though Miriam seems to think I ate less than I thought I did.

I neither measured my food intake, nor tried to restrict it in any way. As you can see from the weight chart above, between Friday morning and Sunday morning, I put on 1.7kg, which I believe would be entirely accounted for by water weight. I don’t believe I had any fat gain or “refeeding” issues,” though I acknowledge that the body fat estimates paint a different picture.

Plans for the future

This was a win for me. I have to see if it significantly impacts performance in the gym, but otherwise, I found this far easier than trying to do a prolonged weight loss “cut.” Assuming all goes well, I may try to do alternating weeks of eating a high fat, moderate protein diet, followed by a week with a multiday fast (between 3 and 5 days), and see how that affects weight and strength.

I’ll continue taking body measurements, and will share results when I have more meaningful data.

If anyone has specific questions they’d like me to answer, let me know!

July 15, 2018 05:55 AM

Day	Weight	Body fat % (est)	Fat mass (est)	Lean mass (est)
July 4	81.8kg	21%	17.4kg	64.4kg
July 9	79.3kg	21%	16.9kg	62.4kg
July 11	77.7kg	20%	15.5kg	62.2kg
July 13	76.8kg	19%	14.3kg	62.5kg
July 15	78.5kg	20%	15.7kg	62.8kg

July 14, 2018

Edward Z. Yang

A year into Backpack

It's been a year since I got my hood and gown and joined Facebook (where I've been working on PyTorch), but while I've been at Facebook Backpack hasn't been sleeping; in fact, there's been plenty of activity, more than I could have ever hoped for. I wanted to summarize some of the goings on in this blog post.

Libraries using Backpack

There's been some really interesting work going on in the libraries using Backpack space. Here are the two biggest ones I've seen from the last few months:

unpacked-containers. The prolific Edward Kmett wrote the unpacked-containers package, which uses the fact that you can unpack through Backpack signatures to give you generic container implementations with hypercharged performance (15-45%) way better than you could get with a usually, boxed representation. A lot of discussion happened in this Reddit thread.

hasktorch. hasktorch, by Austin Huang and Sam Stites, is a tensor and neural network library for Haskell. It binds to the TH library (which also powers PyTorch), but it uses Backpack, giving the post Backpack for deep learning from Kaixi Ruan new legs. This is quite possibly one of the biggest instances of Backpack that I've seen thus far.

Backpack in the Ecosystem

Eta supports Backpack. Eta, a JVM fork of GHC, backported Backpack support into their fork, which means that you can use Backpack in your Eta projects now. It was announced in this Twitter post and there was some more discussion about it at this post.

GSOC on multiple public libraries. Francesco Gazzetta, as part of Google Summer of Code, is working on adding support for multiple public libraries in Cabal. Multiple public libraries will make many use-cases of Backpack much easier to write, since you will no longer have to split your Backpack units into separate packages, writing distinct Cabal files for each of them.

Backpack in GHC and Cabal

By in large, we haven't changed any of the user facing syntax or semantics of Backpack since its initial release. However, there have been some prominent bugfixes (perhaps less than one might expect), both merged and coming down the pipe:

#13955: Backpack now supports non-* kinds, so you can do levity polymorphism with Backpack.

#14525: Backpack now works with the CPP extension

#15138: Backpack will soon support data T : Nat signatures, which can be instantiated with type T = 5. Thank you Piyush Kurur for diagnosing the bug and writing a patch to fix this.

A fix for Cabal issue #4754: Backpack now works with profiling

Things that could use help

Stack support for Backpack. In Stack issue #2540 I volunteered to implement Backpack support for Stack. However, over the past year, it has become abundantly clear that I don't actually have enough spare time to implement this myself. Looking for brave souls to delve into this; and I am happy to advise about the Backpack aspects.

Pattern synonym support for Backpack. You should be able to fill a signature data T = MkT Int with an appropriate bidirectional type synonym, and vice versa! This is GHC issue #14478 We don't think it should be too difficult; we have to get the matchers induced by constructors and check they match, but it requires some time to work out exactly how to do it.

by Edward Z. Yang at July 14, 2018 11:34 PM

Magnus Therning

QuickCheck on a REST API
Since I’m working with web stuff nowadays I thought I’d play a little with translating my old post on using QuickCheck to test C APIs to the web.

The goal and how to reach it

I want to use QuickCheck to test a REST API, just like in the case of the C API the idea is to

generate a sequence of API calls (a program), then

run the sequence against a model, as well as

run the sequence against the web service, and finally

compare the resulting model against reality.

The REST API

I’ll use a small web service I’m working on, and then concentrate on only a small part of the API to begin with.

The parts of the API I’ll use for the programs at this stage are

Method Route Example in Example out

POST /users {"userId": 0, "userName": "Yogi Berra"} {"userId": 42, "userName": "Yogi Berra"}

DELETE /users/:id

The following API calls will also be used, but not in the programs

Method Route Example in Example out

GET /users [0,3,7]

GET /users/:id {"userId": 42, "userName": "Yogi Berra"}

POST /reset

Representing API calls

Given the information about the API above it seems the following is enough to represent the two calls of interest together with a constructor representing the end of a program
data ApiCall = AddUser Text
 | DeleteUser Int
 | EndProgram
 deriving (Show)
and a program is just a sequence of calls, so list of ApiCall will do. However, since I want to generate sequences of calls, i.e. implement Arbitrary, I’ll wrap it in a newtype
newtype Program = Prog [ApiCall]
Running against a model (simulation)

First of all I need to decide what model to use. Based on the part of the API I’m using I’ll use an ordinary dictionary of Int and Text
type Model = M.Map Int Text
Simulating execution of a program is simulating each call against a model that’s updated with each step. I expect the final model to correspond to the state of the real service after the program is run for real. The simulation begins with an empty dictionary.
simulateProgram :: Program -> Model
simulateProgram (Prog cs) = foldl simulateCall M.empty cs
The simulation of the API calls must then be a function taking a model and a call, returning an updated model
simulateCall :: Model -> ApiCall -> Model
simulateCall m (AddUser t) = M.insert k t m
 where
 k = succ $ foldl max 0 (M.keys m)
simulateCall m (DeleteUser k) = M.delete k m
simulateCall m EndProgram = m
Here I have to make a few assumptions. First, I assume the indeces for the users start on 1. Second, that the next index used always is the successor of highest currently used index. We’ll see how well this holds up to reality later on.

Running against the web service

Running the program against the actual web service follows the same pattern, but here I’m dealing with the real world, so it’s a little more messy, i.e. IO is involved. First the running of a single call
runCall :: Manager -> ApiCall -> IO ()
runCall mgr (AddUser t) = do
 ireq <- parseRequest "POST http://localhost:3000/users"
 let req = ireq { requestBody = RequestBodyLBS (encode $ User 0 t)}
 resp <- httpLbs req mgr
 guard (status201 == responseStatus resp)

runCall mgr (DeleteUser k) = do
 req <- parseRequest $ "DELETE http://localhost:3000/users/" ++ show k
 resp <- httpNoBody req mgr
 guard (status200 == responseStatus resp)

runCall _ EndProgram = return ()
The running of a program is slightly more involved. Of course I have to set up the Manager needed for the HTTP calls, but I also need to

ensure that the web service is in a well-known state before starting, and

extract the state of the web service after running the program, so I can compare it to the model
runProgram :: Program -> IO Model
runProgram (Prog cs) = do
 mgr <- newManager defaultManagerSettings
 resetReq <- parseRequest "POST http://localhost:3000/reset"
 httpNoBody resetReq mgr
 mapM_ (runCall mgr) cs
 model <- extractModel mgr
 return model
The call to POST /reset resets the web service. I would have liked to simply restart the service completely, but I failed in automating it. I think I’ll have to take a closer look at the implementation of scotty to find a way.

Extracting the web service state and packaging it in a Model is a matter of calling GET /users and then repeatedly calling GET /users/:id with each id gotten from the first call
extractModel :: Manager -> IO Model
extractModel mgr = do
 req <- parseRequest "http://localhost:3000/users"
 resp <- httpLbs req mgr
 let (Just ids) = decode (responseBody resp) :: Maybe [Int]
 users <- forM ids $ \ id -> do
 req <- parseRequest $ "http://localhost:3000/users/" ++ show id
 resp <- httpLbs req mgr
 let (Just (user:_)) = decode (responseBody resp) :: Maybe [User]
 return user
 return $ foldl (\ map (User id name) -> M.insert id name map) M.empty users
Generating programs

My approach to generating a program is based on the idea that given a certain state there is only a limited number of possible calls that make sense. Given a model m it makes sense to make one of the following calls:

add a new user

delete an existing user

end the program

Based on this writing genProgram is rather straight forward
genProgram :: Gen Program
genProgram = Prog <$> go M.empty
 where
 possibleAddUser _ = [AddUser <$> arbitrary]
 possibleDeleteUser m = map (return . DeleteUser) (M.keys m)
 possibleEndProgram _ = [return EndProgram]

 go m = do
 let possibles = possibleDeleteUser m ++ possibleAddUser m ++ possibleEndProgram m
 s <- oneof possibles
 let m' = simulateCall m s
 case s of
 EndProgram -> return []
 _ -> (s:) <$> go m'
Armed with that the Arbitrary instance for Program can be implemented as¹
instance Arbitrary Program where
 arbitrary = genProgram
 shrink p = []
The property of an API

The steps in the first section can be used as a recipe for writing the property
prop_progCorrectness :: Program -> Property
prop_progCorrectness program = monadicIO $ do
 let simulatedModel = simulateProgram program
 runModel <- run $ runProgram program
 assert $ simulatedModel == runModel
What next?

There are some improvements that I’d like to make:

Make the generation of Program better in the sense that the programs become longer. I think this is important as I start tackling larger APIs.

Write an implementation of shrink for Program. With longer programs it’s of course more important to actually implement shrink.

I’d love to hear if others are using QuickCheck to test REST APIs in some way, if anyone has suggestions for improvements, and of course ideas for how to implement shrink in a nice way.
<section class="footnotes">

Yes, I completely skip the issue of shrinking programs at this point. This is OK at this point though, because the generated Programss do end up to be very short indeed.↩

</section>
July 14, 2018 12:00 AM

Method	Route	Example in	Example out
`POST`	`/users`	`{"userId": 0, "userName": "Yogi Berra"}`	`{"userId": 42, "userName": "Yogi Berra"}`
`DELETE`	`/users/:id`

Method	Route	Example out
`GET`	`/users`	`[0,3,7]`
`GET`	`/users/:id`	`{"userId": 42, "userName": "Yogi Berra"}`
`POST`	`/reset`

July 13, 2018

Paul Johnson

Donald Trump is Zaphod Beeblebrox

Here are some quotes from the Hitchhikers Guide to the Galaxy, lightly edited...

One of the major difficulties ~~Trillian~~ Theresa May experienced in her relationship with ~~Zaphod~~ Donald Trump was learning to distinguish between him pretending to be stupid just to get people off their guard, pretending to be stupid because he couldn’t be bothered to think and wanted someone else to do it for him, pretending to be outrageously stupid to hide the fact that he actually didn’t understand what was going on, and really being genuinely stupid.

It is a well known fact that those people who most want to rule people are, ipso facto, those least suited to do it. To summarize the summary: anyone who is capable of getting themselves made President should on no account be allowed to do the job.

The President in particular is very much a figurehead — he wields no real power whatsoever. He is apparently chosen by the ~~government~~ voters, but the qualities he is required to display are not those of leadership but those of finely judged outrage. For this reason the President is always a controversial choice, always an infuriating but fascinating character. His job is not to wield power but to draw attention away from it. On those criteria ~~Zaphod Beeblebrox~~ Donald Trump is one of the most successful Presidents the ~~Galaxy~~ United States has ever had — ~~he has already spent two of his ten presidential years in prison for fraud..~~

by Paul Johnson (noreply@blogger.com) at July 13, 2018 10:21 PM

July 10, 2018

Philip Wadler

Lambda Days Research Track

CFP for the Lambda Days Research Track is out. Please submit!

by Philip Wadler (noreply@blogger.com) at July 10, 2018 02:10 PM

Michael Snoyman

Thoughts on Fasting

Yesterday on Twitter, a lot of people were interested in the multiday fast I’m currently doing. Since I’m awake at 4am (more on that below), now seems like a great time to explain a bit about the fasting. I will drop the major caveat at the start: I am in no way an expert on fasting. For that, you’d want Dr. Jason Fung, and likely his book The Complete Guide to Fasting. This will be my personal anecdotes version of that information.

There are many reasons to consider fasting, including:

Religious reasons. As many know, I’m a religious Jew, so this concept is not at all foreign to me, and probably helped me more easily get into fasting. However, that’s not my motivation today, or related to the rest of this blog post.

Losing weight. It’s pretty hard to put on weight when you’re not eating anything. (But you probably wanted to burn fat, not muscle, right?)

Mental clarity. Many people—myself included—report feelings of clear-mindedness and focus during a fast. I find I get some of my best writing and coding done when fasting.

Extra energy. This may seem counter-intuitive: where’s the energy coming from? We’ll get to that.

General health benefits. Fasting has been well demonstrated to help treat epilepsy, but more recently also have claims of anti-cancer benefits. It can also be a highly effective treatment for type 2 diabetes.

Alright, let’s get into the details of how to do this.

Caveats

I’ll get this out of the way right now. I am not a doctor. I cannot give you health advice. I’m telling you about what works for me, a decently healthy person without preexisting conditions. If you are taking medication, especially insulin or anything that affects your blood sugar, talk with a doctor before doing this, or at the very least read one of Dr. Fung’s books.

How to fast

The process is simple: stop eating. This isn’t a “bread and water” fast. This isn’t a “maple syrup and cayenne pepper” fast (worst TED talk I’ve ever seen by the way, I refuse to link to it). You are consuming virtually no calories. (We’ll get to virtually in a second.)

You should continue drinking water, and lots of it. Drinking green tea is helpful too, and black and herbal teas are fine. There’s also no problem with coffee. In fact: the caffeine in coffee can help you burn fat, which will help the fast progress more easily.

You should not drink any sugary drinks. (That’s not just advice for a fast, that’s advice for life too.) You should probably avoid artificial sweeteners as well, since they can cause an insulin spike, and some contain calories.

There are three other things you can include in your fast if desired:

Salts, including sodium (normal table salt), potassium, and magnesium. Personally, I’ve used a bit of normal table salt, himalayan salt, or high-potassium salt.

If you’re wondering: how do you consume the salt? Yup: I drink salt water sometimes. Delicious.

Some cream in your coffee. Don’t overdo it: you’re not making bulletproof coffee here. This is intended to just take some of the edge off of your coffee if you can’t stand black coffee.

Bone broth, essentially beef (or other) bones cooking in a crockpot with salt for 24 hours straight. This is a nice way to get in some salts, a few other trace minerals, and give you a satisfied feeling before going to sleep.

The latter two do contribute some calories, almost entirely from fat. Don’t overdo this, you’ll be counteracting the point of the fast. And definitely avoid getting protein or any carbs mixed in; do not eat some of the meat off the bones, or throw in carrots or other starchy vegetables.

If you’re doing a fast for anti-cancer reasons, I’ve read that you should eliminate the cream and broth as well, and maybe consider leaving out the coffee and even tea. Again: I’m not an expert here, and I’ve never tried that kind of fast.

When to fast

Fasting does not require any preparation. Just decide to do it, and stop eating! I typically like to stop eating around 6pm one day, and see how many days I can go before I cave in and eat. I’ll mention some reasons to cave in below.

My maximum fasting time is currently four days. It’s doubtful I’ll ever get beyond six days due to the weekly Jewish Sabbath, but that’s currently my goal. If you’re doing a multiday fast, I’d recommend targeting at least three days, since the second day is by far the hardest (from personal experience, and what I’ve read), and you should see it through till it gets easier.

By the way, the world record longest fast is 382 days. The rules for fasting change a bit at that point, and you would need to take vitamins and minerals to make it through.

Hunger

The biggest fear people have is hunger. This is a normal, natural reaction. As someone who has done fasts plenty of times, I still sometimes feel the fear of being hungry. Allow me to share some personal experience.

When I’m in the middle of eating food, the thought of purposely witholding from eating is terrifying. Once I’ve stopped eating for half a day or so, that terror seems in retrospect to be completely irrational. I strongly believe that I, like many others, can react with an almost chemical addiction-like response to food. It’s nice to occassionally break that dependence.

Many people assume that they’ll be overcome with hunger once they’ve gone somewhere around 8 hours without eating. I’d recommend thinking of it as a challenge: can you handle not eating? Your body is built to withstand times of no food, you’ll be fine. This is a straight mind-over-matter moment.

Another concern many have is memories of trying to diet, and feeling miserable the whole time. Let me relate that it is significantly easier to spend a day not eating anything, and another day eating normally, than it is to spend two days eating less. The simple decision to not eat at all is massively simplifying.

Relationship to ketosis

When most people hear “keto,” they’re thinking of a diet plan that involves eating an absurd amount of bacon with an occassional avocado. In reality, ketosis is a state in the body where your liver is generating ketone bodies for energy. Here’s the gist of it:

The two primary fuel sources for the body are fat and carbs (sugar/glucose)

Most of your body can happily use either of these

However, fat cannot cross the blood-brain barrier, so your brain typically runs exclusively on glucose

When you dramatically restrict your carb intake (and to some extent your protein intake), your body has insufficient glucose to run your brain

Instead: your liver will convert fat into ketones, which is an alternate energy source your body, and in particular your brain, can use

I’m honestly a bit unsure of the whole topic of proteins in ketosis, as I’ve read conflicting information. But the basic idea of restricting carbs is straightforward. One way to do this is to eat a very-high-fat diet. But another approach is to eat nothing at all. The same process will take place in your body, and you’ll end up in ketosis, likely faster than with a ketogenic diet.

At this point, your whole body will be running off of a combination of ketones and fats, with a small amount of sugar circulating for some cells which can only run on glucose. This explains some of the purported benefits I mentioned above:

Running your brain on a different energy source can give you mental focus. This is not universal: some people report no such feeling.

Once you switch over to ketosis on a fast, you’re burning your (likely ample) body fat stores, providing a nearly-unlimited supply of raw calories. Compare this to having 3 meals a day: you are typically dependent on each meal to provide your energy, and are just waiting for your next infusion of food for a pick-me-up.

Using your body fat as a fuel source obviously means you’ll be burning fat, which is the right way to lose weight! But fasting+ketosis does something even better: it trains your body to be better at burning fat, making it easier to continue burning fat in the future.

One final note: people familiar with Type 1 diabetes may be terrified of the term “keto” due to ketoacidosis. Ketoacidosis is a dangerous medical condition, and does involve ketones. However, it is not the same state as ketosis, and being in ketosis is not dangerous. (But remember my caveats about not being a doctor above, especially if you are a type 1 diabetic.)

Exercise

My personal approach to exercise on a fast is:

Follow my normal lifting routine

Try to train as hard and heavy as I can, accepting that the lack of incoming food will make me a bit weaker.

Schedule a lifting session at the very beginning of the fast, followed by a High Internsity Interval Training (HIIT) session. I still have plenty of energy and glycogen stores to get me through this session on the first day, and the session helps drain those glycogen stores and kick me into ketosis faster.

For weight lifting, I follow an RPE-based program, which essentially adjusts the weight on the bar to how hard it feels. Therefore, as I progress through the fast, I can typically continue following the same program, but the weight I lift will naturally go down a bit.

Side note: at the time of writing this blog post, I’m recovering from wrist tendonitis, and was already deloaded in my lifting, which is why I’m not lifting hard. It’s not because of the fast, but it is affecting how I’m responding to the fast most likely.

Side effects

There are some side effects to fasting worth mentioning, including why I’m writing this blog post now:

Insomnia. For me, the ketone rush seems to disrupt my sleep cycle. I don’t actually feel tired during the day, so maybe this is a good thing.

I won’t do it justice, but Dr. Fung describes many hormonal changes that occur when you’re in a fasted state. These include things like increased human growth hormone and insulin-like growth factor 1. The upshot of this is that you should experience less protein and muscle wasting during a fast than when following a calorite-restricted diet.

This is the primary reason I’m doing the multiday fast right now: I’ve been on a “cut” for a few months and unhappy with the amount of muscle loss I’ve had. I want to finish up the cut quickly and get back into maintenance mode eating, without incurring greater muscle loss. I intend to continue experimenting into the future with using multiday fasts as mini-cuts.

Nausea. The first time I did a multiday fast, I got so nauseous that by the end of the third day I had to break the fast. It was bad enough that I couldn’t stand the taste of coffee for the next two months. However, that first fast included no cream or bone broth. Since I’ve added those two things, I haven’t had any more nausea when fasting.

Dizziness. Especially when first adapting to the fasted state, you may feel lightheaded. Just be careful, and be sure to drink enough water, and supplement salts as needed. More generally: make sure you get enough fluids.

There are certainly others, these are just the ones that have most affected me.

Ending the fast

I’ve ended the fast in the past because I either felt sick, or because of some personal obligation where I didn’t want to be “compromised” in a fasted state. (This was likely just a cop-out on my part, going on a 4 hour trip with a group of fourth graders isn’t that taxing.) I would recommend setting a goal for how long you want to try to fast for, and be ready to be flexible with that goal (either longer or shorter) depending on how you’re responding.

I don’t really have any great recommendations on what to break your fast with. However, you may want to continue eating a low carb or ketogenic diet. You’ve just put yourself into a deep state of ketosis, which many people struggle to do. May as well take advantage of it!

This may not be universal, and I won’t go into details, but expect some GI distress after the fast ends. Your digestive system has been off duty for a few days, it needs to reboot.

Recommendations

Alright, so that was a lot of information all over the place. You’re probably wondering: what should I do? Frankly, you can do whatever you want! You can choose to dive in at the deep end and start off immediately with a multiday fast. Dr. Fung mentions this in his book. However, in my own experience, I started much more gradually:

Low carb and ketogenic diets

Intermittent fasting: only eating between 12pm and 8pm, for example

Experience with religious fasts

Randomly skipping meals

A 24-hour fast (stop eating at 6pm, eat the next day at 6pm)

A multiday fast

Keep in mind: many people in the world today have never skipped a meal. Consider starting with something as easy as not having breakfast to prove to yourself that you don’t need to consume calories all waking hours of the day.

If you have questions you’d like me to answer in a follow up post, either on fasting, or other related health topics, let me know in the comments below or on Twitter.

Extra: muscle loss

I’m not going to claim that fasting is the miracle that allows us to gain muscle and lose fat. I don’t have enough personal experience to vouch for that even in my own body, and the research I’ve seen is conflicted on the topic. As I love doing n=1 experiments on myself, I intend to do more tests with fasting following periods of moderate over eating to see what happens.

Extra: some calorie math

For anyone in a healthy or above weight range, your body is carrying more than enough calories in fat to sustain you for days, likely weeks. If you do some quick math: there are 3,500 calories in 1 pound (0.45 kg) of fat. If you burn about 2,000 calories a day, you can burn roughly half a pound (.22kg) of fat a day. A 165 pound (70kg) person at 20% bodyfat would have 115,500 calories in fat storage, enough to survive over 55 days. Point being: once you’ve entered the ketosis stage of your fast, you essentially have unlimited energy stores available to use, as opposed to needing another hit from a meal to recharge.

Extra: anti-cancer

To be a broken record: I’m not an expert on this topic. But the basic idea of anti-cancer claims for fasting come down to starving out the cancer cells. Cancer cells require lots of glucose (and a bit of protein) for energy. Fasting starves out the cancer cells. I’m not telling anyone to skip chemo or radiation. But I do personally know someone who defeated breast cancer with an (I believe) 11 day fast.

Extra: relevant tweets

Here are some of the relevant tweets from the discussion yesterday.

Day 2.5 of a multiday fast. The ketones have kicked in big time. I'm feeling clear headed, it's easier to focus on tasks/ignore distractions, and physically feeling great. If you haven't tried a multiday fast, I highly recommend it!
— Michael Snoyman (@snoyberg) July 9, 2018

👌🏻truth👌🏻

fasting is much easier than calorie restriction, but most people won't believe it until they do it once. After that, they'll never go back to "trying to eat less today". The binary decision to eat today or not to eat today is far less stressful. https://t.co/uqvwovvtBV
— Thomas D (@tthomasdd) July 9, 2018

And some Youtube videos I've watched by him. There are many others as well, I'm going to assume also very good, but likely lots of repeated content. There's only so much to say about "stop eating" :)https://t.co/FPfBZ1UpAy https://t.co/OGjnA4tgcz
— Michael Snoyman (@snoyberg) July 9, 2018

No, not at all, it's the exact opposite. Once you have the mental decision "I'm not going to eat today," it's much easier to just move on from food completely. Much harder is to say "I'm only going to eat 500 calories today" or whatever.
— Michael Snoyman (@snoyberg) July 9, 2018

July 10, 2018 03:10 AM

Tweag I/O

Funflow Example: emulating Make
Divesh Otwani, Nicholas Clarke
Funflow is a workflow management tool. It turns out that workflow management tools and build tools are closely related. So if you're more familiar with the latter, this post might be of interest to you. We'll be illustrating some of Funflow's features by implementing Make on top.

All the code for this example as well as some documentation can be found here.

Today's example: Make

Our example is a simple version of GNU's Make restricted to building C files (though it could be generalized). It takes a makefile that looks like this
source-files: main.cpp factorial.cpp hello.cpp functions.h

hello: main.o factorial.o hello.o functions.h
 g++ main.o factorial.o hello.o -o hello

main.o: main.cpp functions.h
 g++ -c main.cpp

factorial.o: factorial.cpp functions.h
 g++ -c factorial.cpp

hello.o: hello.cpp functions.h
 g++ -c hello.cpp
and can build the hello executable:
$ ls
factorial.cpp functions.h hello.cpp main.cpp makefile
$ stack exec makefile-tool
$ ./hello
Hello World!
The factorial of 5 is 120
Because we used Funflow, our tool has several desirable properties, both of the tool and of the code itself:

No repeated builds: If we've built something before, we don't build it again. Period. With make, if you make a tiny change and find out it isn't what you want, when you revert back make will rebuild something it had built before. Our tool won't.

Enforced target dependencies: We build each target file in a docker container with exactly the dependencies listed in the Makefile. There's no opportunity for hidden dependencies or hidden requirements on the environment. Further, such 'hidden' preconditions are caught early and flagged making it easy to fix the Makefile.

Clean Sequencing Code: The function that makes a target file sequences file processing, recusive calls for making the dependencies of the given target, and running docker containers. Usually, this sequencing is messy and difficult to follow. With Funflow, however, we can inject these various forms of computation into Flows and sequence them seamlessly with arrow notation.

Concise Code: Because of the abstractions Funflow provides, we can focus on the essential algorithm and get some efficiency & safety for free.

No Repeat Builds: CAS Gives Us Free Dynamic Programming

The essential function is buildTarget which, given a Makefile and a specific rule in that Makefile, creates a flow to build the target specified by that rule. A rule specifies a target file by a list of file dependencies and a command to build that target file. Each dependency is either a source file or itself a target file.

Here is a slightly simplified version of that function:
-- For readability, we introduce a type alias for Flow
type a ==> b = Flow a b

buildTarget :: MakeFile -> MakeRule -> (() ==> (Content File))
buildTarget mkfile target@(MakeRule targetNm deps cmd) = proc _ -> do
 -- 1) Get source file contents
 contentSrcFiles <- grabSrcsFlow -< neededSources
 -- 2) Zip these with the names of each source file
 let fullSrcFiles = Map.fromList $ zip neededSources contentSrcFiles
 -- 3) Recursively build all dependent targets
 depFiles <- flowJoin depTargetFlows -< (replicate countDepFlows ())
 -- 4) Compile this file given
 -- a) the name of the target
 -- b) the dependencies that are source files
 -- c) the dependencies that were targets
 -- d) the gcc command to execute
 compiledFile <- compileFile -< (targetNm, fullSrcFiles, depFiles,cmd)
 returnA -< compiledFile
 where
 srcfiles = sourceFiles mkfile
 neededTargets = Set.toList $ deps `Set.difference` srcfiles
 neededSources = Set.toList $ deps `Set.intersection` srcfiles
 depRules = (findRules mkfile neededTargets :: [MakeRule])
 depTargetFlows = map (buildTarget mkfile) depRules
 countDepFlows = length depTargetFlows
 grabSources srcs = traverse (readFile . ("./" ++)) srcs
 grabSrcsFlow = stepIO grabSources
The code for building the flow is straightforward.

First, we do some file processing to get the dependent source files (in steps 1 & 2). Then, we recursively call buildTarget to create flows for each of the dependent target files and then run those flows to build the dependent targets (in step 3). Finally, we put these dependencies in a docker container in which we run the gcc command and extract the produced target file (provided the compilation succeeded).

On the surface, this code appears inefficient. Step 3, the recursive building of dependent target files, looks like it repeats a lot of work since many of the recursive calls are identical. For example, if the rule for main.o in our sample Makefile listed factorial.o as a dependency, it looks like this code would build factorial.o twice -once as a dependency of hello and once as a dependency of main.o. If factorial.o took a long time to build, this would be disastrous.

Yet, this code isn't inefficient? Why? This problem of 'overlapping' recursive calls is solved by dynamic programming, the algorithmic design pattern of saving the values of function calls in a dictionary and checking this dictionary to avoid repeated recursive calls. Funflow's caching gives this to us for free. Hence, we can write DP-algorithms without dealing with the added complexity of keeping track of the dictionary ourselves. This is precisely what happens in buildTarget.

Each time a file is compiled with compileFile, a hash of the inputs and output is cached. So, on a repeated recursive call building say, target4.o, the use of compiledFile is constant time.

However, this goes a step further. Because of Funflow's caching our tool, unlike GNU's make, doesn't re-build targets even after reverting back changes. Say factorial.cpp took a long time to build and was part of a larger project. Suppose further that to fix a bug in this large project, we tried something out in factorial.cpp and found out it didn't work. When we revert back, our tool would build factorial.cpp in constant time whereas plain ol' make would not.

Enforced Dependencies

makefile-tool also showcases Funflow's docker capabilities. We compile each target in its own docker container with exactly its list of dependencies.

This prevents hidden preconditions. If some rule fails to mention a source file it needs, the docker container in which the rule's target file is being compiled won't have that missing source file. Hence, if a file dependency is missing from the dependency list of a certain target, that target won't build. In the same vein, if there was a hidden requirement on the environment, like a custom gcc executable, the build would fail inside the docker container.

Further, this approach doesn't merely prevent hidden preconditions; it flags them. For example, if our Makefile above had the line factorial.o : factorial.cpp instead of factorial.o : factorial.cpp functions.h, we would get an error from gcc indicating that it couldn't find functions.h. With ordinary make, the build would succeed and this hidden precondition would last. Within the scope of a large project, this could be maddening.

This dependency enforcement could work for more than just C projects. As suggested earlier, the makefile-tool can be generalized. We could extend this tool by having the user provide a docker container for the build command and a way of directing the naming of the target file. (For C projects, this would be the gcc container with the -o command line argument.)

Clean Sequencing: Diverse Injection & Arrow Notation

This example also demonstrates Funflow's ability to inject various forms of computation into Flows and sequence them in fancy ways. This makes the code readable and maintainable.

Injecting IO and External Steps

At one point, we needed to inject the IO action
parseRelFile :: String -> IO (Path Rel File)
and could easily do so:
flowStringToRelFile :: Flow String (Path Rel File)
flowStringToRelFile = stepIO parseRelFile
Then, inside the compileFile flow, we were able to sequence this with dockerFlow, a flow that was made from an external step. That is, dockerFlow was made from the Funflow library function docker:
import qualified Control.Funflow.External.Docker as Docker
import qualified Control.Funflow.ContentStore as CS

docker :: (a -> Docker.Config) -> Flow a CS.Item

dockerConfFn :: (Content Dir, Content File) -> Docker.Config

dockerFlow = docker dockerConfFn


data Config = Config
 { image :: T.Text -- e.g., "gcc", "ubuntu", "python".
 , optImageID :: Maybe T.Text
 , input :: Bind -- Files in the content store & locations to
 -- put them in the docker container. This
 -- includes a bash script to execute.
 , command :: FilePath -- A path to the bash script.
 , args :: [T.Text] -- Command line arguments to 'command'.
} deriving Generic
Then by using arrow notation, a generalization of 'do notation', we were able to elegantly and easily sequence these Flows. Without going into the details, we can see the sequencing is as readable and intuitive as 'do notation':
compiledFile <- dockerFlow -< (inputDir,compileScript)
relpathCompiledFile <- flowStringToRelFile -< tf
returnA -< (compiledFile :</> relpathCompiledFile)
Further, these properties persist when we need more sophisticated forms of sequencing.

Recursive Calls & Linearly Sequencing Similar Flows

The buildTarget function calls itself and recursively builds a list of Flows for the other targets:
depTargetFlows :: [Flow () (Content File)]
depTargetFlows = map (buildTarget mkfile) depRules
where
buildTarget :: MakeFile -> MakeRule -> (Flow () (Content File))
mkfile :: MakeFile
depRules :: [MakeRule]
Now, to actually use these we need to linearly sequence these Flows. (We can't sequence them in parallel because then repeated recursive calls would repeat work if flows were distributed.) In other words, we need the power to combine an arbitrary amount of similar flows into one flow. Because Funflow is embedded in haskell, we can write the function flowJoin:
flowJoin :: [Flow a b] -> Flow [a] [b]
flowJoin [] = step (\_ -> []) -- step :: (a -> b) -> Flow a b
flowJoin (f:fs) = proc (a:as) -> do
 b <- f -< a
 bs <- flowJoin fs -< as
 returnA -< (b:bs)

joinedDepTargets :: Flow [()] [Content File]
joinedDepTargets = flowJoin depTargetFlows
A careful programmer might note that the base case is ill defined. Indeed, the right approach is to use length indexed vectors and have
safeFlowJoin :: forall (n :: Nat) a b. Vec n (Flow a b) -> Flow (Vec n a) (Vec n b)
but even without this, flowJoin is a clean, simple, and powerful way of sequencing Flows.

Summary

makefile-tool is only 266 lines long of which 180 pertain to following a Makefile and yet,

the CAS gives us free dynamic programming,

we never rebuild targets even when reverting changes (which is an improvement over make), and,

the dependencies are checked and made explicit, which lends to a crisp functional model.
July 10, 2018 12:00 AM

Planet Haskell

September 02, 2018

VGA signal primer

CHIP-8 video

Signal generation from CλaSH

September 01, 2018

August 31, 2018

August 30, 2018

August 29, 2018

What is CλaSH?

What is CHIP-8?

My plan

August 28, 2018

Kids IDE

Pattern matching strings

Pattern matching ints

Type signatures

Enums

Recursion

August 27, 2018

August 26, 2018

August 25, 2018

August 24, 2018

Coding environment

Variables

Functions

Bonus

August 23, 2018

Kids Coding, Part 1

Python portion

Haskell portion

Types

Today’s excercise

To figure out

Next lesson

August 22, 2018

Categories for the Working Hacker

August 20, 2018

August 19, 2018

August 18, 2018

August 17, 2018

Building the closure

Deploying the closure

Adding a profile

Querying system options

Pinning nixpkgs

Building remotely

Conclusion

August 15, 2018

August 14, 2018

Fold right

Fold left

Duality theorems

Characterization

Monoids and list homomorphisms

The Trick

August 13, 2018

Setting up the server

Generate a signing key

Turn on SSH Nix store serving

Setting up the clients

Generating a Root SSH Key

Telling Nix to use the cache

Populating the Cache

Maintenance

August 09, 2018

August 07, 2018

Arithmetic coding, revisited

From fractions to integers

Bounded precision

Trading in sequences

Streaming encoding

Streaming decoding

Summing up

August 06, 2018

August 04, 2018

Background

What happened

A red herring

Why it really happened

Pinning `nixpkgs`