Skip to content

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
Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information