[Haskell-cafe] type level strings?

[Julian Beaumont]

On Thu, Nov 24, 2011 at 10:06 AM, Evan Laforge <qdunkan at gmail.com> 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