Type constraints on all type family instances
-
08-12-2019 - |
Question
I suppose what I want is impossible without Template Haskell but I'll ask anyway.
I have an interface for types like Data.Set
and Data.IntSet
:
type family Elem s :: *
class SetLike s where
insert :: Elem s -> s -> s
member :: Elem s -> s -> Bool
...
type instance Elem (Set a) = a
instance Ord a => SetLike (Set a) where
...
And I have a type family which chooses optimal set implementation:
type family EfficientSet elem :: *
type instance EfficientSet Int = IntSet
type instance EfficientSet String = Set String -- or another implementation
Is there a way to guarantee that EfficientSet
instances will be always SetLike
and that Elem (EfficientSet a)
is a
?
Without this guarantee all function signatures will be like this:
type LocationSet = EfficientSet Location
f :: (SetLike LocationSet, Elem LocationSet ~ Location) => ...
To write each time SetLike LocationSet
is somewhat tolerable, but Elem LocationSet ~ Location
makes code understanding only harder, as for me.
Solution
Using GHC 7.4's constraint kinds you could have something like
type EfficientSetLike a = (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a)
You can (with appropriate extensions) get constraints like this in earlier versions of GHC
class (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a) => EfficientSetLike a
instance (SetLike (EfficientSet a),Elem (EfficientSet a) ~ a) => EfficientSetLike a
But, the new style type
declaration is much nicer.
I'm not exactly sure what you are looking for, but it sounds like you just want easier to write/understand constraint signatures, in which case this will work.
OTHER TIPS
You can write this:
class (SetLike (EfficientSet a), Elem (EfficientSet a) ~ a) =>
HasEfficientSet a where
type EfficientSet a
If you associate the Elem
type family with the SetLike
class, you probably wouldn't even need the SetLike
superclass constraint:
class SetLike s where
type Elem s
insert :: Elem s -> s -> s
member :: Elem s -> s -> Bool
class Elem (EfficientSet a) ~ a => HasEfficientSet a where
type EfficientSet a
I like Daniel Wagner's post, but you can't just write:
test :: (HasEfficientSet a) => EfficientSet a
test = empty
You have to write:
test :: (HasEfficientSet a, SetLike (EfficientSet a)) => EfficientSet a
test = empty
But this can be overcome with a constraint synonym:
class SetLike s where
type Elem s :: *
empty :: s
insert :: Elem s -> s -> s
member :: Elem s -> s -> Bool
class (Elem (EfficientSet a) ~ a) => HasEfficientSet' a where
type EfficientSet a :: *
type HasEfficientSet a = (HasEfficientSet' a, SetLike (EfficientSet a))
newtype UnitSet = UnitSet Bool
deriving (Show, Eq, Ord)
instance SetLike UnitSet where
type Elem UnitSet = ()
empty = UnitSet False
insert () _ = UnitSet True
member () u = UnitSet True == u
instance HasEfficientSet' () where
type EfficientSet () = UnitSet
test :: (HasEfficientSet a) => EfficientSet a
test = empty
test1 :: EfficientSet ()
test1 = empty
test2 :: EfficientSet ()
test2 = test
test3 :: UnitSet
test3 = empty
test4 :: UnitSet
test4 = test