26 December, 2010

cybersyn

I found this in wikipedia:

Project Cybersyn was a Chilean attempt at real-time computer-controlled planned economy in the years 1970–1973 (during the government of president Salvador Allende). It was essentially a network of telex machines that linked factories with a single computer centre in Santiago, which controlled them using principles of cybernetics.

I think that's quite an interesting cross-over between socialism and computer control.

The wikipedia page has a cool pic of the "control room" which looks totally Star Trek (although other reading suggests that was a prototype control room and not actually used in real life).

19 December, 2010

latex double-cite

Turns out LaTeX you can write markup like
\cite{a,b}

to get multiple citations in the same place like this: [1,2]

Which is kinda obvious.

But I'd never thought of it.

26 September, 2010

foreign sim cards work better

international mobile phone roaming has a strange property: in any particular location, a foreign roaming sim card gets better coverage rather than a local sim card: generally all local networks are available for a foreign sim card to connect to, but only one network is available for the local network.

12 September, 2010

extreme diving for work

Some quotes from a paper on the Reduced Gradient Bubble Model for scuba diving decompression calculation which I've been looking at recently. Most of what I've looked at so far has been recreational no-decompression diving, so the dives described below seem quite extreme. (for comparison, the deepest recreational dives are to about 40 metres = 130 feet, and for a maximum of 8 minutes)

Pearling fleets, operating in the deep tidal waters off northern Australia, employed Okinawan divers who regularly journeyed to depths of 300 f sw for as long as one hour, two times a day, six days per week, and ten months out of the year.
[...]
With higher incidence of surface decompression sickness, as might be expected, the Australians devised a simple, but very effective, in-water recompression procedure. The stricken diver is taken back down to 30 fsw on oxygen for roughly 30 minutes in mild cases, or 60 minutes in severe cases. Increased pressures help to constrict bubbles, while breathing pure oxygen maximizes inert gas washout (elimination).

Similar schedules and procedures have evolved in Hawaii, among diving fishermen [...] Harvesting the oceans for food and profit, Hawaiian divers make beween 8 and 12 dives a day to depths beyond 350fsw.
[...]
Consistent with bubble and nucleation theory, these divers make their
deep dive first, followed by shallower excursions.
[...]
In a broad sense, the final shallow dives have been tagged as prolonged safety stops.

05 September, 2010

new photo frame

On sale, €33 at Media Markt, I got a digital photo frame.

It has a slot for a USB stick, and for various memory cards. It looks like an upgraded version of one I bought for my parents a year ago, where the USB interface worked well but the card reader seemed unreliable. So I put one of the many free conference USB sticks in my collection in.

People seem to have an instinct to unplug these things continuously. Why? You don't put curtains over the print photos on your wall and only open the curtains for a few minutes at a time to look at the photos behind.

The frame is 16:9 aspect ratio. My camera makes files of ratio 4:3 (or 3:4 in landscape). (apparently print photos are usually 3:2. my camera has a helper mode that overlays grey bars on screen to show you 3:2 ratio. But it doesn't have a similar mode for 16:9)

On my laptop, I have gimp. But I found that Preview is good enough for rough cropping of photos to size. That's the technical side of cropping easily dealt with. On the artistic side, though, its hard to get in the habit of evaluating photos for such cropping - photos that I think of as "too much space at the top / bottom" are ones that are perfect for this frame, and photos that fill the frame nicely are too full for cropping.

As the frame is so low resolution (~ VGA) its possibly to crop smaller details from a frame, so that you end up with an entirely new picture rather than something that looks like the original photo but a bit cropped.

I've had a desire but not enough motivation to actually look at my photos from a cropping perspective. Perhaps this will provide the motivation.

29 August, 2010

nominal, ordinal, interval, ratio

Decision by Objectives (DBO) classes applications of numbers into a hierarchy of four different types, each building on the properties of the previous one.

The concepts are not unfamiliar at all to a mathematician, but they are approaching from a management direction rather than from pure mathematics, and I think that is an interesting different perspective.

The first application of numbers is nominal. In this application, numbers are used to name things. DBO gives examples from horse racing: The number on a jockey or a horse is a nominal use. It identifies a particular jockey or horse; but it is meaningless to (for example) add two jockey numbers together, or divide one by another. In Maths, that means it is possible to permute the numbers in any way without losing any information. The numbers, ℕ, are used purely as a set of distinct objects without structure or relation. We could equally well use any other sufficiently large set of symbols (such as letters).

The next application of numbers is ordinal. In this application, numbers are used to order things. In the horse racing example, the finishing order of the horses is an ordinal application. Some horse finishes first, another finishes second, yet another finishes third. In Maths, there is a linear order between the numbers, and we have a relation < or ≤ that makes sense. We can compare numbers in this application, with a notion of bigger or faster or stronger). But it still doesn't make sense to (for example) add or subtract those numbers, or to make statements like "horse X finished 3 places ahead of horse y".



The third application of numbers is interval. It makes sense to subtract interval numbers from each other. The authors are a little vague in DSO about whether they think it makes sense to add interval numbers. I think in some applications it does (how much chocolate did you eat? how much chocolate did I eat? we can compute: how much chocolate did we eat together?) but in some it does not (what is the time now? what time did the meeting start? we can compute: how long has the meeting been going on (subtraction), but adding the time now and the meeting start time doesn't make sense). When it does make sense to add, the numbers form a group with operation +. When it only makes sense to take the difference, then the numbers form something like a torsor - a group without identity.

The final application is ratio. These is use of numbers where ratios make sense - for example, a horse might finish in half the time of another, meaning that the ratio of the time of the first horse to the second horse is 1/2. It makes sense to multiply and divide these numbers; and ratios can also be used to scale interval numbers. Mathematically, we have a (meaningful use of a) field, ℝ or ℚ.

The point of them making these distinctions in DSO was to point out that just because you have some information in your decision making represented as numbers, it doesn't always make sense to do things like taking the mean, or summing, or whatever.

22 August, 2010

rsync --fake-super

Every now and then I discover new options on old utilities.

One I am very happy to have discovered in rsync is the --fake-super option.

Scenario:

I have machine A. I want to back up (some portion of) the file system onto machine B. I want to include permissions and ownership (for example, because I am backing up /home.

I can run rsync on machine A as root from a cron job. OK. But then (traditionally) it needs root access to machine B in order to set permissions and ownersip of the files it creates. I can't have it connect to machine B as some normal user because of that. Additionally, the user-id and group-id name/number spaces on both machines need to match up somewhat so that users on machine B don't get access to files they shouldn't have access to.

--fake-super changes that. When rsync tries to change the permission or ownership of a file and finds that it cannot do that, it instead stores that information in extended attributes on that file. So now access to machine B can be through some normal user account without special privileges.

A downside is that if some user has an account on both sides, they don't get full privilege access to the backups of their own files.

Another use I found for this is on my laptop under OS X, where one of my external hard-drives is now mounted with an option to prevent user and group IDs being changed, or makes them ignored somehow (presumably for a better experience when using the hard-drive on multiple machines).
Incremental rsync backups were experience an inability to change group ownership on files, which mean that instead of being hard-linked (using --link-dest) they were being copied afresh each time. This was fixed by --fake-super too - instead of changing ownership on the external HD filesystem, they're added to the extended attributes.

18 August, 2010

fractions and proof-irrelevance IV - forgetting proofs

Continuing from previous posts on implementing fractions in Agda.

We've tried to force our representations of fractions to have a canonical form, but requiring the inclusion of a proof of that canonical form breaks canonicity.

So we need a different approach.

Data.Rational does it something like this, which I found hard to understand at first. Trying to understand isCoprime here was the motivation for this sequence of posts:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : True (coprime? ( ∣ numerator ∣ ) (suc denominator-1))

isComprime is different. Rather than directly expressing a proposition (Coprime numerator (suc denominator-1)) as the type of isCoprime, we instead use a slightly different proposition (coprime?) and wrap it in True.

coprime? has type Decidable Coprime. It is a decidable version of the coprime proposition. A normal proposition type has values that are proofs of that proposition. If I give you a proof, then you know the proposition is true. However, if I don't give you a proof, you don't know that the proposition is false. Perhaps its true but I haven't given you a proof. A decidable proposition type has values that are either proofs that the proposition is true, or proofs that the proposition is false, wrapped in yes or no respectively. coprime? is a function that decide whether two numbers are coprime or not, and return a corresponding proof.

True is a function that maps a decidable proposition type into another type: either ⊤ (when the proposition is true) or ⊥ (when the proposition is false).

⊤ (top) is the unit type, that has only one member value. ⊥ (bottom) is the empty type with no member values at all.

Both of those seem a bit useless to a traditional programmer: if I have a variable of the unit type ⊤, it can only have one value. So then I'll always know what that value is - its pretty much a constant. So why have a variable? And if I have a variable of the empty type ⊥ then I can't ever invent a value. If that variable is an input parameter, I can never even call my program, because I can't give input parameters. But it turns out this weird behaviour is exactly right for Data.Rational.

Say I'm going to construct a half. I'm going to pass numerator = 1 and denominator = 2. We also need to pass an isCoprime parameter.

To start with, what type of parameter is that?

That depends on the value of numerator and denominator (that's what dependent types are). Once we know the numerator and denominator, we can evaluate the expression True (coprime? ( ∣ numerator ∣ ) (suc denominator-1)) to find out the type of isCoprime. 1 and 2 are coprime, so coprime? evaluates to yes _, and so True (yes _) evaluates to ⊤.

So we need to give a value for coprime that is of type ⊤. ⊤ only has one value, so thats the value that we'll put in isCoprime. The resulting structure has no proof of coprimality in it. If two fractions have the same numerator and denominator, then they'll always have the same value of isCoprime. So we've got equality of equivalent fractions!

But now what happens if we try to construct a non-canonical fraction, for example 3/6 ?
Once we have specified a numerator of 3 and a denominator of 6, we can figure out the type of isCoprime. 3 and 6 are not coprime, and True (no _) will return ⊥.
So we need to provide a value of type ⊥. There are no values in ⊥. So there is no way we can call the constructor in this case, because we can't come up with a value for each parameter.

So now the goal is achieved - a data structure for representing rationals, where equal rationals are definitionally equal.

My goal in picking apart Data.Rational like this was two-fold: i) I wanted to use rationals, and wanted to understand what was going on; ii) I want to implement my own canonical forms (for finitely-generated abelian groups) and understanding how its done for rationals seems like a step in the right direction.

fractions and proof-irrelevance III - proofs are too isomorphic to values

Continuing from my earlier post about fractions and proof-irrelevance...

In the previous post, we added a parameter to the rational constructor to require the numerator and denominator of rationals to be coprime, in order that we can only construct canonical rationals, so that we get equality that behaves "right" - when two fractions are the same, they will be equal in the eyes of Agda.

But the way we did it doesn't work quite right:

The Curry-Howard correspondence connects propositions and proofs on one side, and datatypes/sets and values/elements of sets on the other side:

Side A Side B
Programmer view Maths view
Proposition Data type Set
Proof Value Element

When we added the coprimality test to the rational constructor, we added a parameter of type Coprime numerator denominator. That corresponds to the proposition that the numerator and denominator are coprime. Its a parameter so it will have a value when it is used to construct some rational, and that value will be a proof that the numerator and denominator are co-prime.

So now think about constructing a half. We'll put in numerator 1, and denominator 2, and some proof, pr1, that {1,2} are co-prime.

Now somebody else builds a half. They'll put in numerator 1, and denominator 2, and some proof, pr2, that {1,2} are co-prime.

Now I'm going to compare my half to that other person's half to see if they are equal. They're equal if all the constructor parameters are equal. The numerator, 1, matches. The denominator, 2, matches. But we have a third parameter now, the coprimality proof. Do they match? Does pr1 = pr2 ? In general, no, that isn't the case. There could be many different proofs of the same proposition.

So we've ended up with a canonical form for the numerator and denominator, but we've just pushed the problem into a different field of the data structure, and we still don't have a canonical data structure.

Somehow we want to insist that the coprime proposition is true, but without different proofs of that causing different representations of fractions. That is proof irrelevance.

Read on for part IV, the final part

fractions and proof-irrelevance II - equality of fractions

This continues from the first in a series of posts reviewing the implementation of Data.Rational in Agda.

We've got a datatype for representing fractions, ensuring that the denominator is strictly positive. So now any element of the mathematical set ℚ can be represented by an element in our datatype ℚ; and vice-versa any element of our datatype ℚ represents an element of the mathematical set ℚ.

Sometimes, we want to be able to compare fractions to see if they are the same or not. It's fairly straightforward to define an equivalence relation between two fractions, using integer multiplication, something like this:
p ≃ q  =  P.numerator ℤ* Q.denominator ≡ Q.numerator ℤ* P.denominator

But sometimes we want to use equivalence where we don't get to specify the equivalence relation. One example of that is type-checking: say we want to use a fraction (for some purpose) as part of a type specification. In that case, we need equivalent fractions to be definitionally equal: they must have been constructed with the same constructor, and the parameters to the constructor must be the same.

The numerator, denominator representation described in the previous post breaks down here: we can represent a half as numerator = 1, denominator = 2; but equally well as numerator = 3, denominator = 6. Yet, 1 ≠ 3 and 2 ≠ 6 so the two representations are not definitionally equal.

One way of solving this is by forcing the representations to be in some canonical form. For fractions, one such form is when the numerator and denominator are co-prime so that there are no shared factors. This way, 1/2 is the canonical representation of a half. 3/6 = (3*1) / (3*2) is not, because 3 is a factor of both the numerator and denominator.

So maybe we could demand that when you call the constructor for a fraction, you have to prove that the numerator and denominator are co-prime, by defining something like this:
record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : Coprime ( | numerator | ) (suc denominator-1)

That way, whenever we construct an element of ℚ, we'll know that the numerator and denominator are co-prime, because we give a proof of the proposition "Coprime numerator denominator" (see that we would add one onto denominator-1 to get the denominator).

Read on for part III...

fractions and proof-irrelevance I - sane denominators

This begins a series of posts reviewing the implementation of rationals in Agda.

I'll talk about broken ways of building the rationals ℚ in Agda, how its desirable to be able to compare rationals for equality, how having proofs in the language can get in the way of that, and how to cope with that.

This is all based on the code I found in the Data.Rational standard library module, which I have been trying to understand as I want to use both the module itself, and its techniques, in a scientific units-of-measurement library that I am writing.

Rationals

A rational (or a fraction) can be described as an integer (the numerator) divided by a strictly positive integer (the denominator).

It's not hard to build an Agda data type to represent a fraction as a pair of two integers:
data ℚ : Set where
    field
      numerator : ℤ
      denominator : ℤ

This implemenation doesn't require the denominator to be a positive integer, though. So we can represent "invalid" fractions. Most importantly, we can represent a fraction with denominator 0 this way, which is nonsensical.

So lets store the denominator minus 1 as a natural number (0, 1, 2, ...) like this:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ

The denominator minus 1 can be 0 or higher, which means the denominator can be 1 or higher - a positive integer as desired.

On the downside, now every time we want to compute with the denominator, we have to compute it first by adding one to the denominator minus 1.

This is a pattern I found strange (and still find unintuitive) in Agda. Rather than storing something in a format that you want (the denominator), you instead store it in a format that makes correctness work.

Read on for part II...

15 August, 2010

acetate slides

This pdf shows an interesting style of PDF slide generation that seems to be "acetates + digital camera". I guess they were presented on acetates to begin with and scanned in? Not so weird as I first though, which was that they were drawn on whiteboard and photographed... but still novel compared to powerpoint.

08 August, 2010

Erdős number

There's this concept of an Erdős number for an academic author: take the graph of academic authors where two authors are joined together if they have written a paper together; then your Erdős number is the number of hops from you to the currently deceased mathematician Paul Erdős.

I first read about him a decade ago in The Man Who Loved Only Numbers but I've never got round to actually computing my number 'till now.

Borja Sotomayor shares a co-author with me (Ian Foster), so my number is less than or equal to his. He is number 6, so my number is ≤6, through this chain:

Ben Clifford → Ian T. Foster → Patrick H. Worley → Robert S. Schreiber → John Russell Gilbert → Roger C. Entringer → Paul Erdös

(p.s. its hard to type the ő in Erdős. Its not ö, although it looks like it)

29 July, 2010

weight-based electrical measurement and other fun stuff

From a paper On the security economics of electricity metering by Ross Anderson and Shailendra Fuloria (via Bruce Schneier's blog), a few of quotes that amused me.
Edison invented a meter consisting of a jar holding two zinc plates: each month the electrodes were weighed and the customer billed according to the change in their weight.
and
For example, customers in Soweto noticed that their meters would set themselves to maximum credit in a brown-out (a voltage reduction to 160-180V) because they had not been tested adequately for African conditions; this only came to light when customers started throwing chains over the 11kV feeders in order to credit their meters.
and (about california):
generators had enough market power to boost peak prices by shutting down some of their plants for “maintenance reasons”. They had learned this trick in 1998 when the replacement reserve price of electricity peaked at $9,999.99/MW in July as against the average of $10/MW for the first three months of the year

A bit later they talk about contract languages, which reminds me very much of recent talk of expressing stock market contracts in Python:
This analysis suggests a technical research project: to design a command language for meters that enables an energy company to specify complex tariffs in a piece of signed downloaded code that would implement a particular contract between the supplier and the customer. The sort of tariff we have in mind is: “Your basic rate is 5p from midnight to 0600, 15p for the peak from 1730 to 2100 and 10p the rest of the time; however the 15p basic peak rate applies only provided you restrict demand to two kilowatts else it becomes 50p. Furthermore we may at any time request you to limit consumption to 1kW and if you don’t then any half-hour segment during which you draw more than 1kW at any time will be charged at 50p”. The code would have to export to the energy company enough data for it to bill the customer correctly, and enough to the distibution company for it to operate the system efficiently. This problem is nontrivial but we believe it is solvable.

23 July, 2010

branching on the left vs branching on the right (agda bubble sort part 3)

I gave a definition of onepass, the inner loop of my Agda bubblesort implementation, in an earlier post.

That wasn't the first implementation that I tried.

Instead, first I wrote it like this, in a way that uses with expressions. The difference is that the version I wrote uses an if construct that is manually defined. Agda seems to prefer doing case analysis / branching using with, which makes it seem as if you're getting a new parameter to pattern match on - in the below example, the results of y ≤? y which is either yes _ or no _.

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) with y ≤? y'
  ... | yes _ = y :: (onepass {suc n} (y' :: y0))
  ... | no _ = y' :: (onepass {suc n} (y :: y0))

For comparison, here's the definition in my first post:

onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then        
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0))  

The two implementations do the same thing at runtime - they swap the first two elements of the list and recurse. But their compile-time behaviour is different.

The with-based version doesn't pass the termination checker. The if-based one does.

The with-based version with with the proofs that I gave in part 2. The if based version doesn't.

So I pretty much am forced to choose: I can use the with-based definition, and turn off the termination checker in the Agda compiler. Or not. Either way seems pretty lame. In order to proof all this stuff, I have to turn off the termination checker which is a key part of checking the proofs that I'm writing.

I don't really understand what is going on inside Agda to make the first version not work. But that's what I actually use in practice (with termination checking turned off) - perhaps I can investigate a bit more later. But for now, I want to continue working on a proof (albeit not termination checked) that bubblesort actually sorts...

22 July, 2010

permutations (bubble sort in agda, pt 2)

(following from part 1)

I implemented bubblesort in Agda, and it looks bug-free. But I want to prove that it is correct. First I want to prove that the output is a permutation of the input. I'm not going to try proving anything about the ordering yet, but I want to know that at least I'm getting back the same list, rearranged.

This is where Agda starts getting really hard for me, and becomes more like stuff I did in my maths degree courses than stuff I've done with hobby computer hacking. Except you can't write "clearly, .... is true" in your Agda programs like you could in your maths homework, so you don't get to bluff your way through proofs quite so easily.

The previous post showed how you could augment the datatypes of the functions in your program to carry more information about how those functions behave. That's one way of using dependent types. In this post, I'm going to use a different style to prove that the output of bubblesort is a permutation.

The Curry-Howard isomorphism which (for the purposes of this post) says (for the purposes of this post) that you can regard propositions as types, and proofs of those propositions as values in those types.

So you define a type to represent whatever proposition it is you want to prove, and then you write a function that creates a value of that type - that value is then a proof of the proposition. When you use values normally, you care what that value is. When you use proofs though, you don't care so much what the proof is. You just care that the proof exists.

First I need to make a definition of what I mean by permutation. There are a few different ways I could have done this. I ended up settling on this one:

data SwapBasedPermutation {A : Set} : {n : ℕ} -> (Vec A n) -> (Vec A n) -> Set where

    reflexivity : {n : ℕ} -> (i : Vec A n) -> SwapBasedPermutation i i

    transitivity : {n : ℕ} -> {a : Vec A n} -> {b : Vec A n} -> {c : Vec A n} -> (SwapBasedPermutation a b) -> (SwapBasedPermutation b c) -> SwapBasedPermutation a c

    prepend : {pn : ℕ} -> {l r : Vec A pn } -> (e : A) -> (SwapBasedPermutation l r) -> SwapBasedPermutation (e :: l) (e :: r)

    swapheads : {pn : ℕ} -> {first second : A} -> {rest : Vec A pn} -> SwapBasedPermutation ( first :: second :: rest ) ( second :: first :: rest)

My permutations are swap-based. Given a list, you can swap the first two elements (using the swapheads constructor, and you get a proof that the first list (but only the first two elements, not some arbitrary pair of elements) is a permutation of the second; and given two lists that are permutations of each other, you can add the same element onto the front of both, and you get a proof that those two new lists will be permutations of each other (using the prepend constructor).

I also declare that permutations are reflexive and transitivitive by definition (although I think I could build those up from more fundamental parts, but I'm more interested in looking at the higher level behaviour of bubblesort).

Those are proofs-by-definition and so they are trivially true (at least as far as the type-checker is concerned).

Now given this SwapBasedPermutation type, I can write a theorem that the top level sortlist function (defined in my previous post) outputs a permutation of its input.

The theorem is a type signature for a function, and body of the function needs to generate a proof of that theorem:

The type signature for my theorem looks like this:

sortlist-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (sortlist l)

It says: for all ℕumbers n: for all Vectors l of length n: l is a permutation of sortlist l.

If we can write a definition for this function that typechecks correctly, then this theorem holds. We never actually need to invoke the function at runtime - it is enough to know that we could. (That's another thing thats a bit weird in Agda- you're writing functions that will never be called at runtime but they're still useful. I guess its like writing javadocs...)

Here its important that Agda functions are total - we need to know that our proof generating function really will return a value and not loop forever or error out. Otherwise, our theorem could typecheck but not really be proved.

Now that we've stated the theorem (as a type), we need to build the body (the proof).

To get there, we can define lemmas, in the same way that you can define helper functions to help implement your main function.

First, invoking onepass on a list permutes that list. onepass is the code in my implementation that actually re-orders the list, so the proof of this lemma makes use of the swaphead definition. It also recursively calls itself on a smaller list - that means we're using proof by induction. This definition roughly follows the shape of the definition of onepass itself.

lemma-onepass-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (onepass l)
  lemma-onepass-permutes [] = reflexivity []
  lemma-onepass-permutes (e :: []) = reflexivity (e :: [])
  lemma-onepass-permutes (y :: y' :: rest) with  y ≤? y'
  ... | yes _ = prepend y (lemma-onepass-permutes (y' :: rest))
  ... | no _ = let                      
       p1 = lemma-onepass-permutes (y :: rest)                              
       p2 = prepend y' p1
       p3 = swapheads -- magically the list that we're swapping the             
                      -- heads for is inferred (from use in p4)                 
       p4 = transitivity p3 p2
    in p4

Another lemma, this time about the behaviour of innersort:
lemma-innersort-permutes : {vn : ℕ } -> (sn : ℕ) -> (l : Vec ℕ vn) -> SwapBasedPermutation l (innersort sn l)
  lemma-innersort-permutes zero l = reflexivity l
  lemma-innersort-permutes (suc sm) l = let
             a = lemma-onepass-permutes l
                  -- this shows l is a permutation of onepass l                                  
             b = lemma-innersort-permutes sm (onepass l)
                  -- this shows that (onepass l) is a permutation of (innersort sm (onepass l))               
          in transitivity a b

and finally we can give our definition for our theorem, sortlist-permutes, using these lemmas:

sortlist-permutes {n} l = lemma-innersort-permutes  n l

And now, because sortlist-permutes typechecks correctly at compile time, I know that I can generate a proof that sortlist really does permute a list, no matter what list I give it.

Tada!

Except this doesn't actually typecheck in Agda due to a problem with my definition of onepass... see the next post.

21 July, 2010

bubblesort in agda (part 1)

I've been playing with Agda, a dependently typed programming language (where types of expressions can depend on earlier values).

Dependent types let you make quite rich compile-time assertions about the behaviour of your program. These assertions are written and checked using the type system.

One of the examples for Agda seems to be quicksort. So, I thought I'd experiment with bubblesort - similar but different.

First I want an implementation of bubblesort in Agda. Then I want to use dependent types to express something interesting that I cannot express in another language: that bubblesort really sorts.

Agda looks syntactically quite like Haskell, so I first made a Haskell implementation. This doesn't look like a procedural normal bubblesort implementation, as I wanted to keep a functional style.

bubblesort t = applyLoop t

applyLoop t = if isSorted t then t else applyLoop (onePass t)

onePass [e] = [e]
onePass t =
  let a:b:rest = t
      (as,bs) = if a < b then (a,b) else (b,a)
      newlist = as:bs:rest  -- list with head two elements in order
      bsrest = onePass (bs:rest)
      endlist = as:bsrest
    in endlist

Next I wanted to convert the above Haskell code into Agda. Syntactically, this translates quite easily.

My only major stumbling block comes with termination.

Functions in Agda must be total.

That means they must always terminate with a value. They can't fail with an error, and they can't run forever (which means that Agda is not a turing-complete language, I think!)

Agda contains a termination checker that gives a compile error if it can't prove that your functions terminate.

Bubblesort does always terminate. But the Agda compiler can't see that from the above definition. The proof looks something like: every iteration of applyLoop makes the list more sorted, and once you've called it enough times (as many as there are elements in the list) then the list will be sorted.

So I changed my implementation to run the outer loop a fixed number of times, rather than until the list is sorted. That makes the termination provable. But it makes it less obvious that the final result is actually sorted: now we end after a certain number of runs, rather than when the isSorted test is true...

Here's the Agda code:

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then                   
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0)) 

  innersort : {n : ℕ} -> ℕ -> Vec ℕ n -> Vec ℕ n
  innersort zero list = list
  innersort (suc i) sorted = innersort i (onepass sorted)

  sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n
  sortlist {n} l = innersort n l
(I actually started with a different definition of onepass - I'll come back to that in a different post).

Now, that's enough (given wrappers for main, etc) to successfully sort a list:

$ ./run
2 :: 3 :: 5 :: 8 :: 11 :: 12 :: 14 :: []
So what's different from doing this in Haskell?

Well, on the downside, it is not as obvious that this sort actually returns a sorted list, as mentioned above.

On the upside: we know that this program won't loop forever (although it might loop for a very long time) - because of the termination checker.

And the types of the functions, which I haven't mentioned yet, tell us something that relates the inputs and the outputs. sortlist has a type that tells us that its output will be the same length as its input. This is not a full definition of sortedness but its more than is offered by Haskell lists.

The type signature looks like this:
sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n
which says something like: sortlist is defined for every natural number n, and takes as input a Vector (of ℕumbers) of length n and returns as output a Vector (of ℕumbers) of that same length n.

The type checker checks that this is true at compile time, so the inner functions must have the length similarly encoded in their types.

At compile time, when we call n, we don't know what the n will be for every invocation (this is not Pascal statically-sized arrays) - but we do know that the output will be the same size as the input.

Compare that to type of the Haskell implementation:

bubblesort :: [Int] -> [Int]
which says that bubblesort takes a list of numbers and returns a list of numbers. Typewise, a perfectly valid implementation of quicksort here could return the empty list [] for every input. This can't happen here.

So in subsequent posts, I want to try to make compile-time assertions richer. I want to prove that bubblesort really sorts, by which I mean (I think):the output is a permutation of the input; and the output is in order.

(note 1) actually the Haskell type is: bubblesort :: (Ord t) => [t] -> [t] meaning Lists of anything that can be ordered, rather than lists of integers. That same abstraction is mostly achievable in Agda, but not quite - it doesn't have typeclasses in the same way that Haskell does.

Read part 2...

15 July, 2010

autoconf and portable programs: the joke

This is not my rant, but I like it:

I have a simple request for you: each time you run into software that does
this idiotic kind of test, please interact with the idiots upstream for
whom all the world is linux, and try to get them to replace their "joke"
of an autoconf macro with actual genuine tests that actually CHECK FOR THE
FUCKING FEATURE.

http://marc.info/?l=openbsd-ports&m=126805847322995&w=2

03 July, 2010

chess rankings for photos

I have a lot of photos - around 50000. I want to have some kind of scoring system for them.

The obvious one is something like a 5-star scale: when presented with a photo, you can award it from 0 to 5 stars, with 5 being best and 0 being worst.

But thats not very granular, and it is not clear to me that clearly defined standards for the 6 different scores will emerge.

I preferred something that says "this is better than that, so this should have a higher score than that".

But I don't want to have to manually make a strict linear order of all photos (despite the fact that a numerical score would do so), and I want the system to tolerate inconsistencies (eg. A>B, B>C, C>A) somehow.

Eventually I read about chess ranking, where each player is assigned a numerical score indicating their "goodness" and the scores are adjusted by pairwise comparisons between players - chess matches.

I adapted this for scoring my photographs. I started with the glicko system and modified it some.

The way this works is:

Photos compete against each other, as chess players compete against each other. The equivalent of a chess match is a presentation of two photos alongside each other in a web browser, with the user clicking on the photo they prefer. So, users do not assign an absolute score to a photo. Nor do they pick how much better one photo is than the other. They pick have a simple choice: "a>b" or "b>a".

Each photo is assumed to have a single numeric score, such that the difference in the score reflects the probability that one photo will win over the other photo. (this is affine: 900 vs 1000 is the same probability as 4000 vs 4100)

It is assumed that the score cannot be known exactly, but is approximated by a normal distribution (so there is a mean, and a standard deviation).

Adding a comparison between two photos gives information about the distributions for both photos causing the mean and standard deviation to be changed to more accurately reflect the score, as described in the glicko paper.

For my 50000 photos from the past 5 years, I have about 20% voted on at least once.

For a recent trip to rome, where I took about 1000 photos, it took a few hours to include each photo in at least one vote, where each comparison was an unvoted photo vs a random photo (which may or may not have been previously voted). This does not give a huge amount of information per photo.
Once that was done, I spent some hours making other votes: sometimes random vs random, sometimes random vs the photo with the closest mean. This caused rankings to become somewhat refined (sometimes causing surprisingly large changes in mean score)

So here are the top 3 photos from that trip:



and here are the bottom 3:



It seems to work reasonably well, though I think I need many more votes to get more accuracy. But that will come over time: as new photos are added, they'll get their scores by being compared against old photos, which will give more information about the old photos too.

19 June, 2010

normally distributed random numbers in haskell

somehow I expected to be able to get a normally distributed random number in haskell really easily by typing some term like "haskell random normal" into google. that came up with a bunch of stuff but nothing so simple as:
n <- getNormal mean dev
.

The most promising seemed to be the cabal package random-fu - although it looks like it has a lot of stuff in it and really all I want is the above single monadic action.

Cue the usual BS about installing packages (not haskell specific, just damned packaging in general) - today I need to edit my local hackage repository to remove some malformed packages, and upgrade GHC. frr. 6 hours just getting cabal install random-fu to work.

But once that was all done, the next morning, I got what I wanted - a short IO Double action: sampleFrom DevURandom (normal mean dev)

Hurrah.

12 June, 2010

rlwrap

I got frustrated when some application I was using *still* didn't support delete properly and discovered that the solution in that community (the OCaML world) seems to be (at least for commandline use) to use 'rlwrap' to add readline support to arbitrary applications.

eg:
$ rlwrap cat
Now you can use readline features (eg delete, cursor movement) to edit text

Neat.

http://utopia.knoware.nl/~hlub/rlwrap/

05 June, 2010

pink panther usb hub

I got this pink panther USB hub from mediamarkt - it was the same price as a USB extension cable (which is what I was looking for) - €7.99

Now I have three extra USB ports too, which is useful for attaching (for example) bamboo encrusted memory sticks, or my wide SD card reader.

One problem: when there are two of them chained with my ext hd on the end, the ext hd makes terrible clicking sound and doesn't start up properly. maybe thats a power problem?

28 May, 2010

64 bit linux BS

Several years ago I shied away from using 64-bit linux because many programs seem to have obscure bugs related to that. Its frustrating that I am still to this day encountering such bugs.

21 May, 2010

For reasons which might not be intuitively obvious, the broken behavior is required

I previously regarded /usr/bin/env as being portable onto any sane unix platform.

But now I've had to work with FreeBSD and my beliefs are dashed.

FreeBSD /usr/bin/env implements what posix says, rather than what everyone else does. That leads to trouble when you want to pass a parameter in a shebang, like this: #!/usr/bin/env perl -w which works almost everywhere but not in FreeBSD :(

15 May, 2010

monads: overloading semicolon, && and ||

Monads are sometimes described as 'overloading semicolon', aimed at eg. the C or Java programmer. This is some text about that idea.

But references there don't seem to refer to && and || - two other control operators that are regularly used (especially in C) and that I think are interesting to compare to ;

&& and || are defined primarily as 'boolean or' and 'boolean and'. But its very common to write expressions like this:
succeeded = (p != NULL && *p==5)
Evaluation of this uses more than the 'boolean and' functionality of &&. It also uses the property that && only evaluates its second parameter if its first parameter returned true - if the first parameter returned false, then the second parameter is never evaluated. That's a little bit of laziness sneaking into an otherwise strict language. In the example above, it stops the evaluation of *p when p is a null pointer.

So contrast ; and &&.

If you're a C programmer, they're totally different things - ; sequences statements, and && is an operator. Try to forget that difference for now.

You can write:
f() ; g()
which executes f, discards its result and then executes g.

Or you can write:
f() && g()
which executes f, then if f does not fail, it executes g - if either f or g fail then the expression as a whole fails, otherwise the expression succeeds. What do I mean by fail? I mean that f and g must return booleans indicated whether they succeeded or failed at doing whatever it was they were supposed to do.

So there are different ways to sequence operations (; and &&, and the operations (f and g) need to have different interfaces depending on the particular way of sequencing: when using ; there are no particular constraints. When using && we must indicate success or failure in every operation.

Both of these look like the Haskell operator >>: In Haskell, you can write:
f >> g
meaning "first do f, and then do g". But the novelty is that >> has different meanings in different contexts - and those contexts are called monads.

For example, the IO monad behaves quite like ;
print "hello" >> print "World"
hello
World
which looks like:
printf("hello\n") ; printf("world\n");

and the Maybe monad behaves a bit like (but also a bit different from) &&
main() {
 test() && printf("world\n");
}

int test() {
  return (2==3); // fail...
}
prints nothing.

In Haskell, the Maybe monad looks more like this:
Nothing >> Just 5
Nothing
Just 1 >> Just 5
Just 5
Just 1 >> Nothing
Nothing

In the Haskell example, Nothing means failure, and Just something means success (more on that in a bit).

In the first Maybe expression, Nothing >> Just 5, our first statement fails, so we don't run the second.

In the second example, Just 1 >> Just 5, the first statement succeeds (it returns Just something - so then we run the second statement which also succeeds (because it returns Just something) and so the statement as a whole succeeds.

And in the third example, the first statement succeeds, but second one fails, so the whole expression fails.

To add confusion, there are two distinct syntaxes in Haskell for writing monadic expressions. They do the same thing, and there is no real advantage to one over the other so far, but in a bit, the differences will be exposed. The above has introduced one form, using >>. The other form looks like this, using the do keyword
do
  putStrLn "hello"
  putStrLn "world"
and
do
  Just 1
  Just 5
Those are the same as earlier example, but in a different syntax. When you write something using do notation it is automatically translated into >> notation by the compiler. For now, that is just joining the lines together and putting in >>, which is not much difference. But there will be bigger differences later.

The Maybe example looks quite contrived - and it is - because so far I haven't explained the other important part of monads, which is value binding. That's where the analogy with ; and && breaks down and you start getting into more functional programming territory.

Note that all the above examples are missing some things that are used all the time (in C, Java and Haskell): return values, and variable assignment. (in one of the examples, I used p but only to read, not to write). This is an area where Haskell can be quite different from languages like C and Java.

Now, remember how I said that depending on what you're using to sequence your statements, those statements must match a particular interface. For example, if you're using &&, then those statements must return a boolean success. Using && hides away that return value - you write f() && g() without actually mentioning or testing the return value. Instead you let && deal with it; and in the Maybe monad, you let >> deal with it, and if using do notation you just put statements in sequence on separate lines, and magically they'll stop running when one of them fails!

What happens when I want variables and return values though?

In the ; style of writing C, you can write:
x = f(); g(x)
Now we expect f to return a value, and later on in a subsequent statement, we want to be able to access that value. In this C example, we do that by assigning the return value of f() into a variable x and then when we want to pass a parameter to g, we can write x again to get that value back. People do that every day. Nothing fancy - just normal programming like you learned when you were 8 years old.

So now how does that work in C using && to sequence statements? We can't write:
( x = f() ) && g(x)
because we're already using the return value of f() to indicate success or
failure - we can't return some arbitrary value too. (and remember we're using && here to sequence our statements - you're not allowed to suddenly say "ok lets put a ; and then an if statement). Uh oh.

Well, actually sometimes in C, we do manage to return a value and indicate success/failure at the same time. For example, fopen returns a pointer to a FILE or returns a null pointer to indicate failure. So fopen is reporting two things: did it succeed? (null or not-null), and if it did succeed then we can extract some more information - the pointer to the FILE struct.

The Maybe monad in Haskell does something similar. Remember a statement in the Maybe monad above returns Nothing if the operation failed, or Just something if the operation succeeded. I coughed politely and ignored the something at the time. But now see that the something what the operation returns on success.

This is more general than the fopen NULL pointer case. The fopen style only works when your data-type has a "magic value" to indicate failure - when using pointers, NULL, or perhaps countDinosaurs() could return -1 if it failed. But this isn't always possible (for example, if I am using some xor() function then any output is possible and there is nowhere for me to indicate failure)... and it is awkward for every procedure to use its own convention.

So now consider our Maybe monad example from before (slightly rewritten):
f = Just 1
g = Nothing
f >> g
In this, f succeeds and returns 1, and g fails and so does not return a value.

Well, what can we do with that return value? Just like in other languages, we can use it in later computations.

Now, there are two ways of writing this: the do style and the >> style. The do style is most like C and Java, and the >> style looks totally different.

I'll try to explain both. Try to understand both - the do style should be pretty easy to understand because it looks (aside from which symbols are used) quite like Java. But the >> style is more "functional" and might steer your thinking into writing functional code functionally, rather than "writing C in Haskell" as the do notation leads to (or at least I find it tempts me to).

Lets look at the IO monad. This lets us have functions which do IO (something which is forbidden in plain Haskell code (for better or worse)).

I want to have a program which will read a line from stdin, and output it on stdout. In C, that might be (assuming we have a nice readline function):
x=readline();
puts(x);

So in Haskell: As building blocks, we have print, which is a command you can run in the IO monad that will output the string that you pass to it (this was used right up near the top of this article); and we have getLine which is a command you can run in the IO monad that reads in a line from stdin and returns it.

So we want to run getLine, and then we want to run putStrLn, passing in the value that we got from getLine.

First lets write it in do notation:
do
  x <- getLine
  putStrLn x
This style runs getLine and binds its return value to x. That means whenever you refer to x later on in the do block, you mean whatever value was returned by getLine. This style is very similar to C or Java - it looks like we do some computation, assign its value to a variable, and then later on use that variable. Now here's the more functional way:
getLine >>= print
This uses an operator >>=. This behaves a bit like >> in that it puts two operations in sequence. But it also wires up the return value of the first statement to be the parameter of the second statement. Now remember that >> is different for each monad. It represents that monad's particular way of sequencing operations. >>= is likewise different for each monad. In the IO monad, it sequences operations and passes their values around just like above. But what about in the Maybe monad? Here's an example. First we have an operation in the maybe monad that takes an integer and succesfully returns that integer incremented. We use Just something to indicate success, and that something is x+1 to increment our integer.
increment x = Just (x+1)
Lets use this: In do notation:
do
  v <- Just 5
  increment v
which gives us:
Just 6
or the same in >>= notation:
Just 5 >>= increment
In the do notation, you can write as many lines as you like, and similarly in the >> notation you can write as many statements as you like:
Just 5 >>= increment >>= increment >>= increment
Just 8
But the point of the Maybe monad is to handle failures nicely. So what happens if we have a failure? What do these two fragments do:
Nothing >>= increment
or equivalently:
do
  x <- Nothing
  increment x
Now >>= will behave like >> which in the Maybe monad is quite like how && behaves in C. Ignore the value passing bit of >>= and concentrate just on the >> bit of it: in the Maybe monad, >> behaves like && - if the left-hand side fails, then we don't evaluate the right hand side. And thats what happens here - the left hand side fails (by returning Nothing) and so we never even to try evaluate increment. So now look at the do notation version. First we try to bind x to some computation, but that computation fails, so we don't evaluate the rest of the line. Now look at this Java code fragment:
x = v();
 y = increment(x);
That sets x to the some value caused by running a function v, and then runs increment on that value. First we run v and then we always run increment. Right? Yes, if v looks something like:
static int v() { return 5; }
But what about this:
static int v() { throw new RuntimeException(); }
Now we evaluate v but it fails, and so we don't evaluate increment. Instead, the program as a whole fails. So now the Maybe monad looks like && but also looks like exception handling - && and exception handling are almost the same thing! (which is quite surprising sounding, but they're often used for very similar purposes). What's the difference then? Well, an Exception propagates upwards and makes the whole of your program fail, unless you explicitly catch that exception, and you use ; to separate statements. Failures with && don't propagate out of the expression using the && - instead the expression returns a boolean false to whatever program code is surrounding it, and continues running. Essentially, you are forced to catch the failure, because you get told explicitly "I succeeded" or "I failed" (by the expression as a whole evaluating to true or false). So, I've shown two notations for monads - do notation and >> notation - and a few examples of code written in both styles. Turns out you've already probably written code in both styles if you've programmed in C and programmed in Java, because you will have used && for error handling in some places, and Java exceptions in some other places. So there's nothing new here. Which style is better? Well, it depends... If you are passing a value from one operation to the next, with nothing else going on, then the >> style is very concise: getLine >> print - we don't waste space assigning the line to a variable only to use it immediately and then forget about it. But when there are lots of actions returning lots of values, it can be easier to use the variables of do notation to keep track of them all:
do
  print "what is your name?"
  name <- getLine
  print "what is your age?"
  age <- getLine
  print ( "Hello "++name++". You are "++age++" years old and you are cool!" )
Using >> notation is awkward here - somehow you need to combine 5 actions into a linear sequence of actions to perform: print >> getline >> print >> getline >> print but you need to wire the values from getline around in non-linear fashion. Its possible (indeed, when you write in do notation it is translated into >> form by the compiler, as I said above) but it looks ugly - its easier often to use do notation and let the compiler sort it out for you. The Maybe monad adds failure handling to sequenced operations. It turns out that you already probably used that functionality without explicitly realising that was happening. What other interesting stuff can we build by making a monad with its own >> behaviour? One that gives behaviour that you don't find natively in C or Java is backtracking and filtering computation using the list ([]) monad. In the IO monad, a monadic action always returns a value. In the Maybe monad, a monadic action either returns a value or fails. In the [] monad, a monadic action can return multiple values (or one or zero values). We can use the [] monad to try out all combinations of some sets of values. For example:
do
  x <- [1,2,3,4]
  y <- [100,1000, 1000000]
  [x * y]
gives the result:
[100,1000,1000000,200,2000,2000000,300,3000,3000000,400,4000,4000000]
This looks like a normal do block, but instead of Just and Nothing from the Maybe monad, we now specify values using []. And we can put many values inside the brackets. In this code, x will iterate over each the value of [1,2,3,4], and inside that, y will iterate over each value of [100,1000,1000000], and then we'll evaluate the value of [x*y], and then all the results for every iteration will be collected together into the output list. You can write list filters like this too:
do
  x <- [1,2,3,4,5]
  y <- if isEven x then x else []
  [y]
(assuming we've defined: isEven x = x `rem` 2 == 0) This gives [2,4] as output. And we can write searches that combine both of the above iteration and filtering. For example, say we want to find all of the pairs of digits that add to 5 (for example, 3+2 = 5, so (3,2) is a solution, but 8+1=9 so (8,1) is not a solution) We can write it like this:
do
  l <- [0,1,2,3,4,5,6,7,8,9]
  r <- [0,1,2,3,4,5,6,7,8,9]
  if l+r==5 then [(l,r)] else []  
which gives us this answer: [(0,5), (1,4), (2,3), (3,2), (4,1), (5,0)] There's a more specific syntax for the list monad in Haskell, called list comprehensions. The above could be written as:
[(l,r) | l <- [0,1,2,3,4,5,6,7,8,9], r<-[0,1,2,3,4,5,6,7,8,9], l+r == 5]
To keep tying in with other langauges, Python has list comprehensions too with a very similar syntax:
>>> [(x,y) for x in [0,1,2,3,4,5,6,7,8,9] for y in [0,1,2,3,4,5,6,7,8,9] if x+y==5]
[(0, 5), (1, 4), (2, 3), (3, 2), (4, 1), (5, 0)]
This article is about overloading ; which the above seems to be drifting away from. So what does our overloaded semicolon operator (>> and >>=) look like in the list monad? Lets look at f >>= g. In general, this runs f then runs g feeding in the result of f - onto that behaviour we add our monad-specific behaviour. Lets look at how this behaves in a simple [] monad expression to increment the numbers in a list. First define increment:
increment x = [x+1]
which is used like this:
increment 10
11
Now use increment in a monadic expression:
[1,2,3] >>= increment
[2,3,4]
What did >>= do here? It seems to have run increment three times, to increment three different numbers. And indeed it did. In the [] monad, our sequencing operator will run its right hand side operation multiple times, once for each of the values returned by the left hand side, and then it will collect the results together into a list. How does that tie into the do notation? It means that when I say x<-[4,5,6], then the whole rest of the program will be run three times - once with x=4, once with x=5 and once with x=6, and then the final result of the program will be joined together in a list. Almost done with rambling for now, but I'll make one final comment: I used increment twice in the above text, once with the Maybe monad:
increment x = Just (x+1)
and once with the [] list monad:
increment x = [x+1]
These are almost the same - they both mean "return a value" in the language of the particular monad they live in. But just as >> and do syntax is independent of the particular monad being used, there is an independent way to "return a value", using return:
increment x = return (x+1)
When you use increment in the Maybe monad, then it will mean Just x+1, and when you use it in [] then it will mean [x+1], but even better, someone else can use that definition of increment in a monad that I have never even heard of - because return will do the 'right thing' whatever that happens to be.

ok definitely enough rambling for now.

07 May, 2010

making haskell EDSLs shebangable

There's a mindset that says to solve your problem, first write a language to solve your problem in, and then solve your problem in that language. And there's a mindset that says that your language should be an embedded language inside Haskell. In many ways that is appealing.

I wanted to write something that would delete old rsync snapshots. I took the domain-specific language approach, where the language specifies the retention policy for snapshots, like this:
policy = recent <||> weekly <||> monthly
meanings the final policy is to keep 'recent', 'weekly' and 'monthly' backups, with other statements defining what those three other policies mean. I won't write more about the language here - there's more on the webpage for the tool, snaprotate.

One particular piece of this I don't feel terribly comfortable with, and thats how to invoke/run the policy files.

I can imagine two different interfaces:
$ snaprotate -f policyfile
or
$ policyfile

I took the second approach, making policies first order unix executables - commands that can be run like any other command.

In unix tradition the way you indicate the language of a script is with a shebang line (#!/something) at the start of the script.

So then I want my scripts to look like something like this:
#!/usr/bin/snaprotate

policy = recent <||> weekly <||> monthly

This is almost a valid Haskell program, but: i) I need to import the SnapRotate module, and ii) I don't want to specify a main routine (which looks something like:
main = runPolicy policy
).

So the snaprotate commandline looks almost like runhaskell but does some source file rearranging to address the above two points, and to remove the #! shebang line.
#!/bin/bash
FN=$(mktemp /tmp/snaprotateXXXXX).hs
FNHS=$FN.hs
LIBDIR=$(dirname $0)

cat > $FNHS << 32804384892038493284093
import SnapRotate
main = runLevels policy

32804384892038493284093

cat $1 | grep --invert-match '^#!' >> $FNHS
shift
runhaskell -i$LIBDIR $FNHS $@
I wonder if this is the best way to implement such an embedding?

01 May, 2010

ALTER

I discovered the ALTER command in COBOL, in this note on eliminating that command, allowing self-modifying code. A couple of quotes:

ALTER changes the destination of a GO TO statement elsewhere in the program. It complicates the task of eliminating GO TO, especially if you don't notice that the ALTER is present.
and even worse:
In the presence of segmentation, ALTER can behave in unexpected ways. If an independent segment contains an altered GO TO, and the segment is overlaid and then reloaded, the GO TO is reset to its original destination.
If you ever encounter this form of pathology, proceed with extreme caution. You have found either a bizarre and subtle bug or a vicious marauding style of programming. Quite possibly both.

24 April, 2010

google chart venn diagram of disk usage



This compares disk usage of a backup I made of /home two years ago with one made this month. There's a lot of overlap - more than I expected.

Method: creating the second backup, I used rsync with --link-dest specified; for measuring, I used du -hsc old new; du -hsc new old. The size of the overlap is the size of new given by the second du minus the size of new given by the first du.

I'm trying to figure out ways of showing overlapping disk usage for more than two or three rsync trees created in this way (for example, to visualise monthly, weekly and daily backups over a long time period)

17 April, 2010

versions from version control systems

Sometimes its nice for built software to contain version information from the version control system - this means less to users and more to developers.

This is useful when people, for whatever reason, incorrectly report their version: "please test the release candidate for version 1.0 // I found bug B // That's strange because I thought bug B only got introduced yesterday in the dev code // oh yes, well I checked out the dev code and tested that, not actually version 1.0"; or "I have a new bug C // Are you building from a pristine source checkout? // Yes // Why does your log file contain a warning message that the source was modified? // oh, well I hacked at component Q // yes, that's why you're seeing bug C."

Different version control systems have different version representations. SVN has a sequential revision number; git has directory tree hashes; darcs doesn't seem to have any explicit version representation.

So here is code I've used at different times for svn, git and darcs:

For darcs, here's code I found in darcs issue tracker 1142:
echo "$(darcs show tags | head -1) (+ $(darcs changes --count --from-tag .) patches)"
which gives the most recent tag in the repository and how many additional patches have been added:
v1.1 (+ 39 patches)

For svn, we used something like this in Swift
R=$(svn info | grep '^Revision' | sed "s/Revision: /$1-r/")
M=$(svn status | grep --invert-match '^\?' > /dev/null && echo "($1 modified locally)")
echo $R $M
which we use to form version strings like this:
swift-r1833 (swift modified locally)

Using git-svn, so that I was interested in the SVN version information rather than git version information, swap out R and M above for these:
    R=$(git svn info | grep '^Revision' | sed "s/Revision: /$1-r/")
    if git status -a >/dev/null ; then
      M="($1 modified locally)"
    fi 

Both of the above two return the version of the last change in a particular checkout. When there are many modules, its sometimes desirable to give version information for those modules independently. The svnversion command that gives that:
svnversion -c somecomponent
that will produce different output forms that vary depending on the state of the checkout but at simplest gives something like:
4168

To get similar per-directory handling for git, you can do something like this anywhere except in the root of a repository:
SUBDIRPREFIX=$(git rev-parse --show-prefix | sed 's%/$%%')
cd ./$(git rev-parse --show-cdup)
git ls-tree HEAD $SUBDIRPREFIX | (read a b c d ; echo $c)
which will emit a tree hash.

So there are a bunch of different techniques for different version control systems. It would be nice if they were all a bit more consistent - really cool would be a single command that knew all version control systems and could output in a consistent format.

10 April, 2010

size as a hash function

Sometimes its been desirable to de-dupe a large collection of data files.

I wrote a tool called lsdupes to do that.

Originally, it was going to run md5sum to hash every file, and then list files with matching hashes to be deleted.

To optimise it a bit, I put in a size check: a first round happens looking at the size of each file, and only when there are multiple files for a given size will md5sums be computed. I though this would the md5sum load a bit.

It turns out that in my photo collection of 44590 photos and videos, the size is a perfect hash - there are no photos with the same size that have different content.

So while md5sum does get run on the dupes, it doesn't find anything different from what the size-based hash does; and the size-based hash runs a lot faster: to walk the tree and get sizes takes around 15 seconds. To then take md5sums of the roughly 5000 files that have non-unique size takes around 7 minutes.

03 April, 2010

HTML forms in the early 90s

Before HTML forms used the <form> tag, there was a simpler mechanism called <ISINDEX>. I was reminded about this because someone asked why CGI examples showed urls without name=value pairs in the ?query section, like this: http://ive.got.syphil.is/disease-registry.html?pox

I then went to see if <ISINDEX> still worked in modern browsers. I discovered that in
Safari, it renders a box, but there seems to be no way to submit the query (traditionally, pressing enter would submit it). Lynx and w3m still support it.

From others, I hear:
apparently the default browser on the g1 doesn't even recognize isindex as some sort of input field, although it renders it as such.
sort of weird; won't let you type in it but it renders an input box

and Chrome is also reported to work correctly.

Anyway, this post has an isindex tag right here:



<--- there, so you can see how it works in your browser...

27 March, 2010

stack trace in perl

As a user, I hate java stack traces (because they expose the guts of the program, when I don't care about those guts). But as a programmer, I have come to realise how much I like them, when faced with errors like this:

Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.

where the error is actually deep inside the call on line 27.

So googling around I found this line to put at the start of a program:

$SIG{ __DIE__ } = sub { Carp::confess( @_ ) };

which replaces those short die messages with a stack dump produced by Carp:

Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.
at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 7
Stupid::C::__ANON__('Can\'t call method "emitCode" on an undefined value at /Users...') called at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27
Stupid::LanguageWrapper::emitCode('Stupid::LanguageWrapper=HASH(0x8ff9b4)') called at ../src/stupid.pl line 44

which I hope I'll find more useful...

20 March, 2010

so many ways to hash

I was making commandline tools for stupid to drive the example sha256 code, resulting in multiple tools that deliberately did the same but using different language backends. Then I realised I have a shitload of (where shitload==4) md5sum commandline tools already:

$ echo abc | md5
0bee89b07a248e27c83fc3d5951213c1

$ echo abc | gmd5sum
0bee89b07a248e27c83fc3d5951213c1  -

$ echo abc | openssl dgst 
0bee89b07a248e27c83fc3d5951213c1

$ echo abc | gpg2 --print-md md5
0B EE 89 B0 7A 24 8E 27  C8 3F C3 D5 95 12 13 C1

13 March, 2010

seq

You(*) whisper to X, "the same package [GNU coreutils] which provides seq"
You(*) whisper to X, "the command line utility"
You(*) whisper to X, "also provides factor"
You(*) whisper to X, "which outputs prime factors"
You(*) whisper to X, "makes me want to start making fucked up shell scripts"
You(*) whisper to X, "that use goedel numbering"
You(*) whisper to X, "for some purpose."
You(*) whisper to X, "i have to wonder how a commandline utility for factoring primes is 'core' in any way, though"

06 March, 2010

ASCII art C++ constants

I came across Multi-Dimensional Analog Literals in C++. This is an implementation in standard C++ templates that lets you write constants out using ASCII art (in 1, 2 or 3 dimensions):


unsigned int c = ( o-----o
| !
! !
! !
o-----o ).area;

assert( c == (I-----I) * (I-------I) );


I think the same would be straightforward to implement using Template Haskell's quasiquoting mechanism, which allows you to embed parsers for fairly arbitrary sublanguages inside Haskell source. I wonder what other languages you could also implement something like this in.

27 February, 2010

slide controller

I just brought my third one of these:



(my first got lost at an event a few years ago, and I lost the USB dongle for my 2nd a few months ago)

If you want something to change your PowerPoint (or powerpoint-like) slides, this is the tool to get. Its worked with every computer I've tried it on, and every piece of presentation software (PDF viewers and HTML slidy in addition to PowerPoint and Open Office).

No software to install either - the dongle appears as a USB keyboard - the four keys send PgUp and PgDown to change slides; the laser beam button sends an F5 (which is start-presentation in PowerPoint) and the bottom button sends 'b' (which is blank screen in PowerPoint).

binary numeric promotion in java numeric types

I've been working on a Java backend for stupid, a crypto algorithm language proposed by Ben Laurie.

This has led me to look at Java numeric types a little more closely (and with a decade more cynicism than last time).

I'd forgotten entirely that there were short and long numeric types - for pretty much any use I've made of numbers in Java ever, int has been fine.

short behaves a little surprisingly:

If a and b are both long, then a & b is a long.

If a and b are both int, then a & b is an int.

If a and b are both short, then a & b is an ... int. wtf. why?

Likewise byte & byte -> int.

This is specified in 5.6.2 Binary Numeric Promotion of the Java language specification.


(later:)
Its pointed out that C also does implicit casting of smaller types to int; but gcc is a little gentler with its warnings. a+b gives a warning (not an error) similar to the Java code above, but a&b does not (presumably because it knows that this can't make the number be any bigger than the types you started out with... something that gets lost in the Java type checking)