Thursday, August 7, 2014

First Programming with my Daughter

Today I had a short programming session with my 7 year old. I had shown her earlier what a list is and she came back several times already to show her "more lists".
So this time I thought we could do something more interesting. A letter-changing game! I fired up GHCi and entered:

Prelude⟩ let satz = "Leleka hat Kacke in der Hose"
Prelude⟩ print satz
"Leleka hat Kacke in der Hose"


She loved it so far. Fun is the strongest motivator to learn for kids…

Then came the changer for letters:

Prelude⟩ let tausch = \x → case x of {'L' → 'K'; 'e' → 'i'; 'i' → 'u'; 'u' → 'e'; x → x }


Then I applied it on the phrase defined earlier:

Prelude⟩ map tausch satz
"Kilika hat Kacki un dir Hosi"


This did it. She kept repeating the transformed sentence for an hour, giggling. I tried to explain to her what we did just now, but I guess I'll wait till next time to make her repeat this exercise.

Thursday, July 31, 2014

Rank-2 PHOAS

Lately I've been experimenting with finally-tagless (typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the parametric higher-order abstract syntax (PHOAS) technique to obtain variable bindings that are automatically well-scoped.
I arrived at this formulation:

class LC rep where
  var :: p → rep
  lam :: (forall p . p → rep) → rep


(I am ignoring applications as they are not important for making my point.)
As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the p type variable as the second class parameter and the rank-2 forall would appear from "outside".
But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:

instance LC ([String] → String) where
  var = ??? -- const "VAR"
  lam f = \supply → ...


It turns out that implementing var is only possible by giving a constant result, and for lam I am in trouble, because I cannot call f as it expects a polymorphic argument. Both problems are due to the fact that p is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?
Thinking about it I came up with the idea of giving each instance a way to constrain the p variable as it fits. So I changed class LC such:

class LC rep where
  type Restricted rep p :: Constraint
  var :: Restricted rep p ⇒ p → rep
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


Now my instance can pick the restriction as it fits:

instance LC ([String] → String) where
  type Restricted ([String] → String) p = ([String] → String) ~ p
  var = id
  lam f = \supply → ...


As you see I chose the restriction to be type equality which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in p becomes easy now.

  lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f $ const n) ns

Let's try it out! But in order to do that we need an instance of Show for name supplies. This could be one:

instance Show ([String] → String) where
  show f = f $ map (('v':) . show) [0..]


Now we can interpret a lambda term as a name supply.

*Main› lam (\x → lam $ \y → var x) :: [String] → String
\v0.\v1.v0


It works™ :-)

But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement var as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:

class LC rep where
  type Restricted rep p :: Constraint
  type Restricted rep p = rep ~ p
  var :: Restricted rep p ⇒ p → rep
  default var :: rep ~ p ⇒ p → rep
  var = id
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


I like it so far.

PS: Here are the prerequisites if you want to compile the above yourself:

{-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-}

import GHC.Exts

Sunday, January 12, 2014

Testing LaTeX with MathJax

$3_{5}$ $$42^{25}$$
extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"],
Does not work

But this:
<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>
<script type='math/tex; mode=display'>   \{ 0, 1, 2 \} </script>
Results in something pretty:

Monday, September 2, 2013

Now it's evident — totally!

In one of my posts about logics I have shown that a proof of a true proposition consists of constructing a function from ⊤ (truth) to an inhabitant of that proposition (interpreted as a type).

Dually, one would hope, we must construct a function between false propositions and ⊥ (bottom, the empty set).

The big question is: How? There appear to be many functions into the empty set. These surely cannot mean to be proofs!

There is a catch: totality. For every possible input we are obliged to provide a well-defined, deterministic result. A hard job when the target set is empty!

On the other hand it is easy enough for positive proofs: (considering the finite case...) say, we seek a proof of the Bool proposition. Bool has two inhabitants, so the function space from ⊤ (single inhabitant) to Bool must have 21 of them. Here is one:

provebool () = True

(Do you find the other one?)

But for negative proofs, it isn't really obvious how to do it. Since refutable propositions (allegedly) have no inhabitants, how do we write a pattern-matching function between them?

But remember, in the finite proof case our arrows had nm inhabitants, picking any one of these constituted a valid proof.

For the uninhabited case such a way of counting gives us a clue: 00 can be interpreted as 1! And this is the key, we need to do pattern matching with no patterns to get that inhabitant:

refutation = \case of {}

When this function is total, we have our sought-for unique proof. And for actual negative proofs it evidently is!

Tuesday, August 20, 2013

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.

Monday, August 19, 2013

Compiling GHC on RHEL6

Compared to building GHC on RHEL5 this is a breeze.

git is in the installation — check
perl bootcheck
./configurebreaks, 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 -j14check

Then I dared running the test suite:

make testcheck

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 installcheck

nothing unexpected here.

Have fun with GHC on RHEL6!

Saturday, August 10, 2013

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.