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