[Haskell-cafe] Restricted categories

[Sjoerd Visscher]

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