Old Cabal Subhell

Sometimes I have a cabal that is too old for generating up-to-date boilerplate files for package installs, so I have to install a new cabal-install. But unfortunately I run into the same problem when installing the HTTP package, which is needed for cabal itself. So I am in a (pun totally intended, as you'll see later on) catch-22, and each time I feel being lost completely.

But there is a cure to this particular problem:

create a modified

mv dist/build/autogen/Paths_HTTP.hs dist/build

and patch it with

$ diff -u dist/build/autogen/Paths_HTTP.hs dist/build
--- dist/build/autogen/Paths_HTTP.hs 2013-02-27 20:07:01.437225000 +0100
+++ dist/build/Paths_HTTP.hs 2013-02-27 20:20:36.735526000 +0100
@@ -6,6 +6,7 @@

import Data.Version (Version(..))
import System.Environment (getEnv)
+import Control.Exception

version :: Version
version = Version {versionBranch = [4000,2,8], versionTags = []}
@@ -17,11 +18,14 @@
datadir = "/home/ggreif/share/HTTP-4000.2.8"
libexecdir = "/home/ggreif/libexec"

+hardCoded :: FilePath -> IOException -> IO FilePath
+hardCoded dir = const $ return dir
+
getBinDir, getLibDir, getDataDir, getLibexecDir :: IO FilePath
-getBinDir = catch (getEnv "HTTP_bindir") (\_ -> return bindir)
-getLibDir = catch (getEnv "HTTP_libdir") (\_ -> return libdir)
-getDataDir = catch (getEnv "HTTP_datadir") (\_ -> return datadir)
-getLibexecDir = catch (getEnv "HTTP_libexecdir") (\_ -> return libexecdir)
+getBinDir = catch (getEnv "HTTP_bindir") (hardCoded bindir)
+getLibDir = catch (getEnv "HTTP_libdir") (hardCoded libdir)
+getDataDir = catch (getEnv "HTTP_datadir") (hardCoded datadir)
+getLibexecDir = catch (getEnv "HTTP_libexecdir") (hardCoded libexecdir)

getDataFileName :: FilePath -> IO FilePath
getDataFileName name = do


This file is then preferably found by GHC and all is okay. Incidentally I already employed this trick in the past, but forgot about the details so I had to reinvent it again.

After escaping this particular subhell of cabal I came up with this blog post in order to not lose my way in the future. Hopefully it helps you too.

Decidable equality

Trailing Richard Eisenberg's blog post I've been triggered to recollect what I have read about the matter so far. Turns out that I was about 17 when I first came into contact with the concept. After my brother hinted to me a month ago that he is reading "Gödel, Escher, Bach", I grabbed my own copy from my bookshelf and quickly found the page about the fractal nature of provable propositions and the true-false divide. I have scanned it and showing it below.

What is the connection to decidable equality? I believe this illustration shows it:

I have depicted T (truth, top, any nullary constructor, e.g. ()) at the north pole, and bottom (false, ⊥) at the south pole. The way or reasoning on the north hemisphere is to transport truth into a type, i.e. construct a function of type ()→P, where P is the proposition we want to prove in Curry-Howard encoding. As the figure shows we may have a finite number of stops on our way. We can note that a function of type ()→P is isomorphic to P, so simply constructing an object of type P suffices.

Dually, proving that a proposition is false, we have to construct a path to bottom from Q, again possibly via a finite number of stops. Since (Q→⊥) cannot be simplified we really have to construct functions here.

The equator divides true from false and thus separates the duals.

Since each proof (when computable in finite time) will either result in something from the blue or red island, the type for decidable equality must be Either (a :~: b) ((a :~: b) -> Void).

Thrist sightings

It's been a bit quiet recently, but not inactive. Edward Kmett has adopted the name and the concept in two of his libraries. Of course the concept is much older than the name, being a path in some category.

If you look carefully, in the middle of his ICFP '12 keynote Conor McBride derives thrists (he keeps the name List in his development) and they may also appear in the JFP article where they are named Path.

Only with the advent of GADTs and user defined kinds in systems like Ωmega, SHE and Agda the concept of threading types begins to blossom. Since the release of GHC v7.6.1 the most popular Haskell compiler also supports kind polymorphism. This prompted me to re-spin the thrist package to take advantage of GHC's new feature.

Have fun,

    Gabor

Showing Thrists Revisited

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

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

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

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