[Haskell-cafe] type level strings?

[Felipe Almeida Lessa]

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

Did you try something like below?

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

thing :: String -> [Int] -> Exists Thing
thing id stuff =
    case istring id of
      Exists id_ -> Exists (Thing id_ stuff)

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

maybeAppend :: Exists Thing -> Exists Thing -> Maybe (Exists Thing)
maybeAppend (Exists t1) (Exists t2) =
    case thing_id t1 `equal` thing_id t2 of
      Just Refl -> Just $ Exists (t1 `mappend` t2)
      Nothing   -> Nothing

Cheers,

-- 
Felipe.