Hi all, I want restricted categories, just like the rmonad package provides restricted monads. The ultimate goal is to have a product category: http://en.wikipedia.org/wiki/Product_category
{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
import Prelude hiding ((.), id, fst, snd) import qualified Prelude
First lets create a clone of Data.Suitable from the rmonad package, but this time for types with two arguments:
class Suitable2 m a b where data Constraints m a b constraints :: m a b -> Constraints m a b
withResConstraints :: forall m a b. Suitable2 m a b => (Constraints m a b -> m a b) -> m a b withResConstraints f = f (constraints undefined :: Constraints m a b)
withConstraintsOf :: Suitable2 m a b => m a b -> (Constraints m a b -> k) -> k withConstraintsOf v f = f (constraints v)
Now we can define a restricted category:
class RCategory (~>) where id :: Suitable2 (~>) a a => a ~> a (.) :: (Suitable2 (~>) b c, Suitable2 (~>) a b, Suitable2 (~>) a c) => b ~> c -> a ~> b -> a ~> c
(->) (or "Hask") is an instance of this class:
instance Suitable2 (->) a b where data Constraints (->) a b = HaskConstraints constraints _ = HaskConstraints
instance RCategory (->) where id = Prelude.id (.) = (Prelude..)
Now on to the product category. Objects of the product category are types that are an instance of IsProduct:
class IsProduct p where type Fst p :: * type Snd p :: * fst :: p -> Fst p snd :: p -> Snd p
For example:
instance IsProduct (a, b) where type Fst (a, b) = a type Snd (a, b) = b fst = Prelude.fst snd = Prelude.snd
Arrows from the product of category c1 and category c2 are a pair of arrows, one from c1 and one from c2:
data (c1 :***: c2) a b = c1 (Fst a) (Fst b) :***: c2 (Snd a) (Snd b)
The instance for Suitable2 restricts objects to IsProduct, and requires the Fst and Snd parts of the objects to be suitable in c1 resp. c2:
instance (IsProduct a, IsProduct b, Suitable2 c1 (Fst a) (Fst b), Suitable2 c2 (Snd a) (Snd b)) => Suitable2 (c1 :***: c2) a b where data Constraints (c1 :***: c2) a b = (IsProduct a, IsProduct b, Suitable2 c1 (Fst a) (Fst b), Suitable2 c2 (Snd a) (Snd b)) => ProdConstraints constraints _ = ProdConstraints
Finally the RCategory instance:
instance (RCategory c1, RCategory c2) => RCategory (c1 :***: c2) where id = withResConstraints $ \ProdConstraints -> id :***: id -- f@(f1 :***: f2) . g@(g1 :***: g2) = -- withResConstraints $ \ProdConstraints -> -- withConstraintsOf f $ \ProdConstraints -> -- withConstraintsOf g $ \ProdConstraints -> -- (f1 . g1) :***: (f2 . g2)
Here I am running into problems. I get this error: Could not deduce (Suitable2 c2 (Snd a) (Snd b), Suitable2 c1 (Fst a) (Fst b)) from the context (IsProduct b, IsProduct c, Suitable2 c1 (Fst b) (Fst c), Suitable2 c2 (Snd b) (Snd c)) arising from a use of `withConstraintsOf' In the first argument of `($)', namely `withConstraintsOf g' I don't understand this, as I thought the constraints the error is complaining about is just what withConstraintsOf g should provide. I guess there's something about the Suitable trick that I don't understand, or possibly the type families Fst and Snd are biting me. Who can help me out? Thanks. greetings, Sjoerd