GADTs, type classes, existentials

Hello all, I'm trying to build a variation on Maps which supports a fast "concat-like" operation, for a library I'm writing. I'd rather not re-implement Data.Map, so I'm having a try with GADTs. The relevant part of my source file: ------------------------------------------------------------------------- data MetaMap k v where Map :: Ord k => Map.Map k v -> MetaMap k v Cat :: MetaMap k1 (MetaMap k2 v) -> MetaMap (k1,k2) v {- other, similar constructors -} lookup :: Monad m => k -> MetaMap k v -> m v lookup k (Map m) = Map.lookup k m lookup k (Cat m) = case k of (k1,k2) -> lookup k1 m >>= lookup k2 ------------------------------------------------------------------------- Unfortunately, this doesn't work: Data/MetaMap.hs:45:20: Could not deduce (Ord k) from the context (Monad m) arising from use of `Map.lookup' at Data/MetaMap.hs:45:20-33 Possible fix: add (Ord k) to the type signature(s) for `lookup' In the expression: Map.lookup k m In the definition of `lookup': lookup k (Map m) = Map.lookup k m This error happens because the Ord constraint isn't propagated into the function body. Of course, I can't add Ord k to the type signature for lookup, because one can't deduce Ord k from Ord (k1,k2). Is there a clean way around this error? Thanks for your time, Mike Hamburg

On Sunday 06 May 2007, Mike Hamburg wrote:
data MetaMap k v where Map :: Ord k => Map.Map k v -> MetaMap k v Cat :: MetaMap k1 (MetaMap k2 v) -> MetaMap (k1,k2) v {- other, similar constructors -}
lookup :: Monad m => k -> MetaMap k v -> m v lookup k (Map m) = Map.lookup k m lookup k (Cat m) = case k of (k1,k2) -> lookup k1 m >>= lookup k2
What version of ghc are you using? The snippet works here, but I believe that GADTs only store the Ord dictionary as is needed here in HEAD. It won't work if you're trying to do this with 6.6. -- Dan Doel

On Sun, May 06, 2007 at 03:11:12AM -0700, Mike Hamburg wrote:
Hello all,
I'm trying to build a variation on Maps which supports a fast "concat-like" operation, for a library I'm writing. I'd rather not re-implement Data.Map, so I'm having a try with GADTs.
The relevant part of my source file:
------------------------------------------------------------------------- data MetaMap k v where Map :: Ord k => Map.Map k v -> MetaMap k v Cat :: MetaMap k1 (MetaMap k2 v) -> MetaMap (k1,k2) v {- other, similar constructors -}
lookup :: Monad m => k -> MetaMap k v -> m v lookup k (Map m) = Map.lookup k m lookup k (Cat m) = case k of (k1,k2) -> lookup k1 m >>= lookup k2 -------------------------------------------------------------------------
Unfortunately, this doesn't work:
Data/MetaMap.hs:45:20: Could not deduce (Ord k) from the context (Monad m) arising from use of `Map.lookup' at Data/MetaMap.hs:45:20-33 Possible fix: add (Ord k) to the type signature(s) for `lookup' In the expression: Map.lookup k m In the definition of `lookup': lookup k (Map m) = Map.lookup k m
This error happens because the Ord constraint isn't propagated into the function body. Of course, I can't add Ord k to the type signature for lookup, because one can't deduce Ord k from Ord (k1,k2).
Is there a clean way around this error?
Yes, upgrade. Type classes and GADTs are broken in all versions prior to HEAD (at which point Simon made a heroic effort to do something I don't quite understand to the type checker). Stefan

On Sun, 2007-05-06 at 07:10 -0700, Stefan O'Rear wrote:
On Sun, May 06, 2007 at 03:11:12AM -0700, Mike Hamburg wrote:
Is there a clean way around this error?
Yes, upgrade.
Type classes and GADTs are broken in all versions prior to HEAD (at which point Simon made a heroic effort to do something I don't quite understand to the type checker).
Stefan
Ah. Well, thanks for your time, and props to Simon! Mike

| Type classes and GADTs are broken in all versions prior to HEAD (at | which point Simon made a heroic effort to do something I don't quite | understand to the type checker). Well, not that heroic, but certainly long-postponed :-) Simon
participants (4)
-
Dan Doel
-
Mike Hamburg
-
Simon Peyton-Jones
-
Stefan O'Rear