[Haskell-cafe] Restricted categories

[Sjoerd Visscher]

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