Verschiedenes

Mein Vater wäre morgen 72 geworden. Ich habe mich schon lange daran gewöhnt, daß er nicht da ist, dennoch habe ich ruhige Momente, wo ich mir wünschte ich könnte ihm erzählen was ich so mache.

Er würde es verstehen.

Er sagte mir einmal "Ich hätte es geschafft dich in die Medizin zu bugsieren, wenn ich dort eine Zukunft gesehen hätte." Ich glaube er sah im ganzen medizinischen Komplex keine Zukunft, mit Sicherheit auch im finanziellen Aspekt. Oder er sah einfach keine Perspektive darin, für mich. Auf alle Fälle stand er meinen mathematischen Ambitionen sehr aufgeschlossen gegenüber. Er kaufte mir das Buch das ich immer noch sehr verehre, "A fizika kultúrtörténete" (die Kulturgeschichte der Physik). Ich habe es vor kurzem meinem Sohn auf englisch gekauft.

Das aus meinen Ambitionen nicht wirklich viel wurde, lag wahrscheinlich daran, daß ich in die Informatik gegangen bin ;-)

Aber egal, es macht mir ja viel Spaß, und die beiden Gebiete verzahnen sich ja zusehends. Es gibt einen signifikanten Trend, die Grundlagen der Mathematik auf das Fundament der Typentheorie zu stellen, und somit die Mengenlehre praktisch zu entthrohnen, nach mehr als 100 Jahren Herrschaft.

In einem kleinen Winkel dieses Kriegsschauplatzes mache ich mir selber gedanken. Gestern Abend fuhr ich nach Ansbach, um meine Mutter zu besuchen, und nahm auch Hamster Daniela mit. Ich war wirklich müde geworden nach dem Abendessen, las noch ein Paar Seiten Kategorientheorie und schlief ein. Aber zwischen 2 und 3 wachte ich auf, und ich denke in dem Moment verstand ich, daß meine Idee von Typen als Flächen sich mit den Opetopen vereinbaren lassen, wenn man sich nur in die Kodimension versetzt. Das Stichwort Poincaré-Dualität kommt da auf, was alles erklären könnte.
Ich nahm den Hamster mit runter, wir setzten uns vor die Terrassentür, und der Schein des Vollmondes fiel auf uns. Es war mystisch.

Außerdem arbeite ich an einer Kodierung, so daß etwas gleichwertiges zum Lambda-Kalkül mit Opetopen kodiert werden kann. Mal schauen wie das alles zusammenkommt.

Ich denke mein Vater wäre der einzige aus meinem Umkreis der für solche Gedanken ein wirklich offenes Ohr gehabt hätte, selbst wenn er das meiste gar nicht verstanden hätte. Aber er wäre auf mich manchmal stolz gewesen.

Compiling GHC on RHEL6

Compared to building GHC on RHEL5 this is a breeze.

git is in the installation — check
perl boot — check
./configure — breaks, linker does not find libgmp.so
I built gmp from sources, and installed it into my home directory.

But... it still did not build :-(

As always, Stack Overflow for the win!

Specifying
setenv LIBRARY_PATH $HOME/lib
did the trick.

For good measure I also added
--with-gmp-libraries=$HOME/lib --with-gmp-includes=$HOME/include
to the configure line, but this might be redundant?

(Another thought, find seems to reveal some  libgmp.so under /usr, I might point it there.)

So, finally,

./configure ... — check

The part that involves building was the pleasure part:

nice make -j14 — check

Then I dared running the test suite:

make test — check

This step takes its time, as it is not parallelizable.

There is only one drop of bitterness, namely the stage2 compiler does not run on RHEL5. But that is something I did not expect, actually.

make install — check

nothing unexpected here.

Have fun with GHC on RHEL6!

Proudly presenting the »nopetope«!

(This is is jotted down, raw posting, that may never get finished. I am publishing it anyway, as it pretty much reflects my current mood.)

I am about to do some research with coverings of trees, and it was only natural to look at Baez-Dolan metatrees and the corresponding notion of opetopes. The paper contains a famous 5-minute definition and it is a brain teaser worth reading. They introduce trees and nestings (actually two sides of the same coin) and their superposition, called a constellation, which has to follow some rules, but drawing spheres is a creative process.

Then there are zooms which connect constellations as long as the left nesting and the right tree are morally identical.

My lambda graphs are basically search trees and a nesting would add the operational notion of evaluation. Since we can freely choose our evaluation strategy (confluence?), the latter corresponds to a nesting. It remains to find out what the degenerate zooms are under this aspect.

I am just reading the "Polynomial functors and opetopes" paper (http://arxiv.org/pdf/0706.1033.pdf) and it asserts that it's starting constellation is a one leafed tree: But I wonder if this is fundamental, and since leaves are stripped by zooms, any number will do.
So I'll suggest starting with zero leaves, and calling the resulting zoom complex(es) the nopetopes. This might be the first mathematical term I have coined :-)

For the mathematically-challenged, a nopetope is just a lollipop wrapped in cellophane, while an opetope is the two-stick version thereof.

It is a funny coincidence that "one" and "ope-" contain the same vocals. Going on, we could also have twopetopes and thropetopes, fouretopes etc. But I doubt these are significant in any way.

And now back to the paper and then to an Ωmega implementation of nopetopes...

PS: while writing this my imagination went though... Are trees and nestings compatible with the famous correspondences energy-mass, wave-particle of physics? Looks like I have to start some more research.

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...