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!