[Haskell-cafe] type level strings?

[Holger Reinhardt]

You can do this with phantom types, i.e.:

> data Thing a = Thing Stuff
>
> instance Monoid (Thing a) where
>   mappend (Thing stuff1) (Thing stuff2) = Thing (stuff1 `mappend` stuff2)
>   mempty = Thing mempty
>
> data ID1
> data ID2
>
> thing1 :: Thing ID1
> thing1 = Thing Stuff
>
> thing2 :: Thing ID2
> thing2 = Thing Stuff
>
> -- will not typecheck:
> f = thing1 `mappend` thing2


2011/11/23 Evan Laforge <qdunkan at gmail.com>

> 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?
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111124/5ad44224/attachment.htm>