To allow hask
type Cat k = k -> k -> Type
type Fun i j = i -> j
data Nat :: Cat i -> Cat j -> Cat (Fun i j) where
Nat :: (FunctorOf cat cat' f, FunctorOf cat cat' f') => (forall a. Ob cat a => cat' (f a) (f' a)) -> Cat cat cat' f f'
type (~>) = Nat (->) (->)
data (~>) :: Cat (Type -> Type) where
N :: (FunctorOf (->) (->) f, FunctorOf (->) (->) f')
=> (forall a. f a -> f' a)
-> f ~> f'
to be used as liftCoT0M :: (Comonad w, Monad m) => (forall a. w a -> m s) -> CoT w m s
data (~??>) :: Cat (Type -> Type) where
CM :: (Comonad w, Monad m)
=> (forall a. w a -> m a)
-> w ~??> m
where every ~??>
implies ~>
since both Comonad
, Monad
have Funtor
s as superclasses..
to :: w ~??> m
-> w ~> m
to (CM nat) = Nat nat
from :: (Comonad w, Monad m)
=> w ~> m
-> w ~??> m
from (Nat nat) = CM nat
hell could be defined
data (~??>) :: Cat (Type -> Type) where
CM :: (Comonad w, Monad m)
=> w ~> m
-> w ~??> m
So now the tricky part is, I want subsumption between them. This requires ImplicationConstraints, I believe this monstrosity could be it
Okay so, now we can specify, “is at least a” for both of the constraints