Restricted categories

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Restricted categories

Sjoerd Visscher-2
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restricted categories

Alexander Solla-2

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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restricted categories

Doralicio
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restricted categories

Alexander Solla-2

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._______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Restricted categories

Sjoerd Visscher-2
In reply to this post by Sjoerd Visscher-2
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_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe