-- |
-- 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 = 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 = 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 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
. 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 = 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 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 = 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 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
. 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 (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 = 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 forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd 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
. 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 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
. forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement 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
. forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap 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
. 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 = 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 = 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 = 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 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 = forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const 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 = 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 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 = 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 = 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 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
. 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 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 = 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 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
. 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> 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 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
. 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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' = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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' = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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
. 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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
. 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 
               \(a
b,b
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 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
. 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 (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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$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
. forall (m :: * -> *) (k :: * -> * -> *) a b.
Kleisli m k a b -> k a (m b)
runKleisli) 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> 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 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 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')
*** 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> 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 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
. (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> 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 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> 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 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> 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 (forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
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
. 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 = 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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
. 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case { Left b
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 forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
x
                                           ; Right d
y-> (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd)forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf`k b (m c)
f 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) = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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
. 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case { Left d
x -> (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst)forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf`k b (m c)
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ d
x
                                           ; Right b
y-> 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 forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli 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
. 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \case
       Left b
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 forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst 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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
x
       Right b'
y -> 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 forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd 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 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b (m c)
f 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall (m :: * -> *) (k :: * -> * -> *) a b.
k a (m b) -> Kleisli m k a b
Kleisli forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (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 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
. 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 forall (m :: * -> *) (k :: * -> * -> *) a.
(MonadZero m k, Object k a, Object k (m a)) =>
k (UnitObject k) (m a)
fmzero 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 = 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 = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
when Bool
False = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
unless Bool
True = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure 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
. 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 = 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 (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 forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd 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
<<< 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 forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) 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
<<< 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 (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 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 forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& 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 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
. 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 = (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 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
. 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 (forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const 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)) forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf` k (m b) (m b)
i 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 = 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 = 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 forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal