Re: [Haskell-cafe] type level strings?

23 Nov 2011

      On Wed, Nov 23, 2011 at 4:25 PM, Julian Beaumont
 wrote:
...
On Thu, Nov 24, 2011 at 10:06 AM, Evan Laforge  wrote:
...
Well yes, but the key feature is that the IDs are arbitrary strings.
And they're not knowable at compile time, since they are read from
user input...
You can still use phantom types for this, you just need existentials
as well. For example, you could define a type for indexed strings/id's
as:
data IString s
 = IString String
data Exists f
 = forall x. Exists (f x)
read :: String -> Exists IString
read stuff = Exists (IString stuff)
I assume you'll also want to compare strings/id's, in which case
you'll also need (using GADT's):
data Equal a b where
 Refl :: Equal a a
equal :: IString s -> IString t -> Maybe (Equal s t)
equal (IString x) (IString y) | x == y = Just (unsafeCoerce Refl)
equal _ _ = Nothing
I don't fully understand this but it looks interesting!  I guess
'read' is a constructor for a sort of witness of the id, but I don't
see how to get this value into the type parameter, or how Equal would
be used in my mappend example.  Could you help me figure out how it
relates?  Here's the closest I could get:

data Thing thing_id = Thing {
    thing_id :: Exists IString
    , thing_stuff :: [Int]
    }

thing :: String -> [Int] -> Thing thing_id
thing thing_id stuff = Thing (istring thing_id) stuff

instance Monoid.Monoid (Thing thing_id) where
    mempty = Thing undefined []
    mappend (Thing id1 stuff1) (Thing _ stuff2) =
        Thing id1 (Monoid.mappend stuff1 stuff2)

istring :: String -> Exists IString
istring thing_id = Exists (IString thing_id)

data IString s = IString String
data Exists f = forall x. Exists (f x)

data Equal a b where
    Refl :: Equal a a

equal :: IString s -> IString t -> Maybe (Equal s t)
equal (IString x) (IString y) | x == y = Just (Coerce.unsafeCoerce Refl)
equal _ _ = Nothing

But as you can see it's not right, because the 'thing_id' goes into
the existential but is not expressed in the type parameter to Thing
(the real usage is that Things are Pitches which have a Scale and a
Signal, and it only makes sense to combine Pitches with the same
scale, which is probably a more interesting example, but I started
with Stuff and Things so I guess I should stick with it).  I don't see
how I could use Equal, because the signature for mappend already
expresses that the arguments should be the same type.  And while I can
see how to extract the String from the IString, I don't see how to
figure out the String from the *type* of the IString, as I would need
to do in mempty, since IString has no type parameter.