[GHC] #11740: RFC kind synonyms

21 Mar 2016

      #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