-- |
-- Module      :  Control.Monad.Constrained
-- Copyright   :  (c) 2013 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
{-# LANGUAGE ConstraintKinds              #-}
{-# LANGUAGE TypeFamilies                 #-}
{-# LANGUAGE FunctionalDependencies       #-}
{-# LANGUAGE TypeOperators                #-}
{-# LANGUAGE FlexibleContexts             #-}
{-# LANGUAGE FlexibleInstances            #-}
{-# LANGUAGE CPP                          #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses      #-}
#endif
{-# LANGUAGE ScopedTypeVariables          #-}
{-# LANGUAGE TupleSections                #-}
{-# LANGUAGE LambdaCase                   #-}


module Control.Monad.Constrained( module Control.Applicative.Constrained 
                                -- * Monads                                
                                , Monad(..), return, (>>=), (=<<), (>>), (<<)
                                -- * Kleisli arrows
                                , (>=>), (<=<)
                                , Kleisli(..)
                                -- * Monoid-Monads
                                , MonadZero(..), mzero, MonadPlus(..), mplus
                                , MonadFail(..)
                                -- * Utility
                                , mapM, mapM_, forM, forM_, sequence, sequence_
                                , guard, when, unless
                                , forever, void
                                , filterM
                                ) where


import Control.Category.Constrained
import Control.Applicative.Constrained
import Data.Foldable.Constrained
import Data.Traversable.Constrained
import Data.Tagged

import Prelude hiding (
     id, const, fst, snd, (.), ($)
   , Functor(..), Applicative(..), Monad(..), MonadFail(..), (=<<)
   , uncurry, curry, filter
   , mapM, mapM_, sequence, sequence_
   )
import qualified Control.Category.Hask as Hask
import qualified Control.Monad.Fail as HaskFail

import Control.Arrow.Constrained


class ( Applicative m k k
      , Object k (m (UnitObject k)), Object k (m (m (UnitObject k)))
      ) => Monad m k where
  join :: (Object k a, Object k (m a), Object k (m (m a)))
       => m (m a) `k` m a

-- | This is monomorphic in the category /Hask/, thus exactly the same as 'Hask.return'
--   from the standard prelude. This allows writing expressions like
--   @'return' '$' case x of ...@, which would always be ambiguous with the more general 
--   signature @Monad m k => k a (m a)@.
-- 
--   Use 'pure' when you want to \"return\" in categories other than @(->)@; this always
--   works since 'Applicative' is a superclass of 'Monad'.
return :: Monad m (->) => a -> m a
return :: forall (m :: * -> *) a. Monad m (->) => a -> m a
return = a -> m a
forall a. (Object (->) a, Object (->) (m a)) => a -> m a
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure

         

infixr 1 =<<
(=<<) :: ( Monad m k, Object k a, Object k b
         , Object k (m a), Object k (m b), Object k (m (m b)) )
      => k a (m b) -> k (m a) (m b)
=<< :: forall (m :: * -> *) (k :: * -> * -> *) a b.
(Monad m k, Object k a, Object k b, Object k (m a), Object k (m b),
 Object k (m (m b))) =>
k a (m b) -> k (m a) (m b)
(=<<) k a (m b)
q = k (m (m b)) (m b)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m b)) (m b) -> k (m a) (m (m b)) -> k (m a) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b) -> k (m a) (m (m b))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k a (m b)
q

infixl 1 >>=
(>>=) :: ( Function f, Monad m f, Object f a, Object f b
         , Object f (m a), Object f (m b), Object f (m (m b)) ) 
             => m a -> f a (m b) -> m b
m a
g >>= :: forall (f :: * -> * -> *) (m :: * -> *) a b.
(Function f, Monad m f, Object f a, Object f b, Object f (m a),
 Object f (m b), Object f (m (m b))) =>
m a -> f a (m b) -> m b
>>= f a (m b)
h = f a (m b) -> f (m a) (m b)
forall (m :: * -> *) (k :: * -> * -> *) a b.
(Monad m k, Object k a, Object k b, Object k (m a), Object k (m b),
 Object k (m (m b))) =>
k a (m b) -> k (m a) (m b)
(=<<) f a (m b)
h f (m a) (m b) -> m a -> m b
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m a
g

infixr 1 <<
(<<) :: ( Monad m k, WellPointed k
        , Object k a, Object k b, Object k (m a), ObjectPoint k (m b), Object k (m (m b))
        ) => m b -> k (m a) (m b)
<< :: forall (m :: * -> *) (k :: * -> * -> *) a b.
(Monad m k, WellPointed k, Object k a, Object k b, Object k (m a),
 ObjectPoint k (m b), Object k (m (m b))) =>
m b -> k (m a) (m b)
(<<) m b
b = k (m (m b)) (m b)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m b)) (m b) -> k (m a) (m (m b)) -> k (m a) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b) -> k (m a) (m (m b))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (m b -> k a (m b)
forall b x. (Object k b, ObjectPoint k x) => x -> k b x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const m b
b)

infixl 1 >>
(>>) :: ( WellPointed k, Monad m k
        , ObjectPair k b (UnitObject k), ObjectPair k (m b) (UnitObject k)
        , ObjectPair k (UnitObject k) (m b), ObjectPair k b a
        , ObjectPair k a b, Object k (m (a,b)), ObjectPair k (m a) (m b)
        , ObjectPoint k (m a)
        ) => m a -> k (m b) (m b)
>> :: forall (k :: * -> * -> *) (m :: * -> *) b a.
(WellPointed k, Monad m k, ObjectPair k b (UnitObject k),
 ObjectPair k (m b) (UnitObject k),
 ObjectPair k (UnitObject k) (m b), ObjectPair k b a,
 ObjectPair k a b, Object k (m (a, b)), ObjectPair k (m a) (m b),
 ObjectPoint k (m a)) =>
m a -> k (m b) (m b)
(>>) m a
a = k (a, b) b -> k (m (a, b)) (m b)
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k (a, b) b
forall x y. ObjectPair k x y => k (x, y) y
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd k (m (a, b)) (m b) -> k (m b) (m (a, b)) -> k (m b) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (m a, m b) (m (a, b))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip k (m a, m b) (m (a, b)) -> k (m b) (m a, m b) -> k (m b) (m (a, b))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (UnitObject k) (m a) -> k (UnitObject k, m b) (m a, m b)
forall b d c.
(ObjectPair k b d, ObjectPair k c d) =>
k b c -> k (b, d) (c, d)
forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (m a -> k (UnitObject k) (m a)
forall x. ObjectPoint k x => x -> k (UnitObject k) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement m a
a) k (UnitObject k, m b) (m a, m b)
-> k (m b) (UnitObject k, m b) -> k (m b) (m a, m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (m b, UnitObject k) (UnitObject k, m b)
forall a b. (ObjectPair k a b, ObjectPair k b a) => k (a, b) (b, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap k (m b, UnitObject k) (UnitObject k, m b)
-> k (m b) (m b, UnitObject k) -> k (m b) (UnitObject k, m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (m b) (m b, UnitObject k)
forall unit a.
(unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  -- where result = arr $ \b -> (join . fmap (const b)) `inCategoryOf` result $ a


instance (Hask.Applicative m, Hask.Monad m) => Monad m (->) where
  join :: forall a.
(Object (->) a, Object (->) (m a), Object (->) (m (m a))) =>
m (m a) -> m a
join = m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
Hask.join
  

-- | 'Hask.MonadPlus' cannot be adapted quite analogously to 'Monad',
--   since 'mzero' is just a value with no way to indicate its morphism
--   category. The current implementation is probably not ideal, mainly
--   written to give 'MonadFail' ('fail' being needed for @RebindableSyntax@-@do@
--   notation) a mathematically reasonable superclass.
--   
--   Consider these classes provisorial, avoid relying on them explicitly.
class (Monad m k) => MonadZero m k where
  fmzero :: (Object k a, Object k (m a)) => UnitObject k `k` m a

mzero :: (MonadZero m (->)) => m a
mzero :: forall (m :: * -> *) a. MonadZero m (->) => m a
mzero = () -> m a
UnitObject (->) -> m a
forall a.
(Object (->) a, Object (->) (m a)) =>
UnitObject (->) -> m a
forall (m :: * -> *) (k :: * -> * -> *) a.
(MonadZero m k, Object k a, Object k (m a)) =>
k (UnitObject k) (m a)
fmzero ()

class (MonadZero m k) => MonadPlus m k where
  fmplus :: (ObjectPair k (m a) (m a)) => k (m a, m a) (m a)

mplus :: (MonadPlus m (->)) => m a -> m a -> m a
mplus :: forall (m :: * -> *) a. MonadPlus m (->) => m a -> m a -> m a
mplus = ((m a, m a) -> m a) -> m a -> m a -> m a
forall a b c.
(ObjectPair (->) a b, ObjectMorphism (->) b c) =>
((a, b) -> c) -> a -> b -> c
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k (a, b) c -> k a (k b c)
curry (m a, m a) -> m a
forall a. ObjectPair (->) (m a) (m a) => (m a, m a) -> m a
forall (m :: * -> *) (k :: * -> * -> *) a.
(MonadPlus m k, ObjectPair k (m a) (m a)) =>
k (m a, m a) (m a)
fmplus
  
instance (Hask.MonadPlus m, Hask.Applicative m) => MonadZero m (->) where
  fmzero :: forall a.
(Object (->) a, Object (->) (m a)) =>
UnitObject (->) -> m a
fmzero = m a -> () -> m a
forall b x. (Object (->) b, ObjectPoint (->) x) => x -> b -> x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const m a
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
Hask.mzero
instance (Hask.MonadPlus m, Hask.Applicative m) => MonadPlus m (->) where
  fmplus :: forall a. ObjectPair (->) (m a) (m a) => (m a, m a) -> m a
fmplus = (m a -> m a -> m a) -> (m a, m a) -> m a
forall a b c.
(ObjectPair (->) a b, ObjectMorphism (->) b c) =>
(a -> b -> c) -> (a, b) -> c
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry m a -> m a -> m a
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
Hask.mplus


class (MonadPlus m k) => MonadFail m k where
  fail :: (Object k (m a)) => k String (m a) 

instance (Hask.MonadPlus m, Hask.Applicative m, HaskFail.MonadFail m) 
          => MonadFail m (->) where
  fail :: forall a. Object (->) (m a) => String -> m a
fail = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Hask.fail
  

infixr 1 >=>, <=<

(>=>) :: ( Monad m k, Object k a, Object k b, Object k c
         , Object k (m b), Object k (m c), Object k (m (m c)))
       => a `k` m b -> b `k` m c -> a `k` m c
k a (m b)
f >=> :: forall (m :: * -> *) (k :: * -> * -> *) a b c.
(Monad m k, Object k a, Object k b, Object k c, Object k (m b),
 Object k (m c), Object k (m (m c))) =>
k a (m b) -> k b (m c) -> k a (m c)
>=> k b (m c)
g = k (m (m c)) (m c)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m c)) (m c) -> k a (m (m c)) -> k a (m c)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c) -> k (m b) (m (m c))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k b (m c)
g k (m b) (m (m c)) -> k a (m b) -> k a (m (m c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b)
f
(<=<) :: ( Monad m k, Object k a, Object k b, Object k c
         , Object k (m b), Object k (m c), Object k (m (m c)))
       => b `k` m c -> a `k` m b -> a `k` m c
k b (m c)
f <=< :: forall (m :: * -> *) (k :: * -> * -> *) a b c.
(Monad m k, Object k a, Object k b, Object k c, Object k (m b),
 Object k (m c), Object k (m (m c))) =>
k b (m c) -> k a (m b) -> k a (m c)
<=< k a (m b)
g = k (m (m c)) (m c)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m c)) (m c) -> k a (m (m c)) -> k a (m c)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c) -> k (m b) (m (m c))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k b (m c)
f k (m b) (m (m c)) -> k a (m b) -> k a (m (m c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b)
g

newtype Kleisli m k a b = Kleisli { forall (m :: * -> *) (k :: * -> * -> *) a b.
Kleisli m k a b -> k a (m b)
runKleisli :: k a (m b) }

instance (Monad m k) => Category (Kleisli m k) where
  type Object (Kleisli m k) o = (Object k o, Object k (m o), Object k (m (m o)))
  id :: forall a. Object (Kleisli m k) a => Kleisli m k a a
id = k a (m a) -> Kleisli m k a a
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli k a (m a)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure
  Kleisli k b (m c)
a . :: forall a b c.
(Object (Kleisli m k) a, Object (Kleisli m k) b,
 Object (Kleisli m k) c) =>
Kleisli m k b c -> Kleisli m k a b -> Kleisli m k a c
. Kleisli k a (m b)
b = k a (m c) -> Kleisli m k a c
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k a (m c) -> Kleisli m k a c) -> k a (m c) -> Kleisli m k a c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (m (m c)) (m c)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m c)) (m c) -> k a (m (m c)) -> k a (m c)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c) -> k (m b) (m (m c))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k b (m c)
a k (m b) (m (m c)) -> k a (m b) -> k a (m (m c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b)
b

instance ( Monad m a, Cartesian a ) => Cartesian (Kleisli m a) where
  type PairObjects (Kleisli m a) b c 
          = ( ObjectPair a b c
            , ObjectPair a (m b) c, ObjectPair a b (m c), ObjectPair a (m b) (m c) )
  type UnitObject (Kleisli m a) = UnitObject a
  swap :: forall a b.
(ObjectPair (Kleisli m a) a b, ObjectPair (Kleisli m a) b a) =>
Kleisli m a (a, b) (b, a)
swap = a (a, b) (m (b, a)) -> Kleisli m a (a, b) (b, a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (a, b) (m (b, a)) -> Kleisli m a (a, b) (b, a))
-> a (a, b) (m (b, a)) -> Kleisli m a (a, b) (b, a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (b, a) (m (b, a))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (b, a) (m (b, a)) -> a (a, b) (b, a) -> a (a, b) (m (b, a))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (a, b) (b, a)
forall a b. (ObjectPair a a b, ObjectPair a b a) => a (a, b) (b, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (Kleisli m a),
 ObjectPair (Kleisli m a) a unit) =>
Kleisli m a a (a, unit)
attachUnit = a a (m (a, unit)) -> Kleisli m a a (a, unit)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a a (m (a, unit)) -> Kleisli m a a (a, unit))
-> a a (m (a, unit)) -> Kleisli m a a (a, unit)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (a, unit) (m (a, unit))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (a, unit) (m (a, unit)) -> a a (a, unit) -> a a (m (a, unit))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a a (a, unit)
forall unit a.
(unit ~ UnitObject a, ObjectPair a a unit) =>
a a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (Kleisli m a),
 ObjectPair (Kleisli m a) a unit) =>
