don't count on finding me

Showing Thrists Revisited

2011-12-26T17:11:00.000-08:00

More than three years ago I lamented that it's impossible to to define a show function on thrists, generally, even when the element type is member of the Show class.

In the meantime I succeeded to declare certain thrist parametrizations and convince GHC to accept show instances for them. The Appli thrist is such an example.

With the upcoming GHC 7.4 things may improve considerably, as it will bring constraint kinds. Remember, thrists are (currently) parameterized like this (* → * → *) → * → * → *, i.e. on types, and with the new kind variable feature we can probably generalize to user-defined kinds. Then the parameters may match Ωmega's: (a → a → *) → a → a → *. So we still result in a type, but we can choose our indices from a vastly bigger domain. Enter constraint kinds! These may be part of our user-defined kinds, so we can form stuff like (Show, *) and supply it for the parameter a. With some luck deriving Show can be more successful and not attached to particular parametrizations.

I regrettably still haven't gotten around building a GHC v7.4.1 candidate, so I cannot verify the above, but my gut feeling is that this'll work out...

Pondering about the Foundations

2011-11-22T15:03:00.000-08:00

As I am thinking about how a possible Ωmega 2.0 could be implemented, I am trying to come up with some interesting concepts w.r.t. parsing and type checking. Since no single line is written yet, it is easy and cheap to ponder.

Some key elements are already taking shape in my mind. These are:

parsed entities carry their start and end coordinates in their types
there is no difference between patterns and expressions
each expression carries a typing thrist.

The second item has been elaborated by me in an earlier post. The third must wait a bit until I have something coherent (but the curious reader might visit my sketch of ideas).

I'd like to talk about item one here. The essence is that every grammar element obtains a type that describes where this element is located. For example a function declaration may occupy the text portion between start and end, where these are type-level triples (file, line, column). In order to consider parsed input consistent, the start coordinates must be aligned with the prior element's end coordinates, i.e. we have another thrist here.

Things get interesting when we model naming and scope. Name definition and referral must somehow match the types, after the match is done the semantics can be read off the user. To give an example:

Ref definer :: Exp (`foo, 42, 7) (`foo, 42, 11)
where definer :: Exp (`foo, 41, 1) (`foo, 45, 37) = ...

Both the reference and the definition live in the same file "foo.prg". The former is on line 42 from column 7 to 11 (exclusive). The definition it refers to is in fact enclosing it (a recursive call, maybe?) extending from line 42 to 45. With this representation the name of the indentifier becomes secondary, all that counts is the evidence in definer which contributes to its type! We have created a globally nameless representation.

We can expand this world view to also include the level of the grammatical entity (value, type, kind, etc.) as a fourth coordinate. So a reference to a ›25‹ somewhere in the text at floor 0 would point to an integer literal, the same place at floor 1 to the type Int and at floor 2 it would be the kind *.

My hope is that all the proof obligations arising in such a scheme can be cleverly extracted from a parsec-like engine.

Macs and me

2011-10-05T21:39:00.000-07:00

I am profoundly saddened since I woke up at 4:00am in the morning, and saw the news headline about the passing of Steve Jobs. I have seen this coming for a long time, as my father died in a very similar way back 1993 with only 52. Looking at the thin appearance of Jobs in the last month or even years I constantly get reminded of him. Basically the same story of suffering, loss of weight, liver transplant (in vain), death. RIP, Dad, RIP, Steve.

I am writing this on a rusty vintage 2000 PowerBook G4 Titanium, I bought on eBay last year, because the video of my own 2001 TiBook went black. By today's web standards completely inadequate, it serves me well for news reading, terminal logins, etc. My son Pedro got his MacBook Pro 15'' delivered just today. An awesome piece of technology.

My father bought the first Mac in 1986, just after opening his practice as a neurologist. This was two years after cutting all strings in Hungary and fleeing to Germany in a pretty bold move. Must have been a moment of total self-overestimation when I promised to my dad "if you buy that Mac Plus I'll write you the best software for it for your doctor's office". A crazy time began. At day the Mac was used to keep patient's data with a DTP program "RagTime", at 5pm I hauled the Mac home (in a big black bag) and started writing the program. Sometimes deep into the night. I used Turbo Pascal (and later MPW) after figuring out that the Lisp environment I preferred simply did not cut it due to insufficient support of the Toolbox. In the morning my father carried the Mac back and powered it up.

Less than year later the program was ready for productive work. A Mac SE joined the party and we had a networked doctor's application with a really neat windowed user interface, that would put even today's programs to shame in this regard.

There was even a time when we fancied marketing this product, but my university duties and the early death of my father simply negated all plans to this end.

When I had my diploma in my hands I picked up the phone and called the guy who sold us the Mac Plus and a copy of "Inside Macintosh" back in '86. In the meantime he founded a pretty successful company around a networked admin solution called 'netOctopus' which was his baby. We occasionally met at Apple developer events and I new that he was a pretty damn good coder. He hired me and I was earning money by programming Macs!

So yes, I love Macs and there is no reason that this will change in the foreseeable future.

I kept telling to myself, should Jobs die one day, I'll put that Mac Plus (now in my basement and still functional) up for sale at eBay. My thought today: "screw it – too many fond memories attached".

GHC 7.0.4 on CentOS

2011-09-09T12:02:00.000-07:00

This is mainly a post for myself so that I can look back any time how I did it.

Basically I fell in every possible hole while wandering around in the dark but I could get out of them :-)

after downloading I configured the binary installation for x86-64. configure starts ghc-pwd, which is built with the wrong glibc-versions. Bummer.
found out that I have to get the source install. Downloaded and configured, it died in the middle because base-4.2 was not available. Bummer.
so I had to install ghc-6.12.3 first. Fortunately this went smoothly (binary install). With this new friend I reconfigured v7.0.4 and started building. When linking the stage1 compiler I got an error from binutils that some relocation went awry. Bummer.
the internets are full of hints that the system compiler (gcc-4.1) uses the bad linker. To my luck I found a new gcc-4.4 in an amicable colleague's home directory, so I reconfigured thus:
./configure --prefix=/home/gabor --with-gcc=/home/msichel/local_x86/bin/gcc
but configure told me that the shiny new gcc cannot build executables. Bummer.
it turned out (I had to write a hello-world to figure that out) that some gcc-internal shared libraries were not found. Luckily they came into scope with
LD_LIBRARY_PATH=/home/msichel/local_x86/lib:/opt/lsf/6.2/linux2.6-glibc2.3-x86_64/lib
at this point I could smell victory, but it was still out of reach. A blog post suggested to cp mk/build.mk.sample mk/build.mk and edit it in two ways:

uncomment BuildFlavour = quick
and change to GhcLibWays = v p dyn, i.e. append "p dyn"

I did both, reconfigured and typed make install.

It went through without a hitch :-)

Poor Man's Haskell Kinds

2011-08-21T22:58:00.000-07:00

After finalizing some of my idea prototypes in Ωmega, I intend to port a part of the code to Haskell, to enjoy the speed advantages of a compiled language.

Unfortunately Haskell does not support user-defined kinds, so I was wondering how to simulate them at least, in order to get some confidence that my type-level constructs do not drift into no-no-land.

This literate haskell file demonstrates how I put instance constraints to work, and thereby define the inference rules for well-kinded phantom type indexes. I am sure somebody has already done this, I would like to hear about it. Anyway, this almost allows me to introduce Ωmega's checked singleton types in Haskell.

Sadly GHC does not yet allow instance definitions for type families, but it would be cool if somebody could provide me a workaround.

My Thoughts about Inertia

2011-02-10T18:45:00.000-08:00

Big caveat: I am very much of a layman when it comes to physics and this is consequence of having heard elementary physics lectures more than 15 years ago.

But I like the occasional book on the subject (The Elegant Universe comes to my mind) and am fascinated by the theoretical possibility of a grand unified theory of Nature's forces.

There is a small niggling idea in my head that wants to get out from time to time, and this post is the evidence that it finally made it into the wild. (I will probably appear as a bloody idiot because of this...)

Being Hungarian-born has made me somewhat receptive for advances in physics performed by the pretty smart folks coming from this small country, and already as a pupil I was taught that the "equivalence principle" (of gravitational mass and inertial mass coinciding to an amazing degree) was shown by Eötvös. This cannot be a simple coincidence but must be a fundamental thing.

A completely ununderstood fundamental thing, as it appears to me. A quick googling for "inertia quantum gravity" brings up some outright lunatics and some rather exotic theory of "zero field fluctuations" causing inertia:

http://www.calphysics.org/articles/PRA94.pdf
http://www.calphysics.org/articles/gravity_arxiv.pdf

But, electromagnetism causing the same mass as gravity (i.e. linking two of the fundamental forces with an unbelievable precision) appears very far-fetched to me.

Wikipedia seems to be no help when inquiring for the source of inertia. Mach's principle referenced therein, namely that the existence of the rest of the universe leads to the phenomenon of inertia does not sound right; after all, when all the other stars (galaxies etc.) would be removed but the Sun, would you expect that the inertia of your body suddenly would fall to almost zero?

I cannot believe that modern theories of gravity (such as quantum gravity approaches) do not try to explain the equivalence of gravitational mass and inertial mass. My intuition says that this should be the first step!

Now I'll begin a steep descent in the land of speculation and respectlessly mix stuff told by others with vague ideas and metaphors of mine. I won't even make effort to cite or link, but at some point I'll tell what my main idea is. Be warned: at that point probably each self-respecting physicist (that is, a person who successfully solved a differential equation about movement of a body under external force) will turn away with disgust, but okay, let it be...

There is this idea that gravity is so weak in comparison to electromagnetism, because the circular (closed) strings corresponding to the graviton do not permanently bind to our three dimensional space (or four-dimensional spacetime). They are just passing through, and there is little time for them to establish the force between bodies. So, the gravitational force exerted between two glasses of red wine is very small on each other. But when they are accelerated (say, by clinking them) perceptible forces appear. So I conjecture that both forces are caused by the same mass, and by the same gravitons, but they differ in magnitude, because the gravitons stay around longer in the second case, so as messenger particles they establish a force many orders of magnitude stronger.

How can they stay around longer to become relevant? Perhaps by traveling orthogonally to the gravitational gravitons. Okay, inertial gravitons travel (more or less) orthogonally to our space, that is, along the time axis and thus following the trajectories of the particles the matter is built of.

I think it was Feynman who mentioned that an anti-particle traveling 'backwards' in time can be equated with its particle traveling forward in time. Now, what is the anti-graviton? I believe that I read sometime that it is the same as the graviton. Just like a photon is not differing from an anti-photon. So the time inversion does not change any property of the graviton. Good. We have gravitons which make a short visit in our spacetime, and vanish just as fast as they appeared, and there are those which accompany mass-like particles (even when at rest) along their trajectory in time, possibly bouncing back and forth between earlier and later. This constitutes (my IDEA!) a force between a body now and its earlier appearance in spacetime. Of course this is the same as a force between now and the future of the body. Actually there is a force between me and (me one second later). Or ten seconds or even a year!

Two things become clear now. First we have to perform an integration (over all time destinations) to get the resulting force. And second, the force toward the past will bear a negative sign, so for stationary bodies all inertial forces will cancel out. I think this can be asserted for uniform movement too (i.e. constant velocity vector) but I did not waste any thoughts on this yet. Anyway, this is Newton's first law.

Time to get to the second one. Here I want to make some further remarks. The inverse-square(-like) law should hold for inertial gravitons too, so that a longer time-span enters into the integral with a smaller effect. Kind of like the gravitational force between objects a light-second apart also decrease substantially. Second, causality is a bit smeared at the very short intervals where the forces are really relevant (Planck time?) so the reality a bit before pulls hard backwards and the reality a bit later pulls hard forward. Both look pretty much the same, differing only in the arrow of the force. I do not know whether this is essential, though.

Back to Newton's second law. Imagine a stroboscope lighting a scene where a body moves, accelerated by a constant force along its movement direction. When you make a photo (with reasonable exposition time) you'll obtain a picture of several bodies, with the earlier ones nearer together, and the later ones successively more distant. Now let's declare the middle one as being now. Then the prior one is less distant than the next one so the force between the prior and now is bigger than the force between now and next. These do not cancel out any more. This is a consequence of the inverse-square law. Of course the stroboscope should flash with Planck frequency etc. (so that the spacetime distance is small enough), but the principle is clear: We get a resultant force that points backwards, namely the difference between the (bigger) half-integral towards the past and the (smaller) half-integral towards the future.

All the time I was using the wrong word 'force' for something space-time-like (a vector with 4 components). What we perceive or measure as accelerating force is the projection of that 4 component vector into our 3-dimensional space. So I conjecture that F = ma is the projection of the resultant 4-force which I explained in the last paragraph to our 3 dimensions.

If this little idea holds any water then it should be possible to calculate the inverse law for the 4-force. I'd bet it is inverse-cubic. If this succeeds, then the next test would be to figure out how the 4-force looks like when a relativistic (say half-lightspeed) particle is accelerated by a 3-force. Clearly the 4-speed rotates out of time, but does the the mass of the particle increase?
I do not dare to think about whether we can ever get to the point where this idea gets tested in an even more comprehensive setting.

