Lift constraint products
I want to get a discussion going, could we lift constraint products automatically.
Although not partially applicable, we can consider (,)
as having kind
(,) :: Constraint -> Constraint -> Constraint
I propose also giving it kinds
(,) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
(,) :: (k -> k' -> Constraint) -> (k -> k' -> Constraint) -> (k -> k' -> Constraint)
-- etc.
Translation
(Eq, Num, Show)
(Monad, Foldable)
(Category, Profunctor)
gets turned into something like
class (c a, d a) => (c :&: d) a
instance (c a, d a) => (c :&: d) a
infixl 7 :&:
Eq:&:Num:&:Show
Monad:&:Foldable
Category:&:Profunctor
Uses
Very often I need to be able to combine constraints.
A small modification of SuperClasses
type c :~ d = forall xx. c x :- d xx
class HasSuperClasses (c :: k -> Constraint) where
type SuperClasses c :: k -> Constraint
type SuperClasses c = c
superClasses :: c :~ SuperClasses c
containsSelf :: SuperClasses c :~ c
instance HasSuperClasses Functor where
superClasses :: Functor :~ Functor
superClasses = Sub Dict
containsSelf :: Functor :~ Functor
containsSelf = Sub Dict
instance HasSuperClasses Foldable where
superClasses :: Foldable :~ Foldable
superClasses = Sub Dict
containsSelf :: Foldable :~ Foldable
containsSelf = Sub Dict
I want to be able to write
instance HasSuperClasses Traversable where
type Traversable = (Traversable, Functor, Foldable)
superClasses :: Traversable :~ (Traversable, Functor, Foldable)
superClasses = Sub Dict
containsSelf :: (Traversable, Functor, Foldable) :~ Traversable
containsSelf = Sub Dict
If this doesn't pose any difficulties I'll open a GHC proposal.
Etc.
With #12369 (closed), why not make them all instances of the same data family (including (,)
and Product
)
data family (,) :: k -> k -> k
-- (,) :: Type -> Type -> Type
data instance (a, b) = (a, b)
-- Data.Functor.Product.Product :: (k -> Type) -> (k -> Type) -> (k -> Type)
data instance (f, g) a = f a `Pair` g a
-- Data.Bifunctor.Product.Product :: (k -> k' -> Type) -> (k -> k' -> Type) -> (k -> k' -> Type)
data instance (f, g) a b = f a b `Pair2` g a b
the type class could be made an instance of this “data” family:
-- (,) :: Constraint -> Constraint -> Constraint
class (c, d) => (c, d)
-- from https://github.com/ghc/ghc/blob/master/libraries/ghc-prim/GHC/Classes.hs#L477
-- (,) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
class (c a, d a) => (c, d) a
instance (c a, d a) => (c, d) a
-- (,) :: (k -> k' -> Constraint) -> (k -> k' -> Constraint) -> (k -> k' -> Constraint)
class (c a b, d a b) => (c, d) a b
instance (c a b, d a b) => (c, d) a b