Kleisli m a (a, unit) a
detachUnit = a (a, unit) (m a) -> Kleisli m a (a, unit) a
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (a, unit) (m a) -> Kleisli m a (a, unit) a)
-> a (a, unit) (m a) -> Kleisli m a (a, unit) a
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a a (m a)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a a (m a) -> a (a, unit) a -> a (a, unit) (m a)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (a, unit) a
forall unit a.
(unit ~ UnitObject a, ObjectPair a a unit) =>
a (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  regroup :: forall a b c.
(ObjectPair (Kleisli m a) a b, ObjectPair (Kleisli m a) b c,
 ObjectPair (Kleisli m a) a (b, c),
 ObjectPair (Kleisli m a) (a, b) c) =>
Kleisli m a (a, (b, c)) ((a, b), c)
regroup = a (a, (b, c)) (m ((a, b), c))
-> Kleisli m a (a, (b, c)) ((a, b), c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (a, (b, c)) (m ((a, b), c))
 -> Kleisli m a (a, (b, c)) ((a, b), c))
-> a (a, (b, c)) (m ((a, b), c))
-> Kleisli m a (a, (b, c)) ((a, b), c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a ((a, b), c) (m ((a, b), c))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a ((a, b), c) (m ((a, b), c))
-> a (a, (b, c)) ((a, b), c) -> a (a, (b, c)) (m ((a, b), c))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (a, (b, c)) ((a, b), c)
forall a b c.
(ObjectPair a a b, ObjectPair a b c, ObjectPair a a (b, c),
 ObjectPair a (a, b) c) =>
a (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup
  regroup' :: forall a b c.
(ObjectPair (Kleisli m a) a b, ObjectPair (Kleisli m a) b c,
 ObjectPair (Kleisli m a) a (b, c),
 ObjectPair (Kleisli m a) (a, b) c) =>
Kleisli m a ((a, b), c) (a, (b, c))
regroup' = a ((a, b), c) (m (a, (b, c)))
-> Kleisli m a ((a, b), c) (a, (b, c))
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a ((a, b), c) (m (a, (b, c)))
 -> Kleisli m a ((a, b), c) (a, (b, c)))
-> a ((a, b), c) (m (a, (b, c)))
-> Kleisli m a ((a, b), c) (a, (b, c))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (a, (b, c)) (m (a, (b, c)))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (a, (b, c)) (m (a, (b, c)))
-> a ((a, b), c) (a, (b, c)) -> a ((a, b), c) (m (a, (b, c)))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a ((a, b), c) (a, (b, c))
forall a b c.
(ObjectPair a a b, ObjectPair a b c, ObjectPair a a (b, c),
 ObjectPair a (a, b) c) =>
a ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'

instance ( Monad m k, CoCartesian k
         , Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))
         ) => CoCartesian (Kleisli m k) where
  type SumObjects (Kleisli m k) b c 
          = ( ObjectSum k b c
            , ObjectSum k (m b) c, ObjectSum k b (m c), ObjectSum k (m b) (m c) )
  type ZeroObject (Kleisli m k) = ZeroObject k
  coSwap :: forall a b.
(ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b a) =>
Kleisli m k (a + b) (b + a)
coSwap = k (a + b) (m (b + a)) -> Kleisli m k (a + b) (b + a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (a + b) (m (b + a)) -> Kleisli m k (a + b) (b + a))
-> k (a + b) (m (b + a)) -> Kleisli m k (a + b) (b + a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (b + a) (m (b + a))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (b + a) (m (b + a)) -> k (a + b) (b + a) -> k (a + b) (m (b + a))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (a + b) (b + a)
forall a b. (ObjectSum k a b, ObjectSum k b a) => k (a + b) (b + a)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: forall a zero.
(Object (Kleisli m k) a, zero ~ ZeroObject (Kleisli m k),
 ObjectSum (Kleisli m k) a zero) =>
Kleisli m k a (a + zero)
attachZero = k a (m (a + zero)) -> Kleisli m k a (a + zero)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k a (m (a + zero)) -> Kleisli m k a (a + zero))
-> k a (m (a + zero)) -> Kleisli m k a (a + zero)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a + zero) (m (a + zero))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + zero) (m (a + zero)) -> k a (a + zero) -> k a (m (a + zero))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (a + zero)
forall a zero.
(Object k a, zero ~ ZeroObject k, ObjectSum k a zero) =>
k a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  detachZero :: forall a zero.
(Object (Kleisli m k) a, zero ~ ZeroObject (Kleisli m k),
 ObjectSum (Kleisli m k) a zero) =>
