Recently Implemented Syntax Extensions

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

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:

1. the treatment of patterns that are values was missing,
2. the handwavy argument how the proposition corresponding to the condition is encoded,
3. that the dependent sum binder introduced two variables (where lambdas only introduce one),
4. 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

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:

1. the left-associate thrist (usually holding the already visited portion),
2. the focus element e,
3. 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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. re-merged the backed out revision, postponing conflicts;
2. saved the diff away and reverted the repository;
3. wrote a small awk script to massage the hunks in the diff to get a new patch;
4. fired up emacs with the patch and applied each hunk after thorough review (and seldom with minor changes);
5. some hunks are not ready to go in yet as they do not qualify as refactoring, these are kept for later;
6. 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

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

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

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?