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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