Kleisli m k (a + zero) a
detachZero = k (a + zero) (m a) -> Kleisli m k (a + zero) a
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (a + zero) (m a) -> Kleisli m k (a + zero) a)
-> k (a + zero) (m a) -> Kleisli m k (a + zero) a
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k a (m a)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k a (m a) -> k (a + zero) a -> k (a + zero) (m a)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (a + zero) a
forall a zero.
(Object k a, zero ~ ZeroObject k, ObjectSum k a zero) =>
k (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  coRegroup :: forall a c b.
(Object (Kleisli m k) a, Object (Kleisli m k) c,
 ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b c,
 ObjectSum (Kleisli m k) a (b + c),
 ObjectSum (Kleisli m k) (a + b) c) =>
Kleisli m k (a + (b + c)) ((a + b) + c)
coRegroup = k (a + (b + c)) (m ((a + b) + c))
-> Kleisli m k (a + (b + c)) ((a + b) + c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (a + (b + c)) (m ((a + b) + c))
 -> Kleisli m k (a + (b + c)) ((a + b) + c))
-> k (a + (b + c)) (m ((a + b) + c))
-> Kleisli m k (a + (b + c)) ((a + b) + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k ((a + b) + c) (m ((a + b) + c))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k ((a + b) + c) (m ((a + b) + c))
-> k (a + (b + c)) ((a + b) + c)
-> k (a + (b + c)) (m ((a + b) + c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (a + (b + c)) ((a + b) + c)
forall a c b.
(Object k a, Object k c, ObjectSum k a b, ObjectSum k b c,
 ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
coRegroup
  coRegroup' :: forall a c b.
(Object (Kleisli m k) a, Object (Kleisli m k) c,
 ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b c,
 ObjectSum (Kleisli m k) a (b + c),
 ObjectSum (Kleisli m k) (a + b) c) =>
Kleisli m k ((a + b) + c) (a + (b + c))
coRegroup' = k ((a + b) + c) (m (a + (b + c)))
-> Kleisli m k ((a + b) + c) (a + (b + c))
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k ((a + b) + c) (m (a + (b + c)))
 -> Kleisli m k ((a + b) + c) (a + (b + c)))
-> k ((a + b) + c) (m (a + (b + c)))
-> Kleisli m k ((a + b) + c) (a + (b + c))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a + (b + c)) (m (a + (b + c)))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + (b + c)) (m (a + (b + c)))
-> k ((a + b) + c) (a + (b + c))
-> k ((a + b) + c) (m (a + (b + c)))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k ((a + b) + c) (a + (b + c))
forall a c b.
(Object k a, Object k c, ObjectSum k a b, ObjectSum k b c,
 ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
coRegroup'
  
  maybeAsSum :: forall u a.
(ObjectSum (Kleisli m k) u a, u ~ UnitObject (Kleisli m k),
 Object (Kleisli m k) (Maybe a)) =>
Kleisli m k (Maybe a) (u + a)
maybeAsSum = k (Maybe a) (m (u + a)) -> Kleisli m k (Maybe a) (u + a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (Maybe a) (m (u + a)) -> Kleisli m k (Maybe a) (u + a))
-> k (Maybe a) (m (u + a)) -> Kleisli m k (Maybe a) (u + a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (u + a) (m (u + a))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (u + a) (m (u + a))
-> k (Maybe a) (u + a) -> k (Maybe a) (m (u + a))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (Maybe a) (u + a)
forall u a.
(ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) =>
k (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  maybeFromSum :: forall u a.
(ObjectSum (Kleisli m k) u a, u ~ UnitObject (Kleisli m k),
 Object (Kleisli m k) (Maybe a)) =>
Kleisli m k (u + a) (Maybe a)
maybeFromSum = k (u + a) (m (Maybe a)) -> Kleisli m k (u + a) (Maybe a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (u + a) (m (Maybe a)) -> Kleisli m k (u + a) (Maybe a))
-> k (u + a) (m (Maybe a)) -> Kleisli m k (u + a) (Maybe a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (Maybe a) (m (Maybe a))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (Maybe a) (m (Maybe a))
-> k (u + a) (Maybe a) -> k (u + a) (m (Maybe a))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (u + a) (Maybe a)
forall u a.
(ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) =>
k (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  boolAsSum :: forall u.
(ObjectSum (Kleisli m k) u u, u ~ UnitObject (Kleisli m k),
 Object (Kleisli m k) Bool) =>
Kleisli m k Bool (u + u)
boolAsSum = k Bool (m (u + u)) -> Kleisli m k Bool (u + u)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k Bool (m (u + u)) -> Kleisli m k Bool (u + u))
-> k Bool (m (u + u)) -> Kleisli m k Bool (u + u)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (u + u) (m (u + u))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (u + u) (m (u + u)) -> k Bool (u + u) -> k Bool (m (u + u))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k Bool (u + u)
forall u.
(ObjectSum k u u, u ~ UnitObject k, Object k Bool) =>
k Bool (u + u)
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum
  boolFromSum :: forall u.
(ObjectSum (Kleisli m k) u u, u ~ UnitObject (Kleisli m k),
 Object (Kleisli m k) Bool) =>
Kleisli m k (u + u) Bool
boolFromSum = k (u + u) (m Bool) -> Kleisli m k (u + u) Bool
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (u + u) (m Bool) -> Kleisli m k (u + u) Bool)
-> k (u + u) (m Bool) -> Kleisli m k (u + u) Bool
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k Bool (m Bool)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k Bool (m Bool) -> k (u + u) Bool -> k (u + u) (m Bool)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (u + u) Bool
forall u.
(ObjectSum k u u, u ~ UnitObject k, Object k Bool) =>
k (u + u) Bool
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum
  
instance ( Monad m a, Arrow a (->), Function a ) => Curry (Kleisli m a) where
  type MorphObjects (Kleisli m a) c d
          = ( Object a (Kleisli m a c d), Object a (m (Kleisli m a c d))
            , Object a (a c (m d))
            , ObjectMorphism a c d, ObjectMorphism a c (m d), ObjectMorphism a c (m (m d)) )
  curry :: forall a b c.
(ObjectPair (Kleisli m a) a b, ObjectMorphism (Kleisli m a) b c) =>
Kleisli m a (a, b) c -> Kleisli m a a (Kleisli m a b c)
curry (Kleisli a (a, b) (m c)
fUnc) = a a (m (Kleisli m a b c)) -> Kleisli m a a (Kleisli m a b c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a a (m (Kleisli m a b c)) -> Kleisli m a a (Kleisli m a b c))
-> a a (m (Kleisli m a b c)) -> Kleisli m a a (Kleisli m a b c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (Kleisli m a b c) (m (Kleisli m a b c))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (Kleisli m a b c) (m (Kleisli m a b c))
-> a a (Kleisli m a b c) -> a a (m (Kleisli m a b c))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (a b (m c) -> Kleisli m a b c) -> a (a b (m c)) (Kleisli m a b c)
forall b c.
(Object (->) b, Object (->) c, Object a b, Object a c) =>
(b -> c) -> a b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr a b (m c) -> Kleisli m a b c
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli a (a b (m c)) (Kleisli m a b c)
-> a a (a b (m c)) -> a a (Kleisli m a b c)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (a, b) (m c) -> a a (a b (m c))
forall a b c.
(ObjectPair a a b, ObjectMorphism a b c) =>
a (a, b) c -> a a (a b c)
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k (a, b) c -> k a (k b c)
curry a (a, b) (m c)
fUnc
  uncurry :: forall a b c.
(ObjectPair (Kleisli m a) a b, ObjectMorphism (Kleisli m a) b c) =>
Kleisli m a a (Kleisli m a b c) -> Kleisli m a (a, b) c
uncurry (Kleisli a a (m (Kleisli m a b c))
fCur) = a (a, b) (m c) -> Kleisli m a (a, b) c
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (a, b) (m c) -> Kleisli m a (a, b) c)
-> (((a, b) -> m c) -> a (a, b) (m c))
-> ((a, b) -> m c)
-> Kleisli m a (a, b) c
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. ((a, b) -> m c) -> a (a, b) (m c)
forall b c.
(Object (->) b, Object (->) c, Object a b, Object a c) =>
(b -> c) -> a b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr (((a, b) -> m c) -> Kleisli m a (a, b) c)
-> ((a, b) -> m c) -> Kleisli m a (a, b) c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 
               \(a
b,b
c) -> a (m (m c)) (m c)
forall a.
(Object a a, Object a (m a), Object a (m (m a))) =>
a (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join a (m (m c)) (m c) -> a a (m (m c)) -> a a (m c)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (Kleisli m a b c) (m c) -> a (m (Kleisli m a b c)) (m (m c))
forall a b.
(Object a a, Object a (m a), Object a b, Object a (m b)) =>
a a b -> a (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap ((Kleisli m a b c -> m c) -> a (Kleisli m a b c) (m c)
forall b c.
(Object (->) b, Object (->) c, Object a b, Object a c) =>
(b -> c) -> a b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr ((Kleisli m a b c -> m c) -> a (Kleisli m a b c) (m c))
-> (Kleisli m a b c -> m c) -> a (Kleisli m a b c) (m c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (a b (m c) -> b -> m c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$b
c) (a b (m c) -> m c)
-> (Kleisli m a b c -> a b (m c)) -> Kleisli m a b c -> m c
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. Kleisli m a b c -> a b (m c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
Kleisli m k a b -> k a (m b)
runKleisli) a (m (Kleisli m a b c)) (m (m c))
-> a a (m (Kleisli m a b c)) -> a a (m (m c))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a a (m (Kleisli m a b c))
fCur a a (m c) -> a -> m c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a
b
  

  

instance (Monad m a, Arrow a q, Cartesian a) => EnhancedCat (Kleisli m a) q where
  arr :: forall b c.
(Object q b, Object q c, Object (Kleisli m a) b,
 Object (Kleisli m a) c) =>
q b c -> Kleisli m a b c
arr q b c
f = a b (m c) -> Kleisli m a b c
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a b (m c) -> Kleisli m a b c) -> a b (m c) -> Kleisli m a b c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a c (m c)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a c (m c) -> a b c -> a b (m c)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. q b c -> a b c
forall b c.
(Object q b, Object q c, Object a b, Object a c) =>
q b c -> a b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr q b c
f
instance (Monad m a, Morphism a, Curry a) => Morphism (Kleisli m a) where
  first :: forall b d c.
(ObjectPair (Kleisli m a) b d, ObjectPair (Kleisli m a) c d) =>
Kleisli m a b c -> Kleisli m a (b, d) (c, d)
first (Kleisli a b (m c)
f) = a (b, d) (m (c, d)) -> Kleisli m a (b, d) (c, d)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (b, d) (m (c, d)) -> Kleisli m a (b, d) (c, d))
-> a (b, d) (m (c, d)) -> Kleisli m a (b, d) (c, d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (m c, m d) (m (c, d))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip a (m c, m d) (m (c, d))
-> a (b, d) (m c, m d) -> a (b, d) (m (c, d))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (a b (m c)
f a b (m c) -> a d (m d) -> a (b, d) (m c, m d)
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a d (m d)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure)
  second :: forall d b c.
(ObjectPair (Kleisli m a) d b, ObjectPair (Kleisli m a) d c) =>
Kleisli m a b c -> Kleisli m a (d, b) (d, c)
second (Kleisli a b (m c)
f) = a (d, b) (m (d, c)) -> Kleisli m a (d, b) (d, c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (d, b) (m (d, c)) -> Kleisli m a (d, b) (d, c))
-> a (d, b) (m (d, c)) -> Kleisli m a (d, b) (d, c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (m d, m c) (m (d, c))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip a (m d, m c) (m (d, c))
-> a (d, b) (m d, m c) -> a (d, b) (m (d, c))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (a d (m d)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a d (m d) -> a b (m c) -> a (d, b) (m d, m c)
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a b (m c)
f)
  Kleisli a b (m c)
f *** :: forall b b' c c'.
(ObjectPair (Kleisli m a) b b', ObjectPair (Kleisli m a) c c') =>
Kleisli m a b c -> Kleisli m a b' c' -> Kleisli m a (b, b') (c, c')
*** Kleisli a b' (m c')
g = a (b, b') (m (c, c')) -> Kleisli m a (b, b') (c, c')
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (b, b') (m (c, c')) -> Kleisli m a (b, b') (c, c'))
-> a (b, b') (m (c, c')) -> Kleisli m a (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (m c, m c') (m (c, c'))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip a (m c, m c') (m (c, c'))
-> a (b, b') (m c, m c') -> a (b, b') (m (c, c'))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (a b (m c)
f a b (m c) -> a b' (m c') -> a (b, b') (m c, m c')
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a b' (m c')
g)
instance (Monad m a, PreArrow a, Curry a) => PreArrow (Kleisli m a) where
  Kleisli a b (m c)
