[GHC] #11740: RFC kind synonyms
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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: -------------------------------------+------------------------------------- Are any of these useful now that we have kind synonyms: {{{#!hs -- Control.Category type Cat k = k -> k -> Type -- Data.Kind type Kind = Type type Types = [Type] type TypeClass = Type -> Constraint }}} `Cat` is not limited to `Control.Category` but applies in all [https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs#L68 hask], [https://github.com/mikeizbicki/subhask/blob/b5433b959914d8214bcc4f130ff1b3dd... subhask] and is defined by [https://github.com/ttuegel/recategorize/blob/master/src/Category/Category.hs... recategorize]. It lets you rewrite: {{{#!hs -- newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a } newtype Yoneda :: Cat i -> Cat i where Op :: { getOp :: p b a } -> Yoneda p a b -- type family Op (p :: i -> i -> *) :: i -> i -> * where type family Op (p :: Cat i) :: Cat i where Op (Yoneda p) = p Op p = Yoneda p -- data CatT (cat :: * -> * -> *) (a :: k) (b :: k) (cat1 :: k -> k -> *) (cat2 :: k -> k -> *) data CatT (cat :: Cat Type) (a :: k) (b :: k) (cat1 :: Cat k) (cat2 :: Cat k) -- class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where -- type Dom f :: i -> i -> * -- type Cod f :: j -> j -> * class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where type Dom f :: Cat i type Cod f :: Cat j -- data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) where -- instance Cartesian ((->) :: * -> * -> *) where instance Cartesian ((->) :: Cat Type) where }}} and {{{#!hs -- class (f x, g x) => And (f :: * -> Constraint) (g :: * -> Constraint) (x :: *) -- instance (f x, g x) => And (f :: * -> Constraint) (g :: * -> Constraint) (x :: *) class (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *) instance (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *) -- ToContext (fs :: [TypeClass]) :: TypeClass where type family ToContext (fs :: [* -> Constraint]) :: * -> Constraint where ToContext (f:g:fs) = And f (ToContext (g:fs)) ToContext '[f] = f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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): I write `type Fun = i -> j` in my own code: {{{#!hs class (Category' (Dom f), Category' (Cod f)) => Functor (f :: Fun i j) where data Nat (p :: Cat i) (q :: Cat j) (f :: Fun i j) (g :: Fun i j) where }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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: @@ -66,1 +66,1 @@ - -- ToContext (fs :: [TypeClass]) :: TypeClass where + -- ToContext (fs :: [* -> Constraint]) :: * -> Constraint where @@ -68,1 +68,1 @@ - ToContext (fs :: [* -> Constraint]) :: * -> Constraint where + ToContext (fs :: [TypeClass]) :: TypeClass where New description: Are any of these useful now that we have kind synonyms: {{{#!hs -- Control.Category type Cat k = k -> k -> Type -- Data.Kind type Kind = Type type Types = [Type] type TypeClass = Type -> Constraint }}} `Cat` is not limited to `Control.Category` but applies in all [https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs#L68 hask], [https://github.com/mikeizbicki/subhask/blob/b5433b959914d8214bcc4f130ff1b3dd... subhask] and is defined by [https://github.com/ttuegel/recategorize/blob/master/src/Category/Category.hs... recategorize]. It lets you rewrite: {{{#!hs -- newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a } newtype Yoneda :: Cat i -> Cat i where Op :: { getOp :: p b a } -> Yoneda p a b -- type family Op (p :: i -> i -> *) :: i -> i -> * where type family Op (p :: Cat i) :: Cat i where Op (Yoneda p) = p Op p = Yoneda p -- data CatT (cat :: * -> * -> *) (a :: k) (b :: k) (cat1 :: k -> k -> *) (cat2 :: k -> k -> *) data CatT (cat :: Cat Type) (a :: k) (b :: k) (cat1 :: Cat k) (cat2 :: Cat k) -- class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where -- type Dom f :: i -> i -> * -- type Cod f :: j -> j -> * class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where type Dom f :: Cat i type Cod f :: Cat j -- data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) where -- instance Cartesian ((->) :: * -> * -> *) where instance Cartesian ((->) :: Cat Type) where }}} and {{{#!hs -- class (f x, g x) => And (f :: * -> Constraint) (g :: * -> Constraint) (x :: *) -- instance (f x, g x) => And (f :: * -> Constraint) (g :: * -> Constraint) (x :: *) class (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *) instance (f x, g x) => And (f :: TypeClass) (g :: TypeClass) (x :: *) -- ToContext (fs :: [* -> Constraint]) :: * -> Constraint where type family ToContext (fs :: [TypeClass]) :: TypeClass where ToContext (f:g:fs) = And f (ToContext (g:fs)) ToContext '[f] = f }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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 goldfire): I think these are fine definitions for a separate library, but I don't personally see a compelling reason to put them into, say, `base` at this point. It's just too soon to know what will be helpful and widely used. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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): Agreed. I found it interesting that the most worthwhile synonym was `Cat` and should note that `TypeClass` could be more general: {{{#!hs type TTypeClass k = k -> Constraint And :: TTypeClass k -> TTypeClass k -> TTypeClass k Typeable :: TTypeClass k }}} And what about multi-parameter type classes like `(~) :: k -> k -> Constraint`? Let's see what happens. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 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): {{{#!hs type NoConstraint = (() :: Constraint) }}} from [https://www.cs.ox.ac.uk/projects/utgp/school/andres.pdf Applying Type-Level and Generic Programming in Haskell] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: wontfix | 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: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => wontfix Comment: Since @goldfire and @Iceland_jack both agree this shouldn't go in base at the moment, I'm going to close this ticket, to give those other 1825 tickets some more room to breathe. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: wontfix | 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): I'll jot down some [https://github.com/kylcarte/type- combinators/blob/master/src/Type/Family/Constraint.hs data points] for posteriority {{{#!hs -- | The empty 'Constraint'. type ØC = (() :: Constraint) type Fail = (True ~ False) }}} That library also has a lot of ideas -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11740: RFC kind synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: wontfix | 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): {{{#!hs type Monadish = Type -> Type type Transformer = Monadish -> Monadish }}} with many examples from Edward's work on [https://www.reddit.com/r/haskell/comments/50rxci/edward_kmett_monad_homomorp... monad morphisms] {{{#!hs newtype Tensor :: Transformer -> Transformer -> Transformer where Tensor :: s (t m) a -> Tensor s t m a class MonadTrans (t :: Transformer) class Commute (s :: Transformer) (t :: Transformer) where commute :: Monad m => s (t m) a -> t (s m) a newtype StateT s :: Transformer where StateT :: (s -> m (a, s)) -> StateT s m a newtype WriterT w :: Transformer where WriterT :: m (a, w) -> WriterT w m a }}} etc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11740#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC