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