f &&& :: forall b c c'.
(Object (Kleisli m a) b, ObjectPair (Kleisli m a) c c') =>
Kleisli m a b c -> Kleisli m a b c' -> Kleisli m a b (c, c')
&&& Kleisli a b (m c')
g = a b (m (c, c')) -> Kleisli m a b (c, c')
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a b (m (c, c')) -> Kleisli m a b (c, c'))
-> a b (m (c, c')) -> Kleisli m a b (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (m c, m c') (m (c, c'))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip a (m c, m c') (m (c, c')) -> a b (m c, m c') -> a b (m (c, c'))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (a b (m c)
f a b (m c) -> a b (m c') -> a b (m c, m c')
forall b c c'.
(Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& a b (m c')
g)
  terminal :: forall b.
Object (Kleisli m a) b =>
Kleisli m a b (UnitObject (Kleisli m a))
terminal = a b (m (UnitObject a)) -> Kleisli m a b (UnitObject a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a b (m (UnitObject a)) -> Kleisli m a b (UnitObject a))
-> a b (m (UnitObject a)) -> Kleisli m a b (UnitObject a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (UnitObject a) (m (UnitObject a))
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (UnitObject a) (m (UnitObject a))
-> a b (UnitObject a) -> a b (m (UnitObject a))
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a b (UnitObject a)
forall b. Object a b => a b (UnitObject a)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  fst :: forall x y. ObjectPair (Kleisli m a) x y => Kleisli m a (x, y) x
fst = a (x, y) (m x) -> Kleisli m a (x, y) x
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (x, y) (m x) -> Kleisli m a (x, y) x)
-> a (x, y) (m x) -> Kleisli m a (x, y) x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a x (m x)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a x (m x) -> a (x, y) x -> a (x, y) (m x)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (x, y) x
forall x y. ObjectPair a x y => a (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  snd :: forall x y. ObjectPair (Kleisli m a) x y => Kleisli m a (x, y) y
snd = a (x, y) (m y) -> Kleisli m a (x, y) y
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (x, y) (m y) -> Kleisli m a (x, y) y)
-> a (x, y) (m y) -> Kleisli m a (x, y) y
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a y (m y)
forall a. (Object a a, Object a (m a)) => a a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a y (m y) -> a (x, y) y -> a (x, y) (m y)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (x, y) y
forall x y. ObjectPair a x y => a (x, y) y
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd
instance (SPDistribute k, Monad m k, PreArrow (Kleisli m k), PreArrChoice (Kleisli m k)) 
             => SPDistribute (Kleisli m k) where
  distribute :: forall a b c.
(ObjectSum (Kleisli m k) (a, b) (a, c),
 ObjectPair (Kleisli m k) a (b + c), ObjectSum (Kleisli m k) b c,
 PairObjects (Kleisli m k) a b, PairObjects (Kleisli m k) a c) =>
Kleisli m k (a, b + c) ((a, b) + (a, c))
distribute = k (a, b + c) (m ((a, b) + (a, c)))
-> Kleisli m k (a, b + c) ((a, b) + (a, c))
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (a, b + c) (m ((a, b) + (a, c)))
 -> Kleisli m k (a, b + c) ((a, b) + (a, c)))
-> k (a, b + c) (m ((a, b) + (a, c)))
-> Kleisli m k (a, b + c) ((a, b) + (a, c))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k ((a, b) + (a, c)) (m ((a, b) + (a, c)))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k ((a, b) + (a, c)) (m ((a, b) + (a, c)))
-> k (a, b + c) ((a, b) + (a, c))
-> k (a, b + c) (m ((a, b) + (a, c)))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (a, b + c) ((a, b) + (a, c))
forall a b c.
(ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
distribute
  unDistribute :: forall a b c.
(ObjectSum (Kleisli m k) (a, b) (a, c),
 ObjectPair (Kleisli m k) a (b + c), ObjectSum (Kleisli m k) b c,
 PairObjects (Kleisli m k) a b, PairObjects (Kleisli m k) a c) =>
Kleisli m k ((a, b) + (a, c)) (a, b + c)
unDistribute = k ((a, b) + (a, c)) (m (a, b + c))
-> Kleisli m k ((a, b) + (a, c)) (a, b + c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k ((a, b) + (a, c)) (m (a, b + c))
 -> Kleisli m k ((a, b) + (a, c)) (a, b + c))
-> k ((a, b) + (a, c)) (m (a, b + c))
-> Kleisli m k ((a, b) + (a, c)) (a, b + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a, b + c) (m (a, b + c))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a, b + c) (m (a, b + c))
-> k ((a, b) + (a, c)) (a, b + c)
-> k ((a, b) + (a, c)) (m (a, b + c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k ((a, b) + (a, c)) (a, b + c)
forall a b c.
(ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
unDistribute
  boolAsSwitch :: forall a.
(ObjectSum (Kleisli m k) a a, ObjectPair (Kleisli m k) Bool a) =>
Kleisli m k (Bool, a) (a + a)
boolAsSwitch = k (Bool, a) (m (a + a)) -> Kleisli m k (Bool, a) (a + a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (Bool, a) (m (a + a)) -> Kleisli m k (Bool, a) (a + a))
-> k (Bool, a) (m (a + a)) -> Kleisli m k (Bool, a) (a + a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a + a) (m (a + a))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + a) (m (a + a))
-> k (Bool, a) (a + a) -> k (Bool, a) (m (a + a))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (Bool, a) (a + a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
  boolFromSwitch :: forall a.
(ObjectSum (Kleisli m k) a a, ObjectPair (Kleisli m k) Bool a) =>
Kleisli m k (a + a) (Bool, a)
boolFromSwitch = k (a + a) (m (Bool, a)) -> Kleisli m k (a + a) (Bool, a)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (a + a) (m (Bool, a)) -> Kleisli m k (a + a) (Bool, a))
-> k (a + a) (m (Bool, a)) -> Kleisli m k (a + a) (Bool, a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (Bool, a) (m (Bool, a))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (Bool, a) (m (Bool, a))
-> k (a + a) (Bool, a) -> k (a + a) (m (Bool, a))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (a + a) (Bool, a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
boolFromSwitch
instance (Monad m a, WellPointed a, ObjectPoint a (m (UnitObject a))) 
             => WellPointed (Kleisli m a) where
  type PointObject (Kleisli m a) b = (PointObject a b, PointObject a (m b))
  globalElement :: forall x.
ObjectPoint (Kleisli m a) x =>
x -> Kleisli m a (UnitObject (Kleisli m a)) x
globalElement x
x = a (UnitObject a) (m x) -> Kleisli m a (UnitObject a) x
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (a (UnitObject a) (m x) -> Kleisli m a (UnitObject a) x)
-> a (UnitObject a) (m x) -> Kleisli m a (UnitObject a) x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a (UnitObject a) x -> a (m (UnitObject a)) (m x)
forall a b.
(Object a a, Object a (m a), Object a b, Object a (m b)) =>
a a b -> a (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (x -> a (UnitObject a) x
forall x. ObjectPoint a x => x -> a (UnitObject a) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x) a (m (UnitObject a)) (m x)
-> a (UnitObject a) (m (UnitObject a)) -> a (UnitObject a) (m x)
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a (UnitObject a) (m (UnitObject a))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *).
Monoidal f r t =>
t (UnitObject t) (f (UnitObject r))
pureUnit
  unit :: CatTagged (Kleisli m a) (UnitObject (Kleisli m a))
unit = CatTagged (Kleisli m a) (UnitObject a)
CatTagged (Kleisli m a) (UnitObject (Kleisli m a))
forall (m :: * -> *) (a :: * -> * -> *).
(Monad m a, WellPointed a) =>
CatTagged (Kleisli m a) (UnitObject a)
kleisliUnit


-- | /Hask/-Kleislis inherit more or less trivially 'Hask.ArrowChoice'; however this
--   does not generalise greatly well to non-function categories.
instance ( Monad m k, Arrow k (->), Function k, PreArrChoice k
         , Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))
         ) => MorphChoice (Kleisli m k) where
  left :: forall b d c.
(ObjectSum (Kleisli m k) b d, ObjectSum (Kleisli m k) c d) =>
Kleisli m k b c -> Kleisli m k (b + d) (c + d)
left (Kleisli k b (m c)
f) = k (Either b d) (m (c + d)) -> Kleisli m k (Either b d) (c + d)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (Either b d) (m (c + d)) -> Kleisli m k (Either b d) (c + d))
-> ((Either b d -> m (c + d)) -> k (Either b d) (m (c + d)))
-> (Either b d -> m (c + d))
-> Kleisli m k (Either b d) (c + d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (Either b d -> m (c + d)) -> k (Either b d) (m (c + d))
forall b c.
(Object (->) b, Object (->) c, Object k b, Object k c) =>
(b -> c) -> k b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr ((Either b d -> m (c + d)) -> Kleisli m k (Either b d) (c + d))
-> (Either b d -> m (c + d)) -> Kleisli m k (Either b d) (c + d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case { Left b
x -> k c (c + d) -> k (m c) (m (c + d))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k c (c + d)
forall a b. ObjectSum k a b => k a (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst k (m c) (m (c + d)) -> k b (m c) -> k b (m (c + d))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c)
f k b (m (c + d)) -> b -> m (c + d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
x
                                           ; Right d
y-> (k (c + d) (m (c + d))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (c + d) (m (c + d)) -> k d (c + d) -> k d (m (c + d))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k d (c + d)
forall a b. ObjectSum k a b => k b (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd)k d (m (c + d)) -> k b (m c) -> k d (m (c + d))
forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf`k b (m c)
f k d (m (c + d)) -> d -> m (c + d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ d
y }
  right :: forall d b c.
(ObjectSum (Kleisli m k) d b, ObjectSum (Kleisli m k) d c) =>
Kleisli m k b c -> Kleisli m k (d + b) (d + c)
right(Kleisli k b (m c)
f) = k (Either d b) (m (d + c)) -> Kleisli m k (Either d b) (d + c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (Either d b) (m (d + c)) -> Kleisli m k (Either d b) (d + c))
-> ((Either d b -> m (d + c)) -> k (Either d b) (m (d + c)))
-> (Either d b -> m (d + c))
-> Kleisli m k (Either d b) (d + c)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (Either d b -> m (d + c)) -> k (Either d b) (m (d + c))
forall b c.
(Object (->) b, Object (->) c, Object k b, Object k c) =>
(b -> c) -> k b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr ((Either d b -> m (d + c)) -> Kleisli m k (Either d b) (d + c))
-> (Either d b -> m (d + c)) -> Kleisli m k (Either d b) (d + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case { Left d
x -> (k (d + c) (m (d + c))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (d + c) (m (d + c)) -> k d (d + c) -> k d (m (d + c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k d (d + c)
forall a b. ObjectSum k a b => k a (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst)k d (m (d + c)) -> k b (m c) -> k d (m (d + c))
forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf`k b (m c)
f k d (m (d + c)) -> d -> m (d + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ d
x
                                           ; Right b
y-> k c (d + c) -> k (m c) (m (d + c))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k c (d + c)
forall a b. ObjectSum k a b => k b (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd k (m c) (m (d + c)) -> k b (m c) -> k b (m (d + c))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c)
f k b (m (d + c)) -> b -> m (d + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
y                }
  Kleisli k b (m c)
f +++ :: forall b b' c c'.
(ObjectSum (Kleisli m k) b b', ObjectSum (Kleisli m k) c c') =>
Kleisli m k b c
-> Kleisli m k b' c' -> Kleisli m k (b + b') (c + c')
+++ Kleisli k b' (m c')
g = k (Either b b') (m (c + c')) -> Kleisli m k (Either b b') (c + c')
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (Either b b') (m (c + c'))
 -> Kleisli m k (Either b b') (c + c'))
-> ((Either b b' -> m (c + c')) -> k (Either b b') (m (c + c')))
-> (Either b b' -> m (c + c'))
-> Kleisli m k (Either b b') (c + c')
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (Either b b' -> m (c + c')) -> k (Either b b') (m (c + c'))
forall b c.
(Object (->) b, Object (->) c, Object k b, Object k c) =>
(b -> c) -> k b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr ((Either b b' -> m (c + c')) -> Kleisli m k (Either b b') (c + c'))
-> (Either b b' -> m (c + c'))
-> Kleisli m k (Either b b') (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case
       Left b
x  -> k c (c + c') -> k (m c) (m (c + c'))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k c (c + c')
forall a b. ObjectSum k a b => k a (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst k (m c) (m (c + c')) -> k b (m c) -> k b (m (c + c'))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (m c)
f k b (m (c + c')) -> b -> m (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
x
       Right b'
y -> k c' (c + c') -> k (m c') (m (c + c'))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k c' (c + c')
forall a b. ObjectSum k a b => k b (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd k (m c') (m (c + c')) -> k b' (m c') -> k b' (m (c + c'))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b' (m c')
g k b' (m (c + c')) -> b' -> m (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b'
y
instance ( Monad m k, Arrow k (->), Function k, PreArrChoice k
         , Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))
         ) => PreArrChoice (Kleisli m k) where
  Kleisli k b (m c)