But it was sure a lovely night when I was drinking that red wine with a good friend from Brasil two days ago, who dared to ask a quantum-mechanical question and received a long story as an answer, unknowingly liberating this small niggling idea from the confines of my head!

Quantifiers: Dark Matter

2011-01-09T12:38:00.000-08:00

Modern cosmology routinely deals with dark matter, a source of gravity necessary to explain certain things. In the last days I discovered a kind of dark matter in Ωmega too, and here is the related story.

As we know type constructors arise when the data definition is equipped with parameters, like below:

data Tree a = Tip a | Fork (Tree a) (Tree a)

a is a type variable and gets instantiated (to a type) when we want the tree to contain actual information.

Actually I could have written the second recursive occurrence of Tree a in the Fork branch as Tree Char, and the type checker would have accepted it. Why? Because at each instantiation site the type variable a is created fresh, and can be bound to a new expression.

But what is the kind of a? In Haskell it can only be *, which classifies all types, as the other possible kinds (* → *, etc.) do not classify types. But this kinding relation is not spelled out directly, so let's choose a more explicit definition:

data Tree :: * → * where ...

When talking about Tree Integer, then it gets pretty clear that Integer's kind must be * and that the resulting Tree Integer is itself kinded by *.
But there is a fine distinction between explicit and implicit kinding in Ωmega: in the latter case a is kinded by a unification variable instead of by *. The reason is that Ωmega allows us to define custom kinds, which can classify other type-like things. These are usually used for indexing of type constructors.

The unification variables that are present, but hidden from the user only become manifest when we have multiple levels of data definitions, with the higher levels indexing the lower ones and some constructor function tries to bind the unification variable to different kinds. Of course that won't work and all you'll see is a very cryptic error message. The smallest example I have encountered is issue 70, which I will present as an example here.

