cnostrained.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}

import Prelude hiding ((.), id, Functor)
import Data.Constraint
import Data.Kind

class Category (cat :: k -> k -> Type) where
    type Domain cat (x :: k) :: Constraint
    id :: Domain cat a => cat a a
    (.) :: (Domain cat a, Domain cat b, Domain cat c)
        => cat b c
        -> cat a b
        -> cat a c

newtype Functor (c :: k -> k -> Type) (c' :: k -> k -> Type)  = Functor { runFunctor :: forall a b. c a b -> c' a b }

instance Category (->) where
    type Domain (->) a = ()
    id = \x -> x
    f . g = \x -> f (g x)

instance Category Functor where
    type Domain Functor c = Category c
    id = Functor (\x -> x)
    Functor f . Functor g = Functor (\x -> f (g x))