RFC kind synonyms
Are any of these useful now that we have kind synonyms:
-- 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 hask, subhask and is defined by recategorize.
It lets you rewrite:
-- 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
-- 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