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