What Ωmega has joined, no one can take apart

Some days ago I became enthusiastic about creating data structures with some pretty strong invariants. What I did not expect were the difficulties actually providing the evidence that the preconditions hold, and that taking apart the the data into pieces without losing the constraints can become a challenge. In fact, when embarking on programming with SingleLabel, a bunch of proof obligations arise.

So the title is actually misleading (sounds cool nevertheless!) and should read "... no one can take apart losslessly". Of course a non-empty SingleLabel can be taken apart by pattern matching! This article is about propositional facts, and their propagation.

The More data constructor is only accessible if the constraint Equal rest {drop l rest} is given. Last time no evidence was needed, because rest was explicitly known, so the drop type function could be evaluated and the equality checked. But when we just want to join a new head with an unknown tail?
This should still be possible in case that a witness is provided, that testifies that the tail does not contain the label occurring in the new head. Simple enough,

join :: Label a -> v -> SingleLabel tail -> Equal {drop a tail} tail -> SingleLabel {a=v; tail}r
join a v t Eq = {a=v; t}s

should do it. Unfortunately I am running against the wall again. The Eq witness is not accepted by Ωmega, on the grounds that no refinement can be established. The debugging session tomorrow promises to become an adventure!

When this problem is fixed, I'll come back and tell you the story of the lossless decomposition (so that calling join with the results gives us the original back).

Only one of each, please!

Must be all those sleepless nights (no, I do not want to blame my 6 month old daughter) that light the fire of creativity sometimes...

Two nights ago I had this marvelous idea: how to say that a list is indeed a set. Dear reader, if you do not like maths, please go home now. I am in the happy state of a half bottle of Shiraz and only want people around who share my interests!

Okay let's come to the point. As you probably know, Ωmega provides a Row kind, it is a classifier for associations at the type level.

The shorthand notation {`a=Int, `b=Char}r can express a record where a component labelled with `a contains values of type Int while under the key `b we can store Chars. This is probably boring stuff if you already understand extensible records.

Now let's descend to the value plane. A value can have a type SingleLabel {`a=Int, `b=Char}r when we define following datatype:

data SingleLabel :: Row Tag * ~> * where

None :: SingleLabel RNil

More :: Label l -> t -> SingleLabel rest -> SingleLabel {l=t;rest}r

deriving Record(s)

As usual we have two data constructors, one for the empty record and one for augmenting an existing one. The "deriving" clause just tells Ωmega to enable the following syntactic sugar for None and More: More `lab 42 None === {`lab=42}s, nothing exciting.

But no one can hinder us to define a record value with repeated identical keys: {`a=25, `a="42"}s is a perfectly legal value of type {`a=Int, `a=[Char]}s but it really is incompatible with our aim of defining a one-to-one correspondence between labels and values.

Now enters my cunning idea: using a constraint, we can restrict the tail of the list to not contain a key we are about to add. Constraints are much like Haskell's type classes, but they are less ad-hoc and mirror propositional facts (properties). The new definition could look like this:

data SingleLabel :: Row Tag * ~> * where

None :: SingleLabel RNil

More :: Equal rest {drop l rest} => Label l -> t -> SingleLabel rest ->
SingleLabel {l=t;rest}r

deriving Record(s)

We have defined following semantics: Under the restriction that dropping the tag l from the tail does not change it at all (a fixpoint!), we can construct an augmented list. We have almost reached our self imposed objective: it only remains to provide a suitable definition for drop!

Now, Ωmega helps us in this respect too (but not entirely so for Tags), as we can define functions on types (or kinds for that matter). We can do it this way:

drop :: Tag ~> Row Tag * ~> Row Tag *

{drop o RNil} = RNil

{drop `a (RCons `a v r)} = {drop `a r}

{drop `b (RCons `b v r)} = {drop `b r}

{drop `b (RCons `a v r)} = RCons `a v {drop `b r}

{drop `a (RCons `b v r)} = RCons `b v {drop `a r}

This should be enough for demonstration purposes. (We get a quadratic blowup with increasing number of desired labels, since we have to write our definition in an inductively sequential fashion).

With all of this in place we can give a whirl to our SingleLabel datatype:

prompt> {`a=42}s

--> {`a=42}s :: SingleLabel {`a=Int}r

prompt> {`a=42,`b='K'}s

--> {`a=42,`b='K'}s :: SingleLabel {`a=Int,`b=Char}r

prompt> {`a=42,`a='K'}s

--- Type error: cannot find a solution for equation {`a=Char}r == {}r

We can now go to bed with the feeling of having accomplished a thing...

PS: Ωmega in its last released form cannot compile the code presented here. You will need some patches to get various bugs ironed out. With some luck this all will work out of the box in the next release!