[Haskell-cafe] type level strings?

Felipe Almeida Lessa felipe.lessa at gmail.com
Thu Nov 24 05:47:07 CET 2011

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



More information about the Haskell-Cafe mailing list