data Pat :: *3 where Q :: Pat ~> Pat data Pat' :: Pat ~> *2 where Q' :: Pat' n ~> Pat' (Q n) data Pat'' :: Pat' p ~> *1 where Q'' :: Pat'' n ~> Pat'' (Q' n) data Pat''' :: Pat'' p ~> *0 where Q :: Pat''' n → Pat''' (Q'' n)

Look at the last line, it induces these two kind equations:

n = Pat'' p1 Q'' n = Pat'' p2

Each equality at some level induces an equality at one level up. But p1 and p2 are kinded by the same unification variable, k. Let's note the two equations with k in the middle:

m = k = Q' m

where m is the kind of n.
You can see now that m is forced to be equal to Q' m, which is clearly incommensurable.
The solution is clearly to spell out kinding quantifiers explicitly with type variables. Since these get instantiated to fresh copies on the fly, the above problem does not occur.

So we arrive at (only showing the last definition for brevity's sake)

data Pat''' :: forall (o::Pat) (p::Pat' o) . Pat'' p ~> *0 where Q :: Pat''' n → Pat''' (Q'' n)

Black magic? Only when you let the kinds live in the dark!

Recently Implemented Syntax Extensions

2010-12-27T14:57:00.000-08:00

The alert reader must have noticed that in my recent post I refer to a syntax extension called LeftList, intended to model left-associative lists, which are naturally showing up in many contexts.

But that's not all, I've been busy adding more goodness. After realizing that the frontend for expressions of the form ()u and (42)i was already present, I decided to add these as Unit and Item syntactic extensions. I documented them in the manual, so the next release will be up-to-date documentation-wise.

Today, being given some idle time, I came around to finish up the LeftRecord extension, which is just what you would expect. Implementing it turned out to be even easier than the same process performed for LeftList, not only because of the lessons learned, but for want of the ambiguous parsing of {tail; tag=val}lr which does happen with LeftLists: [tail; head]ll.

There is one itch left: adding LeftPairs, which should be a piece of cake, and could happen anytime. And then there is a pie-in-the-sky enhancement request (a.k.a. issue 64), which is somewhat tricky, so do not expect it being done any day now.

Singleton Types are the Key to Co-dependency

2010-12-14T00:01:00.000-08:00

Since the last time I wrote about existentials I had a plenty of time to ponder how they fit into the qualifier-typed typed lambda calculus which de Bruijn has proposed, and I am very proud of implementing a formalization for.

The headline has already spoiled the suspense, but the interesting part is how I arrived at that assertion. It happened last night and it carries all the attributes of an epiphany :-)

There were some anomalies that worried me about the introduction of existential qualifiers in the prequel post:

the treatment of patterns that are values was missing,
the handwavy argument how the proposition corresponding to the condition is encoded,
that the dependent sum binder introduced two variables (where lambdas only introduce one),
and finally that parenthesized condition after the ∃-quantor which do not seem to appear in logic textbooks.

It was the first worry that kept me awake this night. Here is a prototypic definition:

fac 0 = 1

fac (1+n) = (1+n) * fac n

In Dylan (an object-oriented functional language) one would write the first branch of same function as

define method fac (n :: singleton(0)) 1 end

Here the singleton function returns a type whose sole inhabitant is the argument to singleton. This analogy pushed me over the top. What if I introduced the concept of co-dependency in my formalization? Say,

∃x:singleton 1 . x

where values can be lifted up in the type realm and appear at the right-hand-side of the type judgement (:). I prefer to call this co-dependency because it is opposite to regular dependency which happens in the returned expression. Consider the following type-theory expression:

λx:Int . 〈y:singleton (5*x)〉 . y

here a universally quantified variable (x) is entering an expression which is the argument to the singleton construct giving the type to y. What does it mean? That for every x there is an y of 5 times the magnitude, which becomes the result.

With this interpretation all my worries have vanished: there is just one variable added by the dependent sum quantification and the condition is now neatly tucked away on the right side of the colon!

Next to come: introduce this idea into the formalization.

Zipping through it

2010-12-11T04:23:00.000-08:00

In my email conversation with Brandon prior to the release of thrist-0.2, I told him that I did not come around implementing reverse thrists, and I showed how they arise naturally when doing computational passes over thrists: (((a, b), c), d) e (f, (g, (h, i))). He asked me whether this has anything to do with zippers, which I answered to the affirmative, my previous ideogram being essentially a thrist zipper. As it maneuvers through the data structure it deconstructs the original thrist, places a new element into focus and zips together a left-associative structure behind. Visually it (kind of) corresponds to the zipper on your jacket.

This post is dedicated to this versatile tool being applied to thrists to obtain an isomorphic data structure which I call the ThristZipper.

As the ideogram demonstrates, this zipper consists of three parts:

the left-associate thrist (usually holding the already visited portion),
the focus element e,
the (right-associative) thrist (usually to be iterated over).

So first we have to define LeftThrist (this is how I prefer to call it).

data LeftThrist :: (* → * → *) → * → * → * where

LeftNil :: LeftThrist k a a

LeftCons :: LeftThrist k a b → k b c → LeftThrist k a c

Again, the types match up. Now we can define ThristZipper:

data ThristZipper :: (* → * → *) → * → * → * where

Focus :: LeftThrist k a b → k b c → Thrist k c d → ThristZipper k a d

It remains to define all the operations on ThristZipper that will make it a versatile tool.

We start with zipInto:

zipInto :: Thrist k a b → Maybe (ThristZipper k a b)

zipInto Nil = Nothing

zipInto (Cons e r) = Just (Focus LeftNil e r)

We can similarly define zipLeftInto, advancing, focus manipulation, maps, folds and getting out on the right or in the left. These are of course left as an exercise to the reader, but I will define retract (the opposite movement from advance) here for good measure:

retract :: ThristZipper k a b → Maybe (ThristZipper k a b)

retract (Focus LeftNil _ _) = Nothing

retract (Focus (LeftCons r e') e t) = Just (Focus r e' (Cons e t))

And a lot prettier in Ωmega (svn HEAD):

retract (Focus []lt _ _) = Nothing

retract (Focus [r; e']lt e t) = Just (Focus r e' [e; t]l)

PS: I definitely plan to make all this part of thrist-1.0 when it arrives.

The Sky was the Limit

2010-12-10T15:09:00.000-08:00

Everyone remembers Tom Petty's song 'Into the Great Wide Open' with it's famous refrain

The sky was the limit

I was thinking about limits (the category theory ones) for many years now, but could never really visualize the concept. (I should really start reading Awodey's 'Category Theory' which will be my present to self at Xmas.) I tried to get hold of the related problems with a mental construction of a lazy, self-building thrist. It was clear that each element should increase the type, Z, (S Z), (S (S Z)), etc. ad infinitum, so the start type would be clear: Thrist Up Z ?. But the ?, let's call it the limit, is not clear at all. Anyway it would be an infinite type, not like in the simple analogy of let count = 0 : count in count, where count :: [Int] holds. As we know type checkers do not like infinite types, as it would take forever and two days to check them :-)

Fortunately the sky is not a limit anymore and I came up with a solution that is nice and short even in Ωmega, which is a strict language (albeit with a lazy construct). Since it is only a few lines I can effortlessly reproduce it here.

data Count :: Nat ~> Nat ~> * where

Incr :: Nat' n -> Count n (1+n)t

The Incr constructor states the typing rule, namely one higher to the right than to the left. We can try it out:

prompt> [Incr 0v, Incr 1v, Incr 2v]l

[(Incr 0v),(Incr 1v),(Incr 2v)]l : Thrist Count 0t 3t

Not surprisingly, this is the only value of type Thrist Count 0t 3t. We follow the example of count above and write:

a = [Incr 0v; lazy (shift a)]l

Naturally shift will shift a Count thrist to the right, thus satisfying the type constraint of thrists, that at each joining point the left and right types must match up. The lazy keyword is needed here to delay the evaluation, it is however pointless in Haskell.

All that remains is to write the shift function which will create the ominous limit type:

shift :: Thrist Count n a -> Thrist Count (1+n)t a

shift [Incr n; r]l = [Incr (1+n)v; lazy (shift r)]l

It is probably not a surprise that the limit value is ⊥ (i.e. nonexistent), so any type will do (along the constraints of the kind in question). I settled with a universal type.

Now we can pattern match on a to see that it really grows into the sky:

case a of {[a,aa,aaa,aaaa; b]l -> show b}

prints "[(Incr 4v) ; ...]l" thanks to show's magic. The ... corresponds to the suspended computation.

Hey, it wasn't that hard at all! Where is the infinite type? It is hidden behind the existential barrier that is formed at each thrist joining point, and since it cannot escape we do not have to worry it...

Good night!

Es taut nicht

2010-12-01T18:08:00.000-08:00

The subject is German, meaning "it doesn't thaw", which is rather true: as I write this we have chilly -10 °C (14 °F) and 25 cm (10 inches) snow on the ground. And it keeps snowing. I cannot remember a winter like this.

But this is not the reason of my posting! Instead I have hidden a pun in there: "there is no tau", yes, the Greek letter (τ). Which proposition is definitely false, because as of today I succeeded to encode de Bruijn's higher degree binders in Ωmega. I've fought a lot (on and off) against this fortress...

The code is here, see and comment.

PS: Does anybody know a better quality URL for this paper?

More on Existentials

2010-11-27T16:27:00.000-08:00

In a previous post I suggested a new (?) interpretation for pattern variables in case branches. This post is my way to understand matters more.

Let's start with the basic example

data Temp :: * where
Kelvin :: Float -> Temp

Then Kelvin 273.2 is about the temperature at which water freezes (or dually, thaws). Okay, let's demonstrate my point by this code:

diff :: Temp -> Temp -> Bool
diff (Kelvin a) (Kelvin b) = a == b
test t = case t of { Kelvin a -> diff t (Kelvin a) }

What do you expect the function test is? Yes, the const True one! The explanation is simple, as we are in a referentially transparent context, destructuring a value by pattern matching and reconstructing it the same way from its parts creates a value undistinguishable from the original. This of course means that diff will not be able to detect a difference.

Let's switch to a different interpretation. Some oracle invokes the case branch and says: I am not allowed to tell you what it is but here is a Float named a and you can assume that Kelvin a is indistinguishable from t!

Look ma, no 'pattern matching' or 'destructuring' needed!

a may contain 3.14 or 3.15 or 100.1 or ..., ad infinitum, we simply do not know. But we know that it names a Float! It exists as a Float. Mathematically the case branch can be written as

∃a:Float (t ≡ Kelvin a) . diff t (Kelvin a)

which is the english phrase "compute diff t (Kelvin a) under the assumption that there is a Float-valued number that when passed to the function Kelvin becomes undistinguishable from the case scrutinee".

After seeing the same thing in three languages we have to reformulate it one more time. Into logic, that is the language of type theory. Types are propositions and any value one type inhabit proves the corresponding proposition. The existential quantifier (∃) above gets mapped to a dependent sum that is the input to the computation

t : Temp ⊦ 〈a : Float, proof : SomeProp(t, a)〉. diff t (Kelvin a)

I took this formulation (and other wisdom) from Appendix A of Steve Awodey's recent paper. This part unfortunately is not my strongest side. My best guess is that SomeProp(t, a) is a type that encodes the sameness fact, and depends on a. Moreover, proof is an inhabitant of that type. The 〈a : Float, proof : SomeProp(t, a)〉 construct binds two existential variables. The I hope to come up with a nicer formulation sometime. (Please comment if I got something wrong, thanks!)

After understanding this, we can advance to more involved issues, namely one level higher. Take a look at this gorgeous definition:

data Ex :: * where
Hide :: a -> Ex

This is a pretty useless data type but should be sufficient for my purposes. Then we need a function that pattern matches on it:

f :: Ex -> Bool
f e = case e of { Hide it -> True }

We see that pattern matching unhides the hidden value. It is said that it receives an existential type in the case branch where it is bound. But you will see no type annotation on it, ever.

So, what happens in the case branch this time? While the type of it might have been known at the moment of construction, at this point the type system does not know it. So it is assumed to have some type t. After giving our unknown a name (thus qualifying it existentially) we can ponder about the value of it. This is something we have explored above already, so we can reformulate the case branch mathematically like follows:

∃a:* (true) . ∃it:a (e ≡ Hide it) . True

The first qualifier has just a trivial condition attached to it, I believe I could also have omitted it. I am on pretty thin ice at this point so I'll refrain from giving a type-theoretic transcription, but you can imagine that there will be two dependent sum binders where the first enters in the second in the classifier position.

One more closing thought on the oracles involved. They sound mysterious but they aren't at all. For example in Ωmega the oracle for values it the reduction machinery for runtime values. It is obvious how this machinery is able to look into closures and deconstruct instances of polynomial datatypes. On the type (also kind and up) level, however Ωmega resorts to narrowing, an evaluation mechanism usually employed in logic programming. In the typing rules these mechanisms do not have a place, thus how the variables get bound remains elusive to those.

Applicative Structures and Thrists

2010-11-27T06:37:00.001-08:00

I've been toying with the idea of furnishing the the applicative framework into thrist-like clothing, with early attempts here.

Last night I might have gotten it, finally...

Here is the idea. Since function application is left-associative, but thrists are right associative, I'll reverse the application's direction to right-to-left, i.e. f a b c will become c b a f. This uglyness is another reason to finally whip up a RevThrist, which would be SNOC-like and left-associative.

We need following ingredients:

Fun - functions perform the reduction to a new object,
Arg - arguments successively saturate the applicable structure to the right,
Par - partial application (or parent) initiates the reduction.

I'll explain these elements next, but first rewrite the above expression a bit to get a parentesized form (c(b(a f))), and now with roles marked up in thrist syntax:

Cons (Arg c) $ Cons (Arg b) $ Cons (Arg a) $ Cons (Fun f) Nil

Looks almost reasonable. Time to define the ingredients mentioned above. Remember, that it must be a two-parameter data type and that the types must match up between Arg c and Arg b, etc., and finally between Arg a and Fun f. This is a pretty hefty requirement!

We can attempt passing the effective application type between the ingredients, defining the data structure as

data Appli :: * → * → * where
Fun :: (a → b) → Appli (a → b) c
Arg :: a → Appli b (a → b)

This means functions pass their own type to the left (and ignoring what comes from the right), while arguments expect a saturable effective type from the right, store an appropriate value and propagate the remaining type to the left. This should work now: Cons (Arg 'a') $ Cons (Fun ord) Nil, with the type being Thrist Appli Int c. As you can see, no function type gets passed to the left, so you cannot prepend any more arguments.

But this all appears useless since we cannot nest things. The Par ingredient will take care of this:

Par :: Thrist Appli a c → Appli b (a → b)

Par has a double role, it acts just like an argument, but holding a thrist inside, and thus groups a sub-application.

The c type variable occurring in Par and Fun troubled me a lot, because it allows building up illegal thrists. Consider Cons (Fun f) $ Cons (Fun f) Nil. This gibberish cannot be assigned any reasonable semantics! Finally it occurred to me to use a phantom type for filling in this breach:

data Peg

Since Peg is uninhabited, no function signature can include it (unless it is a divergent one). It also ensures that the leftmost ingredient in a thrist is a function, how practial for Par! Anyway, our Appli is done now:

data Appli :: * → * → * where
  Fun :: (a → b) → Appli (a → b) Peg
  Arg :: a → Appli b (a → b)
  Par :: Thrist Appli a Peg → Appli b (a → b)

So what brave soul will try this out? Because I must confess, up to this point I've been too lazy to fire up GHC!

You might be inclined to say, why this whole circus? An awkward notation for something as simple as function application? Any Haskell implementation can do this with a beautiful syntax!

Yes, we can build up applications but can't even compute them. This is a toy at the moment. But try to pull apart an application in Haskell! You can't! Here you can add an evaluator (foldlThrist?) and also instrument, trace, debug your evaluation process.

Also, there is a reason I say 'Applicative Structures' in the title. Here is a generalization of Appli that is parametrized:

data Appli :: (* → * → *) → * → * → * where
  Fun :: (a ~> b) → Appli (~>) (a ~> b) Peg
  Arg :: a → Appli (~>) b (a ~> b)
  Par :: Thrist (Appli (~>)) a Peg → Appli (~>) b (a ~> b)

You are free now to create your own function and value space with attached typing rules and still be able to use Thrist (Appli MySpace)...

The possibilities are endless, e.g. encrypted execution on remote hosts or abstract interpretation, you say it.

Have Fun!

Type Synonyms Generalized

2010-11-25T15:06:00.000-08:00

Type functions are the new trend. Ωmega has them with the following syntax:

tfun :: Nat ~> Nat
{tfun Z} = S Z

Haskell (that is GHC) has them in the flavor of type families.

It has just occurred to me that they can be considered as a syntactic relaxation of type synonyms! Look:

tfun :: Nat ~> Nat
type tfun Z = S Z
type tfun (S n) = Z

When conventional type synonyms are used they must be fully applied. This should be the case here too. I am not sure whether type families or Ωmega-style type functions can be partially applied, though.

Anyway, a bit more to write at the definition site but less curlies to type at the call site; it may well be worth it.

Patterns and Existentials

2010-11-25T14:21:00.000-08:00

I am reading papers again and this always activates my creative fantasy. I want to explain a small revelation I had just now.

Patterns are the same thing as declaring existential values corresponding to all pattern variables according to their respective types as stated in their respective constructors and asserting that the pattern interpreted as a value is the same as the scrutinee.

The body behind the pattern in turn is similarly evaluated with the existential variables in scope. Of course the existential values are filled in by some oracle which is uninteresting from the typing perspective. A strong corollary of the asserted value identity is that we can also assert that the type of the scrutinee unifies with the type of the pattern-value (in the scope of the existentials, but not outside of it)!

Just as universally quantified values are typed by dependent products (∏-stuff) the existentially quantified values are typed by dependent sums (∑-stuff). Note that the stuff is at stratum 1, e.g. types. This is in contrast to the Haskell data declaration

data Foo = forall a . Foo a

where a is at stratum 1, being an existential type.

Hmm, when thinking this to the end we may either end up at the conventional non-inference for GADTs or something like the generalized existentials as proposed in Chuan-kai Lin's thesis.

I conjecture also that this is the same thing as the post-facto type inference I suggested here.

Now all remains to is to reinterpret function calls as a data type being a tuple with existential values and to apply the above trick.

Hats off

2010-11-23T18:09:00.000-08:00

The types subreddit references Chuan-kai Lin's PhD thesis about GADT type inference. I already have read the pointwise paper, but this is of course a revelation. He actually did implement an algorithm that inferred types for 25 (out of 30) little benchmark programs with GADTs. Previous attempts accomplished at most one!

But the thing that impressed me the most wasn't the technical side of his story but the beautifully crafted slides of his PhD defense talk. I am baffled...

Congratulations Chuan-kai!

Cooperation

2010-11-12T17:55:00.000-08:00

I have just uploaded the thrist-0.2 package to hackage. All credit goes to Brandon Simmons, who has added significant functionality and now provides some functions for thrists that are more in line with the prelude. Brandon has accepted to be a co-author to the library and I am very happy about it. Welcome, Brandon!

For the users of the package this is good news, as I am a little dim spot on the outer sectors of the haskell radar, while Brandon is a savvy and ambitioned person, and to continue with my previous metaphor, a bright green dot on the screen, swiftly moving towards the center :-)

This post is a kind of mini release note for the release. Being an experimental package we do not intend to guarantee API stability, so we took the freedom to rename routines to make naming more consistent with the prelude. foldThrist is now foldrThrist and it got a bunch of new cousins too. Notably the types are much wider now, which allows for some more magic to happen. Finally, the haddock comments have been enhanced and as-of-present actually tell something.

Please ignore the sub-modules for now, they are unfinished, and much more experimental than the rest (I have not got around researching a compelling solution yet). A RevThrist (or similar) GADT did not make it into the release, I hope I can cram it in sometime later.

Anyway, enjoy the lib!

Lion's Share

2010-10-18T13:56:00.000-07:00

I am sick. Five days already, and counting. My brain feels like Sauerkraut and thinking is hard. But my dysregulated sleep cycle lets me ponder all kinds of idle things.

One of them is the upcoming "Back to Mac" announcements on Wednesday 11/9. It seems pretty sure that Mac OS X 10.7 (or 11.0 possibly) will be introduced under the 'Lion' code name. This is pretty exciting as nothing really revolutionary happened in the Mac world since 'Leopard'.

Many people are speculating what the foundations will be. My bet is a fully-LLVM compiled system: good-bye GCC, we had a nice time together. The majority of the LLVM team is virtually absent from the IRC channel and the mailing lists, they must be working on something big...

That is, ironing out the latest bugs so that nothing embarrassing can happen while Steve is on stage. But clang v2.8 already compiles e.g. the FreeBSD kernel and userland with pretty good quality, so this cannot be the entire reason. The (already filled-in) job posting for a "revolutionary new feature in the very foundations of Mac OS X" is probably LLVM-related. Modern GPUs have hundreds of very potent processors that excel at floating-point computations. To use them effectively one needs a flexible compiler that can specialize snippets of code to run on each with optimal throughput. OpenCL attempts this but mostly in the graphical domain, and it sources from a C-like language. What we have in this case, however, is not about graphics... I am going on a limb here and suggest that the new feature is about ... conscience! Yeah, a primitive (compared to humans) but effective way of reflection, that is, understanding of its own existence and goals. Also the goals of the user! This will pave the way to new forms of assistance the OS can provide for us to get our jobs done. It has been tried many times, but to cite the job description, "Something that has never been done before and will truly amaze everyone".

My neuronal storm has ceased, I feel limp and tired. Time for another nap. Bye.

Link as link can

2010-08-27T20:29:00.000-07:00

Today I made my first significant contribution to clang, by fixing PR8007, which was a showstopper for building the codebase that I develop at my workplace. I added a testcase that validates the fix, too. In a nutshell, everything compiled well, but failed to link because of a non-instantiated type-dependent friend function.

Admittedly, I am a green-horned newbie when it comes to clang, but even so I succeeded debugging the problem with some hints from Doug Gregor (on IRC) in two hours. The fix arrived on short order after the conception of the solution idea.

That I could get this working in a few hours is an astonishing feat (that I am pretty proud of) and a tell-tale aspect of clang's awesome design. Naturally, I still have to survive post-commit review, especially w.r.t. performance regressions; OTOH I am rather confident that I got the semantics right. Some loose ends in testing remain, which I hope to wrap up this weekend, so that I can see my application linking with clang (LLVM) on monday. That will burst up the doors towards static analysis...

Go CLANG!

PS: Hopefully I won't need months to make this working ;-)

64-bit Waymarking

2010-07-21T15:00:00.000-07:00

Finally I came around working on the 64bit variant of my (array) waymarking algorithm, the result of which can be observer here (starting at line 77). But I'd like to provide some background first.

Back when I implemented the original waymarking algorithm with a 2-bit alphabet used as the marks, I hoped that extending the alphabet to have 3 bits could be a major win. 64-bit pointers are by ABI rules aligned on an eight byte boundary, so pointers to these have their 3 lowest bits cleared, and I can use this space for jotting down the marks. With eight letters I can fully encode four digits and the two stops. This almost halves the number of accesses. The big question is how to assign a lucrative rôle to the remaining two characters! After some thinking I settled with the idea to make them valued stops. Clearly, increasing the frequency of stops reduces the chance of long linear searches. In the current incarnation 'x' carries a value of (binary) 01 at the start and at the end of a digit sequence, while 'y' carries 02 in the start rôle only. 's' is not carrying any value and is used when neither of the others fit. Since "s0" is a silly fragment to create, so I assign a special meaning of "s10" to it.

I designed the decoder (d3code) first. It is essential that it obtains the correct length for the string tail wherever it starts out. And it should minimize the number of accesses to characters in the string. The decoding rules are taylored to only need maximally 4 accesses to compute the correct length for the last 12 characters. Actually the last couple of marks were a result of a co-evolution with the decoder's rules. In the front of this part the digit sequences become longer and there is less wiggle room, this part can be automatically generated.

The code as it is now needs some serious cleanup, but it does QuickCheck and I am pretty confident that it is correct for all lengths. Of course you are encouraged to find a better scheme, but so far I am happy with it.

PS: As I wrote this I discovered that I can eliminate another 2 characters of my hand-written seed string.

PPS: I do not employ the 'x' terminates with a value rule in the generator yet, only in the hand-written seed. But it should be easy enough to change every "3sx" to "x" in the generator.

The Proof is in the Pudding

2010-07-14T16:12:00.000-07:00

Looks like I've finally done it! r108240 stuck and no broken external projects have been reported. I've prepared some little statistic and quietly celebrating the 1%+ speed gain of LLVM in the last week.

Now on, plucking some more low-hanging fruit before adventuring into some more hard-core changes!

Update: The ClangBSD project will surely put it through some serious regression testing...

Emacs the Lifesaver

2010-06-24T07:55:00.000-07:00

I was not thrilled of the task in front of me. Refreshing an old mega-patch, revise virtually every hunk to use a different interface, and committing it piecemeal to the repository again. Sounds like a long error prone job of suffering.

Fortunately here is where the power tools come in. I

re-merged the backed out revision, postponing conflicts;
saved the diff away and reverted the repository;
wrote a small awk script to massage the hunks in the diff to get a new patch;
fired up emacs with the patch and applied each hunk after thorough review (and seldom with minor changes);
some hunks are not ready to go in yet as they do not qualify as refactoring, these are kept for later;
commit almost every file as a separate revision.

I spend the most time in Emacs (the Mac OS X incarnation, Aquamacs is fantastic). It provides me all the comfort and productivity I need:

it provides all necessary hunk operations such as apply, reverse, go to original, drop etc.
I can transparently work from a remote machine via ssh, including editing, version control and the above diff operations
peace of mind, by being rock solid and autosaving stuff.

The only inconvenience is the sheer amount of keyboard equivalents, but I am getting used to them too.

Thanks Emacs, without you I would probably drop!

Burning ISO CDs

2010-06-22T17:24:00.000-07:00

I wasted some hours with trying to burn ISO CDs on the mac.

I tried various methods like converting .dmg to .cdr (CD Master) in Disk Utility, but the resulting CD always mounted as HFS+.

Finally I googled a nice method:

hdiutil makehybrid -iso -o MyImage.iso /Volumes/SomeFolder/

will create an ISO filesystem, which can be burnt with Disk Utility and shows up like that in the Finder. That is - well, I am pretty sure - readable on PCs.

Alternatively I may use

hdiutil burn MyImage.iso

I believe...

In retrospect, some of my burn products may have ended up as PC-readable too, since hybrid filesystems may have been created. I'll test them on a PC tomorrow for sure.

Sized types

2010-06-18T12:01:00.000-07:00

I have always liked the idea of assigning some notion of size to (tree-like) values, and track its changes along pattern matching and construction to be able to reason about termination-unaffecting recursive calls.

Many years ago, when reading the Hughes-Pareto-Sabry paper I did not see the point yet why termination is fundamental in various aspects.

Only when sitting on the park bench on the isle of Margitsziget (Budapest) and discussing with Tim about sound logic in Ωmega, it dawned to me how termination checking with sized types can be exploited.

I developed the intuition of the tree-like data floating heads down in the water and we are reasoning about criteria that it can still float without touching the ground at depth n. Still, this metaphor was rather hazy.

In the meantime I have tried to digest the relevant papers from Barthe and Abel, brainstormed somewhat here and let my brain background.

Yesterday, I found (on reddit) a link to Abel's new MiniAgda implementation and its description. It made clear to me that my early intuition was not bad at all, the water depth is the upper limit of the size, and recursion is to reduce this to obtain a well-founded induction.

Now it is time to rethink my ideas about infinite function types and how they can be reconciled with sized types.

But it looks like Abel has done the hard work and his Haskell implementation of MiniAgda could be married with Ωmega in the following way: Derive a sized variant of every (suitable) Ωmega datatype and try to check which functions on them terminate. These can be used as theorems in Ωmega.

Hopefully Tim is paying attention to this when implementing Trellys...

My grief with out-of-tree code

2010-06-08T03:23:00.000-07:00

This post is a long-standing todo item in my brain, but this checkin actually prompted me to do it.

A little bit of history first. As a software developer currently mostly active in the embedded space, I like solutions which allow me to save some CPU cycles or bytes of RAM here and there as long as they still allow me to use the same interfaces. Exploiting the characteristics of the underlying hardware and algorithms is often low-hanging fruit when it comes to optimizations.
So I have this little agenda of about 10 items I wish to implement in the future to make the LLVM framework a little more efficient.

One of these was to reorder the operands inside of the call instruction, to obtain faster access to the callee but mainly to allow fast visitation of all instructions that have a certain callee. I explained all my motives in a separate mail, so I want to save you from the gory details here. To make a long story short, it took me several iterations to catch all places in the optimizers where the operand order was assumed to be in the (callee, arg1, arg2, ...) fashion, instead of the new (arg1, arg2, ..., callee) one, and some miscompilations were only revealed by running the nightly tests. It was a work of blood and sweat because there are many intrinsics and transformations on them and they are often manipulating via the low-level interface getOperand(n). Actually there is a nice helper interface, called CallSite, which makes it easy to access the call instruction's arguments in a high-level fashion and this interface probably the best for LLVM clients, since its also handles the invoke instructions. However, I regard it ok to use the low-level interface in the LLVM tree directly, since it is possible to consistently change things in one atomic commit.
Finally, the day where all regression and nightly tests succeeded, has dawned. My patch seemingly stuck, with all buildbots green. I left for downtown and returned late at night. Just to discover that all has been backed out, because my change broke havoc in an Apple project that obviously used the low-level interface. This was especially frustrating, since I cannot even submit a correcting patch against that project.

I did receive very little encouraging support, not even moral one. Some comments were even pretty dismissive, like this patch has already caused many problems, it is not worth it for such a marginal gain. I have no problem with the comment itself, since I would utter such words in comparable situations too, but this time it was my investment that was at stake. I was pretty determined to keep fighting.

I wondered whether new measurements with higher arity calls would find a significant speedup with my patch applied. So I did some benchmarking for cases where the change is expected to make a difference, and actually found (roughly) a 3% speedup. Clearly this number is only achieved in specific situations, so the generic case would be well below that, but still it could compensate for many little time eaters that are necessary for an advanced optimization pass or analysis.

In my conversation with the involved engineer I enumerated following reasons why resorting to low-level interface in out-of-tree projects is a bad idea:

they are not conveying the intent
they are depending on implementation details by reaching over abstraction barriers
they are an impediment to change

(these are mostly the same reasons which you can find in the above commit message too). He did agree to all this and promised to nudge the OpenGL implementors. I also received a request to submit a patch that guarantees that no silent breakage can happen. Well, I acknowledged that this is a valid concern, so I did some brainstorming.

I succeeded to put together a small patch that detected all instances of get/setOperand(0), the major potential cause of breakage in external projects. Compiling with this patch would pinpoint all places where getCalledValue() should be used.

But I cannot promise more than that!

Why it is impossible to guarantee that with my proposed change either everything keeps working or there is a compilation error with a clear fixing indication? Because the User baseclass does provide the low-level getOperand interface too and I cannot disallow that. C++ only lets me protect parts of the CallInst class...
Would a patch to make getOperand private in CallInst be accepted? Probably not now, but read on.

What aggravates the problem with private trees is file ownership. The engineer who detects the breakage is not entitled to fix simple cases, but needs to lobby the project/file owner first. This results in additional inertia. (Disclaimer: I am not sure whether Apple does have a file-ownership model internally.)

Surprisingly the same thing that happened to me theoretically could happen to any Apple engineer too. Imagine some checkin to LLVM broke the dragonegg GCC plugin which is effectively licensed as GPLv3, so no Apple engineer is allowed to inspect its sources. What would happen if the dragonegg maintainer backed out the change on grounds of "broke an important external project"?

What to do next? Now, whining is not one of the things I like to do, so let's advance in some way. Bill's patch I mentioned in the beginning is a possible first step, as I could rework a large portion of my patch in terms of getArgOperand(n-1) instead of getOperand(n-1), without actually changing the operand order for now. These kinds of incremental refactorings that do not change functionality are mostly welcome in the LLVM world. Then I am dependent on the goodwill of some Apple engineer to make a similar change in that internal project too. Finally the switch (i.e. the operand order) could be flipped.

Why I am reluctant to begin? Because it is lots of work, many new intrinsics have been introduced, I definitely will get a bunch of merge conflicts, and finally, who knows, there might be another internal project that chokes and the whole misery enters a new iteration.

Why do I feel that the change is urgent? Because LLVM is getting popular with an extraordinal speed. As more and more external projects use LLVM as a foundation, more and more code will exhibit bad habits of using low-level interfaces. The few post-v2.7 months are probably the last chance to make the switch in argument order, before things become de-facto cemented. Maybe it is too late already. That would be a pity, though, LLVM as a compilation infrastructure should be as fast and nimble as possible. Every one of its clients would profit.

So, dear external tree developers, I hope you get rid of the low-level calls and use the high-level ones instead. It should not cost you more than touching a couple of lines and retesting. I would be happy to assist you.

Regarding development policy, I would welcome a clear statement about what amount of testing in the LLVM ecosystem is "sufficient" and excludes the risk of a patch being backed out.

Bottom line, I'd love to get this patch wrapped up, but I am dependent on the support of external tree owners. Are you willing to help me?

Patrícia's New Hobby

2009-11-25T14:45:00.000-08:00

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

2009-11-02T15:47:00.000-08:00

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

2009-10-01T14:37:00.000-07:00

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

2009-08-04T15:52:00.000-07:00

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

the LLVM type system (on defs, uses and constants),
that Phi nodes must not go into entry blocks,
that Phi nodes must preceed other instructions in the basic block,
every use must happen in the scope of a corresponding def,
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

2009-06-14T14:56:00.000-07:00

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

2009-05-27T06:43:00.000-07:00

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 …

2009-03-31T22:15:00.000-07:00

… 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

2009-03-21T15:04:00.000-07:00

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

2009-03-11T05:05:00.000-07:00

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

2009-03-03T14:55:00.000-08:00

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

2009-01-30T16:27:00.000-08:00

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

2009-01-28T15:27:00.000-08:00

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 :-)

Hauskauf

2008-10-09T09:30:00.000-07:00

Heute war doch ein recht spezieller Tag. Notartermin zwecks Vertragsunterzeichnung. Ich kann nur sagen daß mein Herz doch ziemlich in die Hose geruscht ist...
...noch nie habe ich so eine Menge Geld auf eine Karte gesetzt. Als nächstes nun wird bezahlt und dann beginnt der lange, schweißtreibende Weg zur Tilgung. Darüber später mehr.

Hoare Triples and Thrists

2008-09-10T12:54:00.000-07:00

While mousing through the L4.verified presentation that took place at Galois, I could not help but build an association bridge between Hoare triples and thrists. Especially when you go to p. 52 and thereabout.
Here is my take on the connection:

We have some commands that belong to a data type C, and C has two type parameters:

data C :: * -> * -> * where
  C1 :: ... -> C a b

The first type parameter can be interpreted as the precondition of the command while the second as its postcondition ({P} and {Q} in Hoare's notation). This convention employs the types-as-properties interpretation.
If commands are sequenced, the postconditions of the former commands must imply the preconditions of the latter. This is referred to as the composition rule and corresponds to appending two thrists.

Now, in Ωmega the situation is even prettier, because C need not be a two-type-parameter entity, but can be parameterized over arbitrary kinds. The built-in evaluation mechanism (type functions) allow the most powerful constructs. (Haskell will get something similar at the type level, called type families, with GHC v6.10.)

Saudades

2008-09-03T12:22:00.000-07:00

É muito bom ficar sozinho alguns dias, pensando e trabalhando em paz. Mas quando as semanas passam a distância parece que aumenta e a ausência começa de doer.

Meus amores sinto muito falta de voces, quero que voltam logo.

Meme evolution

2008-09-01T09:38:00.000-07:00

While I am missing family induced distraction, I use the opportunity of reading old papers that I always wanted to revisit.

Yesterday, while reading "A History of Haskell" I was amused by the sentence:

"Wadler misunderstood what Fasel had in mind, and type classes were born!"

This is a concrete case of "meme evolution" (in Dawkins' sense): a mutation of a meme (by transcription error) finds a new habitat where it thrives and blossoms.

Some preconditions are needed for this to happen:

communication
loosening of amorphous ideas
an open mind, not shying away from listening to the unknown

Many great ideas come to me while reading conference papers of others and where I have no idea what they are talking about :-) While trying to make vague sense of what I have in front of me a fireworks of ideas commence, all building in some way on foundations of things (pet projects) I have done in the past.

Now, how can I ensure that I periodically can enjoy the state of minimal disturbances?

Generalized Monads --> Gonads :-)

2008-08-30T04:25:00.000-07:00

Here is the usual (basic) definition of monads:

class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b

This is very much restricted to ordinary function types!
Let's see how this restriction can be lifted...

class Category (~>) => Geonad (g (~>)) where
  return :: a ~> g (~>) a
  (>>=) :: g (~>) a ~> (a ~> g (~>) b) ~> g (~>) b

Since the semantics of gonads are already eminently taken, I settled for the name Geonad.

No idea whether this can produce something relevant for our lives :-)

Cheers,
Gabor

I'd like to see, but do you want to Show?

2008-08-26T09:05:00.000-07:00

So, yesterday I tried to implement

instance Show (Thrist (a ~> b)) where ...

... and ran against several walls. The short story is: Forget it!

The long story comes next, if you are interested.

First of all, what do we want? In my paper I define a nice thrist

[('A', 33), (65, 'a')]l :: Thrist (,) Char Char

and the Ωmega interpreter readily prints it. I wanted to do the same in Haskell too, as a pretty extension of my thrist package. I started like this:

instance Show (a ~> b) => Show (Thrist (~>) a b)
show Nil = "[]l"

I even managed to show singleton thrists (which hold just one element).
But the first obstacle was immediate: When the thrist has more than one element the hidden existential type appears, but the compiler does not know that this (a ~> x) has a Show instance!

So I hoped to extend the context to require Show (forall a b . a ~> b) that is I want all saturations of the type constructor (~>) to be Showable. But GHC does not like this syntax...

At his point I started some fundamental thinking...

Since the type of the thrist only reveals the beginning and the end, there may be arbitrary non-showable types hidden inside, even if the resulting type conveys the illusion of Showability. To wit:

[(5, id), (id, 42)]l :: Thrist (,) Int Int

We can enter such a thing, but there is no hope to show it :-(

So what are our remaining options? Ganesh has brought Show2 to my attention, I might look at it soon, but it won't solve the above problem.

We can say goodbye to (,) and define something like:

newtype Pair a b = (Show a, Show b) => Pair (a, b)

There is some hope that Thrist Pair a b can be declared as a Show2 instance.
Who knows?

PS: Ωmega cheats, of course. It frobs the Show functionality of the underlying Haskell implementation. It also prints functions as <fn>.

Uploaded

2008-08-23T08:44:00.000-07:00

It's done!

My first contribution to the Haskell community has just landed in the belly of the beast...

Overall it was a very pleasurable experience:

the website is well organized and makes it easy to find the relevant information,
the account is obtained unbureaucratically by e-mail, and the answer is prompt,
the upload checker provides helpful guidance how to improve the package.

The package itself is in very early stage, please do not expect a wealth of functionality :-). Also the (constructor) function names are expected to change (Cons --> :~) to better fit into the language's overall feel.

I have already included a crucial foldThrist function, which is Ganesh's idea (thanks for the feedback, btw.!). What comes now is to figure out how mapThrist could be defined. It is somewhat tricky, as there are three type parameters to deal with (let alone all the existential types inside).

One thing comes to my mind as I think about it. mapThrist could change the first parameter, i.e.:

Thrist (->) a b -> Thrist (,) a b

an elegant way to record the intermediate values of function composition.

Fun stuff.

Ca(ni)balized

2008-08-22T17:03:00.000-07:00

Today I finally came around reading my way through the Creating my First Haskell Package tutorial, and have put together my first cabalized library. And I must confess that I found it really enjoyable. Certainly not more complicated than writing a makefile or adding a macport.

Btw., the said library is thrist-0.0 (what a surprise!) and it is just the embryonal first step. I already have some more stuff in the pipeline...

Could not upload it to Hackage yet because I am waiting for my account on the server.

Trotting Forward

2008-08-04T05:56:00.000-07:00

I am in vacation in Brazil, mostly in an apartment building facing the ocean, but I had little chance to enjoy the water so far. There are several reasons for this, the most important being that Helena was sick the past week and still receives antibiotics. It is also raining a lot and is somewhat cold (24 °C) for my taste.
But I have the nights for creative work, so I picked up my recent idea and started fleshing out the design.
I succeeded in writing a QuickCheck generator for randomly creating Insert/Remove sequences steering the lifetime of a Value's def/use chain. I am able to update a given chain according to a history and check that it has still consistently set up waymarks that lead back to the Value.

I am pretty happy with the results so far.

Now it is time to enter the second phase and proactively optimize worn-off waymarks. As discussed in the other blog post the stretchy/shrinky nature of def/use chains leads to deterioration of the waymarks because Stop marks may be punched into the valid (fixed-length) clusters of Zeros/Ones. This happens at Insert events. On the other hand, Remove events may reduce clusters, thus invalidating them. So it is important to refresh the waymarks when longer islands of invalid marks are encountered. The twist is to retain O(1) complexity, which is not too challenging, but given the volatility of the chain some cleverness is needed.

I have a smallish plan how to do it: Since I expect that the volatility mostly occurs at the head of the chain (short-lived Use object getting inserted and soon removed), I intend to adjust the waymarks as far to the end as possible. So I have to keep a pointer to the start to invalid cluster immediately preceding a found valid cluster (or FullStop) and refresh the waymarks if there are enough elements present to form a valid cluster. Alternatively I could use the Prev members to walk backwards (in the C++ implementation, since these do not appear in Haskell).

But I expect that only a nice histogram of a usage statistics will help to find the optimal strategy anyway.

Draft Thrist Paper Online

2008-07-11T12:10:00.000-07:00

I am happy to announce that my thrist paper I've been working on more than a year is now complete, and downloadable from my ad-hoc web directory. Completeness does not mean absence of errors or lack of room for improvement. If you like my paper and would like to improve the presentation please contact me. You can find my e-mail address in my profile. I am happy for every comment, though I cannot guarantee that I will pick it up. Please consider that this is still a draft so it should not be passed on and also please do not cite or link to it, as all links will break when the final version comes out.

It has been quite a fight to get this far. I started out April 2007, and the initial e-mails turned into a paper of several pages. But then life took over. My wife in final days of pregnancy needed my support, my daughter was born. Everybody who has been through such events knows that it is a different mode of living. Sleep deprivation and all that...

Also, while I have started several papers already, I have never gotten around to finish one. This was quite traumatic, and this time I had sufficient resolve to get through. Hopefully more follow.

A final word: the formatting of source code sometimes line-breaks in ugly ways. The reason is that the format may change to one column page and then all is right. This depends on the channel how the paper gets published. Updates may happen next week, but July 18 is my absolute deadline.

Enjoy.

Clang Server?

2008-07-07T14:31:00.000-07:00

Sometimes things happen that sound like a miracle. There is this guy, Peter, who signs up for Google SoC, with mentor and all. The project plan is to come up with a distcc-like parallel/distributed compilation scheme, only with clang, the aspiring LLVM C frontend.
He gets the deal, but the weeks run away, and no signs of any progress. Peter is missing in action.
Then, suddenly this weekend: a status report.
I did not look at the attached patch, but he promises a working compile server, no less!

Things I hate

2008-07-05T08:48:00.000-07:00

Each year the same tragicomedy. Filling out my tax declaration. After procrastinating the first half of the year, and seeing that everybody else already has done it. Being dragged kicking and screaming by my wife (I love her nevertheless). Sometimes I even volunteer to do the stuff.
But every time I read the forms I do not understand how to fill in the right values. The words make so little sense to me. Even if I figured it out last year, it has almost no value, I have already forgotten it. So I can only stare at the last year's form and try to find the corresponding box, which is not so easy since the boxes tend to wander around. I usually give up and opt for another messed-up evening.

And now there are the tax papers for my wife also to be done, yes, her company is new and the bureaucracy requests 12 reports a year and a final declaration. That is not enough, this all has to be made official and another two exemptions handed in till end of May.

Welcome to Germany!

I definitely prefer programming to this.

Birthday season

2008-06-20T02:20:00.000-07:00

Last Sunday we celebrated my baby daughter Helena's first birthday. She enjoyed it to be in the focal point of the party, but the guests had their fun too. There was another boy, around 16 months old and they played together, hugging each other now and then. Just cute.

My son turns 12 mid-July and he'll celebrate twice, at home and some days later in Brazil. This event will close the string of birthday dates in my family, commencing with mine on 29. of April and about 10 in between :-)
A kind of frenzy, especially when you are looking back. And people keep telling me that there used to happen a different kind of frenzy in respective years ten months before :-P

OpenCL / CLang / CL

2008-06-12T15:46:00.000-07:00

The most exciting thing that happens under sleep deprivation is a kind of stream of consciousness, where the brain goes into a purely associative mode. I am sleepy now and so I can embark on some journey which I tomorrow morning surely will dismiss as utter nonsense.

So, WWDC is progressing at the moment, some under-the-hood technologies are being introduced into the OS X system that is running on the Macs out there. Two of these sound interesting: "Grand Central Dispatcher" and OpenCL. There has been some speculation that utilizing GPU power (which is 99,9% idle, unless you are a framerate-wanking gamer) could be one of the directions of the future (besides multi-cores). Nvidia and ATI both offer technologies to do this at different levels, but they are incompatible. It is hard to imagine that Apple will provide developers several different and incompatible compilers and tell them to compile their compute intensive kernels with them, bundle them up in some big blob of application and ship it untested (how many developers will buy a bunch of video-cards for testing?).

Apple likes to provide seamless solutions. They have a proven concept in their OpenGL implementation, namely a machine-independent binary format that can be JITted to a wide variety of processors: LLVM. This would make Joe Developer's life pretty easy: compile your computing kernels to LLVM bitcode, and submit a quadruple to a runtime component (bitcode, characteristics, input data, continuation/consumer of results). The characteristics could state that it is integer- or FP-heavy code etc. After deciding which target will run the code, the LLVM JIT could distill the optimal machine code for the target and invoke it on the input data. When done, the continuation would be called, and would consume the results. Add some speculative execution (start the same job in several computing resources), a good deal of caching (no need to recompile bitcode again), heuristics and profile guided recompilation. This could be some yummy sauce.

RoughlyDrafted's blog so far provides the best intro to the new technology, and helped to start my association chain. What comes next is the fun part.

When hearing OpenCL the first time, I thought, what a sucky name. It reminds me of OpenGL, but it is not a graphics language. It reminds me of Common Lisp, but that is not an option. Open Computing Language. Hmmm, all programming languages compute stuff...

There is a little gem, still unpolished, called clang. The light footed successor of gcc in corporate environments. Compiling "curly brace" languages to LLVM! Wasn't OpenCL C-based? Those letters CL appear everywhere. What is the initials of the principal LLVM engineer, again?

Merged

2008-05-16T08:27:00.000-07:00

It did not make it into LLVM release 2.3 (let's be conservative), but it looks like my use-diet branch will make it into LLVM 2.4! I have merged the relevant changes on last Saturday (2008-05-10), and so far it has not been reverted :-)

Owen did some memory statistics and found out that the SPEC benchmark 447.dealII had a 13% reduced memory footprint with my patches. This is about what I expected, and a pretty awesome result. Despite of the algorithmic overhead that has been (knowingly) added the compilation did not really get slower, indeed some nightly testers show slightly improved cpu times. Again, this is in line with my observed slight speedup on kimwitu++ benchmark's compilation time.

What's next?

My plans are to do some more API cleanup and then go after even more memory savings which I am already drafting in my fantasies... Whether they are feasible compile-time-wise is still an open question, but I am determined to find out.

Absolutely, Positively Crazy

2008-04-19T01:49:00.000-07:00

My previous two posts revolved around space optimizations in LLVM. The presented technique is a bit unconventional, and paired with the confusing nature of def-use chains, it can leave one quite puzzled...

Today in the LLVM IRC channel, chandlerc wondered whether I am eliminating the Value* from the Use struct. I corrected him, that, no, it is all about eliminating User*. But his question drove a nail im my head, making me think. After all, he was thinking of the def-use chain, and I was always dealing with user-use arrays. But deeply inside it is the same problem, a.k.a. the dual one:

for a user-use array the User* for all array members is constant, while the defs (Value*-s) vary,
for a def-use chain on the other hand the defs (Value*-s) are invariant, while the User*-s vary.

I wondered whether it is feasible to use the tagging technique to get rid of the Use::Val too? After all, it is just a linked list, and I have already demonstrated something similar in my previous posts.

It turns out that it is perfectly feasible, and the rest of this post demonstrates how...
...but please do not misunderstand, I do not propose this for LLVM (yet?).

Let's recapitulate what a def->use chain is:
There is an instruction that generates a value, thus defining it:


      +-------+
Val = | Instr |
      +-------+

Then there are other instructions which consume this value, but the above instruction only sees the Use objects chained up:


   +-------+
   | Instr |
   +----+--+
        |     +---+    +---+    +---+
        +---->|Use|--->|Use|--->|Use|---X
              +---+    +---+    +---+

The X above means that Use::Next is filled with NULL. Otherwise Use::Next obviously contains the pointer to the next Use object.
So to apply waymarking we have to get away with two obstacles:

There is no way to store something around the Use object (layout-wise), as we did with user-use arrays. We cannot go outside to place the Value*.
Def-use chains can be expanded and shrunk dynamically.

It turns out that 1) is pretty easy, we do not store NULL in the last Use's Next field, but the Value*, with the ‹fullstop› waymark. So when we see ‹fullstop›, the Value* can be extracted from the upper bits.
So, let's assume the ‹stop› and ‹0›, ‹1› waymarks are also tucked on the Use::Next fields. Like usual, given any Use* we can pick up the digits, and at the ‹stop› we convert the digits to a Value* and we are done. This is nice and dandy, until we remember 2). It appears a bit more tricky. Obviously the insertion/deletion will remove waymarks or add new ones. Our algorithm may begin producing bogus Value*-s. So is there any solution to this problem?
I believe there is. I have no proof but I conjecture that each destructive operation should simply place a ‹stop›, and when the algorithm is changed to only accept 32 digits between two ‹stop›s, then we are on the safe side. The corruption gets detected, an uncorrupted segment can still be found, downstream. The corruption can be repaired later (e.g. when traversing the def-use chain).

Well this is not a very efficient way of doing things, so it probably only pays off when space is extremely limited and compilation/optimization speed is not paramount. But in these applications an 8-byte (down from 16/12 bytes) Use struct is definitely tempting.

Use-diet Update

2008-04-14T17:47:00.000-07:00

As of r49698 the use-diet branch finishes the testsuite (about 2000 tests) without regressions. Actually the User* member of the structure is not eliminated yet, but instead deliberately set to NULL in various places, and if present, I assert that it equals the computed value.

It was quite a fight to get thus far, but it is done! Time to open a good bottle of wine...

The next days will be devoted to cleaning up the sometimes messy details, doing some statistics and cautiously trying to merge back my work to trunk.

Wish me luck.

LLVM Data Structures, and Putting Use on Diet

2008-04-13T02:17:00.000-07:00

There is a good deal of refactoring going on in the LLVM universe, to wit Dominic's renaming of LLVM*Builder to IRBuilder with assorted simplifications...
The train is moving fast, getting on board is harder, but rewarding. LLVM does not commit to API (or less even, binary) compatibility, so meaningful changes get in swiftly and without much bureaucracy. A simple mail, warning people of the change in advance, and when accomplished, instructions how to do the conversion, are enough to make folks happy.

There are reforms going more than skin deep, too. Clang is is getting a datastructure rewrite with nice gains, and myself is about to reduce the size of the Use struct by 4 bytes, from 16 to 12 (on a 32bit system). The 25% savings is nothing to sneeze at, considering that this struct is the most frequently allocated one in LLVM. And now that I have the functionality basically implemented on a branch, I can say, the idea is working! Consequently, I have the courage to blog about it :-)

So what is this Use-diet all about? The Use struct is the home of the pointers to all Values that an Instruction references. But each Value has to track all of its Users (i.e. the Instructions), and Use provides forward and backward pointers to chain those up. These are the essential 3 pointers. But why is Use 16 bytes? Because in some situations it is important to get back to the User of the referred Value. So it is 4 pointers in total.

Seemingly this is how it works™ and there is nothing that can be shaved off. But wait! Don't all Uses belonging to an Instruction come lined up in a contiguous array? What if we could mark the last Use specially and put a pointer to the Instruction behind it? Or even allocate the Uses immediately in front of Instruction (memory-layout wise)?

These were the first ideas how my brain-storming with Sabre began. After several exchanged emails, we settled on a concept that is IMHO really beautiful. We use 2 bits (the least significant ones, which are always zero, normally) of one of the pointers in Use to implement a serial line-like protocol of waymarks that guides us to the end of the array in some reasonably few steps. I will not detail the algorithm, since it is documented elsewhere, I will only say that there are four kinds of waymarks: ‹fullstop›, ‹stop›, ‹0› and ‹1›.

Fullstop means we are at the end already,
Stop means begin gathering digits, or if already done so, convert them to an offset, that brings us to the end,
0 and 1 are the binary digits to be picked up.

It is clear to see that for small arrays there are only a small number of operations needed to determine the end of the array. The complexity of the algorithm is O(log N). So we do not really have to get concerned with, say, 10000 predecessors to a PHI node :-). The description even contains a Haskell snippet to encode and decode such offset information.
For reference I shall present it here:

> import Test.QuickCheck
>
> digits :: Int -> [Char] -> [Char]
> digits 0 acc = '0' : acc
> digits 1 acc = '1' : acc
> digits n acc = digits (n `div` 2) $ digits (n `mod` 2) acc
>
> dist :: Int -> [Char] -> [Char]
> dist 0 [] = ['S']
> dist 0 acc = acc
> dist 1 acc = let r = dist 0 acc in 's' : digits (length r) r
> dist n acc = dist (n - 1) $ dist 1 acc
>
> takeLast n ss = reverse $ take n $ reverse ss
>
> test = takeLast 40 $ dist 20 []
>

Printing gives: "1s100000s11010s10100s1111s1010s110s11s1S"

The reverse algorithm computes the
length of the string just by examining
a certain prefix:

> pref :: [Char] -> Int
> pref "S" = 1
> pref ('s':'1':rest) = decode 2 1 rest
> pref (_:rest) = 1 + pref rest
>
> decode walk acc ('0':rest) = decode (walk + 1) (acc * 2) rest
> decode walk acc ('1':rest) = decode (walk + 1) (acc * 2 + 1) rest
> decode walk acc _ = walk + acc
>

Now, as expected, printing gives 40.

We can quickCheck this with following property:

> testcase = dist 2000 []
> testcaseLength = length testcase
>
> identityProp n = n > 0 && n <= testcaseLength ==> length arr == pref arr
> where arr = takeLast n testcase

As expected gives:

*Main> quickCheck identityProp
OK, passed 100 tests.

Btw., QuickCheck is awesome!

So where are the uses of this algorithm outside of LLVM?
There is not much of thinking needed to generalize the array to other data structures, which may permit mutating of the node contents, but disallow insertions. Linked lists are an example since one can only cons up stuff to the head. Doubly-ended arrays with fast size() operation (given a pointer to one element) can be implemented if there is another pointer in each node that we can use for storing waymarks to the start of the array. Deques also could work like this, but they too, need to be fully built up before putting in the waymarks.

This all reminds me of cons-hashing but is really a more powerful concept. Let's call it waymarking! And then let the garbage collector put in the waymarks for us...

Down with O(n) complexity on linked-list's length operation!

ETAPS Budapest

2008-03-31T12:15:00.000-07:00

I am in Budapest since Saturday, and I love it. The weather is excellent, I am in the middle of some very nice people and I can do what I like most: brainstorming cool concepts.
At a satellite event yesterday (DCC - Designing Correct Circuits) I met Tim and after the workshop we actually came to chat a plenty on Omega. I very much felt like a satellite, because I did not participate at the conference itself, just hanging around the lobby and the workshop rooms, using the "free" WLAN and thinking about what to do next.
Today then was our first Omega hacking day. Building on the googlecode repository's trunk version Tim checked in everything he had on his laptop, and now we can do concurrent development. Both the documentation and the release management toolchain have been overhauled and checked in, along with a testsuite.

This is already much more than what I dreamed of...

Tomorrow we'll go thru the issue list, squashing as many bugs as possible and I might get back to the LLVM generation branch. Another interested student will join us, an Hungarian guy called Tamás.

This is finally the place to thank Dr. Horváth Zoltán, who has very kindly offered us rooms in the university to have our hacking sessions in complete peace.

Embeddings, Part Two: Monad --> Thrist

2008-02-05T16:27:00.000-08:00

Here comes the second part of my promised embeddings, this time I'll embed any monadic chain (corresponding to the do-syntax in Haskell) into a thrist and provide a semantics. Later I'll try to discuss some convenience features and try my luck with mfix (and the mdo-notation).

As in my post dealing with arrows, we have to define an adapter GADT:

data Monad' :: (* -> *) -> * -> * -> * where
Feed :: Monad m => m b -> Monad' m a b
Digest :: Monad m => (a -> m b) -> Monad' m a b

The semantics is a bit trickier as in the arrow case, but let's find out the type signature first...
Feed sounds like an introduction of a new monadic value, we would like to interpret it as the (>>) connective. Digest on the other hand transforms, and thus corresponds to (>>=). Both expect an already formed monadic value, so we can state:

recoverM :: Monad m => m a -> Thrist (Monad' m) a b -> m b

The effect of an empty thrist is trivial:

recoverM mon Nil = mon

And the other two connectives turn out to be the only sensible way to do it:

recoverM mon (Cons (Feed m) rest) = recoverM (mon >> m) rest
recoverM mon (Cons (Digest f) rest) = recoverM (mon >>= f) rest

Now, we can build up chains:

*Embeddings> :t Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil
Cons (Feed getChar) $ Cons (Digest $ (return . ord)) Nil :: forall a. Thrist (Monad' IO) a Int

and execute them too:

*Embeddings> recoverM getChar (Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil)
Loading package haskell98 ... linking ... done.
GG71

The first 'G' is consumed by the getChar invocation that is given to recoverM, but its result is ignored. The second is having an effect too, and its result is used to obtain the ASCII value. The overall monadic action is then run by ghci, printing the 71.

We have converted >> getChar >>= (return . ord) into a thrist and got it back by means of recoverM! And this works for any monad.

Two shortcuts come to my mind, they can be modelled by adding two simpler variants to the GADT:

Feed' :: Monad m => b -> Monad' m a b
Digest' :: Monad m => (a -> b) -> Monad' m a b

The semantics should be clear, I leave the extension of recoverM to the reader.

Now what about the value fixpoint mfix? Can we dress it in thristy clothes? Frankly, I have no idea, but I would be happy to hear from you. It is late, I need sleep now. Bye.

Embeddings, Part One: Arrow --> Thrist

2008-01-31T13:06:00.000-08:00

Dan Weston asked me how the embeddings of arrows and monads into thrists would look like.
Took me some effort, but I think I have found something that appears to be satisfactory.

This time I shall prove my claim that in Haskell any Control.Arrow instance can be rewritten as a Thrist data structure. I shall also provide a semantics for the resulting data that shall recover the original arrow. Let me recapitulate the Thrist definition before diving in:

data Thrist :: (* -> * -> *) -> * -> * -> * where
Nil :: Thrist p a a
Cons :: p a b -> Thrist p b c -> Thrist p a c

Let's begin with the embedding part. Since the members of thrists are constructors of a two-parameter GADT, we have to construct the Arrow' GADT first. Here is the adapter:

data Arrow' :: (* -> * -> *) -> * -> * -> * where
Arr :: Arrow a => a b c -> Arrow' a b c
First :: Arrow a => Arrow' a b c -> Arrow' a (b, d) (c, d)

Arr takes any arrow and wraps it. This constructor is responsible for the actual embedding and it is easy to see that it is completely general.
First is responsible for defining a transformation on a pair's first component. Clearly this corresponds to the Arrow type class's first member. I refrain from doing the same to the other functions in the Arrow type class. You may scratch your head now, asking whether I have forgotten to handle the >>> member... The answer is no, I'll come back to this later.

Let's see how this works out in the practice...

t1 :: Thrist (->) Char Char
t1 = Cons ord (Cons chr Nil)

This is just the plain chaining of functions as a thrist. Here is the Arrow' embedding:

t2 :: Arrow' (->) Char Int
t2 = Arr ord

We make a thrist of length 1:

t3 :: Thrist (Arrow' (->)) Char Int
t3 = Cons t2 Nil

This is bit more involved, adding a constant second pair component:

t4 :: Arrow' (->) a (a, Int)
t4 = Arr (\a -> (a, 42))

Now it is time to form a longer thrist:

t5 :: Thrist (Arrow' (->)) Int (Int, Int)
t5 = Cons (Arr chr) (Cons t4 (Cons (First t2) Nil))

So, this corresponds to what? Intuitively, it could mean
chr >>> (\a -> (a, 42)) >>> first ord.
The Cons data constructor assumes the rôle of >>>.

To obtain a meaning at all, we have to define a semantics for it! Here it comes, and allows us to recover the embedded arrow:

recover :: Arrow a => Thrist (Arrow' a) b c -> a b c
recover Nil = arr id
recover (Cons (Arr f) r) = f >>> recover r
recover (Cons (First a) r) = first (recover $ Cons a Nil) >>> recover r

Some people call this an (operational) interpreter.

Finally, a little test:

*Embeddings> (recover t5) 55
Loading package haskell98 ... linking ... done.
(55,42)

Cute, isn't it?

PS: To embed monads, you can try embedding them via Kleisli to obtain an arrow and then via Arrow' to construct a thrist. Alternatively wait for a future post here :-)

PPS: For running the above you will need these preliminaries:

module Embeddings where
import Prelude
import Control.Arrow
import Char

What Ωmega has joined, no one can take apart

2007-12-11T19:21:00.000-08:00

Some days ago I became enthusiastic about creating data structures with some pretty strong invariants. What I did not expect were the difficulties actually providing the evidence that the preconditions hold, and that taking apart the the data into pieces without losing the constraints can become a challenge. In fact, when embarking on programming with SingleLabel, a bunch of proof obligations arise.

So the title is actually misleading (sounds cool nevertheless!) and should read "... no one can take apart losslessly". Of course a non-empty SingleLabel can be taken apart by pattern matching! This article is about propositional facts, and their propagation.

The More data constructor is only accessible if the constraint Equal rest {drop l rest} is given. Last time no evidence was needed, because rest was explicitly known, so the drop type function could be evaluated and the equality checked. But when we just want to join a new head with an unknown tail?
This should still be possible in case that a witness is provided, that testifies that the tail does not contain the label occurring in the new head. Simple enough,

join :: Label a -> v -> SingleLabel tail -> Equal {drop a tail} tail -> SingleLabel {a=v; tail}r
join a v t Eq = {a=v; t}s

should do it. Unfortunately I am running against the wall again. The Eq witness is not accepted by Ωmega, on the grounds that no refinement can be established. The debugging session tomorrow promises to become an adventure!

When this problem is fixed, I'll come back and tell you the story of the lossless decomposition (so that calling join with the results gives us the original back).

Only one of each, please!

2007-12-07T12:40:00.000-08:00

Must be all those sleepless nights (no, I do not want to blame my 6 month old daughter) that light the fire of creativity sometimes...

Two nights ago I had this marvelous idea: how to say that a list is indeed a set. Dear reader, if you do not like maths, please go home now. I am in the happy state of a half bottle of Shiraz and only want people around who share my interests!

Okay let's come to the point. As you probably know, Ωmega provides a Row kind, it is a classifier for associations at the type level.

The shorthand notation {`a=Int, `b=Char}r can express a record where a component labelled with `a contains values of type Int while under the key `b we can store Chars. This is probably boring stuff if you already understand extensible records.

Now let's descend to the value plane. A value can have a type SingleLabel {`a=Int, `b=Char}r when we define following datatype:

data SingleLabel :: Row Tag * ~> * where
None :: SingleLabel RNil
More :: Label l -> t -> SingleLabel rest -> SingleLabel {l=t;rest}r
deriving Record(s)

As usual we have two data constructors, one for the empty record and one for augmenting an existing one. The "deriving" clause just tells Ωmega to enable the following syntactic sugar for None and More: More `lab 42 None === {`lab=42}s, nothing exciting.

But no one can hinder us to define a record value with repeated identical keys: {`a=25, `a="42"}s is a perfectly legal value of type {`a=Int, `a=[Char]}s but it really is incompatible with our aim of defining a one-to-one correspondence between labels and values.

Now enters my cunning idea: using a constraint, we can restrict the tail of the list to not contain a key we are about to add. Constraints are much like Haskell's type classes, but they are less ad-hoc and mirror propositional facts (properties). The new definition could look like this:

data SingleLabel :: Row Tag * ~> * where
None :: SingleLabel RNil
More :: Equal rest {drop l rest} => Label l -> t -> SingleLabel rest ->
SingleLabel {l=t;rest}r
deriving Record(s)

We have defined following semantics: Under the restriction that dropping the tag l from the tail does not change it at all (a fixpoint!), we can construct an augmented list. We have almost reached our self imposed objective: it only remains to provide a suitable definition for drop!

Now, Ωmega helps us in this respect too (but not entirely so for Tags), as we can define functions on types (or kinds for that matter). We can do it this way:

drop :: Tag ~> Row Tag * ~> Row Tag *
{drop o RNil} = RNil
{drop `a (RCons `a v r)} = {drop `a r}
{drop `b (RCons `b v r)} = {drop `b r}
{drop `b (RCons `a v r)} = RCons `a v {drop `b r}
{drop `a (RCons `b v r)} = RCons `b v {drop `a r}

This should be enough for demonstration purposes. (We get a quadratic blowup with increasing number of desired labels, since we have to write our definition in an inductively sequential fashion).

With all of this in place we can give a whirl to our SingleLabel datatype:

prompt> {`a=42}s

--> {`a=42}s :: SingleLabel {`a=Int}r

prompt> {`a=42,`b='K'}s

--> {`a=42,`b='K'}s :: SingleLabel {`a=Int,`b=Char}r

prompt> {`a=42,`a='K'}s

--- Type error: cannot find a solution for equation {`a=Char}r == {}r

We can now go to bed with the feeling of having accomplished a thing...

PS: Ωmega in its last released form cannot compile the code presented here. You will need some patches to get various bugs ironed out. With some luck this all will work out of the box in the next release!

Trendy Topics

2007-11-08T13:23:00.000-08:00

There seem to be two important trends in the Haskell universe and I must admit, that I do not want to stay away from them either...

The first one is the exploration of category-theoretic concepts and their showing-off in the blogosphere. Generalizations of monads or the category type class are just two recent picks from the bottomless supply of ideas.
The second trend is more subtle and one has to dive into the recent ICFP papers to perceive it. I have already mentioned the Unimo framework, which guarantees the monad laws and allows to represent the monadic computation as a pure data structure which is then run by recursive analysis. Wouter Swierstra et al. introduced another concept to capture monads (also strongly resembling the free monad) and they have improved testing ability on their minds when doing this. The third paper that comes to my mind is about speeding up arrow computations by analysis and optimization of a data structure closely resembling arrows.

So I am not in bad company announcing that I am preparing a paper about thrists which are the moral equivalents of free categories. The rest of this article gives an appetizer about thrists.

data Thrist :: (* -> * -> *) -> * -> * -> * where
Nil :: Thrist p a a
Cons :: p a b -> Thrist p b c -> Thrist p a c

The definition makes it clear that Thrist is a GADT (I use the Haskell way of defining a GADT here, the paper will use the slightly different Ωmega syntax) and it is a curious mixture of listness and threadedness (this is the reason for its name). The types of the thrist elements must match up in a certain way, resembling function composition.
Indeed, instead of composing functions, we can put them into a thrist:

Cons ord $ Cons chr Nil

gives us an arrow thrist (Thrist (->) Char Char) only showing the start and end types, with the internal types abstracted away existentially.
Of course we have to supply an interpreter for this data structure to get the functionality (the semantics) of function composition, but this easy exercise is left to you.

But... What do thrists buy us?
Two very important things:

Unlike function composition, we can take the thrist apart, analyse and transform it, and
a vast field opens up with the first (p) parameter to the Thrist. It can be the pair constructor (,) or the LE (less-or-equal) proposition, there are many sensible instantiations -- especially with two-parameter user-defined GADTs.

Finally, the category-theoretic twist: think of the parameter p as the morphisms of a category C (with C's objects being the morphisms' domains and ranges) then Thrist p is essentially the free category of C, often written as C*.

I hope you enjoyed reading this in the same way as me writing it!

Traumzimmer

2007-10-29T07:27:00.000-07:00

Some people know, but many more don't, that my wife Patricia is an artist specializing in designing babies' or children's rooms. Back in Brazil she even made a living out of this.
After some creative pause and the arrival of our baby (she has also decorated her space) it is time to get back to work. I am very proud of what she is accomplishing, so I'd love to show you some pieces at Traumzimmer. The website is pretty new, but taking shape slowly, and documents the progress of the firm she opened with another brazilian girl.
Enjoy!

Comonads

2007-09-12T16:50:00.000-07:00

Slowly recovering from vacation-induced ignorance, today I printed out some interesting papers about type-preserving compilation, plans for type-level functions in GHC and dataflow implementations using comonads. Another one about Hoare Type Systems remained on my screen, too heavy for me, a.t.m.
So I am wrapping my head around category theory again. Somehow all these topics seems to interact, and I continuously am trying to fit them into my Thrist framework. Today I tried to implement a Comonad to Thrist adapter (in my mind at least, no code written yet).

Vacation

2007-08-30T04:17:00.000-07:00

I am in jetlag mode. People keep telling that travelling from west to east worsens it. Maybe this is the reason that I am not very motivated to do my day-work. But possibly it is just the memories of the last four weeks.

Brazil.

My wife comes from the north-eastern part of the country, namely Recife-Pernambuco, so we had the best possible guide for our travelling explorations.

just to name a few. Sleeping deep and long, very good food (beef, excellent fish and astonishingly, cheap and tasty sushi) the most important ingredients for a relaxing time away from home. Countless hours with members of an immensely great family and long evenings with friends, guitars, caipirinha.
Should last for some months from now. Thanks to all who made it sweet.

Taming PSNormalizer

2007-07-28T10:20:00.000-07:00

For distilling a PDF on the Mac I had to unlearn almost everything. Or at least I have to use some more tools, while ignoring others. What I shall write down now is the product of one night of intensive research by googling with lots of trial-and-error.

So, producing the .ps with lout was easy and just like on Solaris. But there is no Distiller in my setup, instead I normally use Preview.app. Double-clicking on the .ps file in the Finder usually is sufficient. Not this time, though, because the Latin Modern fonts were missing, and Preview.app substitutes Courier for them. Clearly a suboptimal solution.
Dropping the .pfb and .afm files into the Fonts folder (personal or system Libraries/Fonts) only had the effect of locking up Preview.app with every job. This is what other people also report in support forums. I removed the font files again.
The solution must be including the font into the .ps file. There is a small utility called includeres in the MacPorts psutils package. Unfortunately the script did not run out of the box, I had to edit it to invoke perl by full pathname (#!/opt/local/bin/perl). But then I had to symlink LMRoman9-Regular to lmr9.pfb for this approach to work. Opening the resultant pimped up .ps file with Preview.app resulted in the well-known hangup. Hmmm, .pfb is apparently not palatable for Preview.app.

So I began digging deeper. It looked like there is a PSNormalizer entry in the /tmp/ directory. It seems to be the bastard child of Distiller, licensed to Apple from Adobe. I figured it also has a command-line interface pstopdf too. PSNormalizer seems to be a private system framework, with a certain directory structure. After finding it on my HD, I could examine its contents. There is a Resource/ directory with fonts/ in it. I dropped my .pfb there. Hangup. At least I knew now that I am on the right path. PSNormalizer looks for fonts in Resource/fonts/ and after that in ~/Library/Fonts and the global /Library/Fonts.
Resource/fonts/ has two files in it, one of them being Courier. Looking at the dump, it seemed very close to .pfb files, but all ascii. It must be a .pfa file! From here it was easier to proceed:

grabbing a pfb2pfa converter from CTAN (part of ps2mf)
with a small script converting all .pfbs to .pfas
dropping these into Resource/fonts/
redistilling

This time it worked! But it is tiresome to invoke Preview.app all the time using the mouse, so I am using pstopdf now, which is a perfect substitute for Distiller. Also I have my .pfas in /Library/Fonts/, so everybody on that Mac has access to them.

Nevertheless I could relax at this point, and do some experimentation. Here are some things I stumbled upon:

PSNormalizer/Startup/ can contain arbitrary .ps files that are run before each distillation job starts. This can be useful for customization.
Resource/startupNORM.ps contains some interesting code and can probably also be modified.
Using includeres with .pfa fonts also works.
The PSRESOURCEPATH environment variable does not seen to affect pstopdf.
pstopdf has two brothers, pstopnm and pstops. I still have to find out what they are good for.
And there is more: ps2epsi and many other commands starting with "ps" come from the Ghostscript MacPorts package.

All in all, I feel much better about the PDF-workflow on the Mac now :-)

Taming Distiller

2007-07-27T18:36:00.000-07:00

I happen to use a Mac. This makes me pretty comfortable with viewing and creating PDF files. My favourite typesetting program, lout, can also output PDF, but it is rather limited, especially when it comes to graphics. This is why I normally go the longer (but recommended) route via PostScript files.

Today lout v3.36 arrived, and I gave it a try:
Building on Solaris was a breeze, as always. Thirsting for a challenge, I downloaded some Latin Modern fonts (refined versions of Knuth's original Computer Modern fonts) and tried to get them running under lout.

It was not easy.

Not being a font expert, first I was overwhelmed by the .afm .pfb files from the CTAN site. I did not know where to put them, so that I simply dropped them beside my .lout file. It did not work, of course. I had to pass "-F ." to lout to find them. (Lout is only interested in .afm, font metrics, files.)
I also had to prepare a @FontDef database, but there were enough examples in the web.
After a lot of googling I figured out the PSRESOURCEPATH environment variable. It must have this format: "path1:path2::" and is used for searching diverse PostScript resources. Using it, I could stash my fonts away in a different location.

There is a handy utility I stumbled upon, makepsres, which built up the font inventory inside my newly created /home/ggreif/psres folder. I desisted to fill in the mandatory PSres.upr file inside it after three trials in vain.

So, lout was happy with lm.ld and "-F /home/ggreif/psres" and produced a pretty .ps for me.
Distiller, on the other hand followed PSRESOURCEPATH and PSres.upr, converting the .ps into a .pdf. So far, so good. (There was still this pesky "unsetenv XUSERFILESEARCHPATH" to do, but I shall spare the details.)

After understanding the Solaris workflow, I had some hope to successfully repeat this experiment on my Mac too. But that is a story for another day...

Endo at end?

2007-07-23T05:57:00.000-07:00

The ICFP contest has ended three hours ago. In his blog, Johan is optimistic that Endo can be saved. Looking at the scoreboard's 16+ rankings, this seems unlikely :-/

DylanHackers (the team I contributed to in some previous contests) did not do so well this time. I dropped off in the first night, reaching a stack overflow error when parsing the supplied DNA's first pattern:

13351PCCPFFP
13361PIIPICP
13371PIIPIIP
Stack space overflow: current size 8388608 bytes.
Use `+RTS -Ksize' to increase it.
13381PFFPCCP
13391PIIPICP
13401PIPIIPF
13411PIIPIIP
13421PIIPICP

Well, at least I managed to parse 1% of the DNA! (The number in front of the RNA fragment signifies the byte position where it comes from the DNA.) Ωmega, being an interpreter on top of Haskell has no efficient means of controlling stack usage, which is consumed quickly, even if my parser was written in tail-recursive style. Hmmm. I did not even bother to submit the low hanging prefix that was published in the task itself. I am really curious if any team reached a 50%+ survival probability.

In any case the task was really hard this year. On the positive side I saved myself from some frustration and had a wonderful weekend with my family. We celebrated my son's 11th birthday in a game factory and my brother visited us with wife and his two children. Sometimes you win by losing...

Ωmega Tutorial Posted

2007-07-17T13:54:00.000-07:00

Finally there is a 67 page Ωmega introductory text. Well, actually it is a delta to Haskell, so the audience is Haskell (and perhaps OCaml) savvy folk, but at least one does not need to collect all the information from the scattered papers.
From the first glance I had at it, it describes all the new features neatly, although sometimes the old "#n" notation sneaks in (the new notation is 1v and 1t, for values resp. types).

I guess this is a live document and Tim together with Nathan will keep it current, cleaning up the few anachronisms as they go.

I am using Ωmega more than a year now, and can only say that it is a remarkably powerful system. (I shall come back with a more detailed and subjective analysis some other day.)
The thing that fascinates me most, however, is the astonishing stability of this product. Being essentially a one-man show, Tim corrected dozens of errors, that I mailed him, or filed in the new issue tracker at googlecode. It is really hard to find any more serious bugs in the core system. This is also a consequence of Ωmega being written in Haskell, so it inherits all of Haskell's blessings. I wish I were a good Haskell hacker, then I would fix the bugs myself :-/

The only drawback at the moment is that it is an interpreter, and this fact makes it a bit slow. So a performant version is needed. Then one can think of bootstrapping the interpreter/compiler. Ωmega written in itself would definitely be the dream of formal methods coming true!

A Compiler with a Good Clang

2007-07-16T02:59:00.000-07:00

You probably already know, Apple has open-sourced its new front-end for C-like languages, that has been in development internally for months. Its name is "clang" which is probably a contraction of C LANGuage. This name might be related to the email handle of one of its creators Chris Lattner, who is clattner at apple. Its other father is Steve Naroff, who introduced it at the LLVM-developers' meeting back in May.

Of course, nobody writes a C compiler in six months, so this product is not mature yet, its main omission being structure handling, and there are many loose ends to wrap up. Being open source now, with a developer-friendly BSD license, I offered to fill in a bit-sized hole in the implementation, and chose _Complex multiplication and comparison operators. The parsing part was already done, AST handling too, only code generation to LLVM IR remaining to be done. I used the analogy principle (addition was already there) and came up with a patch in 30 minutes. After some IRC conversation with Chris and another round of tweaks, I got green light and checked in my changes accompanied with a test. That's it. This is open source at work. Trust, ease of implementation (I barely wrote 30 lines, because of the support for assembling fragments of LLVM is pretty good) plus rigorous code review and finally testcases. There is not much room for bugs and malicious code to hide out.

It has been a pleasurable experience. I know C++ code that is a nightmare in comparison. If the fathers of clang continue as they started and let the many external contributors fill in the missing pieces, this compiler will definitely be one with a good "Klang" (sound, in German).

Writing Papers is Hard

2007-07-15T17:06:00.000-07:00

It is some months ago that I started with my paper

"Thrists: Dominoes of Data",

which aims at generalizing function composition and in my opinion is a nice vehicle for other programming tasks too.
It has only nine pages, and the really troublesome areas are still in front:

writing the references
fine-tuning the text flow
stylistic enhancements

I would like to publish it for some serious conference or journal of course, ASAP. This means I have to respect their style guide, which can be non-trivial, as they only provide LaTeX stationery, and I am using lout for my typesetting. Looks like I have to transcribe them :-(

Anyway, today finally I arrived at a point that I can offer an early draft to the interested public.
The feedback so far appears positive, which makes me spin. Thanks to all who took the trouble of reading through a very rough draft.

Overall, one can put an infinite amount of work and time into such a short paper, which makes me marvelling at people who seem to produce high-quality papers at a seemingly monthly rate. They must have some secret trick I do not know -- yet!

Heating up for ICFP Contest

2007-07-13T10:43:00.000-07:00

Today I started to analyze the ICFP Contest organizers' blog in detail. The pictures remind me of MiB, the commentaries suggest that some fictive language must be decoded.
Fortunately I speak some and learned even more when young, so maybe this is a advantage, we will see.
Anyway, I shall register as a team captain again, maybe I can organize a team here locally. Last year's experience has shown that the contest does not need a geographically concentrated team, but it surely helps.

After last year's pretty good result (place #101) we have a record to break!

The HaL2 Harvest

2007-07-11T08:38:00.000-07:00

Yesterday's Haskell in Leipzig was an interesting and entertaining mix of demonstrations of Haskell programming in real life. It was definitely worth my long travel.
The organization of the meeting was excellent, the venue somewhat esoteric for a conference, but could not have been selected better.
Of course I preferred some talks over the others, all in all I returned with some new clues.

The best thing is that the talks and subsequent discussions have been videotaped and should show up on Youtube soon. This way everybody can participate.

Personally I managed to seed some attendants with an early draft of my paper on thrists, I am really curious and anxious about the feedback I get. Already in the car I established a connection between categories and thrists, objects being Ωmega's type level entities and morphisms being the values that populate the first parameter to the thrist. It was very helpful to have a student in my car whom I could abuse as an idea-sink :-). On the return (me being really sleepy) he payed it back.
At the meeting this idea got consolidated in my discussion to Mr. Zirnstein, who suggested free categories. I am already in the process of integrating this feedback into the paper.

More on Tail Merging

2007-07-09T15:01:00.000-07:00

In an earlier post I speculated that factoring out Cat combinators other than Dup would just be a matter of copy-and-paste (I used the euphemism boilerplate back then). It came to me as a shocking revelation that the Ωmega interpreter did not agree. It asserted that

type _d is equated to type _e

which is inacceptable. The error message was not exactly like this, but very similar. It took me some time to understand it. First I wrote an even shorter function than the one-liner that caused the error. It only happened when I recombined the two shortened If legs (that is, after removing a Print from each).
This piqued my curiosity and I made an excursion into Ωmega's interactive typecheck mode, just to discover that the two If legs ended with different stack configurations!

This put me over the top, and I could come up with an example immediately:

If [Push 42, Print] [Push True, Print]

is a case where the Print cannot be removed without violating the invariant that the exit stack configurations at both If legs must be the same. In this case the yes-leg would have an Int at TOS and the no-leg a Bool. Since I have to cater for the general case, the removal of a Print is unsound. Ωmega discovered this.

There are two lessons to be learned from this incident, namely:

If you see a mysterious error (message), simply provoke the same with a smaller program, and
Ωmega's error messages need to be improved in a way that somehow the piece of code is indicated that gives rise to the erroneous types.

In the meantime I have an idea how to find a way to remove that Print anyway. The key is abstract interpretation of the two If legs, to construct a proof that the stacks have the same shape immediately before the Print. Given this proof the typechecker can be persuaded to allow the recombination of the shortened legs. But to implement this idea there are many more hours to be spent hacking. It will surely be worth blogging about.

The Grief with "Greif"

2007-07-08T15:45:00.000-07:00

Are you American? So do you see a difference in the two words of the title beginning with G?
If not, you are in good company. Let me explain...

My family name (last name) is Greif, it is pronounced with a vowel like in Friday. It is German, and means griffin.

I first noted that the spelling of my name is causing difficulties for Americans, after my colleagues returned from a WWDC in the late '90es. When they mentioned their affiliation while talking to a Metrowerks compiler engineer, he responded something like

"we know a guy from the same shop, his name is Gabor Grief."

They surely remembered my name because back then I bombarded them with many obscure C++ template compilation bug reports, actually causing them a considerable amount of grief. (They were really good in fixing them.)

Since then this is happening regularly. And I always explain patiently. Now, thanks to this blog, it will suffice to provide an URL :-)

As an aside, after spending my vacation at Fuerteventura in 2001, back on the airport I bought a bottle of Lanzarote wine with the name El Grifo. I have sworn to myself to only open it when I get a son. It took 6 years, and Helena came. The wine still tasted good, we enjoyed it with the family.

Tail Merging in Ωmega

2007-07-07T16:18:00.000-07:00

Today finally I got around improving my Cat-like language optimizer with a new twist:
I can finally factor out common instructions from the end of the two If legs and prepend them to the If's continuation. This wouldn't be an interesting achievement if it wouldn't be written in Ωmega's type-pedantic fragment. To wit:

tailMerge False [If [Dup]l [Dup]l, Print]l (revThrist' [Dup]l) (revThrist' [Dup]l) [Print]l
becomes: [(PopN 1v),Dup,Print]l : forall a (b:Prod *0).Thrist Cat [Bool,a; b]sh [a; b]sh

If you think the above lines are in Chinese, you can stop now. If you discover that the If has completely been eliminated and replaced by popping a boolean and duplicating the TOS, then you are pretty good in reading obscure code.
The funny thing is that all the types of values that are on the stack are painstakingly tracked, and the transformation is automatically type correct in Cat because it is type checked in the metalanguage.

I am sure that similar transformations have been proven type correct (and thus pretty correct) before, however I would like to know whether this particular optimization has been already formalized using expressive types.

The big surprise for me was the fact that writing down the transformation only needed a dozen lines of code, support functions included. Of course, my proof of concept only matches on Dup instructions, but the rest is basically boilerplate.

The second surprise is, that so far I did not need a single theorem declaration, an indication that either I am still in very shallow waters regarding the power of Ωmega's typechecker, or my Thrist construction is so clever that it provides enough type hints to the narrowing engine to deduce all types.

I am in the process of writing a paper on all this, and - as always - need some encouragement. Tail merging will definitely belong to the beef part of it.

Haskell in Leipzig

2007-07-06T15:38:00.000-07:00

Next Tuesday I shall visit HaL2 in the beautiful city of Leipzig, again. Back in December I already attended, and it has proven to be an excellent platform for encountering members of the functional programming community. Living in a university city myself, I sent a mail to a local Haskell tutor and offered to give a lift to interested people.

To my amazement a student did answer my message and so I won't drive the three hours alone (plus another three backward). It will be a long day, and the last time when I attended with a colleague it has proven very good to have somebody to talk to.

And I expect there will be plenty to talk about. Johan Jeuring will give a short talk, and though I do not expect him to chat about the ICFP contest's secrets, he well may give hints :-)

The functional programming community is sadly very weak in Germany. All the good people fled the country and are doing research in anglophile countries (UK, US, even Singapore) only few universities are actively supporting FP, such as Aachen and Bonn. In any case some serious networking is needed to spread the acceptance of Haskell in this part of the World. Many professionals would love to do a Haskell job, but there is simply no possibility. Small companies are the most likely ones to venture in the Haskell experiment, the big ones are extremely cautious and full of fear. Security relevant applications could be covered first, and when the productivity and maintainability gains are becoming obvious FP could expand into the classical areas of machine steering and automotive software. Germany has a lot of these.

I often use the metaphor of "building pyramids with toothpicks" when some gigantic project is started in Java or (horror!) C++. Who has never written a line of Haskell or Dylan code will never understand this metaphor. Pity.

So what can we do? I am trying to help others who bring people together. We badly need self-confidence and some pioneering folks who stand up and say: "let's do this task in FP for half the cost and 1/10th of the bugs of the conventional approach, even if it takes the same time in the beginning". Who shoots first?

Committed to LLVM

2007-07-05T04:38:00.000-07:00

Yesterday I got accepted to the inner circle of LLVM developers by becoming a committer. For now I have very humble plans, such as periodically plowing through the sources and sanitizing a bit here and there. This may change to a more active role, but probably not in the form of contributing to llvm-core.

At least version 2.0 already does contain some stuff from me (improved memory efficiency).

My first contact to LLVM happened when I started a new backend for the d2c compiler. I found out that the Dylan language and LLVM would be a good match, and that d2c was modular enough to nicely marry these two worlds. I did produce some llvm output, but got distracted soon and the project never became functional. Ah well...

How to start?

2007-07-04T09:58:00.000-07:00

There has been quite a lot movement in my life in the last 2 years, which culminated almost 3 weeks ago with the birth of my daughter Helena. (Needless to say that I am the proudest father in the world :-)
So where I am standing now? I have a pretty happy family life, I am feeling the rewards of my professional career and my hobbies give me the self esteem that the researcher is still alive deep inside.

And what is missing? I miss the time to do more of all this. I also missed a way of articulating my thoughts, sketching my dreams.

This blog could fill in the latter gap (at the cost of losing even more time ?!?).
Sometimes I need external impulse to drive me in a certain direction. What I put on these pages may motivate others to demand that I implement a cool idea or think harder about some problem.

Even if it just remains a reminder to self, it may be worth it.