f ||| :: forall b b' c.
(ObjectSum (Kleisli m k) b b', Object (Kleisli m k) c) =>
Kleisli m k b c -> Kleisli m k b' c -> Kleisli m k (b + b') c
||| Kleisli k b' (m c)
g = k (b + b') (m c) -> Kleisli m k (b + b') c
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (b + b') (m c) -> Kleisli m k (b + b') c)
-> k (b + b') (m c) -> Kleisli m k (b + b') c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b (m c)
f k b (m c) -> k b' (m c) -> k (b + b') (m c)
forall b b' c.
(ObjectSum k b b', Object k c) =>
k b c -> k b' c -> k (b + b') c
forall (k :: * -> * -> *) b b' c.
(PreArrChoice k, ObjectSum k b b', Object k c) =>
k b c -> k b' c -> k (b + b') c
||| k b' (m c)
g
  initial :: forall b.
Object (Kleisli m k) b =>
Kleisli m k (ZeroObject (Kleisli m k)) b
initial = k (ZeroObject k) (m b) -> Kleisli m k (ZeroObject k) b
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (ZeroObject k) (m b) -> Kleisli m k (ZeroObject k) b)
-> k (ZeroObject k) (m b) -> Kleisli m k (ZeroObject k) b
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b (m b)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k b (m b) -> k (ZeroObject k) b -> k (ZeroObject k) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (ZeroObject k) b
forall b. Object k b => k (ZeroObject k) b
forall (k :: * -> * -> *) b.
(PreArrChoice k, Object k b) =>
k (ZeroObject k) b
initial
  coFst :: forall a b. ObjectSum (Kleisli m k) a b => Kleisli m k a (a + b)
