[GHC] #13341: Lift constraint products

[GHC]

#13341: Lift constraint products
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

> I want to get a discussion going, could we lift constraint products
> automatically.
>
> Although not partially applicable, we can consider `(,)` as having kind
>
> {{{#!hs
> (,) :: Constraint -> Constraint -> Constraint
> }}}
>
> I propose also giving it kinds
>
> {{{#!hs
> (,) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
>
> (,) :: (k -> k' -> Constraint) -> (k -> k' -> Constraint) -> (k -> k' ->
> Constraint)
>
> -- etc.
> }}}
>
> == Translation
>
> {{{#!hs
> (Eq, Num, Show)
> (Monad, Foldable)
> (Category, Profunctor)
> }}}
>
> gets turned into something like
>
> {{{#!hs
> 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 [https://hackage.haskell.org/package/free-
> functors-0.7.2/docs/Data-Constraint-Class1.html SuperClasses]
>
> {{{#!hs
> 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
>
> {{{#!hs
> 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, why not make them all instances of the same data family
> (including `(,)` and `Product`)
>
> {{{#!hs
> 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:
>
> {{{#!hs
> -- (,) :: Constraint -> Constraint -> Constraint
>
> -- (,) :: (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
> }}}

New description:

 I want to get a discussion going, could we lift constraint products
 automatically.

 Although not partially applicable, we can consider `(,)` as having kind

 {{{#!hs
 (,) :: Constraint -> Constraint -> Constraint
 }}}

 I propose also giving it kinds

 {{{#!hs
 (,) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)

 (,) :: (k -> k' -> Constraint) -> (k -> k' -> Constraint) -> (k -> k' ->
 Constraint)

 -- etc.
 }}}

 == Translation

 {{{#!hs
 (Eq, Num, Show)
 (Monad, Foldable)
 (Category, Profunctor)
 }}}

 gets turned into something like

 {{{#!hs
 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 [https://hackage.haskell.org/package/free-
 functors-0.7.2/docs/Data-Constraint-Class1.html SuperClasses]

 {{{#!hs
 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

 {{{#!hs
 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, why not make them all instances of the same data family
 (including `(,)` and `Product`)

 {{{#!hs
 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:

 {{{#!hs
 -- (,) :: 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
 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13341#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler