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?