Skip to content

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
Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information