coFst = k a (m (a + b)) -> Kleisli m k a (a + b)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k a (m (a + b)) -> Kleisli m k a (a + b))
-> k a (m (a + b)) -> Kleisli m k a (a + b)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a + b) (m (a + b))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + b) (m (a + b)) -> k a (a + b) -> k a (m (a + b))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (a + b)
forall a b. ObjectSum k a b => k a (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst
  coSnd :: forall a b. ObjectSum (Kleisli m k) a b => Kleisli m k b (a + b)
coSnd = k b (m (a + b)) -> Kleisli m k b (a + b)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k b (m (a + b)) -> Kleisli m k b (a + b))
-> k b (m (a + b)) -> Kleisli m k b (a + b)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (a + b) (m (a + b))
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + b) (m (a + b)) -> k b (a + b) -> k b (m (a + b))
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b (a + b)
forall a b. ObjectSum k a b => k b (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd


kleisliUnit :: forall m a . (Monad m a, WellPointed a)
                    => CatTagged (Kleisli m a) (UnitObject a)
kleisliUnit :: forall (m :: * -> *) (a :: * -> * -> *).
(Monad m a, WellPointed a) =>
CatTagged (Kleisli m a) (UnitObject a)
kleisliUnit = Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
-> Tagged
     (Kleisli m a (UnitObject a) (UnitObject a)) (UnitObject a)
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: CatTagged a (UnitObject a))


guard ::( MonadPlus m k, Arrow k (->), Function k
        , UnitObject k ~ (), Object k Bool
        ) => Bool `k` m ()
guard :: forall (m :: * -> *) (k :: * -> * -> *).
(MonadPlus m k, Arrow k (->), Function k, UnitObject k ~ (),
 Object k Bool) =>
k Bool (m ())
guard = k (m ()) (m ())
i k (m ()) (m ()) -> k Bool (m ()) -> k Bool (m ())
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (UnitObject k) (m ()) -> k (UnitObject k) (m ()) -> k Bool (m ())
forall (f :: * -> * -> *) a.
(Arrow f (->), Function f, Object f Bool, Object f a) =>
f (UnitObject f) a -> f (UnitObject f) a -> f Bool a
choose k (UnitObject k) (m ())
forall a. (Object k a, Object k (m a)) => k (UnitObject k) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(MonadZero m k, Object k a, Object k (m a)) =>
k (UnitObject k) (m a)
fmzero k () (m ())
k (UnitObject k) (m ())
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure
 where i :: k (m ()) (m ())
