Wednesday, December 19, 2012

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

Tuesday, September 18, 2012

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