-- |
-- 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.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 :: a -> m a
return = 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)
=<< :: k a (m b) -> k (m a) (m b)
(=<<) k a (m b)
q = k (m (m b)) (m b)
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 κ (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 (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 >>= :: 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)
<< :: m b -> k (m a) (m b)
(<<) m b
b = k (m (m b)) (m b)
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 κ (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 (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 (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)
>> :: m a -> k (m b) (m b)
(>>) m a
a = k (a, b) b -> k (m (a, b)) (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 (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 κ (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 κ (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 (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 (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 κ (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 (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 κ (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 (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 :: 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 :: m a
mzero = () -> 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 :: m a -> m a -> m a
mplus = ((m a, m a) -> m a) -> m a -> m a -> m a
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 (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 :: UnitObject (->) -> m a
fmzero = m a -> () -> m a
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const m a
forall (m :: * -> *) a. MonadPlus m => m a
Hask.mzero
instance (Hask.MonadPlus m, Hask.Applicative m) => MonadPlus m (->) where
  fmplus :: (m a, m a) -> m a
fmplus = (m a -> m a -> m a) -> (m a, m a) -> m a
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 (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 :: String -> m a
fail = 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 >=> :: k a (m b) -> k b (m c) -> k a (m c)
>=> k b (m c)
g = k (m (m c)) (m c)
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 κ (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 (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 κ (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 <=< :: k b (m c) -> k a (m b) -> k a (m c)
<=< k a (m b)
g = k (m (m c)) (m c)
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 κ (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 (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 κ (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 { 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 :: 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 (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 . :: 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 (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 κ (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 (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 κ (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 :: 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 (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 κ (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 (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: Kleisli m a a (a, unit)
attachUnit = a a (m (a, UnitObject a)) -> 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, UnitObject a)) -> Kleisli m a a (a, unit))
-> a a (m (a, UnitObject a)) -> 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, UnitObject a) (m (a, UnitObject a))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure a (a, UnitObject a) (m (a, UnitObject a))
-> a a (a, UnitObject a) -> a a (m (a, UnitObject 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
. a a (a, UnitObject a)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  detachUnit :: Kleisli m a (a, unit) a
detachUnit = a (a, UnitObject a) (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, UnitObject a) (m a) -> Kleisli m a (a, unit) a)
-> a (a, UnitObject a) (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 (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, UnitObject a) a -> a (a, UnitObject a) (m 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
. a (a, UnitObject a) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  regroup :: 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 (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 κ (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 (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' :: 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 (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 κ (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 (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 :: 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 (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 κ (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 (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: Kleisli m k a (a + zero)
attachZero = k a (m (a + ZeroObject k)) -> 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 + ZeroObject k)) -> Kleisli m k a (a + zero))
-> k a (m (a + ZeroObject k)) -> 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 + ZeroObject k) (m (a + ZeroObject k))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (a + ZeroObject k) (m (a + ZeroObject k))
-> k a (a + ZeroObject k) -> k a (m (a + ZeroObject k))
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 + ZeroObject k)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  detachZero :: Kleisli m k (a + zero) a
detachZero = k (a + ZeroObject k) (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 + ZeroObject k) (m a) -> Kleisli m k (a + zero) a)
-> k (a + ZeroObject k) (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 (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 + ZeroObject k) a -> k (a + ZeroObject k) (m 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 + ZeroObject k) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  coRegroup :: 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 (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 κ (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 (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' :: 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 (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 κ (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 (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 :: Kleisli m k (Maybe a) (u + a)
maybeAsSum = k (Maybe a) (m (UnitObject k + 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 (UnitObject k + a))
 -> Kleisli m k (Maybe a) (u + a))
-> k (Maybe a) (m (UnitObject k + 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 (UnitObject k + a) (m (UnitObject k + a))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (UnitObject k + a) (m (UnitObject k + a))
-> k (Maybe a) (UnitObject k + a)
-> k (Maybe a) (m (UnitObject k + 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 (Maybe a) (UnitObject k + 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 :: Kleisli m k (u + a) (Maybe a)
maybeFromSum = k (UnitObject k + 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 (UnitObject k + a) (m (Maybe a))
 -> Kleisli m k (u + a) (Maybe a))
-> k (UnitObject k + 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 (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 (UnitObject k + a) (Maybe a)
-> k (UnitObject k + a) (m (Maybe 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 (UnitObject k + 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 :: Kleisli m k Bool (u + u)
boolAsSum = k Bool (m (UnitObject k + UnitObject k))
-> Kleisli m k Bool (u + u)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k Bool (m (UnitObject k + UnitObject k))
 -> Kleisli m k Bool (u + u))
-> k Bool (m (UnitObject k + UnitObject k))
-> Kleisli m k Bool (u + u)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (UnitObject k + UnitObject k) (m (UnitObject k + UnitObject k))
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure k (UnitObject k + UnitObject k) (m (UnitObject k + UnitObject k))
-> k Bool (UnitObject k + UnitObject k)
-> k Bool (m (UnitObject k + UnitObject k))
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 (UnitObject k + UnitObject k)
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum
  boolFromSum :: Kleisli m k (u + u) Bool
boolFromSum = k (UnitObject k + UnitObject k) (m Bool)
-> Kleisli m k (u + u) Bool
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (UnitObject k + UnitObject k) (m Bool)
 -> Kleisli m k (u + u) Bool)
-> k (UnitObject k + UnitObject k) (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 (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 (UnitObject k + UnitObject k) Bool
-> k (UnitObject k + UnitObject k) (m Bool)
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 + UnitObject k) 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 :: 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 (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 κ (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 (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 κ (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 (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 :: 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 κ (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 (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 (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 κ (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 (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 (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 κ (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 κ (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 :: 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 (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 κ (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 (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 :: 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 κ (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 (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 (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure)
  second :: 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 κ (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 (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 (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 *** :: 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 κ (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 (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 &&& :: 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 κ (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 (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 :: 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 (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 κ (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 (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  fst :: 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 (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 κ (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 (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  snd :: 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 (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 κ (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 (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 :: 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 (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 κ (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 (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 :: 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 (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 κ (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 (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 :: 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 (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 κ (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 (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
  boolFromSwitch :: 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 (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 κ (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 (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 :: 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 (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 (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 κ (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 (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 :: Kleisli m k b c -> Kleisli m k (b + d) (c + d)
left (Kleisli k b (m c)
f) = k (b + d) (m (c + d)) -> Kleisli m k (b + d) (c + d)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (b + d) (m (c + d)) -> Kleisli m k (b + d) (c + d))
-> (((b + d) -> m (c + d)) -> k (b + d) (m (c + d)))
-> ((b + d) -> m (c + d))
-> Kleisli m k (b + d) (c + d)
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
. ((b + d) -> m (c + d)) -> k (b + d) (m (c + d))
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 (((b + d) -> m (c + d)) -> Kleisli m k (b + d) (c + d))
-> ((b + d) -> m (c + d)) -> Kleisli m k (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 (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 (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 κ (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 (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 κ (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 (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 :: Kleisli m k b c -> Kleisli m k (d + b) (d + c)
right(Kleisli k b (m c)
f) = k (d + b) (m (d + c)) -> Kleisli m k (d + b) (d + c)
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (d + b) (m (d + c)) -> Kleisli m k (d + b) (d + c))
-> (((d + b) -> m (d + c)) -> k (d + b) (m (d + c)))
-> ((d + b) -> m (d + c))
-> Kleisli m k (d + b) (d + 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
. ((d + b) -> m (d + c)) -> k (d + b) (m (d + 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 (((d + b) -> m (d + c)) -> Kleisli m k (d + b) (d + c))
-> ((d + b) -> m (d + c)) -> Kleisli m k (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 (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 κ (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 (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 (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 (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 κ (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 +++ :: Kleisli m k b c
-> Kleisli m k b' c' -> Kleisli m k (b + b') (c + c')
+++ Kleisli k b' (m c')
g = k (b + b') (m (c + c')) -> Kleisli m k (b + b') (c + c')
forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli (k (b + b') (m (c + c')) -> Kleisli m k (b + b') (c + c'))
-> (((b + b') -> m (c + c')) -> k (b + b') (m (c + c')))
-> ((b + b') -> m (c + c'))
-> Kleisli m k (b + b') (c + 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
. ((b + b') -> m (c + c')) -> k (b + b') (m (c + 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 (((b + b') -> m (c + c')) -> Kleisli m k (b + b') (c + c'))
-> ((b + b') -> m (c + c')) -> Kleisli m k (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 (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 (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 κ (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 (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 (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 κ (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 ||| :: 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 (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 :: 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 (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 κ (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 (k :: * -> * -> *) b.
(PreArrChoice k, Object k b) =>
k (ZeroObject k) b
initial
  coFst :: 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 (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 κ (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 (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst
  coSnd :: 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 (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 κ (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 (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 :: 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 :: k Bool (m ())
guard = k (m ()) (m ())
i k (m ()) (m ()) -> k Bool (m ()) -> k Bool (m ())
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 (m :: * -> *) (k :: * -> * -> *) a.
(MonadZero m k, Object k a, Object k (m a)) =>
k (UnitObject k) (m a)
fmzero k (UnitObject k) (m ())
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 κ (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 :: Bool -> k (m u) (m u)
when Bool
True = k (m u) (m u)
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
when Bool
False = k u (m u)
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 κ (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
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 :: Bool -> k (m u) (m u)
unless Bool
False = k (m u) (m u)
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
unless Bool
True = k u (m u)
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 κ (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
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 :: 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 (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 (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 (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 (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 (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 (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 (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 (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 :: 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 κ (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 (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 (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 κ (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 (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 (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 κ (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 :: k (m a) (m (UnitObject k))
void = k a u -> k (m a) (m u)
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
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal