Russell O’Connor’s Blog2015-08-27T02:03:14ZRussell O’Connorhttp://r6.ca/http://r6.ca/blog/http://r6.ca/blog/20150827T020314Z.htmlClearing Up “Clearing Up Mysteries”2015-08-27T02:03:14Z2015-08-27T02:03:14Z
<p>I am a big fan of <a title="Jaynes on Entropy" href="20100802T005835Z.html">E. T. Jaynes</a>.
His book <cite>Probability Theory: The Logic of Science</cite> is the only book on statistics that I ever felt I could understand.
Therefore, when he appears to rail against the conclusions of Bell’s theorem in his paper
“<a href="http://bayes.wustl.edu/etj/articles/cmystery.ps.gz">Clearing up Mysteries—The Original Goal</a>”, I take him seriously.
He suggests that perhaps there could be a time-dependent hidden variable theory that could yield the outcomes that quantum mechanics predicts.</p><p>However, after reading Richard D. Gill’s paper,
“<a href="http://arxiv.org/abs/quant-ph/0301059v2">Time, Finite Statistics, and Bell’s Fifth Position</a>”
it is very clear that there can be nothing like a classical explanation that yields quantum predictions, time-dependent or otherwise.
In this paper Gill reintroduces Steve Gull’s computer network, where a pair of classical computers is tasked to recreate probabilities predicted in a <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> delayed choice experiment.
The catch is that the challenger gets to choose the stream of bits sent to each of the two spatially separated computers in the network.
These bits represent the free choice an experimenter running a <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> experiment has to choose which polarization measurements to make.
No matter what the classical computer does, no matter how much time-dependent fiddling you want to do, it can never produce correlations that will violate the <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> inequality in the long run.
This is Gull’s “You can’t program two independently running computers to emulate the EPR experiment” theorem.</p><p>Gill presents a nice analogy with playing roulette in the casino.
Because of the rules of roulette, there is no computer algorithm can implement a strategy that will beat the house in roulette in the long run.
Gill goes on to quantify exactly how long the long run is in order to place a wager against other people who claim they can recreate the probabilities predicted by quantum mechanics using a classical local hidden variable theory.
Using the theory of supermartingales, one can bound the likelihood of seeing the <a title="CHSH inequality" href="https://en.wikipedia.org/w/index.php?tilte=CHSH_inequality&oldid=676806380">Bell-CHSH</a> inequality violated by chance by any classical algorithm in the same way that one can bound the likelihood of long winning streaks in roulette games.</p><p>I liked the casino analogy so much that I decided to rephrase Gull’s computer network as a coin guessing casino game I call <a title="Bell’s Casino Problem" href="20150816T185621Z.html">Bell’s Casino</a>.
We can prove that any classical strategy, time-dependent or otherwise, simply cannot beat the house at that particular game in the long run.
Yet, there is <a>a strategy</a> where the players employ entangled qubits and beat the house on average.
This implies there cannot be any classical phenomena that yields quantum outcomes.
Even if one proposes some classical oscollating (time-dependent) hidden variable vibrating at such a high rate that we could never practically measure it, this theory still could not yield quantum probabilities,
because such a theory implies we could simulate it with Gull’s computer network.
Even if our computer simulation was impractically slow, we could still, in principle, deploy it against Bell’s Casino to beat their coin game.
But no such computer algorithm exists, in exactly the same way that there is no computer algorithm that will beat a casino at a fair game of roulette.
The fact that we can beat the casino by using qubits clearly proves that qubits and quantum physics is something truly different.</p><p>You may have heard the saying that “correlation does not imply causation”.
The idea is that if outcomes <var>A</var> and <var>B</var> are correlated, the either <var>A</var> causes <var>B</var>, or <var>B</var> causes <var>A</var>, or there is some other <var>C</var> that causes <var>A</var> and <var>B</var>.
However, in quantum physics there is a fourth possibilty.
We can have correlation without causation.</p><p>In light of Gull and Gill’s iron clad argument, I went back to reread Jaynes’s “Clearing up Mysteries”.
I wanted to understand how Jaynes could have been so mistaken.
After rereading it I realized that I had misunderstood what he was trying to say about Bell’s theorem.
Jaynes just wanted to say two things.</p><p>Firstly, Jaynes wanted to say that Bell’s theorem does not necessarily imply action at a distance.
This is not actually a controversial statement.
The many-worlds interpretation is a local, non-realist (in the sense that experiments do not have unique definite outcomes) interpretation of quantum mechanics.
This interpretation does not invoke any action at a distance and is perfectly compatible with Bell’s theorem.
Jaynes spends some time noting that correlation does not imply causation in an attempt to clarify this point although he never talks about the many-worlds interpretation.</p><p>Secondly, Jaynes wanted to say that Bell’s theorem does not imply that quantum mechanics is the best possible physical theory that explains quantum outcomes.
Here his argument is half-right and half-wrong.
He spends some time suggesting that maybe there is a time-dependent hidden variable theory that could give more refined predictions than predicted by quantum theory.
However, the suggestion that any classical theory, time-dependent or otherwise, could underlie quantum mechanics is refuted by Bell’s theorem and this is clearly illustrated by Gull’s computer network or by Bell’s casino.
Jaynes learned about Gull’s computer network argument at the same conference that he presented “Clearing Up Mysteries”.
His writing suggests that he was surprised by the argument, but he did not want to rush to draw any conclusions to from it without time to get a deeper understanding of it.
Nevertheless, Jaynes larger point was still correct.
Bell’s theorem does not imply that there is not some, non-classical, refinement of quantum mechanics that might yield more informative predictions than quantum mechanics does and Jaynes was worried that people would not look for such a refinement.</p><p>Jaynes spent a lot of effort trying to separate epistemology, where probability theory rules how we reason in the face of imperfect knowledge, from ontology, which describes what happens in reality if we had perfect information.
Jaynes thought that quantum mechanics was mixing these two branches together into one theory and worried that if people were mistaking quantum mechanics for an ontological theory then they would never seek a more refined theory.</p><p>While Bell’s theorem does not rule out that there may be a non-classical hidden variable theory,
Colbeck and Renner’s paper “<a href="http://arxiv.org/abs/1005.5173v3">No extension of quantum theory can have improved predictive power</a>” all but eliminates that possibility
by proving that there is no quantum hidden variable theory.
This can be seen as a strengthening of Bell’s theorem, and they even address some of the same concerns that Jaynes had about Bell’s theorem.</p><blockquote>
<p>To quote Bell [2], <dfn>locality</dfn> is the requirement that “…the result of a measurement on one system [is] unaffected by
operations on a distant system with which it has interacted in the past…” Indeed, our non-signalling conditions reflect
this requirement and, in our language, the statement that P<sub>XYZ|ABC</sub> is non-signalling is equivalent to a statement that
the model is local (see also the discussion in [28]). (We remind the reader that we do not assume the non-signalling
conditions, but instead derive them from the free choice assumption.)
In spite of the above quote, Bell’s formal definition of locality is slightly more restrictive than these non-signalling
conditions. Bell considers extending the theory using hidden variables, here denoted by the variable Z. He requires
P<sub>XY|ABZ</sub> = P<sub>X|AZ</sub> × P<sub>Y|BZ</sub> (see e.g. [13]), which corresponds to assuming not only P<sub>X|ABZ</sub> = P<sub>X|AZ</sub> and P<sub>Y|ABZ</sub> =
P<sub>Y|BZ</sub> (the non-signalling constraints, also called parameter-independence in this context), but also P<sub>X|ABYZ</sub> =
P<sub>X|ABZ</sub> and P<sub>Y|ABXZ</sub> = P<sub>Y|ABZ</sub> (also called outcome-independence). These additional constraints do not follow
from our assumptions and are not used in this work.</p>
</blockquote>
<p>The probabilistic assumptions are weaker in Colbeck and Renner’s work than in Bell’s theorem, because they want to exclude quantum hidden variable theories in addition to classical
hidden variable theories.
Today, if one wants to advance a local hidden variable theory, it would have to be a theory that is even weirder than quantum mechanics, if such a thing is even logically possible.
It seems that quantum mechanics’s wave function is an ontological description after all.</p><p>I wonder what Jaynes would have thought about this result.
I suspect he would still be looking for an exotic hidden variable theory.
He seemed so convinced that probability theory was solely in the realm of epistemology and not ontology that he would not accept any probabilistic ontology at all.</p><p>I think Jaynes was wrong when he suggested that quantum mechanics was necessarily mixing up epistemology and ontology.
I believe the many-worlds interpretation is trying to make that distinction clear.
In this interpretation the wave-function and Schrödinger’s equation is ontology, but the Born rule that relates the norm-squared amplitude to probability ought to be epistemological.
However, there does remain an important mystery here:
Why do the observers within the many-worlds observe quantum probabilities that satisfy the Born rule?
I like to imagine Jaynes could solve this problem if he were still around.
I imagine that would say that something like, “Due to phase invariance of the wave-function … <i>something something</i> … transformation group … <i>something something</i> … thus the distribution must be in accordance with the Born rule.”
After all, Jaynes did manage to use transformation groups to solve the <a href="https://en.wikipedia.org/w/index.php?title=Bertrand_paradox_%28probability%29&oldid=674563212#Jaynes.27_solution_using_the_.22maximum_ignorance.22_principle">Bertrand paradox</a>, a problem widely regarded as being unsolvable due to being underspecified.
</p>http://r6.ca/blog/20150816T185621Z.htmlBell’s Casino Problem2015-08-16T18:56:21Z2015-08-16T18:56:21Z
<p>A new casino has opened up in town named “Bell’s Casino”. They are offering a coin game. The game works as follows.
</p><p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of the each of the coins are, either HH, HT, TH, or TT. The
casino reveals the coins and if the player is correct, they win $1, and otherwise they lose $1.
</p><dl>
<dt>Problem 1.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
<p>After opening the customers stop coming by to play this boring game, so to boost attendance the casino modifies the game as follows.
</p><p>The house will commit two coins on the table, oriented heads or tails each, and keep them covered. The player calls what the faces of each of the two coins are, either HH, HT, TH, or TT. The
casino reveals one coin, of the players choice. After seeing revealed coin, the player can elect to back out of the game and neither win nor lose, or keep going, and see the second coin.
If the player’s call is correct, they win $1, and otherwise they lose $1.
</p><dl>
<dt>Problem 2.</dt>
<dd>Prove that there is no strategy that can beat the casino.</dd>
</dl>
<p>Even with the new, more fair, game, attendance at the casino starts dropping off again. The casino decides to offer a couples game.
</p><p>The house will commit two coins on two tables, oriented heads or tails each, and keep them covered. The couple, together, calls what the the faces of each of the two coins are, either HH, HT, TH, or
TT. Then, each player in the couple gets to see one coin each. Collectively they get to decide whether they are going to back out of the game or not by the following method. After seeing
their revealed coin, each player will raise either a black flag or a red flag. If both players raise the different colour flags, the game ends and no one wins or loses. If both players raise the
same colour flag, the game keeps going. If the couples original call was right, they win $1, and otherwise, they lose $1. To ensure that the couple cannot cheat, the two tables
are places far enough apart such that each player’s decision on which flag to raise is <a title="Space-like interval" href="https://en.wikipedia.org/wiki/Spacetime#Space-like_interval">space-like separated</a>. Specifically the tables are placed 179 875 475 km apart and
each player has 1 minute to decide which flag to raise otherwise a black flag will be raised on their behalf (or, more realistically, the tables are placed 400 m apart and each player has
100 nanoseconds to decide which flag to raise).
</p><dl>
<dt>Problem 3.</dt>
<dd>Prove that there is no strategy for the couple that can beat the casino.</dd>
</dl>
<dl>
<dt>Problem 4.</dt>
<dd>Devise a physical procedure that a couple can follow to beat the casino on average at this last game without cheating.</dd>
</dl>
<p>The casino cannot figure out how they keep losing money on this game and, soon, Bell’s Casino goes bankrupt.
</p>http://r6.ca/blog/20150222T233125Z.htmlParallel Evaluation of the Typed Lambda Calculus2015-02-22T23:31:25Z2015-02-22T23:31:25Z
<p>There is much written about the <a title="Call-by-Value is Dual to Call-by-Name" href="http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf">duality</a> between strict-order (call-by-value) evalutaion for the lambda calculus and the normal-order (call-by-need) evaluation (or semantic equivently, lazy evaluation).
In the simply typed lambda calculus, all evaluation eventually terminates, so both evaluation strategies result in the same values.
However, when general recursion is added to the simply typed lambda calculus (via a fixpoint operator, for example) then evaluation of some expressions does not terminate.
More expressions terminate with normal-order evaluation than with strict-order evaluation.
In fact, if evaluation terminates in any order, then it terminates with normal-order evaluation.
</p><p>I would like to discuss the possibility of a third, even laxer evaluation strategy available for the typed lambda calculus that allows for even more expressions to terminate.
I did just say that normal-order evaluation is, in some sense, a best possible evaluation order, so, in order to beat it, we will be adding more redexes that add the commuting conversions.
</p><p>The typed lambda calculus enjoys certain commuting conversions for case expressions that allow every elimination term to pass through the case expression.
For example, the commuting conversion for the <code>π₁</code> elimination term and the <code>case</code> experssion says that
</p><pre>π₁(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)</pre>
<p>converts to
</p><pre>case e₀ of σ₁ x. π₁(e₁) | σ₂ y. π₁(e₂)</pre>
<p>These commuting conversions are required so that <a title="Proofs and Types" href="http://www.paultaylor.eu/stable/Proofs+Types.html">the subformula property holds</a>.
</p><p>My understanding is that a corollary of this says that
</p><pre>f(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)</pre>
<p>and
</p><pre>case e₀ of σ₁ x. f(e₁) | σ₂ y. f(e₂)</pre>
<p>are denotationally equivalent whenever <code>f</code> is a strict function.
</p><p>I would like to develop a version of the lambda calculus that allows these two expressions to denote the same value for any <code>f</code>.
Call this, the unrestricted commuting conversion property.
A lambda calculus with this property would necessarily be parallel and thus will require a parallel evaluation strategy.
For example, the natural definition of <code>or</code> becomes the parallel-or operation.
</p><pre>or x y := if x then True else y</pre>
<p>This definition has the usual short-circuit property that <code>or True ⊥</code> is <code>True</code> where <code>⊥</code> is defined by
</p><pre>⊥ := fix id</pre>
<p>If we use the unrestricted commuting conversion property then we also have the that <code>or ⊥ True</code> is <code>True</code>:
</p><pre>or ⊥ True
= {definition of or}
if ⊥ then True else True
= {β-expansion}
if ⊥ then const True ⟨⟩ else const True ⟨⟩
= {commuting}
const True (if ⊥ then ⟨⟩ else ⟨⟩)
= {β-reduction}
True</pre>
<p>Hence <code>or</code> is parallel-or.
</p><p>Other parallel functions, such as the majority function, also follow from their natural definitions.
</p><pre>maj x y z := if x then (or y z) else (and y z)</pre>
<p>In this case <code>maj ⊥ True True</code> is <code>True</code>.
</p><pre>maj ⊥ True True
= {definition of maj}
if ⊥ then (or True True) else (and True True)
= {evaluation of (or True True) and (and True True)
if ⊥ then True else True
= {commuting}
True</pre>
<p>It is easy to verify that <code>maj True ⊥ True</code> and <code>maj True True ⊥</code> are also both <code>True</code>.
</p><p>My big question is whether we can devise some nice operational semantics for the lambda calculus that will have the unrestricted commuting conversions property that I desire.
Below I document my first attempt at such operational semantics, but, spoiler alert, it does not work.
</p><p>The usual rule for computing weak head normal form for the case expression <code>case e₀ of σ₁ x. e₁ | σ₂ y. e₂</code> says to first convert <code>e₀</code> to weak head normal form.
If it is <code>σ₁ e₀′</code> then return the weak head normal form of <code>e₁[x ↦ e₀′]</code>.
If it is <code>σ₂ e₀′</code> then return the weak head normal form of <code>e₂[y ↦ e₀′]</code>.
In addition to this rule, I want to add another rule for computing the weak head normal form for the case expression.
This alernative rules says that we compute the weak head normal forms of <code>e₁</code> and <code>e₂</code>.
If we get <code>C₁ e₁′</code> and <code>C₂ e₂′</code> respectively for introduction terms (<abbr title="also known as">a.k.a.</abbr> constructors) <code>C₁</code> and <code>C₂</code>, and
if additionally <code>C₁</code> = <code>C₂</code> then return the following as a weak head normal form, <code>C₁ (case e₀ of σ₁ x. e₁′ | σ₂ y. e₂′)</code>.
If <code>C₁</code> ≠ <code>C₂</code> or if we get stuck on a neutral term (e.g. a varaible), then this rule does not apply.
</p><p>This new rule is in addition to the usual rule for <code>case</code>. Any implementation must run these two rules in parallel because it is possible that either rule (or both) can result in non-termination when recursivly computing weak head normal forms of sub-terms.
I suppose that in case one has unlifted products then when computing the weak head normal form of a <code>case</code> expression having a product type or function type, one can immediately return
</p><pre>⟨case e₀ of σ₁ x. π₁ e₁ | σ₂ y. π₁ e₂, case e₀ of σ₁ x. π₂ e₁ | σ₂ y. π₂ e₂⟩</pre>
or
<pre>λz. case e₀ of σ₁ x. e₁ z | σ₂ y. e₂ z</pre>
<p>This amended computation of weak head normal form seems to work for computing <code>or</code> and <code>maj</code> functions above so that they are non-strict in every argument, but there is another example where even this method of computing weak head normal form is not sufficent.
Consider the functions that implements associativity for the sum type.
</p><pre>assocL : A + (B + C) -> (A + B) + C
assocL z := case z of σ₁ a. σ₁ (σ₁ a) | σ₂ bc. (case bc of σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c)
assocR : (A + B) + C -> A + (B + C)
assocR z := case z of σ₁ ab. (case ab of σ₁ a. σ₁ a | σ₂ b. σ₂ (σ₁ b)) | σ₂ c. σ₂ (σ₂ c)</pre>
<p>Now let us use unrestricted commuting conversions to evaluate <code>assocR (assocL (σ₂ ⊥))</code>.
</p><pre>assocR (assocL (σ₂ ⊥))
= { definition of assocL and case evaluation }
assocR (case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c)
= { commuting conversion }
case ⊥. σ₁ b. assocR (σ₁ (σ₂ b)) | σ₂ c. assocR (σ₂ c)
= { definition of assocR and case evaluations }
case ⊥. σ₁ b. σ₂ (σ₁ b) | σ₂ c. σ₂ (σ₂ c)
= { commuting conversion }
σ₂ (case ⊥. σ₁ b. σ₁ b | σ₂ c. σ₂ c)
= { η-contraction for case }
σ₂ ⊥</pre>
<p>Even if η-contraction is not a reduction rule used for computation, it is still the case that <code>t</code> and <code>case t. σ₁ b. σ₁ b | σ₂ c. σ₂ c</code> should always be dentotationally equivalent.
Anyhow, we see that by using commuting conversions that a weak head normal form of <code>assocR (assocL (σ₂ ⊥))</code> should expose the <code>σ₂</code> constructor.
However, if you apply even my ammended computation of weak head normal form, it will not produce any constructor.
</p><p>What I find particularly surprising is the domain semantics of <code>assocL</code> and <code>assocR</code>.
<code>assocL</code> seems to map <code>σ₂ ⊥</code> to <code>⊥</code> because no constructor can be exposed.
<code>assocR</code> maps <code>⊥</code> to <code>⊥</code>.
Therefore, according to the denotational semantics, the composition should map <code>σ₂ ⊥</code> to <code>⊥</code>, but as we saw, under parallel evaluation it does not.
It would seem that the naive denotational semantics appears to not capture the semantics of parallel evaluation.
The term <code>case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c</code> seems to be more defined than ⊥, even though no constructor is available in the head position.
</p><p>Although my attempt at nice operational semantics failed, I am still confident some nice computation method exists.
At the very least, I believe a rewriting system will work which has all the usual rewriting rules plus a few extra new redexes that says that an elimination term applied to the <code>case</code> expression commutes the elimination term into all of the branches,
and another that says when all branches of a case expression contain the same introduction term, that introduction term is commuted to the outside of the case expression, and maybe also the rules I listed above for unlifted products.
I conjecture this rewriting system is confluent and unrestricted commuting conversions are convertable (probably requiring η-conversions as well).
</p><p>Without proofs of my conjectures I am a little concerned that this all does not actually work out.
There may be some bad interaction with fixpoints that I am not seeing.
If this does all work out then shouldn’t I have heard about it by now?
</p>http://r6.ca/blog/20150111T040537Z.htmlSecure diffie-hellman-group-exchange-sha2562015-01-11T04:05:37Z2015-01-11T04:05:37Z
<p>Recently I have been working on purging <abbr title="Digital Signature Algorithm">DSA</abbr> from my computer systems.
The problem with <abbr title="Digital Signature Algorithm">DSA</abbr> and <abbr title="Elliptic Curve Digital Signature Algorithm">ECDSA</abbr> is that they fail catastrophically with when nonces are accidentally reused, or if the randomly generated nonces are biased.
At about the same time, I was pleased to discover an article on <a title="Secure Secure Shell" href="https://stribika.github.io/2015/01/04/secure-secure-shell.html">securing <abbr title="Secure Shell">SSH</abbr></a>. It gives further advice in setting up <abbr title="Secure Shell">SSH</abbr> and I have proceeded to apply most of the recommendation listed there.
</p><p>For key exchange algorithms, <a title="Secure Secure Shell" href="https://stribika.github.io/2015/01/04/secure-secure-shell.html">the article</a> suggests using <code>curve25519-sha256</code> and falling back to <code>diffie-hellman-group-exchange-sha256</code> for compatibility purposes if you must.
The <code>diffie-hellman-group-exchange-sha256</code> protocol allows the client and server to negotiate a prime field to perform the key exchange in.
In order to avoid using the smaller prime fields, <a title="Secure Secure Shell" href="https://stribika.github.io/2015/01/04/secure-secure-shell.html">the article</a> suggests deleting prime numbers less than 2000 bits in size from <code>/etc/ssh/moduli</code>.
The problem with this advice is that only the <abbr title="Secure Shell">SSH</abbr> server reads <code>/etc/ssh/moduli</code>; touching this file does nothing to secure your <abbr title="Secure Shell">SSH</abbr> client from using small prime fields during key negotiation.
Securing the client is the important use case for <code>diffie-hellman-group-exchange-sha256</code>, because if you can control the server, then it means you will probably use <code>curve25519-sha256</code> instead.
</p><p>However, <a title="Diffie-Hellman Group Exchange for the Secure Shell (SSH) Transport Layer Protocol" href="https://www.ietf.org/rfc/rfc4419.txt">the protocol for <code>diffie-hellman-group-exchange-sha256</code></a> does allow the client to negotiate the field side.
The problem is that this ability is not exposed for configuration in <abbr title="Secure Shell">SSH</abbr>.
To address this, I created a <a href="data:text/plain;base64,QXV0aG9yOiBSdXNzZWxsIE8nQ29ubm9yIDxvY29ubm9yckBnb29nbGUuY29tPgpkaWZmIC11ciBvcGVuc3NoLTYuOHAxLm9yaWcvZGguaCBvcGVuc3NoLTYuOHAxL2RoLmgKLS0tIG9wZW5zc2gtNi44cDEub3JpZy9kaC5oICAgICAyMDE1LTA1LTA0IDExOjQ4OjA2LjYxODI3ODU0OCAtMDQwMAorKysgb3BlbnNzaC02LjhwMS9kaC5oICAyMDE1LTA1LTA0IDExOjQ4OjM1LjgyNTcwNDM1NSAtMDQwMApAQCAtNDMsOCArNDMsNyBAQAogCiB1X2ludCAgIGRoX2VzdGltYXRlKGludCk7CiAKLS8qIE1pbiBhbmQgbWF4IHZhbHVlcyBmcm9tIFJGQzQ0MTkuICovCi0jZGVmaW5lIERIX0dSUF9NSU4gICAgIDEwMjQKKyNkZWZpbmUgREhfR1JQX01JTiAgICAgMjA0OAogI2RlZmluZSBESF9HUlBfTUFYICAgICA4MTkyCiAKIC8qCmRpZmYgLXVyIG9wZW5zc2gtNi44cDEub3JpZy9rZXhnZXhjLmMgb3BlbnNzaC02LjhwMS9rZXhnZXhjLmMKLS0tIG9wZW5zc2gtNi44cDEub3JpZy9rZXhnZXhjLmMgICAgICAgIDIwMTUtMDUtMDQgMTE6NDg6MDYuNjIxMjc4NTkyIC0wNDAwCisrKyBvcGVuc3NoLTYuOHAxL2tleGdleGMuYyAgICAgMjAxNS0wNS0wNCAxMjowMjo1MS40NzcwMDA0MzAgLTA0MDAKQEAgLTYxLDYgKzYxLDggQEAKICAgICAgICB1X2ludCBuYml0czsKIAogICAgICAgIG5iaXRzID0gZGhfZXN0aW1hdGUoa2V4LT5kaF9uZWVkICogOCk7CisgICAgICAgIG5iaXRzID0gTUlOKERIX0dSUF9NQVgsIG5iaXRzKTsKKyAgICAgICAgbmJpdHMgPSBNQVgoREhfR1JQX01JTiwgbmJpdHMpOwogCiAgICAgICAga2V4LT5taW4gPSBESF9HUlBfTUlOOwogICAgICAgIGtleC0+bWF4ID0gREhfR1JQX01BWDsKZGlmZiAtdXIgb3BlbnNzaC02LjhwMS5vcmlnL2tleGdleHMuYyBvcGVuc3NoLTYuOHAxL2tleGdleHMuYwotLS0gb3BlbnNzaC02LjhwMS5vcmlnL2tleGdleHMuYyAgICAgICAgMjAxNS0wNS0wNCAxMTo0ODowNi42MjEyNzg1OTIgLTA0MDAKKysrIG9wZW5zc2gtNi44cDEva2V4Z2V4cy5jICAgICAyMDE1LTA1LTA0IDEyOjEwOjI1LjE0NTQyODk0NCAtMDQwMApAQCAtODcsMTAgKzg3LDYgQEAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKICAgICAgICAgICAgICAgIGtleC0+bmJpdHMgPSBuYml0czsKICAgICAgICAgICAgICAgIGtleC0+bWluID0gbWluOwogICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXg7Ci0gICAgICAgICAgICAgICBtaW4gPSBNQVgoREhfR1JQX01JTiwgbWluKTsKLSAgICAgICAgICAgICAgIG1heCA9IE1JTihESF9HUlBfTUFYLCBtYXgpOwotICAgICAgICAgICAgICAgbmJpdHMgPSBNQVgoREhfR1JQX01JTiwgbmJpdHMpOwotICAgICAgICAgICAgICAgbmJpdHMgPSBNSU4oREhfR1JQX01BWCwgbmJpdHMpOwogICAgICAgICAgICAgICAgYnJlYWs7CiAgICAgICAgY2FzZSBTU0gyX01TR19LRVhfREhfR0VYX1JFUVVFU1RfT0xEOgogICAgICAgICAgICAgICAgZGVidWcoIlNTSDJfTVNHX0tFWF9ESF9HRVhfUkVRVUVTVF9PTEQgcmVjZWl2ZWQiKTsKQEAgLTk5LDEzICs5NSwxNyBAQAogICAgICAgICAgICAgICAgICAgICAgICBnb3RvIG91dDsKICAgICAgICAgICAgICAgIGtleC0+bmJpdHMgPSBuYml0czsKICAgICAgICAgICAgICAgIC8qIHVudXNlZCBmb3Igb2xkIEdFWCAqLwotICAgICAgICAgICAgICAga2V4LT5taW4gPSBtaW4gPSBESF9HUlBfTUlOOwotICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXggPSBESF9HUlBfTUFYOworICAgICAgICAgICAgICAga2V4LT5taW4gPSBtaW4gPSAxMDI0OworICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXggPSA4MTkyOwogICAgICAgICAgICAgICAgYnJlYWs7CiAgICAgICAgZGVmYXVsdDoKICAgICAgICAgICAgICAgIHIgPSBTU0hfRVJSX0lOVkFMSURfQVJHVU1FTlQ7CiAgICAgICAgICAgICAgICBnb3RvIG91dDsKICAgICAgICB9CisgICAgICAgbWF4ID0gTUlOKERIX0dSUF9NQVgsIG1heCk7CisgICAgICAgbWluID0gTUFYKERIX0dSUF9NSU4sIG1pbik7CisgICAgICAgbmJpdHMgPSBNSU4oREhfR1JQX01BWCwgbmJpdHMpOworICAgICAgIG5iaXRzID0gTUFYKERIX0dSUF9NSU4sIG5iaXRzKTsKIAogICAgICAgIGlmIChrZXgtPm1heCA8IGtleC0+bWluIHx8IGtleC0+bmJpdHMgPCBrZXgtPm1pbiB8fAogICAgICAgICAgICBrZXgtPm1heCA8IGtleC0+bmJpdHMpIHsKCg%3D%3D">patch</a> for <a title="OpenSSH" href="http://www.openssh.com/">OpenSSH</a> that raises the minimum field size allowed for the <code>diffie-hellman-group-exchange-sha256</code> key exchange for both the client and server.
This means you do not need to edit the <code>/etc/ssh/moduli</code> file to increase the minimum field size for the server, but it will not hurt to do so either.
</p><p>If you are running <a title="NixOS Linux" href="https://nixos.org/">NixOS</a> you can download the patch and add it to your <code>/etc/nixos/configuration.nix</code> file with the following attribute.
</p><pre> nixpkgs.config.packageOverrides = oldpkgs: {
openssh = pkgs.lib.overrideDerivation oldpkgs.openssh (oldAttrs: {
patches = oldAttrs.patches ++ [ <a href="data:text/plain;base64,QXV0aG9yOiBSdXNzZWxsIE8nQ29ubm9yIDxvY29ubm9yckBnb29nbGUuY29tPgpkaWZmIC11ciBvcGVuc3NoLTYuOHAxLm9yaWcvZGguaCBvcGVuc3NoLTYuOHAxL2RoLmgKLS0tIG9wZW5zc2gtNi44cDEub3JpZy9kaC5oICAgICAyMDE1LTA1LTA0IDExOjQ4OjA2LjYxODI3ODU0OCAtMDQwMAorKysgb3BlbnNzaC02LjhwMS9kaC5oICAyMDE1LTA1LTA0IDExOjQ4OjM1LjgyNTcwNDM1NSAtMDQwMApAQCAtNDMsOCArNDMsNyBAQAogCiB1X2ludCAgIGRoX2VzdGltYXRlKGludCk7CiAKLS8qIE1pbiBhbmQgbWF4IHZhbHVlcyBmcm9tIFJGQzQ0MTkuICovCi0jZGVmaW5lIERIX0dSUF9NSU4gICAgIDEwMjQKKyNkZWZpbmUgREhfR1JQX01JTiAgICAgMjA0OAogI2RlZmluZSBESF9HUlBfTUFYICAgICA4MTkyCiAKIC8qCmRpZmYgLXVyIG9wZW5zc2gtNi44cDEub3JpZy9rZXhnZXhjLmMgb3BlbnNzaC02LjhwMS9rZXhnZXhjLmMKLS0tIG9wZW5zc2gtNi44cDEub3JpZy9rZXhnZXhjLmMgICAgICAgIDIwMTUtMDUtMDQgMTE6NDg6MDYuNjIxMjc4NTkyIC0wNDAwCisrKyBvcGVuc3NoLTYuOHAxL2tleGdleGMuYyAgICAgMjAxNS0wNS0wNCAxMjowMjo1MS40NzcwMDA0MzAgLTA0MDAKQEAgLTYxLDYgKzYxLDggQEAKICAgICAgICB1X2ludCBuYml0czsKIAogICAgICAgIG5iaXRzID0gZGhfZXN0aW1hdGUoa2V4LT5kaF9uZWVkICogOCk7CisgICAgICAgIG5iaXRzID0gTUlOKERIX0dSUF9NQVgsIG5iaXRzKTsKKyAgICAgICAgbmJpdHMgPSBNQVgoREhfR1JQX01JTiwgbmJpdHMpOwogCiAgICAgICAga2V4LT5taW4gPSBESF9HUlBfTUlOOwogICAgICAgIGtleC0+bWF4ID0gREhfR1JQX01BWDsKZGlmZiAtdXIgb3BlbnNzaC02LjhwMS5vcmlnL2tleGdleHMuYyBvcGVuc3NoLTYuOHAxL2tleGdleHMuYwotLS0gb3BlbnNzaC02LjhwMS5vcmlnL2tleGdleHMuYyAgICAgICAgMjAxNS0wNS0wNCAxMTo0ODowNi42MjEyNzg1OTIgLTA0MDAKKysrIG9wZW5zc2gtNi44cDEva2V4Z2V4cy5jICAgICAyMDE1LTA1LTA0IDEyOjEwOjI1LjE0NTQyODk0NCAtMDQwMApAQCAtODcsMTAgKzg3LDYgQEAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKICAgICAgICAgICAgICAgIGtleC0+bmJpdHMgPSBuYml0czsKICAgICAgICAgICAgICAgIGtleC0+bWluID0gbWluOwogICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXg7Ci0gICAgICAgICAgICAgICBtaW4gPSBNQVgoREhfR1JQX01JTiwgbWluKTsKLSAgICAgICAgICAgICAgIG1heCA9IE1JTihESF9HUlBfTUFYLCBtYXgpOwotICAgICAgICAgICAgICAgbmJpdHMgPSBNQVgoREhfR1JQX01JTiwgbmJpdHMpOwotICAgICAgICAgICAgICAgbmJpdHMgPSBNSU4oREhfR1JQX01BWCwgbmJpdHMpOwogICAgICAgICAgICAgICAgYnJlYWs7CiAgICAgICAgY2FzZSBTU0gyX01TR19LRVhfREhfR0VYX1JFUVVFU1RfT0xEOgogICAgICAgICAgICAgICAgZGVidWcoIlNTSDJfTVNHX0tFWF9ESF9HRVhfUkVRVUVTVF9PTEQgcmVjZWl2ZWQiKTsKQEAgLTk5LDEzICs5NSwxNyBAQAogICAgICAgICAgICAgICAgICAgICAgICBnb3RvIG91dDsKICAgICAgICAgICAgICAgIGtleC0+bmJpdHMgPSBuYml0czsKICAgICAgICAgICAgICAgIC8qIHVudXNlZCBmb3Igb2xkIEdFWCAqLwotICAgICAgICAgICAgICAga2V4LT5taW4gPSBtaW4gPSBESF9HUlBfTUlOOwotICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXggPSBESF9HUlBfTUFYOworICAgICAgICAgICAgICAga2V4LT5taW4gPSBtaW4gPSAxMDI0OworICAgICAgICAgICAgICAga2V4LT5tYXggPSBtYXggPSA4MTkyOwogICAgICAgICAgICAgICAgYnJlYWs7CiAgICAgICAgZGVmYXVsdDoKICAgICAgICAgICAgICAgIHIgPSBTU0hfRVJSX0lOVkFMSURfQVJHVU1FTlQ7CiAgICAgICAgICAgICAgICBnb3RvIG91dDsKICAgICAgICB9CisgICAgICAgbWF4ID0gTUlOKERIX0dSUF9NQVgsIG1heCk7CisgICAgICAgbWluID0gTUFYKERIX0dSUF9NSU4sIG1pbik7CisgICAgICAgbmJpdHMgPSBNSU4oREhfR1JQX01BWCwgbmJpdHMpOworICAgICAgIG5iaXRzID0gTUFYKERIX0dSUF9NSU4sIG5iaXRzKTsKIAogICAgICAgIGlmIChrZXgtPm1heCA8IGtleC0+bWluIHx8IGtleC0+bmJpdHMgPCBrZXgtPm1pbiB8fAogICAgICAgICAgICBrZXgtPm1heCA8IGtleC0+bmJpdHMpIHsKCg%3D%3D">./openssh-dh-grp-min.patch</a> ];
});
};</pre>
<p>As an aside, I noticed that <a title="Diffie-Hellman Group Exchange for the Secure Shell (SSH) Transport Layer Protocol" href="https://www.ietf.org/rfc/rfc4419.txt">this key exchange protocol</a> has a design flaw in it.
The hash signed by the server is the hash of <code>V_C || V_S || I_C || I_S || K_S || min || n || max || p || g || e || f || K</code>.
The details of what those variables stand for is not important.
What is important is that there is a older format of the protocol that is supported for backwards compatibility where the hash signed by the server is the hash of <code>V_C || V_S || I_C || I_S || K_S || n || p || g || e || f || K</code>.
In this older protocol, the client only requests a field size without specifying the minimum and maximum allowed bounds.
This is why the variables <code>min</code> and <code>max</code> are do not appear in the hash of the older protocol.
A short header is sent by the client to determine which of these two versions of this protocol it is using.
</p><p>The problem is that this header is not part of the hashed data.
This little crack has potential to be an exploit.
A <abbr title="Man in the Middle">MITM</abbr> attacker could replace the header the client sends with the old protocol header, and then try to manipulate the remaining communication between the client and server so that both the client and server hash the same serialized byte string allowing the server to appear to be authenticated to the client, but where the client and server are interpreting that serialized byte string in two different ways.
In particular the <abbr title="Man in the Middle">MITM</abbr> wants the client to not be doing computation modulo some safe prime, but instead do modular arithmetic over a different ring entirely.
</p><p>Fortunately this particular little crack does not appear to be wide enough to exploit.
The incidental properties of the serialization format do not allow a successful manipulation, at least not in practical SSH configurations.
</p><p>When one is signing a serialized blob of data, it is important that the data can be unambiguously parsed using only the contents of that data.
This principle is violated here because one cannot decide if one will parse <code>min</code> and <code>max</code> without knowing the header, which is not part of the serialized blob of data.
The reason this failure can so easily creep into the protocol is that neither the client nor the server actually have to parse that blob of data.
They both serialize the data and then create or verify the signature, but parsing is never done. Therefore, parsing is never implemented.
Since parsing is not implemented, it is easy to miss that the data serialization format is ambigous.
</p>http://r6.ca/blog/20140921T175644Z.htmlHard Drive Failure2014-09-22T19:22:01Z2014-09-21T17:56:44Z
<p>A few weeks ago my desktop computer suffered catastrophic hard drive failure.
Not only did it not boot, it soon got to the point where even the <abbr title="Basic Input/Output System">BIOS</abbr> would fail to recognise the device.
At first I did not worry too much.
Although I was not doing automatic backups, I was still doing irregular weekly manual backups of my home directory with <a title="Tarsnap - Online backups for the truly paranoid" href="https://www.tarsnap.com/">tarsnap</a> and I had performed one about three days prior.
I was not specifically making backups of my <a title="NixOS Linux" href="https://nixos.org/">NixOS</a> system and user configuration, but I had some old copies.
The configuration files do not change much and they are less important.
Importantly, I had backups of my <a title="Tarsnap - Online backups for the truly paranoid" href="https://www.tarsnap.com/">tarsnap</a> keys stored in other places, such as my shell account.
</p><p>While waiting for a replacement drive to arrive, I realized I had a serious problem.
My <a title="Tarsnap - Online backups for the truly paranoid" href="https://www.tarsnap.com/">tarsnap</a> keys were encrypted with my <abbr title="Pretty Good Privacy">PGP</abbr> key.
I had two specific places where I kept backup of my <abbr title="Pretty Good Privacy">PGP</abbr> keys.
One place was a USB drive in a safe deposit box.
However, at some point I had taken that one out to update it, and then misplaced it before putting it back.
Naturally, I had been meaning to get around to replacing that USB drive and the data on it, for some number of years.
Also, to my surprise, I had never actually placed my <abbr title="Pretty Good Privacy">PGP</abbr> key in my secondary spot.
</p><p>I was sunk.
I had some very old hard drive images with older versions of my <abbr title="Pretty Good Privacy">PGP</abbr> key on it, but because I rotate my encryption keys every five years, they were not useful.
Within the last five years I had started using full disk encryption.
I had some newer hard drive images that also have my <abbr title="Pretty Good Privacy">PGP</abbr> keys but I need the passphrases to decrypt these images.
I had copies of the passphrase around, but, of course, they were all encrypted with my <abbr title="Pretty Good Privacy">PGP</abbr> keys.
</p><p>After an emotional day and some meditation, slowly my old passphrase came back to me and I was able to decrypt one of my disk images.
I was able to rescue my <abbr title="Pretty Good Privacy">PGP</abbr> keys and from there I was able to recover everything I had.
</p><p>I plan to get a bit more serious about distributing copies of my <abbr title="Pretty Good Privacy">PGP</abbr> key since I use it so widely.
With my <abbr title="Pretty Good Privacy">PGP</abbr> key I should be able to always recover everything since I keep all my other key material encrypted with it.
Instead of a single USB drive in a safe deposit box, I want to keep two identical USB keys, one at home and one in the box.
When I want to update the data, I will update the one at home, swap it with the one in the box, and update the second one and keep it at home until the next update is needed.
</p><p>I have also gotten more serious about automatic backup.
Turns out that <a title="NixOS Linux" href="https://nixos.org/">NixOS</a> already comes with a <a title="Tarsnap - Online backups for the truly paranoid" href="https://www.tarsnap.com/">tarsnap</a> system service.
All that one has to do is place one’s write-only <a title="Tarsnap - Online backups for the truly paranoid" href="https://www.tarsnap.com/">tarsnap</a> key in the appropriate place and specify which directories to back up.
I am hoping to make system recovery even easier by also backing up my <del datetime="20140922T192201Z"><ins datetime="20140922T013824Z"><kbd>~/.nix-profile/manifest.nix</kbd>, <kbd>/root/.nix-profile/manifest.nix</kbd>,</ins></del><ins datetime="20140922T192201Z"><kbd>/nix/var/nix/profiles/default/manifest.nix</kbd>, <kbd>/nix/var/nix/profiles/per-user/*/profile/manifest.nix</kbd>,</ins> <kbd>/etc/nixos</kbd> and <kbd>/var/lib</kbd>.<del datetime="20140922T013824Z">There are probably a few more things I should back up, like my user profiles, but I am not yet sure how best to do that.</del>
</p><p>I also want to restart my programme of escrow for my passwords in case something happens to me.
I need to improve my documentation of password list to make it easier for others to use.
I will use <a title="Shamir's Secret Sharing Scheme" href="http://point-at-infinity.org/ssss/">ssss</a> to split my master password and distribute among my escrow agents.
The nice thing about public-key cryptography is that I can assign escrow agents without requiring anything from them beyond the fact that they already possess and use <abbr title="Pretty Good Privacy">PGP</abbr> keys.
I do not even need to inform them that they are my escrow agents.
The encrypted components will be stored on my USB drive in the safe deposit box.
</p><p>Overall, I am glad to have narrowly avoid disaster and have definitely learned some lessons.
Check your backup policy everyone!
</p>http://r6.ca/blog/20140803T030905Z.htmlICFP 2014 Post-Mortem2014-08-03T03:09:05Z2014-08-03T03:09:05Z
<p>I participated in the 2014 ICFP programming contest this year.
This year’s task was to write an <abbr title="artifical intelligence">AI</abbr> for a simplified Pac-Man game called Lambda-Man.
You could write the <abbr title="artifical intelligence">AI</abbr> in any language you wanted, as long as it complies to a specific <abbr title="Stack, Environment, Control, Dump">SECD</abbr> machine architecture invented for the contest.
At the end of the lightening round, it was announced that the final task included writing an <abbr title="artifical intelligence">AI</abbr> for the ghosts as well.
Again, the ghost <abbr title="artifical intelligence">AI</abbr> could be written in any language, as long as it compiles to a separate 8-bit architecture invented for the contest.
</p><p>I spent the first several hours implementing my own simulator of the arcade.
Eventually I realized that I would have to start working on the <abbr title="artifical intelligence">AI</abbr> if I was going to have an entry for the 24-hour lightening division.
It was at that point I realized that the provided on-line simulator was plenty adequate for my needs and I never completed my simulator.
</p><p>I have some previous experience writing assembler <abbr title="domain specific langauge">DSL</abbr>s in Haskell to handle linking.
After the 2006 ICFP contest, our team wrote a fake UM-DOS shell so that we could submit our solution in UM format.
This lead me to writing <a title="Assembly: Circular Programming with Recursive do" href="https://www.haskell.org/wikiupload/1/14/TMR-Issue6.pdf">an
article in The Monad Reader</a> about how to write an assembler using recursive do.
After that, I encountered a really elegant and simple formulation of an assembler monad on some paste site.
Unfortunately, I do not recall the author, but here is how the implementation looks.
</p><pre>newtype Label = Label { unLabel :: Int }
data ASMMonad w a = ASMMonad { runASM :: Label -> ([w],a) }
instance Monad (ASMMonad w) where
return a = ASMMonad $ \_ -> ([], a)
x >>= y = ASMMonad (\(Label i) -> let (o0, a) = runASM x (Label i)
(o1, b) = runASM (y a) (Label (i+length o0))
in (o0 ++ o1, b))
instance MonadFix (ASMMonad w) where
mfix f = ASMMonad (\i -> let (o0, a) = runASM (f a) i in (o0, a))
execASM :: ASMMonad w a -> [w]
execASM m = fst $ runASM m (Label 0)</pre>
<p>Next one adds two primitive operations.
The <code>tell</code> function is similar to the version for the writer monad.
The <code>label</code> function returns the current index of the output stream.
</p><pre>tell :: [w] -> ASMMonad w ()
tell l = ASMMonad $ \_ -> (l,())
label :: ASMMonad w Label
label = ASMMonad $ \i -> ([],i)</pre>
<p>Lastly one makes an <code>ASMMonad</code>ic value for each assembly instruction
</p><pre>data ASM = LDC Int32 -- load constant
| LD Int Int -- load variable
| LDF Label -- load function
| ADD
{- … -}
deriving Show
ldc x = tell [LDC x]
ld x y = tell [LD x y]
ldf x = tell [LDF x]
add = tell [ADD]
{- … -}</pre>
<p>At the risk of jumping ahead too far, my compiler can produce linked assembly code very simply.
The clause below compiles a lambda abstraction to linked <abbr title="Stack, Environment, Control, Dump">SECD</abbr> assembly using recursive do.
</p><pre>compileH env (Abs vars body) = mdo
jmp end
begin <- label
compileH (update env vars) body
rtn
end <- label
ldf begin</pre>
<p>Thanks to recursive do, the first line, <code>jmp end</code>, refers to the <code>end</code> label which is bound in the second last line.
</p><p>With a <abbr title="domain specific langauge">DSL</abbr> assembler written in Haskell, I turned to creating another <abbr title="domain specific langauge">DSL</abbr> language in Haskell to compile to this assembly language.
The <abbr title="Stack, Environment, Control, Dump">SECD</abbr> machine is designed for Lisp compilers, so I created a little Lisp language.
</p><pre>data Binding a = a := Lisp a
data Lisp a = Var a
| Const Int32
| Cons (Lisp a) (Lisp a)
| Abs [a] (Lisp a)
| Rec [Binding a] (Lisp a)
{- … -}</pre>
<p>The <code>Abs</code> constructor builds an <var>n</var>-ary lambda function.
The <code>Rec</code> constructor plays the role of <kbd>letrec</kbd> to build mutually recursive references.
With some abuse of the <code>Num</code> class and <code>OverloadedStrings</code>, this Lisp <abbr title="domain specific langauge">DSL</abbr> is barely tolerable to program with directly in Haskell.
</p><pre> Rec [ {- … -}
,"heapNew" := ["cmp"]! (Cons "cmp" 0) -- heap layout 0 = leaf | (Cons (Cons /heap is full/ /value/) (Cons /left tree/ /right tree/))
-- "cmp" @@ ["x","y"] returns true when "x" < "y"
,"heapIsFull" := ["h"]! If (Atom "h") 1 (caar "h")
,"heapInsert" := ["cmpHeap", "v"]! Rec ["cmp" := (car "cmpHeap")
,"insert" := ["heap", "v"]! -- returns (Cons /new heap is full/ /new heap/)
If (Atom "heap") (Cons (Cons 1 "v") (Cons 0 0))
(Rec ["root" := cdar "heap"
,"left" := cadr "heap"
,"right" := cddr "heap"
] $
Rec ["swap" := "cmp" @@ ["v", "root"]] $
Rec ["newRoot" := If "swap" "v" "root"
,"newV" := If "swap" "root" "v"
] $
If (caar "heap" `ou` Not ("heapIsFull" @@ ["left"]))
(Rec ["rec" := "insert" @@ ["left", "newV"]] $
Cons (Cons 0 "newRoot") (Cons "rec" "right"))
(Rec ["rec" := "insert" @@ ["right", "newV"]] $
Cons (Cons ("heapIsFull" @@ ["rec"]) "newRoot") (Cons "left" "rec")))
]
(Cons "cmp" ("insert" @@ [cdr "cmpHeap","v"]))
{- … -}</pre>
<p>The <code>@@</code> operator is infix application for the Lisp langauge and the <code>!</code> operator is infix lambda abstraction for the Lisp langauge.
</p><p>This Lisp language compiles to the <abbr title="Stack, Environment, Control, Dump">SECD</abbr> assembly and the assembly is printed out.
The compiler is very simple.
It does not even implement tail call optimization.
There is a bit of an annoying problem with the compiler; the assembly code is structured in exactly the same way that the original Lisp is structured.
In particular, lambda abstractions are compiled directly in place, and since lambda expressions are typically not executed in the location they are declared,
I have to jump over the compiled code.
You can see this happening in the snippet of my compiler above.
I would have preferred to write
</p><pre>compileH env (Abs vars body) = do
fun <- proc (compileH (update env vars) body)
ldf fun</pre>
where <code>proc</code> is some function that takes an <code>ASMMonad</code> value and sticks the assembly code “at the end” and returns a label
holding the location where the assembly code got stashed.
However, I could not figure out a clever and elegent way of modifing the assembly monad to support this new primitive.
This is something for you to ponder.
<p>My Lambda <abbr title="artifical intelligence">AI</abbr>, written in my Lisp variant, is fairly simple and similar to other entries.
Lambda-Man searches out the maze for the nearest edible object.
It searches down each path until it hits a junction and inserts the location of the junction into a binary heap.
It also inserts the junction into a binary tree of encountered junctions.
If the junction is already in the binary tree, it does not insert the junction into the heap because it has already considered it.
The closest junction is popped off the heap, and the search is resumed.
</p><p>There is at least one bit of surprising behaviour.
If there is more than one path from one junction to another, sometimes Lambda-Man ends up taking the longer path.
This behaviour did not seem to be bothersome enough to warrant fixing.
</p><p>This programming task has renewed my appreciation for typed languages.
The Lisp language I developed is untyped, and I made several type errors programming in it.
Although it is true that I did detect (all?) my errors at run-time, they were still frustrating to debug.
In a typed language, when an invariant enforced by the type system is violated, you get a compile time error that, more or less, points to the code location where the invariant is violated.
In an untyped language, when an invariant is violated, you get a run-time error that, more or less, points to some point in the code where missing invariant has caused a problem.
While this often is enough to determine what invariant was violated, I had little idea where the code breaking the invariant was located.
</p><p>With some effort I probably could have used GADTs to bring Haskell’s type checker to the Lisp <abbr title="domain specific langauge">DSL</abbr>, but I was not confident enough I could pull that off in time.
</p><p>I also needed to write some ghost <abbr title="artifical intelligence">AI</abbr>s.
The 8-bit machine that the ghosts run on is so constrained, 256 bytes of data memory; 256 code locations; 8 registers, that it seemed to make sense to write the code in raw assembly.
</p><p>The first thing I tried was to make the ghosts move randomly.
This meant I needed to write my own pseudo-random number generator.
Wikipedia lead me to a paper on how to write long period <a title="Xorshift RNGs" href="http://www.jstatsoft.org/v08/i14/paper">xorshift random number generators</a>.
The examples in that paper are all for 32-bit or 64-bit machines, but I had an 8-bit architecture.
I wrote a little Haskell program to find analogous random number generators for 8-bit machines.
It found 6 possibilities for 32-bit state random number generator composed of four 8-bit words that satisfied the xorshift constraints described in the paper.
Here is the assembly code for getting a 2 bit pseudo-random value.
</p><pre>mov a,[0]
div a,2
xor [0],a
mov a,[0]
mul a,2
xor a,[0]
mov [0],[1]
mov [1],[2]
mov [2],[3]
mul [3],8
xor [3],[2]
xor [3],a
; get 2 bits
mov a,[3]
div a,64</pre>
<p>The random seed is held in memory locations [0] through [3].
After moving to the successive the state, this code takes 2 pseudo-random bits from memory location [3] and puts it into register <code>a</code>.
</p><p>I did not check the quality of this random number generator beyond constructing it so that it has a period of 2<sup>32</sup>-1.
I expect the bit stream to appear to be quite random.
</p><p>My Lambda-Man performed reasonably well against my random ghosts, so I put some effort into making my random ghosts a little smarter.
I wrote a ghost <abbr title="artifical intelligence">AI</abbr> that tried to get above Lambda-man and attack him from above.
Then I made each other ghost try to attack Lambda-man from the other three directions in the same manner.
The idea is to try to trap Lambda-man between two ghosts.
</p><p>These smarter ghosts were quite a bit more successful against my simple Lambda-man <abbr title="artifical intelligence">AI</abbr>.
At this point I was out of contest time, so that was it for my <a href="http://r6.ca/icfp2014/icfp2014.tar.gz">2014 ICFP contest submission</a>.
</p><p>Thanks to the organizers for a terrific contest problem.
I am looking forward to see the final rankings.
</p>http://r6.ca/blog/20140422T142911Z.htmlHow to Fake Dynamic Binding in Nix2014-04-22T14:29:11Z2014-04-22T14:29:11Z
<p>The <a title="About Nix" href="https://nixos.org/nix/">Nix language</a> is a purely functional, lazy, statically scoped configuration
language that is commonly used to specify <a title="The Nix Packages collection" href="https://nixos.org/nixpkgs/">software package configurations</a>, <a title="About NixOS" href="https://nixos.org/nixos/">OS system configurations</a>, <a title="About Disnix" href="https://nixos.org/disnix/">distributed system configurations</a>, and <a title="NixOps, the NixOS-based cloud deployment tool" href="https://github.com/NixOS/nixops">cloud system configurations</a>.
</p><p>Static scoping means that variables are statically bound;
all variable references are resolved based on their scope at declaration time.
For example, if we declare a set with recursive bindings,
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let a = rec { x = "abc"; x2 = x + "123"; }; in a
{ x = "abc"; x2 = "abc123"; }</pre>
then the use of <code>x</code> in the definition of <code>x2</code> is resolved to "abc".
Even if we later update the definition of <code>x</code>, the definition of <code>x2</code> will not change.
<pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let a = rec { x = "abc"; x2 = x + "123"; }; in a // { x = "def"; }
{ x = "def"; x2 = "abc123"; }</pre>
<p>Generally speaking, static binding is a good thing.
I find that languages with static scoping are easy to understand because variable references can be followed in the source code.
Static scoping lets <a title="About Nix" href="https://nixos.org/nix/">Nix</a> be referentially transparent, so, modulo α-renaming, you can always substitute expressions by their (partially) normalized values.
In the previous example, we can replace the expression <code>rec { x = "abc"; x2 = x + "123"; }</code> with <code>{ x = "abc"; x2 = "abc123"; }</code> and the result of the program does not change.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let a = { x = "abc"; x2 = "abc123"; }; in a // { x = "def"; }
{ x = "def"; x2 = "abc123"; }</pre>
<p>That said, on some occasions it would be nice to have some dynamic binding.
Dynamic binding is used in <a title="The Nix Packages collection" href="https://nixos.org/nixpkgs/">Nixpkgs</a> to allow users to override libraries with alternate versions in such a way that all other software packages that depend on it pick up the replacement version.
For example, we might have the following in our <code>nixpkgs</code> declaration
</p><pre><em>…</em>
boost149 = callPackage ../development/libraries/boost/1.49.nix { };
boost155 = callPackage ../development/libraries/boost/1.55.nix { };
boost = boost155;
<em>…</em></pre>
and perhaps we want to make <code>boost149</code> the default boost version to work around some regression.
If we write <code>nixpkgs // { boost = boost149; }</code> then we only update the <code>boost</code> field of the nix package collection and none of the packages depending on boost will change.
Instead we need to use the <a title="Overriding Existing Packages" href="https://nixos.org/w/index.php?title=Nix_Modifying_Packages&oldid=22874#Overriding_Existing_Packages"><code>config.packageOverrides</code></a> to change <code>boost</code> in such a way that all expressions depending on <code>boost</code> are also updated.
Our goal is to understand the technique that <code>packageOverrides</code> and other similar overrides employ to achieve this sort of dynamic binding in a statically scoped language such as <a title="About Nix" href="https://nixos.org/nix/">Nix</a>.
This same technique is also used to give <a title="Closed and Open Recursion" href="http://www.cs.ox.ac.uk/people/ralf.hinze/talks/Open.pdf">semantics to object-oriented languages</a>.
<p>First we need to review normal recursive bindings.
The <code>rec</code> operator is can almost be defined as a function in <a title="About Nix" href="https://nixos.org/nix/">Nix</a> itself by taking a fixed point.
Recall that in <a title="About Nix" href="https://nixos.org/nix/">Nix</a> lambda expressions are written as <code>x: <var>expr</var></code>.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint; in
let a = fix (self: { x = "abc"; x2 = self.x + "123"; }); in
a
{ x = "abc"; x2 = "abc123"; }</pre>
<p>The function <code>self: { x = "abc"; x2 = self.x + "123"; }</code> is an object written in the open recursive style.
By taking the fixpoint of this function, the recursion is closed yielding the desired value.
Written this way, we had to prefix the recursive references to <code>x</code> with <code>self.</code>.
However using <a title="About Nix" href="https://nixos.org/nix/">Nix</a>’s <code>with</code> operator, we can bring the values of <code>self</code> into scope allowing us to drop the prefix.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint; in
let a = fix (self: with self; { x = "abc"; x2 = x + "123"; }); in
a
{ x = "abc"; x2 = "abc123"; }</pre>
<p>This is pretty close to a definition of <code>rec</code>.
We can almost think of <code>rec { <var>bindings</var> }</code> as syntactic sugar for <code>fix (self: with self; { <var>bindings</var> })</code>.
</p><p>In order to override the definition of <code>x</code> instead up updating it, we need to intercept the definition of <code>x</code> before the open recursion is closed.
To this end, we write a <code>fixWithOverride</code> function that takes a set of overriding bindings and an open recursive object and applies the override bindings before closing the recursion.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint;
withOverride = overrides: f: self: f self // overrides;
fixWithOverride = overrides: f: fix (withOverride overrides f); in
let open_a = self: with self; { x = "abc"; x2 = x + "123"; }; in
fixWithOverride { x = "def"; } open_a
{ x = "def"; x2 = "def123"; }</pre>
<p>Success!
We have manage to override the definition of <code>x</code> and get the definition of <code>x2</code> updated automatically to reflect the new value of <code>x</code>.
Let us step through this code to see how it works.
First we defined <code>open_a</code> to be the same as our previous definition of <code>a</code>, but written as an open recursive object.
The expression <code>fixWithOverride { x = "def"; } open_a</code> reduces to <code>fix (withOverride { x = "def"; } open_a)</code>.
What the <code>withOverride</code> function does is takes an open recursive object and returns a new open recursive object with updated bindings.
In particular, <code>withOverride { x = "def"; } open_a</code> reduces to</p><pre>self: (with self; { x = "abc"; x2 = x + "123"; }) // { x = "def"; }</pre>
which in turn reduces to <code>self: { x = "def"; x2 = self.x + "123"; }</code>.
Finally, <code>fix</code> takes the fixpoint of this updated open recursive object to get the closed value <code>{ x = "def"; x2 = "def123"; }</code>.
<p>This is great; however, we do not want to have to work with open recursive objects everywhere.
Instead, what we can do is build a closed recursive value, but tack on an extra field named <code>_override</code> that provides access to <code>withOverride</code> applied to the open recursive object.
This will allow us to perform both updates and overrides at our discretion.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint;
withOverride = overrides: f: self: f self // overrides;
virtual = f: fix f // { _override = overrides: virtual (withOverride overrides f); }; in
let a = virtual (self: with self; { x = "abc"; x2 = x + "123"; }); in rec
{ example1 = a;
example2 = a // { x = "def"; };
example3 = a._override { x = "def"; };
example4 = example3._override { y = true; };
example5 = example4._override { x = "ghi"; };
}
{ example1 = { _override = <LAMBDA>; x = "abc"; x2 = "abc123"; };
example2 = { _override = <LAMBDA>; x = "def"; x2 = "abc123"; };
example3 = { _override = <LAMBDA>; x = "def"; x2 = "def123"; };
example4 = { _override = <LAMBDA>; x = "def"; x2 = "def123"; y = true; };
example5 = { _override = <LAMBDA>; x = "ghi"; x2 = "ghi123"; y = true; };
}</pre>
<p>One remaining problem with the above definition of <code>virtual</code> is that we cannot override the method <code>x2</code> and still get access to <code>x</code>.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint;
withOverride = overrides: f: self: f self // overrides;
virtual = f: fix f // { _override = overrides: virtual (withOverride overrides f); }; in
let a = virtual (self: with self; { x = "abc"; x2 = x + "123"; }); in
a._override { x2 = x + "456"; }
error: undefined variable `x' at `(string):5:23'</pre>
<p>Remembering that <a title="About Nix" href="https://nixos.org/nix/">Nix</a> is statically scoped, we see that the variable <code>x</code> in <code>a._override { x2 = x + "456"; }</code> is a dangling reference and does not refer to anything in lexical scope.
To remedy this, we allow the <code>overrides</code> parameter to <code>withOverride</code> to optionally take a open recursive object rather than necessarily a set of bindings.
</p><pre><a href="data:text/plain;base64,VG8gZm9sbG93IGFsb25nIGF0IGhvbWUsIHJ1biB0aGUgY29tbWFuZCBuaXgtaW5zdGFudGlhdGUgLS1zdHJpY3QgLS1ldmFsLW9ubHkgLSBhbmQgcGFzdGUgdGhlIE5peCBleHByZXNzaW9uIGZvbGxvd2VkIGJ5IGN0cmwtRC4gIEZvciBleGFtcGxlDQoNCiQgbml4LWluc3RhbnRpYXRlIC0tc3RyaWN0IC0tZXZhbC1vbmx5IC0NCmxldCBhID0gcmVjIHsgeCA9ICJhYmMiOyB4MiA9IHggKyAiMTIzIjsgfTsgaW4gYQ0KPGN0cmwtRD4NCnsgeCA9ICJhYmMiOyB4MiA9ICJhYmMxMjMiOyB9DQoNCg%3D%3D">❄</a>> let fix = f: let fixpoint = f fixpoint; in fixpoint;
withOverride = overrides: f: self: f self //
(if builtins.isFunction overrides then overrides self else overrides);
virtual = f: fix f // { _override = overrides: virtual (withOverride overrides f); }; in
let a = virtual (self: with self; { x = "abc"; x2 = x + "123"; }); in rec
{ example6 = a._override (self: with self; { x2 = x + "456"; });
example7 = example6._override { x = "def"; };
}
{ example6 = { _override = <LAMBDA>; x = "abc"; x2 = "abc456"; };
example7 = { _override = <LAMBDA>; x = "def"; x2 = "def456"; };
}</pre>
<p>This illustrates is the basic technique that <code>packageOverrides</code> and other similar overrides use.
The <code>packageOverrides</code> code is a bit more complex because there are multiple points of entry into the package override system, but the above is the essential idea behind it.
The <code>makeOverridable</code> function from <a href="https://github.com/NixOS/nixpkgs/blob/5fef92c4a0c91153e3edac3a61a232581765074a/lib/customisation.nix#L56"><kbd>customisation.nix</kbd></a> creates an <code>override</code> field similar to my <code>_override</code> field above, but overrides function arguments rather than overriding recursive bindings.
</p><p>The syntax <code>virtual (self: with self; { <var>bindings</var> })</code> is a little heavy.
One could imagine adding a <code>virtual</code> keyword to <a title="About Nix" href="https://nixos.org/nix/">Nix</a>, similar to <code>rec</code>, so that <code>virtual { <var>bindings</var> }</code> would denote this expression.
</p><p>After writing all this I am not certain my title is correct.
I called this faking dynamic binding, but I think one could argue that this is actually real dynamic binding.
</p>http://r6.ca/blog/20140210T181244Z.htmlvan Laarhoven Free Monad2014-02-12T02:20:34Z2014-02-10T18:12:44Z
<p>As <a title="On the Static Nature of Traversals" href="20121209T182914Z.html">I mentioned some time ago</a>, <a title="http://www.fceia.unr.edu.ar/~mauro/">Mauro Jaskelioff</a> and I have been working on <a title="A Representation Theorem for Second-Order Functionals" href="http://arxiv.org/abs/1402.1699">a paper</a> discussing Twan van Laarhoven’s representation of second order functionals used in van Laarhoven lenses and traversals.
Mauro’s theorem is a generalization of <a title="Lenses, Stores, and Yoneda" href="http://bartoszmilewski.com/2013/10/08/lenses-stores-and-yoneda/"> Milewski’s proof</a> that, by using two applications of the Yoneda lemma, one can exhibit an isomorphism between <code>PStore i j a</code> and <code>forall f. Functor f => (i -> f j) -> f a</code> where <code>PStore</code> is the parameterized store comonad defined below.
</p><pre>data PStore i j a = PStore { pos :: i; peek :: j -> a }</pre>
<p>Mauro’s theorem, discovered independently at the same time as Milewski’s, adds an adjunction to the mix leading to an isomorphism that works for lenses, traversals, affine traversals, and more.
It is the ‘and more’ that I want to discuss.
</p><p>One application of Mauro’s theorem is the <dfn>van Laarhoven free monad
representation for algebraic effects</dfn>, or <dfn>van Laarhoven free monad</dfn> for short.
The basic theorem states that <code>FreeMonad (PStore i j) a</code> and <code>forall m. Monad m => (i -> m j) -> m a</code> are isomorphic.
The advanced version states that <code>FreeMonad (Σ n. PStore i<sub>n</sub> j<sub>n</sub>) a</code> and <code>forall m. Monad m => (Π n. i<sub>n</sub> -> m j<sub>n</sub>) -> m a</code> are isomorphic.
</p><pre><ins datetime="20140211T022330Z">data FreeMonad f a = Return a | FreeMonad (f (FreeMonad f a))</ins></pre>
<p>A free monad of a sum of store functors is the exactly the sort of free monad that Swierstra uses to model I/O interactions in <a href="http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf">Data Types à la Carte</a>.
For example, Swierstra models teletype I/O by a free monad generated from the following functor.
</p><pre>data Teletype a = GetChar (Char -> a) | PutChar Char a</pre>
<p>The <code>Teletype</code> functor is isomorphic to <code>PStore () Char + PStore Char ()</code>, thus is the sum of store functors.
This means <code>FreeMonad Teletype a</code> is isomorphic to the van Laarhoven free monad type <code>forall m. Monad m => TeletypeOps m -> m a</code> where <code>TeletypeOps</code> is the following record type.
</p><pre>data TeletypeOps m = TeletypeOps { getChar :: m Char; putChar :: Char -> m () }</pre>
<p>A value of type <code>forall m. Monad m => TeletypeOps m -> m a</code> can be interpreted in the standard way by passing in the record <code>TeletypeOps Prelude.getChar Prelude.putChar :: TeletypeOps IO</code>, but we are free to give other interpretations.
For example, if we have a handle <code>h :: Handle</code> in our context then we can interpret our value by passing in the record
<code>TeletypeOps (Prelude.hGetChar h) (Prelude.hPutChar h) :: TeletypeOps IO</code>.
We could give a ‘pure’ interpretation to our value in order to use it in testing à la <a href="http://hackage.haskell.org/package/IOSpec">IOSpec library</a>.
We could give a console interpretation where we also log all inputs.
We could give an interpretation where we replay logged inputs.
The list of possibilities is endless.
</p><p><ins datetime="20140212T022034Z">The van Laarhoven free monad <em>is</em> a monad. Below is how one can implement it in Haskell. Try not to let the impredicativity hurt your head too much.</ins></p><pre><ins datetime="20140212T022034Z">-- (ops m) is required to be isomorphic to (Π n. i_n -> m j_n)
newtype VLMonad ops a = VLMonad { runVLMonad :: forall m. Monad m => ops m -> m a }
instance Monad (VLMonad ops) where
return a = VLMonad (\_ -> return a)
m >>= f = VLMonad (\ops -> runVLMonad m ops >>= f' ops)
where
f' ops a = runVLMonad (f a) ops</ins></pre>
<p>Swierstra notes that by summing together functors representing primitive I/O actions and taking the free monad of that sum, we can produce values use multiple I/O feature sets.
Values defined on a subset of features can be lifted into the free monad generated by the sum.
The equivalent process can be performed with the van Laarhoven free monad by taking the product of records of the primitive operations.
Values defined on a subset of features can be lifted by composing the van Laarhoven free monad with suitable projection functions that pick out the requisite primitive operations.
No doubt someone will develop a library implementing a type class(y) hierarchy to make this process transparent, which may or may not be a good idea.
</p><p>The van Laarhoven free monad provides yet another way of representing a
monadic foreign function interface to <a title="Free Monads for Less (Part 3 of 3)" href="http://comonad.com/reader/2011/free-monads-for-less-3/">Kmett’s list of representations</a>.
Now, I am not much for practical applications of theory, so I will leave it to others to determine how practical the van Laarhoven free monad representation is.
I am optimistic it will be competitive with Kmett’s representation, and might even be cheaper.
</p>http://r6.ca/blog/20130710T012527Z.htmlKey Stretching2013-07-10T01:25:27Z2013-07-10T01:25:27Z
<p>I have been on a bit of a key stretching binge this week.
There is a <a title="Improving the security of your SSH private key files" href="http://martin.kleppmann.com/2013/05/24/improving-security-of-ssh-private-keys.html">wonderful article on how to stretch your ssh keys</a>.
Apparently, by default all that stands between your ssh passphrase and your ssh key is a single round of MD5 with 8 bytes of salt.
However, because ssh relies upon openssl, you can change the password format to use PBKDF2.
It is really easy to do. I highly recommend doing it.</p><p>Next up, I have been wanting to add key streching to my disk encryption for a while.
The problem is that when dm-crypt operates in plain mode, it simply hashes your passphrase once with a given hash.
I am not a big fan of LUKS because the LUKS headers make it really apparent there is encrypted data on your drive rather than a wiped hard disk.
Since I was going to need to stretch my passphrase by hand, I figured I might as well use <a title="The scrypt Password-Based Key Derivation Function" href="http://tools.ietf.org/html/draft-josefsson-scrypt-kdf-01">scrypt</a>.
The problem was that I could not find any stand-alone implementation of scrypt, so I cobbled together <a href="http://r6.ca/crypto_scrypt-0.0/crypto_scrypt.c">my own stand-alone <kbd>crypto_scrypt</kbd> utilty</a>.
It is not pretty; it is in serious need of some command line parameter love; but it works.
I even make <a href="http://r6.ca/crypto_scrypt-0.0/crypto_scrypt.nix">a little <kbd>crypto_scrypt</kbd> nix expression</a> so I could integrate it into my boot process.
</p>http://r6.ca/blog/20121217T010953Z.htmlInvestment Recovery2012-12-17T01:09:53Z2012-12-17T01:09:53Z
<p>I starting investing in mutual funds in 2007 after reading "A Random Walk Down Wall Street".
The book taught me the difference between systematic and non-systematic risk in equities and convinced me that buying equities was a good investment for retirement.
The book also convinced me that one cannot time the market. So I took my existing savings and bought some mutual funds.</p><p>Then the 2008 financial crash hit.</p><p>This week my investments finally recovered.
I now have an <a href="http://en.wikipedia.org/wiki/Internal_rate_of_return">XIRR</a> of 0.08% per year.
Since I measure my value in Canadian dollars, it took me longer to recover than those measuring in US dollars or Euros.
The Canadian dollar has appreciated quite a bit in the last six years.</p><p>I stand by my financial choices. After all, I will have far more in future saving than I have in past savings.
</p>