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
On Feb 20, 2010, at 10:29 AM, Sjoerd Visscher wrote:
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.
You specifically ask withConstraintsOf to accept only Suitable2's when you say
withConstraintsOf :: Suitable2 m a b => m a b -> (Constraints m a b -
k) -> k
But you aren't saying that the argument of withConstraintsOf IS a Suitable2, when you say:
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)
You need to make a type class instance for Suitable2 for whatever type \ProdConstraints -> ... represents. For comparison, try:
data Unordered = A | B | C
A <= B No instance for (Ord Unordered) arising from a use of `<=' at <interactive>:1:0-5 Possible fix: add an instance declaration for (Ord Unordered) In the expression: A <= B In the definition of `it': it = A <= B
and now:
data Ordered = A | B | C deriving (Show, Eq, Ord) -- (easier than writing an instance for Eq, Ord) A <= B True
Alexander Solla wrote:
You specifically ask withConstraintsOf to accept only Suitable2's when you say
withConstraintsOf :: Suitable2 m a b => m a b -> (Constraints m a b -> k) -> k
But you aren't saying that the argument of withConstraintsOf IS a Suitable2, when you say:
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) As I understand, Sjoerd expects this to be done at the definition of (.) in the type class RCategory, so that an instance method can relay on the constraints collected by it: class RCategory (~>) where id :: Suitable2 (~>) a a => a ~> a (.) :: (Suitable2 (~>) b c, Suitable2 (~>) a b, Suitable2 (~>) a c) => b ~> c -> a ~> b -> a ~> c
A simple example: class Show el=> ExceptionNote el where comment:: Show exception=> exception-> el-> String instance ExceptionNote Int where comment exception refId = show refId ++ ": " ++ show exception Here you don't need to constrain ?exception? to be of ?Show? at the instance declaration. So it does not appear wrong for Sjoerd to expect f and g to already be of Suitable2... This is exciting stuff, I am really a little astonished about the giant leap Haskell has made since my efforts to translate the examples of Rydeheart & Burstall, which actually was my intro to categories, from ML to Haskell. This looks very elegant... Maybe it's time for a second edition of the unique approach of Rydeheart & Burstall on basis of Haskell? Wow, really cool stuff... :-) Cheers, Nick
On Feb 20, 2010, at 6:32 PM, Nick Rudnick wrote:
A simple example: class Show el=> ExceptionNote el where comment:: Show exception=> exception-> el-> String
instance ExceptionNote Int where comment exception refId = show refId ++ ": " ++ show exception
Here you don't need to constrain «exception» to be of «Show» at the instance declaration. So it does not appear wrong for Sjoerd to expect f and g to already be of Suitable2...
There really are instances missing. The context is coming from here:
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
Given types A and B, the product A x B has a type Fst which is A, and a type Snd which is B -- by construction:
class IsProduct p where type Fst p :: * type Snd p :: * fst :: p -> Fst p snd :: p -> Snd p
So, if we have two products named a and b, and a = A + B, b = C + D (letting the first type in the addition be Fst, and the latter be Snd in each), a x b has four "components": (A x C) + (B x C) + (A x D) + (B x D). a x b = (A | B) x (C | D) = (Fst a | Snd a) x (Fst b | Snd b) = (Fst a, Fst b) + (Snd a, Fst b) + (Fst a, Snd b) + (Snd a, Snd b) This really comes down to the semantics of Suitability2, but I think Sjoerd made a logic mistake, and is trying to make a product out of a pair of products, in stead of a pair of categories.
Ok, I've got product categories working:
{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, GADTs, RankNTypes, UndecidableInstances #-}
import Prelude hiding ((.), id, fst, snd) import qualified Prelude
Suitable2 could be simplified to one type argument (but it is still different from Data.Suitable, because m is of kind * -> * -> *)
class Suitable2 m a where data Constraints m a constraints :: m a a -> Constraints m a
withResConstraints :: forall m a. Suitable2 m a => (Constraints m a -> m a a) -> m a a withResConstraints f = f (constraints undefined :: Constraints m a)
class RCategory (~>) where id :: Suitable2 (~>) a => a ~> a (.) :: (Suitable2 (~>) a, Suitable2 (~>) b, Suitable2 (~>) c) => b ~> c -> a ~> b -> a ~> c
instance Suitable2 (->) a where data Constraints (->) a = HaskConstraints constraints _ = HaskConstraints
instance RCategory (->) where id = Prelude.id (.) = (Prelude..)
class IsProduct p where type Fst p :: * type Snd p :: * fst :: p -> Fst p snd :: p -> Snd p
instance IsProduct (a, b) where type Fst (a, b) = a type Snd (a, b) = b fst = Prelude.fst snd = Prelude.snd
Adding the restrictions to the constructor made all further problems in the definition of (.) go away:
-- Product category data (c1 :***: c2) a b = (IsProduct a, IsProduct b, Suitable2 c1 (Fst a), Suitable2 c1 (Fst b), Suitable2 c2 (Snd a), Suitable2 c2 (Snd b)) => c1 (Fst a) (Fst b) :***: c2 (Snd a) (Snd b)
instance (IsProduct a, Suitable2 c1 (Fst a), Suitable2 c2 (Snd a)) => Suitable2 (c1 :***: c2) a where data Constraints (c1 :***: c2) a = (IsProduct a, Suitable2 c1 (Fst a), Suitable2 c2 (Snd a)) => ProdConstraints constraints _ = ProdConstraints
instance (RCategory c1, RCategory c2) => RCategory (c1 :***: c2) where id = withResConstraints $ \ProdConstraints -> id :***: id (f1 :***: f2) . (g1 :***: g2) = (f1 . g1) :***: (f2 . g2)
Let's test this:
(@*) :: ((->) :***: (->)) (a, b) (c, d) -> (a, b) -> (c, d) (f :***: g) @* (x, y) = (f x, g y) test1 = ((+10) :***: (*2)) @* (1, 2) -- (11, 4)
So that works, but using type families Fst and Snd gives problems if you start to use this (see below). Here's a functor definition. To allow to define the identity functor, the actual functor itself is not the instance, but a placeholder type is used. The type family F turns the placeholder into the actual functor. The use of type families also means you have to pass a type witness of the placeholder to the fmap function (here called (%)).
type family F (ftag :: * -> *) a :: * class (RCategory (Dom ftag), RCategory (Cod ftag)) => CFunctor ftag where type Dom ftag :: * -> * -> * type Cod ftag :: * -> * -> * (%) :: (Suitable2 (Dom ftag) a, Suitable2 (Dom ftag) b) => ftag x -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
Two examples:
data Opt a = Opt type instance F Opt a = Maybe a instance CFunctor Opt where type Dom Opt = (->) type Cod Opt = (->) (Opt % f) Nothing = Nothing (Opt % f) (Just x) = Just (f x)
So (Opt % (*2)) has type: Num a => Maybe a -> Maybe a.
data Id ((~>) :: * -> * -> *) a = Id type instance F (Id (~>)) a = a instance (RCategory (~>)) => CFunctor (Id (~>)) where type Dom (Id (~>)) = (~>) type Cod (Id (~>)) = (~>) Id % f = f
The diagonal functor works nicely too:
data Diag ((~>) :: * -> * -> *) a = Diag type instance F (Diag (~>)) a = (a, a) instance (RCategory (~>)) => CFunctor (Diag (~>)) where type Dom (Diag (~>)) = (~>) type Cod (Diag (~>)) = (~>) :***: (~>) Diag % f = f :***: f
test2 = (Diag % (*2)) @* (1, 5) -- (2, 10)
But with the projection functors things start to break down. They can be defined, but not used:
data ProjL (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = ProjL type instance F (ProjL c1 c2) a = Fst a instance (RCategory c1, RCategory c2) => CFunctor (ProjL c1 c2) where type Dom (ProjL c1 c2) = c1 :***: c2 type Cod (ProjL c1 c2) = c1 ProjL % (f :***: g) = f
data ProjR (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = ProjR type instance F (ProjR c1 c2) a = Snd a instance (RCategory c1, RCategory c2) => CFunctor (ProjR c1 c2) where type Dom (ProjR c1 c2) = c1 :***: c2 type Cod (ProjR c1 c2) = c2 ProjR % (f :***: g) = g
Here's an example, but GHCI does not know what a is, and so throws a bunch of errors about Fst a and Snd a. test3 = (ProjL % ((+10) :***: (*2))) 1 -- Should evalutate to 11, but doesn't compile. When trying to define the product functor, I run into another problem: data (w1 :*: w2) a = (forall x. w1 x) :*: (forall x. w2 x) type instance F (f1 :*: f2) a = (F f1 (Fst a), F f2 (Snd a)) instance (CFunctor f1, CFunctor f2) => CFunctor (f1 :*: f2) where type Dom (f1 :*: f2) = Dom f1 :***: Dom f2 type Cod (f1 :*: f2) = Cod f1 :***: Cod f2 (w1 :*: w2) % (f1 :***: f2) = (w1 % f1) :***: (w2 % f2) There is no proof that from a Suitable2 (Dom f) a, the functor produces a Suitable2 (Cod f) (F f a), i.e. I need something like: instance (CFunctor f, Suitable2 (Dom f) a) => Suitable2 (Cod f) (F f a) This proof is also needed for functor composition: data Comp g h a = Comp (forall x. g x) (forall x. h x) type instance F (Comp g h) a = F g (F h a) instance (CFunctor g, CFunctor h, Cod h ~ Dom g) => CFunctor (Comp g h) where type Dom (Comp g h) = Dom h type Cod (Comp g h) = Cod g Comp g h % f = g % (h % f) So for now the choice is between being able to define the product category, or dropping the Suitable2 restriction, and being able to do: -- Natural transformations type f :~> g = forall c (~>). (CFunctor f, CFunctor g, Dom f ~ Dom g, (~>) ~ Cod f, (~>) ~ Cod g) => F f c ~> F g c class (CFunctor f, CFunctor g) => Adjunction f g | f -> g, g -> f where unit :: (Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> Id (Cod g) :~> Comp g f counit :: (Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> Comp f g :~> Id (Cod f) leftAdjunct :: (Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> Cod f (F f a) b -> Cod g a (F g b) rightAdjunct :: (Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> Cod g a (F g b) -> Cod f (F f a) b unit f g = leftAdjunct f g id counit f g = rightAdjunct f g id leftAdjunct f g h = (g % h) . unit f g rightAdjunct f g h = counit f g . (f % h) data InitialProperty x u a = InitialProperty (Cod u x (F u a)) (forall y. Cod u x (F u y) -> Dom u a y) data TerminalProperty x u a = TerminalProperty (Cod u (F u a) x) (forall y. Cod u (F u y) x -> Dom u y a) adjTerminalProperty :: (Adjunction f g, Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> TerminalProperty x f (F g x) adjTerminalProperty f g = TerminalProperty (counit f g) (leftAdjunct f g) adjInitialProperty :: (Adjunction f g, Dom f ~ Cod g, Cod f ~ Dom g) => f _x -> g _y -> InitialProperty x g (F f x) adjInitialProperty f g = InitialProperty (unit f g) (rightAdjunct f g) Which, besides having to pass around the functor type witnesses everywhere, is quite nice I think. But if anyone has an idea how to provide proof that Suitable2 (Cod f) (F f a) when Suitable2 (Dom f) a, I would like to hear it! greetings, Sjoerd
participants (3)
-
Alexander Solla -
Nick Rudnick -
Sjoerd Visscher