i = k (m ()) (m ())
forall a. Object k a => k a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id


when :: ( Monad m k, PreArrow k, u ~ UnitObject k
        , ObjectPair k (m u) u
        ) => Bool -> m u `k` m u
when :: forall (m :: * -> *) (k :: * -> * -> *) u.
(Monad m k, PreArrow k, u ~ UnitObject k, ObjectPair k (m u) u) =>
Bool -> k (m u) (m u)
when Bool
True = k (m u) (m u)
forall a. Object k a => k a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
when Bool
False = k u (m u)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k u (m u) -> k (m u) u -> k (m u) (m u)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (m u) u
k (m u) (UnitObject k)
forall b. Object k b => k b (UnitObject k)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
unless :: ( Monad m k, PreArrow k, u ~ UnitObject k
        , ObjectPair k (m u) u
        ) => Bool -> m u `k` m u
unless :: forall (m :: * -> *) (k :: * -> * -> *) u.
(Monad m k, PreArrow k, u ~ UnitObject k, ObjectPair k (m u) u) =>
Bool -> k (m u) (m u)
unless Bool
False = k (m u) (m u)
forall a. Object k a => k a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
unless Bool
True = k u (m u)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k u (m u) -> k (m u) u -> k (m u) (m u)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k (m u) u
k (m u) (UnitObject k)
forall b. Object k b => k b (UnitObject k)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal


filterM :: ( PreArrow k, Monad m k, SumToProduct c k k, EndoTraversable c k
           , ObjectPair k Bool a, Object k (c a), Object k (m (c a))
           , ObjectPair k (Bool, a) (c (Bool, a))
           , ObjectPair k (m Bool) (m a)
           , ObjectPair k (m (Bool, a)) (m (c (Bool, a)))
           , TraversalObject k c (Bool, a)
           ) => a `k` m Bool -> c a `k` m (c a)
filterM :: forall (k :: * -> * -> *) (m :: * -> *) (c :: * -> *) a.
(PreArrow k, Monad m k, SumToProduct c k k, EndoTraversable c k,
 ObjectPair k Bool a, Object k (c a), Object k (m (c a)),
 ObjectPair k (Bool, a) (c (Bool, a)), ObjectPair k (m Bool) (m a),
 ObjectPair k (m (Bool, a)) (m (c (Bool, a))),
 TraversalObject k c (Bool, a)) =>
k a (m Bool) -> k (c a) (m (c a))
filterM k a (m Bool)
pg = k (c (Bool, a)) (c a) -> k (m (c (Bool, a))) (m (c a))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (k (Bool, a) a -> k (c (Bool, a)) (c a)
forall a b.
(Object k a, Object k (c a), Object k b, Object k (c b)) =>
k a b -> k (c a) (c b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k (Bool, a) a
forall x y. ObjectPair k x y => k (x, y) y
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd k (c (Bool, a)) (c a)
-> k (c (Bool, a)) (c (Bool, a)) -> k (c (Bool, a)) (c a)
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
<<< k (Bool, a) Bool -> k (c (Bool, a)) (c (Bool, a))
forall a.
(Object k a, Object k Bool, Object k (c a)) =>
k a Bool -> k (c a) (c a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(SumToProduct f r t, Object r a, Object r Bool, Object t (f a)) =>
r a Bool -> t (f a) (f a)
filter k (Bool, a) Bool
forall x y. ObjectPair k x y => k (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) k (m (c (Bool, a))) (m (c a))
-> k (c a) (m (c (Bool, a))) -> k (c a) (m (c a))
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
<<< k a (m (Bool, a)) -> k (c a) (m (c (Bool, a)))
forall (m :: * -> *) a b.
(k ~ k, c ~ c, Applicative m k k, Object k a, Object k (c a),
 ObjectPair k b (c b), ObjectPair k (m b) (m (c b)),
 TraversalObject k c b) =>
k a (m b) -> k (c a) (m (c b))
forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (m :: * -> *) a b.
(Traversable s t k l, k ~ l, s ~ t, Applicative m k k, Object k a,
 Object k (t a), ObjectPair k b (t b), ObjectPair k (m b) (m (t b)),
 TraversalObject k t b) =>
k a (m b) -> k (t a) (m (t b))
mapM (k (m Bool, m a) (m (Bool, a))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip k (m Bool, m a) (m (Bool, a))
-> k a (m Bool, m a) -> k a (m (Bool, a))
forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
<<< k a (m Bool)
pg k a (m Bool) -> k a (m a) -> k a (m Bool, m a)
forall b c c'.
(Object k b, ObjectPair k c c') =>
k b c -> k b c' -> k b (c, c')
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& k a (m a)
forall a. (Object k a, Object k (m a)) => k a (m a)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure)
    


forever :: ( Monad m k, Function k, Arrow k (->), Object k a, Object k b 
           , Object k (m a), Object k (m (m a)), ObjectPoint k (m b), Object k (m (m b))
           ) => m a `k` m b
forever :: forall (m :: * -> *) (k :: * -> * -> *) a b.
(Monad m k, Function k, Arrow k (->), Object k a, Object k b,
 Object k (m a), Object k (m (m a)), ObjectPoint k (m b),
 Object k (m (m b))) =>
k (m a) (m b)
forever = k (m b) (m b)
i k (m b) (m b) -> k (m a) (m b) -> k (m a) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (m a -> m b) -> k (m a) (m b)
forall b c.
(Object (->) b, Object (->) c, Object k b, Object k c) =>
(b -> c) -> k b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr m a -> m b
loop 
    where loop :: m a -> m b
loop m a
a = (k (m (m b)) (m b)
forall a.
(Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
forall (m :: * -> *) (k :: * -> * -> *) a.
(Monad m k, Object k a, Object k (m a), Object k (m (m a))) =>
k (m (m a)) (m a)
join k (m (m b)) (m b) -> k (m a) (m (m b)) -> k (m a) (m b)
forall a b c.
(Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a (m b) -> k (m a) (m (m b))
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (m b -> k a (m b)
forall b x. (Object k b, ObjectPoint k x) => x -> k b x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (m b -> k a (m b)) -> m b -> k a (m b)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m a -> m b
loop m a
a)) k (m a) (m b) -> k (m b) (m b) -> k (m a) (m b)
forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf` k (m b) (m b)
i k (m a) (m b) -> m a -> m b
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m a
a
          i :: k (m b) (m b)
i = k (m b) (m b)
forall a. Object k a => k a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

void :: ( Monad m k, PreArrow k
        , Object k a, Object k (m a), ObjectPair k a u, u ~ UnitObject k 
        ) => m a `k` m (UnitObject k)
void :: forall (m :: * -> *) (k :: * -> * -> *) a u.
(Monad m k, PreArrow k, Object k a, Object k (m a),
 ObjectPair k a u, u ~ UnitObject k) =>
k (m a) (m (UnitObject k))
void = k a u -> k (m a) (m u)
forall a b.
(Object k a, Object k (m a), Object k b, Object k (m b)) =>
k a b -> k (m a) (m b)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap k a u
k a (UnitObject k)
forall b. Object k b => k b (UnitObject k)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal