[Haskell-cafe] type level strings?

[Evan Laforge]

So suppose I have a simple data type:

> data Thing {
>   thing_id :: ThingId
>   , thing_stuff :: Stuff
>   }
> newtype ThingId = ThingId String

Stuff is a Monoid, and Things need to be combined as well, so:

> instance Monoid Thing where
>   mappend (Thing id1 stuff1) (Thing id2 stuff2)
>     | id1 /= id2 = error "..."
>     | otherwise = Thing id1 (stuff1 `mappend` stuff2)
>   mempty = Thing $ (ThingId "dummy value?") mempty

So clearly both the error and the "dummy value?" are not very nice
(and mappend would need a special hack to treat the dummy as
compatible with everything).  I'd like to be able to lift that ID up
to the type level, and then I don't have to worry about incompatible
IDs and the mempty can figure out the ID from the type.

Now if ThingId were a natural, I gather there's a new GHC feature for
type level naturals that can do this kind of thing.  Of course any
string could be encoded into a large natural, but the resulting type
errors would be less than readable.  There is probably also a way to
encode type level strings in the same way as the traditional way for
type level naturals, e.g. 'data A; ... data Z;' and then a type
encoding for lists.  But I'm guessing that would also lead to
excessive compilation times and crazy type errors.

In any case, I don't think this can work even if I used naturals
instead of ints, because it seems to me I can't write a function
'(NatI n) => ThingId -> Thing n' without a statically knowable
constant value for 'n'.  Otherwise, the value has magically
disappeared into the type system and I can't expect to get it back
after types are erased.

So I need a runtime value for the ThingId, but it still seems like it
should be possible to do something better than the 'error' and "dummy
value?".  Maybe there's a completely different way to ensure that
incompatible Things can't be mappended.  Any ideas?