[GHC] #13341: Lift constraint products
#13341: Lift constraint products -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13341 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): The empty constraint tuple `()` becomes the unit of `:&:` {{{#!hs class Empty a instance Empty a }}} `:&:` and `Empty` would presumably be added to *base*. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13341#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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.
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 = Pair (f a) (g a) -- Data.Bifunctor.Product.Product :: (k -> k' -> Type) -> (k -> k' -> Type) -> (k -> k' -> Type) data instance (f, g) a b = Pair2 (f a b) (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 }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13341#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 = Pair (f a) (g a)
-- Data.Bifunctor.Product.Product :: (k -> k' -> Type) -> (k -> k' -> Type) -> (k -> k' -> Type) data instance (f, g) a b = Pair2 (f a b) (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 -- (,) :: (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:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
participants (1)
-
GHC