Patrícia's New Hobby

The artistic blood of my lovely wife is flowing again :-)

Her newest hobby is orchestrating photo-shootings. Predominantly of pregnant friends and everybody who simply wants to feel marvelous...
Like Lelêca!

Freude, die man sieht

Dieses Photo zeigt Lelêca (alias MausiMausi, alias SchlausiMausi) in mit einem Kopfschmuck, der eigentlich zur pernambucanischen Tracht gehört. Ein Geschenk von Tio Davis – Danke!
Lelê freut sich inzwischen auf den morgentlichen Gang in den Kindergarten (natürlich mit Papa!) und scheut sich auch nicht vor kleineren Wortgefechten ("vai comer não!"). Aber was richtig gut ist heißt dann "muito ótimo" und Akzeptanz wird mit einem klaren "tá certo!" signalisiert. Und wie man sieht, geht es den Jungs auch ganz passabel...

New Thrist Cabbage

Yeah, it took more than a year (and dcoutts help on IRC), but finally I've gathered all my hackage-foo to submit a new thrist package (v1.1.1). Its main purpose is to require base v4.0 or higher. As an added bonus (Thrist p) now provides a Category instance. I have also added an Arrow (Thrist (->)) instance, but its first method is bogus as of now. I plan to correct this with v1.1.2.

My plans for 0.2 are:

• adaptors Data.Thrist.Monad, Data.Thrist.List (aka. R*), Data.Thrist.Arrow, all with their respective sensible class instances,
• tests.

Then sometime I can start setting up some cool stuff to demonstrate hoare-triples in thrist setting.

We'll see.

Static Constraints

In the last months Tim has been adding a new function sameLabel to Ωmega and this finally allowed me to encode the concept of free variables. In just a couple of days I managed to implement environment construction with statically checked proof that no identifier is shadowed. Here is a little example.

Building on this advance I fulfilled a long lasting desire and managed to prototype LLVM basic blocks in Ωmega with thrists. The approach is implemented in 2 steps:

• build up a labelled sequence of preinstructions, and then
• construct sufficient evidence about well-formedness, that the strict type constraints in the thrist can be proven.

Curiously, the defs propagate to the right and the uses to the right in this thrist. The good thing is, that after all this struggle I am pretty confident that many more properties and constraints can be encoded, such as

1. the LLVM type system (on defs, uses and constants),
2. that Phi nodes must not go into entry blocks,
3. that Phi nodes must preceed other instructions in the basic block,
4. every use must happen in the scope of a corresponding def,
5. etc.

The next days will surely see more progress, I have crawled out of the swamp and have firm ground under my feet...

Daddy's Girl

Das Bild zeigt die Ruhe vor dem Sturm. Wenige Minuten später ist Leleka in ihren Festanzug geschlüpft und die Party ging los, mit Geschenken und viel Leckerem. Spruch der letzten Woche:

"Aniversário de Lelêca no domingo!"

Ketchup Problem

In Chapter 6 (page 16) Jeremy Gibbons describes a datatype that models all secure operations that can be applied to a (partially filled) ketchup bottle. I believe that this is the example that Jeremy has shown me at ICFP'07 in Freiburg (when I have introduced him to my thrist concept), and I have been unable to find it ever since. Now, I guess I can add it to the bibliography section of my paper. That is, if I ever get around updating the draft again...

PS: a bibtex-able conference paper is here.

Sieben Tage Regen, Sieben Tage Schnee …

… und es tut nicht mehr weh!

Dieser Winter war der schmerzhafteste den ich bisher in Deutschland erlebt habe. Lang und kalt. Die Natur ist acht Wochen (oder mehr?) hinterher, unser Hunger nach Sonne unvorstellbar.

Wie gut, daß mein Wetter-Widget jetzt sieben Tage Sonne und angenehme Temperaturen verspricht! Das Haus ist nunmehr tiptop eingerichtet, die Gartensaison kann kommen.

Auf wiedersehen, Winter, willkommen Frühling!

Lack of Total Order

My new project is starting to bind my mental resources at work. So some of the fringe projects which I casually do for fun will surely suffer.

• LLVM: Two of my recent patches had to be backed out of the tree, because they caused trouble with bootstrapping llvm-gcc. I am pretty sure these are not caused by bugs on my side (geee!), but frustrating nevertheless. The situation is also aggravated by the fact that I am unable to build a stock llvm-gcc on my Tiger machines I have access to, so I have lost my ability to debug these beasts. A third patch is in-progress (CallInst operand reorg - function to the back) but it is dependent on one of the backed-out ones. It is also pretty stubborn, since there are many hidden assumptions in the codebase which expect the callee in front position. I am slowly weeding out the problems.
• Omega: Little progress on this front. Tim also seems to have reduced his workload on here - probably caused by the "Cyber Milennium" course - so I do not feel a lot of motivation. Which is sad, because there are some nice papers on GADT decidable type inference appearing. Omega could benefit from those.
• Clang: Doug has been working on the template instantiation machinery lately, and I took over a mini-project: instantiation of "?:" expressions. It mostly works, but there is still review feedback to satisfy and the missing middle-expression problem needs a solution. These must be unit-tested as well.

Back to my regular work. The job is demanding, I co-develop the implementation, test framework and test-suite simultaneously. Of course I could accept some help, but it is also important that the basics get in right and unwatered. I have a nice plan for stub-libraries that can invoke TCL commands to fill in out parameters and result values. Fun.

Regarding the headline, it was inspired by thinking about a purely-functional (i.e. immutable) lattice library for use by Clang's (partial) template specialization feature. Yes, and lattices arise as containers of partially-ordered data.

RWH

I am happy because my copy of Real World Haskell arrived today. I ordered it through my employer, and while waiting for it more than two months, it finally got delivered. Anyway, I plan to put QuickCheck to good use by generating testcases automatically. Let's see how far this can carry us.

3^2 Day

Today is 3^2 day, because 3 squared is 9 and today's date is 03.03.09. Number jokes aside, it was a good day, I am finally beginning the implementation part of my new project at work and the ideas keep sprouting.

Good.

PS.: Also I found a nice article about decidable type inference for GADTs. Final version hopefully for ICFP09!

Verhörhämmer

Um ein Paar dieser "rohen Diamanten" zu downloaden, habe ich dieses kleine tcsh script geschrieben:

foreach j ( 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 )
  foreach i ( `curl "http://blog.br-online.de/fruehaufdreher/index.php?/categories/2-Verhoerhammer/P"$j".html" | grep .mp3 | grep value= | grep song_title= | awk -F= '{print $4}' | awk -F"&" '{print $1}' | awk -F/ '{print $6}' ` )
    echo $j : $i
    curl http://blog.br-online.de/fruehaufdreher/uploads/$i > $i
  end
end

Macht Spaß... Danke BR!

:-)

Dan's Birthday

Yesterday was Daniel's birthday. We made a surprise visit and he loved it! I came a bit late (work, work, new project, yadda), which was no problem because people had lots of fun. They fired up the karaoke machine, and after some beers even I took the mike. But Helena on stage was the cutest thing ever! She grabbed the microphone as if she was a seasoned singer. However she did not sing a single tune, just posed :-)