monad-levels (empty) → 0.1.0.0
raw patch · 23 files changed
+2264/−0 lines, 23 filesdep +basedep +constraintsdep +transformerssetup-changed
Dependencies added: base, constraints, transformers
Files
- CHANGELOG.md +3/−0
- Control/Monad/Levels.hs +82/−0
- Control/Monad/Levels/ConstraintPassing.hs +38/−0
- Control/Monad/Levels/Constraints.hs +638/−0
- Control/Monad/Levels/Cont.hs +94/−0
- Control/Monad/Levels/Definitions.hs +464/−0
- Control/Monad/Levels/Except.hs +100/−0
- Control/Monad/Levels/RWS.hs +56/−0
- Control/Monad/Levels/RWS/Lazy.hs +22/−0
- Control/Monad/Levels/RWS/Strict.hs +22/−0
- Control/Monad/Levels/Reader.hs +107/−0
- Control/Monad/Levels/State.hs +106/−0
- Control/Monad/Levels/State/Lazy.hs +25/−0
- Control/Monad/Levels/State/Strict.hs +25/−0
- Control/Monad/Levels/Transformers.hs +77/−0
- Control/Monad/Levels/Writer.hs +143/−0
- Control/Monad/Levels/Writer/Lazy.hs +26/−0
- Control/Monad/Levels/Writer/Strict.hs +26/−0
- LICENSE +20/−0
- README.md +106/−0
- Setup.hs +2/−0
- TODO.md +27/−0
- monad-levels.cabal +55/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+0.1.0.0+-------+* Initial release
+ Control/Monad/Levels.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,+ MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}++{- |+ Module : Control.Monad.Levels+ Description : Explicit level-based monad transformer stacks+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels+ ( -- * Monadic stacks+ MonadTower_(..)+ , MonadTower+ , MonadLevel_(..)+ , MonadLevel+ -- * Helper types\/aliases+ , Unwrapper+ , LowerMonadValue+ , WithLower+ , CanUnwrap+ , CanUnwrapSelf+ , WithLowerC+ -- ** Manipulating internal values+ , AddInternalM(..)+ , CanAddInternalM+ , AddIM(..)+ , AddInternal(..)+ , CanAddInternal+ , AddI(..)+ , AddIdent(..)+ , GetInternal(..)+ , CanGetInternal+ , AddIG(..)+ -- * Basic level manipulation+ , lift+ -- ** Lifting from the base+ , IsBaseMonad+ , HasBaseMonad+ , liftBase+ , BaseMonadOf+ , liftIO+ -- * Lifting from a specific transformer+ , HasTransformer+ , TransformedMonad+ , liftT+ ) where++import Control.Monad.Levels.Constraints+import Control.Monad.Levels.Definitions+import Control.Monad.Levels.Transformers++import Data.Constraint ((\\))++-- -----------------------------------------------------------------------------++lift :: forall m a. (MonadLevel m) => LowerMonad m a -> m a+lift lm = wrap a (\ _unwrap addI -> addInternalM addI lm) \\ proofInst m a+ where+ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy++-- | Ideally, this alias would not be needed as every instance of+-- 'MonadTower' should satisfy the required constraint. However,+-- this is needed for technical reasons.+type HasBaseMonad m = SatisfyConstraint IsBaseMonad m++liftBase :: (HasBaseMonad m) => BaseMonad m a -> m a+liftBase m = liftSat (Proxy :: Proxy IsBaseMonad) m+{-# INLINE liftBase #-}++type BaseMonadOf b m = (HasBaseMonad m, BaseMonad m ~ b, b ~ BaseMonad m)++-- | An alias defined for convenience with existing code.+liftIO :: (BaseMonadOf IO m) => IO a -> m a+liftIO = liftBase
+ Control/Monad/Levels/ConstraintPassing.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, OverlappingInstances, TypeFamilies,+ UndecidableInstances #-}+{- |+ Module : Control.Monad.Levels.ConstraintPassing+ Description : Whether a transformer allows a constraint to pass through+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++This module is defined separately as it's the only one that uses the+@OverlappingInstances@ extension.++ -}+module Control.Monad.Levels.ConstraintPassing where++import Control.Monad.Levels.Definitions++-- -----------------------------------------------------------------------------++-- | Indicates whether a specified constraint is allowed to pass+-- through a particular level.+--+-- (It may not be recognisable in Haddock documentation, but the @b@+-- parameter is of kind @'Bool'@ using the @DataKinds@ extension).+--+-- By default, for all monad levels this is set to the value of+-- 'DefaultAllowConstraints' for all constraints, with the exception+-- of 'IsBaseMonad' for which it is set to 'True'.+--+-- Instances of this class can - and should when appropriate - be+-- overlapped\/overriden.+class (ValidConstraint c, MonadLevel m) => ConstraintPassThrough c m (b :: Bool)++instance (ValidConstraint c, MonadLevel m, DefaultAllowConstraints m ~ b)+ => ConstraintPassThrough c m b++instance (MonadLevel m) => ConstraintPassThrough IsBaseMonad m True
+ Control/Monad/Levels/Constraints.hs view
@@ -0,0 +1,638 @@+{-# LANGUAGE ConstraintKinds, DataKinds, DefaultSignatures, FlexibleContexts,+ FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,+ TupleSections, TypeFamilies, TypeOperators, UndecidableInstances+ #-}++-- unsafeCoerceConstraint is used to prevent the need for a complex+-- induction proof (which I'm not sure can actually be achieved).+{-# LANGUAGE Trustworthy #-}++{- |+ Module : Control.Monad.Levels.Constraints+ Description : A Level-based approach to constraints+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Constraints+ ( -- * Constraints in the monad stack+ liftSat+ , lowerSat+ , lowerSat'+ , lowerFunction+ , SatisfyConstraint+ , SatisfyConstraintF+ , SatMonad+ , SatMonadValue+ , CanLowerFunc+ , SatFunction+ , ValidConstraint(..)+ , ConstraintPassThrough+ -- ** Internal types and classes+ , SatisfyConstraint_(SatMonad_, SatValue_, CanLowerFunc_)+ , SatDepth+ , proofInst+ -- * Variadic functions+ , VariadicFunction+ , VarFunction+ , VariadicLower+ , LowerV+ , SatV+ , CanLower+ , VarFunctionSat+ , MkVarFn+ , MkVarFnFrom+ , Func+ -- ** Variadic arguments+ , VariadicArg(VariadicType)+ , LowerableVArg+ , LiftableVArg+ , WrappableVArg+ , ValueOnly+ , Const+ , MonadicValue+ , MonadicOther+ , MonadicTuple+ -- * Re-exported for convenience+ , Proxy(..)+ ) where++import Control.Monad.Levels.ConstraintPassing+import Control.Monad.Levels.Definitions++import Data.Constraint ((:-) (..), Constraint, Dict (..), (\\))+import Data.Constraint.Unsafe (unsafeCoerceConstraint)+import Data.Monoid (Monoid (mempty))+import Data.Proxy (Proxy (..), asProxyTypeOf)++-- -----------------------------------------------------------------------------++data Nat = Zero | Suc Nat++predP :: Proxy (Suc n) -> Proxy n+predP _ = Proxy++-- | Inductively find the \"floor\" in the 'MonadTower' where the+-- specified constraint is satisfied.+--+-- This class is only exported for documentation purposes: no other+-- instances are possible, and most of the internals are not safe to+-- use outside of this module.+--+-- You should use 'SatisfyConstraint' instead of this in your+-- constraints.+class (ValidConstraint c, MonadTower m) => SatisfyConstraint_ (n :: Nat) c m where++ -- | The monad in the stack that satisfies the constraint.+ type SatMonad_ n c m :: * -> *++ -- | The value in the stack within the monad that satisfies the+ -- constraint.+ type SatValue_ n c m a++ -- | The extra constraints needed to be able to lower the provided+ -- 'VariadicFunction' @f@ to the satisfying monad.+ type CanLowerFunc_ f n c m a :: Constraint++ _liftSat :: Proxy n -> Proxy c -> Proxy m -> Proxy a -> SatMonad_ n c m a -> m a++ _lower :: (VariadicFunction f, CanLowerFunc_ f n c m a)+ => Proxy n -> Proxy c -> Proxy f -> Proxy m -> Proxy a+ -> VarFunctionSat f n c m a+ -> VarFunction f m a++-- | The satisfying monad for the specified constraint.+instance (ValidConstraint c, MonadTower m, c m) => SatisfyConstraint_ Zero c m where++ type SatMonad_ Zero c m = m++ type SatValue_ Zero c m a = a++ type CanLowerFunc_ f Zero c m a = ()++ _liftSat _ _ _ _ m = m++ _lower _n c vf m _a f = f \\ validSatFunc0 c m vf++-- | Inductive step for finding the satisfying monad. Note the usage+-- of 'ConstraintPassThrough' to ensure that only (constraint,monad+-- level) pairings that are valid are considered.+instance (ConstraintPassThrough c m True, SatisfyConstraint_ n c (LowerMonad m))+ => SatisfyConstraint_ (Suc n) c m where++ type SatMonad_ (Suc n) c m = SatMonad_ n c (LowerMonad m)++ type SatValue_ (Suc n) c m a = SatValue_ n c (LowerMonad m) (InnerValue m a)++ type CanLowerFunc_ f (Suc n) c m a = ( (CanLower f m a)+ , (CanLowerFunc_ (LowerV f m) n c (LowerMonad m) (InnerValue m a)))++ _liftSat n c m a sm = wrap a (\ _unwrap addI -> addInternalM addI (_liftSat (predP n) c (lowerP m) a sm))+ \\ proofInst m a++ _lower n c vf m a f = applyVFn vf m a (\ _unwrap _addI -> _lower (predP n)+ c+ (plowerF m vf)+ (lowerP m)+ (innerP m a)+ f+ \\ validLowerFunc m vf+ \\ validSatFunc n c m vf)++lowerP :: (MonadLevel m) => Proxy m -> Proxy (LowerMonad m)+lowerP _ = Proxy+{-# INLINE lowerP #-}++innerP :: (MonadLevel m) => Proxy m -> Proxy a -> Proxy (InnerValue m a)+innerP _ _ = Proxy+{-# INLINE innerP #-}++-- | For a specified constraint @c@ and 'MonadTower' @m@,+-- @SatisfyConstraint c m@ specifies that it is possible to reach a+-- monad in the tower that specifies the constraint.+type SatisfyConstraint c m = ( SatisfyConstraint_ (SatDepth c m) c m+ , c (SatMonad c m)+ -- Best current way of stating that the+ -- satisfying monad is a lower level of+ -- the specified one.+ , BaseMonad (SatMonad c m) ~ BaseMonad m)++-- | An extension of 'SatisfyConstraint' that also ensures that any+-- additional constraints needed to satisfy a 'VariadicFunction' @f@+-- to achieve an end result based upon the type @m a@ are met.+type SatisfyConstraintF c m a f = ( SatisfyConstraint c m+ , VariadicFunction f+ , CanLowerFunc f c m a)++-- | Any additional constraints that may be needed for a specified+-- 'VariadicFunction' to be valid as it is lowered to the satisfying+-- monad.+--+-- This typically matters only if 'ValueOnly' or 'MonadicOther' are+-- used.+type CanLowerFunc f c m a = CanLowerFunc_ f (SatDepth c m) c m a++-- | Lift a value of the satisfying monad to the top of the tower.+liftSat :: forall c m a. (SatisfyConstraint c m) =>+ Proxy c -> SatMonad c m a -> m a+liftSat p = _liftSat (Proxy :: Proxy (SatDepth c m)) p (Proxy :: Proxy m) (Proxy :: Proxy a)++-- | The type of the 'VariadicFunction' @f@ when the provided+-- constraint is satisfied.+type SatFunction c f m a = VarFunctionSat f (SatDepth c m) c m a++-- | Converts @m a@ into what the value in the monadic stack is where+-- the monad satisfies the provided constraint.+type SatMonadValue c m a = SatMonad_ (SatDepth c m) c m (SatValue_ (SatDepth c m) c m a)++-- | Lower a function from the top of the monad tower down to the+-- satisfying monad in which it can be applied.+lowerSat :: forall c m a f. (SatisfyConstraintF c m a f) =>+ Proxy c -> Proxy f -> Proxy m -> Proxy a+ -> SatFunction c f m a -> VarFunction f m a+lowerSat c vf m a f = _lower n c vf m a f+ where+ n :: Proxy (SatDepth c m)+ n = Proxy++type MFunc = MkVarFn MonadicValue++-- | A variant of 'lowerSat' for when @CanLower f m a ~ ()@.+lowerSat' :: forall c m a f. (SatisfyConstraint c m, VariadicFunction f)+ => Proxy c -> Proxy f -> Proxy m -> Proxy a+ -> (() :- CanLower f m a)+ -> SatFunction c f m a -> VarFunction f m a+lowerSat' c vf m a prf f = _lower n c vf m a f \\ simpleFuncProof vf c m a prf+ where+ n :: Proxy (SatDepth c m)+ n = Proxy++-- | A specialised instance of 'lowerSat' where a simple function of+-- type @m a -> m a@ is lowered to the satisfying monad.+lowerFunction :: forall c m a. (SatisfyConstraint c m) => Proxy c+ -> (SatMonadValue c m a -> SatMonadValue c m a)+ -> m a -> m a+lowerFunction c f = lowerSat' c vf m a (Sub Dict) f+ where+ vf :: Proxy MFunc+ vf = Proxy++ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy++simpleFuncProof :: (SatisfyConstraint c m, VariadicFunction f)+ => Proxy f -> Proxy c -> Proxy m -> Proxy a+ -> (() :- CanLower f m a) -> (() :- CanLowerFunc f c m a)+simpleFuncProof _ _ _ _ (Sub Dict) = unsafeCoerceConstraint+{-# INLINE simpleFuncProof #-}+-- Will always be @~ ()@ by construction, but an actual proof would+-- need to be by induction.++-- -----------------------------------------------------------------------------++-- Converts the monadic stack into a list of sub-stacks, and tests if+-- each sub-stack satisfies the constraint.+type TrySatisfy (c :: (* -> *) -> Constraint) (m :: (* -> *)) = TrySatisfy' c (BaseMonad m) m++type family TrySatisfy' (c :: (* -> *) -> Constraint) (b :: (* -> *)) (m :: (* -> *)) :: [Bool] where+ TrySatisfy' c b b = ConstraintSatisfied c b ': '[]+ TrySatisfy' c b m = ConstraintSatisfied c m ': TrySatisfy' c b (LowerMonad m)++type family FindTrue (bms :: [Bool]) :: Nat where+ FindTrue (True ': t) = Zero+ FindTrue (False ': t) = Suc (FindTrue t)++-- | Calculate how many levels down is the satisfying monad.+type SatDepth (c :: (* -> *) -> Constraint) (m :: * -> *) = FindTrue (TrySatisfy c m)++-- | The Monad in the tower that satisfies the provided constraint.+type SatMonad (c :: (* -> *) -> Constraint) (m :: * -> *) = SatMonad_ (SatDepth c m) c m++-- -----------------------------------------------------------------------------++-- | Base class for dealing with variadic functions\/arguments.+class VariadicLower v where++ -- | The type when lowered to the 'LowerMonad'. In most cases this+ -- will be the same value.+ type LowerV v (m :: * -> *) :: *+ type LowerV v m = v++ -- | The type when applied to the satisfying monad.+ type SatV v (n :: Nat) (c :: (* -> *) -> Constraint) (m :: * -> *) :: *+ type SatV v n c m = v++ -- | Any additional constraints needed when lowering @v@.+ type CanLower v (m :: * -> *) a :: Constraint+ type CanLower v m a = ()++-- | Class representing arguments\/parameters for lower-able variadic+-- functions.+--+-- When considering a function with an end result based upon @m a@,+-- the following argument types are available:+--+-- [@'ValueOnly'@] corresponds to @a@.+--+-- [@'Const' b@] corresponds to some other type @b@.+--+-- [@'MonadicValue'@] corresponds to @m a@.+--+-- [@'MonadicOther' b@] corresponds to @m b@.+--+-- [@'MonadicTuple' b@] corresponds to @m (a,b)@.+--+-- [@'Func' v1 v2@] corresponds to @v1 -> v2@.+class (VariadicLower v) => VariadicArg v where++ -- | The type that the variadic guard corresponds to within the+ -- monad @(m a)@.+ type VariadicType v (m :: * -> *) a++ validSatArg0 :: (SatisfyConstraint_ Zero c m)+ => Proxy c -> Proxy m -> Proxy v+ -> SatisfyConstraint_ Zero c m :- SatV v Zero c m ~ v+ default validSatArg0 :: (SatisfyConstraint_ Zero c m)+ => Proxy c -> Proxy m -> Proxy v+ -> SatisfyConstraint_ Zero c m :- v ~ v+ validSatArg0 _ _ _ = Sub Dict++ validSatArg :: (SatisfyConstraint_ (Suc n) c m)+ => Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy v+ -> SatisfyConstraint_ (Suc n) c m+ :- SatV v (Suc n) c m ~ SatV (LowerV v m) n c (LowerMonad m)+ default validSatArg :: (SatisfyConstraint_ (Suc n) c m)+ => Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy v+ -> SatisfyConstraint_ (Suc n) c m+ :- v ~ v+ validSatArg _ _ _ _ = Sub Dict++-- | Variadic arguments that can be lowered. All 'VariadicArg' values+-- are instances of this class.+--+-- This actually defines how a variadic argument is lowered down to+-- the 'LowerMonad'.+class (VariadicArg v) => LowerableVArg v where++ validLowerArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- LowerableVArg (LowerV v m)+ default validLowerArg :: (MonadLevel m, LowerV v m ~ v)+ => Proxy m -> Proxy v -> MonadLevel m :- LowerableVArg v+ validLowerArg _ _ = Sub Dict++ lowerVArg :: (MonadLevel m, CanLower v m a)+ => Proxy v -> Proxy m -> Proxy a+ -> VariadicType v m a+ -> Unwrapper m a (LowerVArg v m a)++-- | In contrast to 'LowerableVArg', this class is for 'VariadicArg'+-- values that can be /lifted/ from the 'LowerMonad'.+--+-- This is important for @'Func' v1 v2@ arguments, as to lower a+-- function we need to /lift/ @v1@ before applying the function, and+-- then subsequently lower the result.+--+-- All instances of 'VariadicArg' are instances of this with the+-- exception of 'ValueOnly' (as it's not always possible to convert+-- an arbitrary @'InnerValue' m a@ back into an @a@).+class (VariadicArg v) => LiftableVArg v where++ validLiftArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- LiftableVArg (LowerV v m)+ default validLiftArg :: (MonadLevel m, LowerV v m ~ v)+ => Proxy m -> Proxy v -> MonadLevel m :- LiftableVArg v+ validLiftArg _ _ = Sub Dict++ liftVArg :: (MonadLevel m, CanLower v m a)+ => Proxy v -> Proxy m -> Proxy a+ -> LowerVArg v m a+ -> Unwrapper m a (VariadicType v m a)++-- | Variadic arguments that can be lifted via a call to 'wrap'. Only+-- those that have a 'VariadicType' that is a monadic value can thus+-- be instances of this class.+class (LiftableVArg v) => WrappableVArg v where++ validWrapArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- WrappableVArg (LowerV v m)+ default validWrapArg :: (MonadLevel m, LowerV v m ~ v)+ => Proxy m -> Proxy v -> MonadLevel m :- WrappableVArg v+ validWrapArg _ _ = Sub Dict++ wrapVArg :: (MonadLevel m, CanLower v m a)+ => Proxy v -> Proxy m -> Proxy a+ -> Unwrapper m a (LowerVArg v m a) -> VariadicType v m a++type LowerVArg v m a = VariadicType (LowerV v m) (LowerMonad m) (InnerValue m a)++-- | A constant type that does not depend upon the current monadic+-- context. That is, @Const b@ corresponds to just @b@. It is kept+-- as-is when lowering through the different levels.+data Const (b :: *)++instance VariadicLower (Const b)++instance VariadicArg (Const b) where+ type VariadicType (Const b) m a = b++instance LowerableVArg (Const b) where++ lowerVArg _ _ _ b _ _ = b++instance LiftableVArg (Const b) where++ liftVArg _ _ _ b _ _ = b++-- | Corresponds to @m a@.+data MonadicValue++instance VariadicLower MonadicValue++instance VariadicArg MonadicValue where+ type VariadicType MonadicValue m a = m a++instance LowerableVArg MonadicValue where++ lowerVArg _ pm pa m unwrap _ = unwrap m \\ (proofInst pm pa)++instance LiftableVArg MonadicValue where++ liftVArg _ m a mv _ _ = wrap a (\ _ _ -> mv) \\ proofInst m a++instance WrappableVArg MonadicValue where++ wrapVArg _ m a f = wrap a f \\ proofInst m a++-- | Whilst 'MonadLevel' requires @CanUnwrap m a a@ for all @a@, the+-- type system can't always determine this. This is a helper+-- function to do so.+proofInst :: (MonadLevel m) => Proxy m -> Proxy a -> (MonadLevel m :- CanUnwrap m a a)+proofInst _ _ = getUnwrapSelfProof+{-# INLINE proofInst #-}++-- | Corresponds to @m b@, where the final result is based upon @m a@.+-- This requires the extra constraint of @'CanUnwrap' m a b@.+data MonadicOther b++instance VariadicLower (MonadicOther b) where+ type LowerV (MonadicOther b) m = MonadicOther (InnerValue m b)++ type SatV (MonadicOther b) n c m = MonadicOther (SatValue_ n c m b)++ type CanLower (MonadicOther b) m a = CanUnwrap m a b++instance VariadicArg (MonadicOther b) where+ type VariadicType (MonadicOther b) m a = m b++ validSatArg0 _ _ _ = Sub Dict++ validSatArg _ _ _ _ = Sub Dict++instance LowerableVArg (MonadicOther b) where++ validLowerArg _ _ = Sub Dict++ lowerVArg _ _ _ m unwrap _ = unwrap m++instance LiftableVArg (MonadicOther b) where++ validLiftArg _ _ = Sub Dict++ liftVArg _ _ a m _ _ = wrap a (\ _ _ -> m)++instance WrappableVArg (MonadicOther b) where++ validWrapArg _ _ = Sub Dict++ wrapVArg _ _ a f = wrap a f++-- | Corresponds to @m (a,b)@. This requires the extra constraints of+-- @'CanAddInternal' m@ and @'AllowOtherValues' m ~ True@ (This is+-- used instead of 'CanUnwrap' as a simplification).+data MonadicTuple b++instance VariadicLower (MonadicTuple b) where+ type CanLower (MonadicTuple b) m a = (CanGetInternal m, AllowOtherValues m ~ True)++instance VariadicArg (MonadicTuple b) where+ type VariadicType (MonadicTuple b) m a = m (a,b)++instance (Monoid b) => LowerableVArg (MonadicTuple b) where++ lowerVArg v _ a lm unwrap addI = fmap shiftI (unwrap lm)+ where+ b = tupleProxy v++ ab = proxyPair a b++ shiftI iv = let bv = getInternal addI mempty (snd . (`asProxyTypeOf` ab)) iv+ in (mapInternal addI (fst . (`asProxyTypeOf` ab)) iv, bv)++tupleProxy :: Proxy (MonadicTuple b) -> Proxy b+tupleProxy _ = Proxy+{-# INLINE tupleProxy #-}++proxyPair :: Proxy a -> Proxy b -> Proxy (a,b)+proxyPair _ _ = Proxy+{-# INLINE proxyPair #-}++instance LiftableVArg (MonadicTuple b) where++ liftVArg _ _ a mab _ addI = wrap a ( \ _ _ -> fmap shiftI mab)+ where+ shiftI (iva,b) = mapInternal addI ((,b) . (`asProxyTypeOf`a)) iva++instance WrappableVArg (MonadicTuple b) where++ wrapVArg _ _ a f = wrap a ( \ unwrap addI -> fmap (shiftI addI) (f unwrap addI))+ where+ shiftI ai (iva, b) = mapInternal ai ((,b) . (`asProxyTypeOf`a)) iva++-- | This corresponds to @a@ when the final result is based upon @m+-- a@. This requires the extra constraint of @'CanAddInternal' m@.+data ValueOnly++instance VariadicLower ValueOnly where+ type CanLower ValueOnly m a = CanAddInternal m++instance VariadicArg ValueOnly where+ type VariadicType ValueOnly m a = a++instance LowerableVArg ValueOnly where++ lowerVArg _ _ _ a _ addI = addInternal addI a \\ addIntProof addI++-- | Represents the function @v1 -> v2@.+data Func (v1 :: *) (v2 :: *)++pfa :: Proxy (Func a b) -> Proxy a+pfa _ = Proxy++pfb :: Proxy (Func a b) -> Proxy b+pfb _ = Proxy++instance (VariadicLower a, VariadicLower b) => VariadicLower (Func a b) where+ type LowerV (Func va vb) m = Func (LowerV va m) (LowerV vb m)++ type SatV (Func va vb) n c m = Func (SatV va n c m) (SatV vb n c m)++ type CanLower (Func va vb) m a = ((CanLower va m a), (CanLower vb m a))++instance (VariadicArg va, VariadicArg vb) => VariadicArg (Func va vb) where+ type VariadicType (Func va vb) m a = VariadicType va m a -> VariadicType vb m a++ validSatArg0 c m f = Sub Dict \\ validSatArg0 c m (pfa f)+ \\ validSatArg0 c m (pfb f)++ validSatArg n c m f = Sub Dict \\ validSatArg n c m (pfa f)+ \\ validSatArg n c m (pfb f)++instance (LiftableVArg va, LowerableVArg vb) => LowerableVArg (Func va vb) where++ validLowerArg m f = Sub Dict \\ validLiftArg m (pfa f)+ \\ validLowerArg m (pfb f)++ -- lower . f . lift+ lowerVArg pf m a f unwrap addI+ = (\ v -> lowerVArg (pfb pf) m a v unwrap addI)+ . f+ . (\ v -> liftVArg (pfa pf) m a v unwrap addI)++instance (LowerableVArg va, LiftableVArg vb) => LiftableVArg (Func va vb) where++ validLiftArg m f = Sub Dict \\ validLowerArg m (pfa f)+ \\ validLiftArg m (pfb f)++ -- lift . f . lower+ liftVArg pf m a f unwrap addI+ = (\ v -> liftVArg (pfb pf) m a v unwrap addI)+ . f+ . (\ v -> lowerVArg (pfa pf) m a v unwrap addI)++-- | A function composed of variadic arguments that produces a value+-- based upon the type @m a@.+class (VariadicLower f) => VariadicFunction f where++ -- | The function (that produces a value based upon the type @m a@)+ -- that this instance corresponds to.+ type VarFunction f (m :: * -> *) a++ validLowerFunc :: (MonadLevel m) => Proxy m -> Proxy f -> MonadLevel m :- VariadicFunction (LowerV f m)++ validSatFunc0 :: (SatisfyConstraint_ Zero c m)+ => Proxy c -> Proxy m -> Proxy f+ -> SatisfyConstraint_ Zero c m :- SatV f Zero c m ~ f++ validSatFunc :: (SatisfyConstraint_ (Suc n) c m)+ => Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy f+ -> SatisfyConstraint_ (Suc n) c m+ :- SatV f (Suc n) c m ~ SatV (LowerV f m) n c (LowerMonad m)++ applyVFn :: (MonadLevel m, CanLower f m a)+ => Proxy f -> Proxy m -> Proxy a+ -> Unwrapper m a (VarFunctionLower f m a)+ -> VarFunction f m a++type VarFunctionLower f (m :: * -> *) a = VarFunction (LowerV f m) (LowerMonad m) (InnerValue m a)++-- | The function represented by the 'VariadicFunction' when lowered+-- to the satisfying monad.+type VarFunctionSat f n c m a = VarFunction (SatV f n c m) (SatMonad_ n c m) (SatValue_ n c m a)++plowerF :: (MonadLevel m, VariadicFunction f) => Proxy m -> Proxy f -> Proxy (LowerV f m)+plowerF _ _ = Proxy++-- | The fundamental way of creating a 'VariadicFunction'. @MkVarFn+-- v@ corresponds to a function of type @'VariadicType' v m a -> m+-- a@ for some specified @m a@.+--+-- If more than one argument is needed for a function, they can be+-- prepended on using 'Func'.+type MkVarFn v = Func v (MkVarFnFrom MonadicValue)++-- | The result of a 'VariadicFunction'. This can't be used on its+-- own, and needs to have at least one 'Func' attached to it.+data MkVarFnFrom va++pmvff :: Proxy (MkVarFnFrom va) -> Proxy va+pmvff _ = Proxy++instance (VariadicLower va) => VariadicLower (MkVarFnFrom va) where+ type LowerV (MkVarFnFrom va) m = MkVarFnFrom (LowerV va m)++ type SatV (MkVarFnFrom va) n c m = MkVarFnFrom (SatV va n c m)++ type CanLower (MkVarFnFrom va) m a = CanLower va m a++instance (WrappableVArg va) => VariadicFunction (MkVarFnFrom va) where++ type VarFunction (MkVarFnFrom va) m a = VariadicType va m a++ validLowerFunc m pmf = Sub Dict \\ validWrapArg m (pmvff pmf)++ validSatFunc0 c m pmf = Sub Dict \\ validSatArg0 c m (pmvff pmf)++ validSatFunc n c m pmf = Sub Dict \\ validSatArg n c m (pmvff pmf)++ applyVFn pmf m a f = wrapVArg (pmvff pmf) m a f++instance (LowerableVArg va, VariadicFunction vf) => VariadicFunction (Func va vf) where+ type VarFunction (Func va vf) m a = (VariadicType va m a) -> VarFunction vf m a++ validLowerFunc m f = Sub Dict \\ validLowerArg m (pfa f)+ \\ validLowerFunc m (pfb f)++ validSatFunc0 c m f = Sub Dict \\ validSatArg0 c m (pfa f)+ \\ validSatFunc0 c m (pfb f)++ validSatFunc n c m f = Sub Dict \\ validSatArg n c m (pfa f)+ \\ validSatFunc n c m (pfb f)++ applyVFn pf m a f va = applyVFn (pfb pf) m a+ (\ unwrap addI ->+ f unwrap addI (lowerVArg (pfa pf) m a va unwrap addI))++-- -----------------------------------------------------------------------------
+ Control/Monad/Levels/Cont.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,+ MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies,+ UndecidableInstances #-}+{- |+ Module : Control.Monad.Levels.Cont+ Description : Continuation monad handling+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++This module allows inclusion of 'ContT' into your monad stack so as to+represent continuation-passing style (CPS) computations.++Note that the behaviour of some monad transformers and how they deal+with continuations differs from how+<http://hackage.haskell.org/package/mtl mtl> handles them. For+example, with a lazy state transformer, using this module results in+<http://hackage.haskell.org/package/transformers/docs/Control-Monad-Trans-State-Lazy.html#v:liftCallCC liftCallCC>,+whereas @mtl@ uses+<http://hackage.haskell.org/package/transformers/docs/Control-Monad-Trans-State-Lazy.html#v:liftCallCC-39- liftCallCC'>.++ -}+module Control.Monad.Levels.Cont+ ( callCC+ , ContT(..)+ , HasCont+ , IsCont+ , ContFn+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints++import Control.Monad.Trans.Cont (ContT (..))+import qualified Control.Monad.Trans.Cont as C++import Control.Monad.Trans.List (ListT)++-- -----------------------------------------------------------------------------++-- We don't use the Transformer constraint here because there's+-- problems with the @r@ when trying to resolve the constraint.++-- | A simple class just to match up with the 'ContT' monad+-- transformer.+class (MonadLevel m) => IsCont m where+ -- Defined just to have it based upon the constraint+ _callCC :: CallCC m a b++instance (MonadTower m) => IsCont (ContT r m) where+ _callCC = C.callCC++instance ValidConstraint IsCont where+ type ConstraintSatisfied IsCont m = IsContT m++type family IsContT m where+ IsContT (ContT r m) = True+ IsContT m = False++-- | Represents monad stacks that can successfully pass 'callCC' down+-- to a 'ContT' transformer.+type HasCont m a b = SatisfyConstraintF IsCont m a (ContFn b)++-- | This corresponds to+-- <http://hackage.haskell.org/package/transformers/docs/Control-Monad-Signatures.html#t:CallCC CallCC>+-- in @transformers@.+type ContFn b = MkVarFn (Func (Func ValueOnly (MonadicOther b)) MonadicValue)++-- This is defined solely as an extra check on 'ContFn' matching the+-- type of 'C.callCC'.+type CallCC m a b = VarFunction (ContFn b) m a++-- Not using CallCC here to avoid having to export it.++-- | @callCC@ (call-with-current-continuation) calls a function with+-- the current continuation as its argument.+callCC :: forall m a b. (HasCont m a b) => ((a -> m b) -> m a) -> m a+callCC = lowerSat c vf m a _callCC+ where+ c :: Proxy IsCont+ c = Proxy++ vf :: Proxy (ContFn b)+ vf = Proxy++ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy++-- -----------------------------------------------------------------------------++instance (MonadTower m) => ConstraintPassThrough IsCont (ListT m) True
+ Control/Monad/Levels/Definitions.hs view
@@ -0,0 +1,464 @@+{-# LANGUAGE ConstraintKinds, DataKinds, DefaultSignatures, FlexibleContexts,+ FlexibleInstances, MultiParamTypeClasses, RankNTypes,+ ScopedTypeVariables, TupleSections, TypeFamilies, TypeOperators,+ UndecidableInstances #-}++{- |+ Module : Control.Monad.Levels.Definitions+ Description : Specific levls of monad transformers+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Definitions where++import Control.Applicative (Applicative, WrappedMonad)+import Data.Coerce (Coercible, coerce)+import Data.Constraint ((:-) (..), Class (..), Constraint, Dict (..),+ trans, weaken1, weaken2, (\\))+import Data.Constraint.Forall (Forall, inst)+import Data.Proxy (Proxy (..))++import Control.Monad.Trans.Cont (ContT (..))+import Control.Monad.Trans.Except (ExceptT (..), runExceptT)+import Control.Monad.Trans.Identity (IdentityT (..))+import Control.Monad.Trans.List (ListT (..))+import Control.Monad.Trans.Maybe (MaybeT (..))+import Control.Monad.Trans.Reader (ReaderT (..))+import qualified Control.Monad.Trans.RWS.Lazy as LRWS+import qualified Control.Monad.Trans.RWS.Strict as SRWS+import qualified Control.Monad.Trans.State.Lazy as LSt+import qualified Control.Monad.Trans.State.Strict as SSt+import qualified Control.Monad.Trans.Writer.Lazy as LW+import qualified Control.Monad.Trans.Writer.Strict as SW+import Data.Functor.Identity (Identity (..))++import Control.Arrow (first)+import Data.Monoid (Monoid, mempty)++-- -----------------------------------------------------------------------------++-- | Monads in a monadic stack.+--+-- For monads that are /not/ instances of 'MonadicLevel_' then it+-- suffices to say @instance MonadTower_ MyMonad@; for levels it is+-- required to define 'BaseMonad' (typically recursively).+--+-- You should use 'MonadTower' in any constraints rather than this+-- class. This includes when writing instances of 'MonadTower_' for+-- monadic transformers.+class (Applicative m, Monad m) => MonadTower_ m where++ type BaseMonad m :: * -> *+ type BaseMonad m = m++-- | This is 'MonadTower_' with additional sanity constraints to+-- ensure that applying 'BaseMonad' is idempotent.+type MonadTower m = ( MonadTower_ m, MonadTower_ (BaseMonad m)+ , BaseMonad (BaseMonad m) ~ BaseMonad m+ , BaseMonad m ~ BaseMonad (BaseMonad m))++-- -----------------------------------------------------------------------------++instance MonadTower_ []+instance MonadTower_ Maybe+instance MonadTower_ IO+instance MonadTower_ (Either e)+instance MonadTower_ ((->) r)+instance (Monad m) => MonadTower_ (WrappedMonad m)++instance MonadTower_ Identity++instance (MonadTower m) => MonadTower_ (ContT r m) where+ type BaseMonad (ContT r m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (ExceptT e m) where+ type BaseMonad (ExceptT e m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (IdentityT m) where+ type BaseMonad (IdentityT m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (ListT m) where+ type BaseMonad (ListT m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (MaybeT m) where+ type BaseMonad (MaybeT m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (ReaderT r m) where+ type BaseMonad (ReaderT r m) = BaseMonad m++instance (Monoid w, MonadTower m) => MonadTower_ (LRWS.RWST r w s m) where+ type BaseMonad (LRWS.RWST r w s m) = BaseMonad m++instance (Monoid w, MonadTower m) => MonadTower_ (SRWS.RWST r w s m) where+ type BaseMonad (SRWS.RWST r w s m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (LSt.StateT s m) where+ type BaseMonad (LSt.StateT s m) = BaseMonad m++instance (MonadTower m) => MonadTower_ (SSt.StateT s m) where+ type BaseMonad (SSt.StateT s m) = BaseMonad m++instance (Monoid w, MonadTower m) => MonadTower_ (LW.WriterT w m) where+ type BaseMonad (LW.WriterT w m) = BaseMonad m++instance (Monoid w, MonadTower m) => MonadTower_ (SW.WriterT w m) where+ type BaseMonad (SW.WriterT w m) = BaseMonad m++-- -----------------------------------------------------------------------------++-- | How to handle wrappers around existing 'MonadTower' instances.+--+-- For newtype wrappers (e.g. 'IdentityT'), it is sufficient to only+-- define 'LowerMonad'.+--+-- You should use 'MonadLevel' rather than this class in+-- constraints.+class (MonadTower m, MonadTower (LowerMonad m)+ , BaseMonad m ~ BaseMonad (LowerMonad m), BaseMonad (LowerMonad m) ~ BaseMonad m+ , CanAddInternalM m)+ => MonadLevel_ m where++ type LowerMonad m :: * -> *++ -- | How the value is represented internally; defaults to @a@.+ type InnerValue m a :: *+ type InnerValue m a = a++ -- | An instance of 'AddInternalM'; this is defined so as to be able+ -- to make it easier to add constraints rather than solely relying+ -- upon its value within 'Unwrapper'.+ type WithLower_ m :: (* -> *) -> * -> *+ type WithLower_ m = AddIdent++ -- | Within the continuation for 'wrap' for @m a@, we can unwrap any+ -- @m b@ if @AllowOtherValues m ~ True@; otherwise, we can only+ -- unwrap @m a@. Defaults to @True@.+ type AllowOtherValues m :: Bool+ type AllowOtherValues m = True++ -- | By default, should all constraints be allowed through this+ -- level? Defaults to @True@.+ type DefaultAllowConstraints m :: Bool+ type DefaultAllowConstraints m = True++ -- | A continuation-based approach to create a value of this level.+ --+ -- A default is provided for newtype wrappers around existing+ -- 'MonadTower' instances, provided that - with the exception of+ -- 'LowerMonad' - all associated types are left as their defaults.+ wrap :: (CanUnwrap m a b) => Proxy a+ -> (Unwrapper m a (LowerMonadValue m b)) -> m b+ default wrap :: (Forall (IsCoercible m), Forall (InnerSame m)+ , WithLower_ m ~ AddIdent, AllowOtherValues m ~ True, DefaultAllowConstraints m ~ True)+ => Proxy a -> (Unwrapper m a (LowerMonadValue m b)) -> m b+ wrap = coerceWrap++coerceWrap :: forall m a b. (MonadLevel_ m, Forall (IsCoercible m), Forall (InnerSame m)+ , WithLower_ m ~ AddIdent, AllowOtherValues m ~ True, DefaultAllowConstraints m ~ True)+ => Proxy a -> (Unwrapper m a (LowerMonadValue m b)) -> m b+coerceWrap _ f = pack (f unpack AddIdent)+ where+ pack :: LowerMonadValue m b -> m b+ pack = coerce \\ (inst :: Forall (InnerSame m) :- InnerSame m b)+ \\ (inst :: Forall (IsCoercible m) :- IsCoercible m b)++ unpack :: m c -> LowerMonadValue m c+ unpack = coerceUnwrap+{-# INLINE coerceWrap #-}++coerceUnwrap :: forall m c. (MonadLevel m, Forall (IsCoercible m), Forall (InnerSame m))+ => m c -> LowerMonadValue m c+coerceUnwrap = coerce \\ (inst :: Forall (InnerSame m) :- InnerSame m c)+ \\ (inst :: Forall (IsCoercible m) :- IsCoercible m c)+{-# INLINE coerceUnwrap #-}++class (MonadLevel m, Coercible (m a) (LowerMonadValue m a), Coercible (LowerMonadValue m a) (m a))+ => IsCoercible m a++instance (MonadLevel m, Coercible (m a) (LowerMonadValue m a), Coercible (LowerMonadValue m a) (m a))+ => IsCoercible m a++type CanUnwrap_ m a b = CheckOtherAllowed (AllowOtherValues m) a b++type family CheckOtherAllowed (allowed::Bool) a b :: Constraint where+ CheckOtherAllowed True a b = ()+ CheckOtherAllowed False a b = (a ~ b)++-- | If we're dealing overall with @m a@, then this allows us to+-- specify those @b@ values for which we can also manipulate @m b@.+--+-- If @'AllowOtherValues' m ~ False@ then we require that @a ~ b@;+-- otherwise, any @b@ is accepted.+class (MonadLevel_ m, CanUnwrap_ m a b) => CanUnwrap m a b+instance (MonadLevel_ m, CanUnwrap_ m a b) => CanUnwrap m a b++-- | Used to ensure that for all monad levels, @CanUnwrap m a a@ is+-- satisfied.+class (MonadLevel_ m, CanUnwrap m a a) => CanUnwrapSelf m a+instance (MonadLevel_ m, CanUnwrap m a a) => CanUnwrapSelf m a++instance (MonadLevel_ m) => Class (MonadLevel_ m, CanUnwrap m a a) (CanUnwrapSelf m a) where+ cls = Sub Dict++getUnwrapSelfProof :: (MonadLevel m) => MonadLevel m :- CanUnwrap m a a+getUnwrapSelfProof = trans weaken2 -- CanUnwrap+ ( trans cls -- Undo CanUnwrapSelf+ (trans inst -- Undo Forall+ (trans weaken1 -- Get Forall+ weaken2 -- Remove MonadLevel_+ )+ )+ )++-- | This is 'MonadLevel_' with some additional sanity constraints.+type MonadLevel m = (MonadLevel_ m, (Forall (CanUnwrapSelf m), WithLowerC m))++-- | The value contained within the actual level (e.g. for+-- @'LSt.StateT' s m a@, this is equivalent to @m (a,s)@).+type LowerMonadValue m a = LowerMonad m (InnerValue m a)++-- | A continuation function to produce a value of type @t@.+type Unwrapper m a t = (forall b. (CanUnwrap m a b) => m b -> LowerMonadValue m b)+ -> (WithLower m a)+ -> t++type WithLower m = WithLower_ m m+type WithLowerC m = AddConstraint (WithLower_ m) m++type CanAddInternalM m = AddInternalM (WithLower_ m)+type CanAddInternal m = AddInternal (WithLower_ m)+type CanGetInternal m = GetInternal (WithLower_ m)++class AddInternalM (ai :: (* -> *) -> * -> *) where++ type AddConstraint ai (m :: * -> *) :: Constraint+ type AddConstraint ai m = ()++ addInternalM :: (MonadLevel m, WithLower_ m ~ ai, CanUnwrap m a b)+ => ai m a -> LowerMonad m b+ -> LowerMonadValue m b++class (AddInternalM ai) => AddInternal ai where+ addInternal :: (MonadLevel m, WithLower_ m ~ ai, CanUnwrap m a b)+ => ai m a -> b -> InnerValue m b++ mapInternal :: (MonadLevel m, WithLower_ m ~ ai, CanUnwrap m a b, CanUnwrap m a c)+ => ai m a -> (b -> c) -> InnerValue m b -> InnerValue m c++class (AddInternal ai) => GetInternal ai where+ -- | This is like a lifted 'maybe' function that applies to+ -- 'InnerValue' values rather than just 'Maybe's.+ getInternal :: (MonadLevel m, WithLower_ m ~ ai, CanUnwrap m a b)+ => ai m a -> c -> (b -> c) -> InnerValue m b -> c++-- | Used for monad transformers like 'ContT' where it is not possible+-- to manipulate the internal value without considering the monad+-- that it is within.+newtype AddIM m a = AddIM { addIMFunc :: forall b. (CanUnwrap m a b)+ => LowerMonad m b -> LowerMonadValue m b }++instance AddInternalM AddIM where+ addInternalM = addIMFunc++-- | In most cases you will want to use 'AddIG' instead of this; this+-- is defined for cases like 'ListT' where it may not be possible to+-- obtain either zero or one value for use with 'getInternal'.+data AddI m a = AddI { setIFunc :: forall b. (CanUnwrap m a b) => b -> InnerValue m b+ , mapIFunc :: forall b c. (CanUnwrap m a b, CanUnwrap m a c)+ => (b -> c) -> InnerValue m b -> InnerValue m c+ }++instance AddInternalM AddI where+ addInternalM ai = fmap (setIFunc ai)++addIntProof :: (MonadLevel m, AddInternalM ai) => ai m a -> MonadLevel m :- CanUnwrap m a a+addIntProof _ = getUnwrapSelfProof++instance AddInternal AddI where+ addInternal = setIFunc++ mapInternal = mapIFunc++-- | Used for monad transformers where it is possible to consider the+-- 'InnerValue' in isolation. If @InnerValue m a ~ a@ then use+-- 'AddIdent' instead.+data AddIG m a = AddIG { setIUFunc :: forall b. (CanUnwrap m a b) => b -> InnerValue m b+ , mapIUFunc :: forall b c. (CanUnwrap m a b, CanUnwrap m a c)+ => (b -> c) -> InnerValue m b -> InnerValue m c+ , getIUFunc :: forall b c. (CanUnwrap m a b)+ => c -> (b -> c) -> InnerValue m b -> c+ }++instance AddInternalM AddIG where+ addInternalM ai = fmap (setIUFunc ai)++instance AddInternal AddIG where+ addInternal = setIUFunc++ mapInternal = mapIUFunc++instance GetInternal AddIG where+ getInternal = getIUFunc++-- | Used for monad transformers where @'InnerValue' m a ~ a@.+data AddIdent (m :: * -> *) a = AddIdent++instance AddInternalM AddIdent where+ type AddConstraint AddIdent m = Forall (InnerSame m)++ addInternalM ai m = m \\ addIdentProof ai (proxyFromM m)++class (MonadLevel_ m, InnerValue m a ~ a) => InnerSame m a+instance (MonadLevel_ m, InnerValue m a ~ a) => InnerSame m a++addIdentProof :: AddIdent m a -> Proxy b -> Forall (InnerSame m) :- InnerSame m b+addIdentProof _ _ = inst++proxyFrom :: a -> Proxy a+proxyFrom _ = Proxy++proxyFromM :: m a -> Proxy a+proxyFromM _ = Proxy++proxyFromF1 :: (a -> b) -> Proxy a+proxyFromF1 _ = Proxy++proxyFromF2 :: (a -> b) -> Proxy b+proxyFromF2 _ = Proxy++instance AddInternal AddIdent where+ addInternal ai b = b \\ addIdentProof ai (proxyFrom b)++ mapInternal ai f = f \\ addIdentProof ai (proxyFromF2 f)+ \\ addIdentProof ai (proxyFromF1 f)++instance GetInternal AddIdent where+ getInternal ai _ f lb = f lb \\ addIdentProof ai (proxyFromF1 f)++-- -----------------------------------------------------------------------------++instance (MonadTower m) => MonadLevel_ (ContT r m) where+ type LowerMonad (ContT r m) = m+ type InnerValue (ContT r m) a = r+ type WithLower_ (ContT r m) = AddIM+ type AllowOtherValues (ContT r m) = False+ type DefaultAllowConstraints (ContT r m) = False++ wrap _ f = ContT $ \ cont -> f (`runContT` cont) (AddIM (>>= cont))++instance (MonadTower m) => MonadLevel_ (ExceptT e m) where+ type LowerMonad (ExceptT e m) = m+ type InnerValue (ExceptT e m) a = Either e a+ type WithLower_ (ExceptT e m) = AddIG++ wrap _ f = ExceptT $ f runExceptT (AddIG Right fmap (either . const))++instance (MonadTower m) => MonadLevel_ (IdentityT m) where+ type LowerMonad (IdentityT m) = m++ -- Using default coerce-based implementation as a test.+ -- wrap _ f = IdentityT $ f runIdentityT AddIdent++instance (MonadTower m) => MonadLevel_ (ListT m) where+ type LowerMonad (ListT m) = m+ type InnerValue (ListT m) a = [a]+ type WithLower_ (ListT m) = AddI+ type DefaultAllowConstraints (ListT m) = False++ wrap _ f = ListT $ f runListT (AddI (:[]) map)+ -- Can't define getInternal as that would require length <= 1++instance (MonadTower m) => MonadLevel_ (MaybeT m) where+ type LowerMonad (MaybeT m) = m+ type InnerValue (MaybeT m) a = Maybe a+ type WithLower_ (MaybeT m) = AddIG++ wrap _ f = MaybeT $ f runMaybeT (AddIG Just fmap maybe)++instance (MonadTower m) => MonadLevel_ (ReaderT r m) where+ type LowerMonad (ReaderT r m) = m++ wrap _ f = ReaderT $ \ r -> f (`runReaderT` r) AddIdent++map1 :: (a -> a') -> (a,b,c) -> (a',b,c)+map1 f (a,b,c) = (f a,b,c)+{-# INLINE map1 #-}++get1 :: (a,b,c) -> a+get1 (a,_,_) = a+{-# INLINE get1 #-}++instance (Monoid w, MonadTower m) => MonadLevel_ (LRWS.RWST r w s m) where+ type LowerMonad (LRWS.RWST r w s m) = m+ type InnerValue (LRWS.RWST r w s m) a = (a,s,w)+ type WithLower_ (LRWS.RWST r w s m) = AddIG++ wrap _ f = LRWS.RWST $ \ r s -> f (\m -> LRWS.runRWST m r s) (AddIG (,s,mempty) map1 (const (. get1)))++instance (Monoid w, MonadTower m) => MonadLevel_ (SRWS.RWST r w s m) where+ type LowerMonad (SRWS.RWST r w s m) = m+ type InnerValue (SRWS.RWST r w s m) a = (a,s,w)+ type WithLower_ (SRWS.RWST r w s m) = AddIG++ wrap _ f = SRWS.RWST $ \ r s -> f (\m -> SRWS.runRWST m r s) (AddIG (,s,mempty) map1 (const (. get1)))++instance (MonadTower m) => MonadLevel_ (LSt.StateT s m) where+ type LowerMonad (LSt.StateT s m) = m+ type InnerValue (LSt.StateT s m) a = (a,s)+ type WithLower_ (LSt.StateT s m) = AddIG++ wrap _ f = LSt.StateT $ \ s -> f (`LSt.runStateT` s) (AddIG (,s) first (const (. fst)))++instance (MonadTower m) => MonadLevel_ (SSt.StateT s m) where+ type LowerMonad (SSt.StateT s m) = m+ type InnerValue (SSt.StateT s m) a = (a,s)+ type WithLower_ (SSt.StateT s m) = AddIG++ wrap _ f = SSt.StateT $ \ s -> f (`SSt.runStateT` s) (AddIG (,s) first (const (. fst)))++instance (Monoid w, MonadTower m) => MonadLevel_ (LW.WriterT w m) where+ type LowerMonad (LW.WriterT w m) = m+ type InnerValue (LW.WriterT w m) a = (a,w)+ type WithLower_ (LW.WriterT w m) = AddIG++ wrap _ f = LW.WriterT $ f LW.runWriterT (AddIG (,mempty) first (const (. fst)))++instance (Monoid w, MonadTower m) => MonadLevel_ (SW.WriterT w m) where+ type LowerMonad (SW.WriterT w m) = m+ type InnerValue (SW.WriterT w m) a = (a,w)+ type WithLower_ (SW.WriterT w m) = AddIG++ wrap _ f = SW.WriterT $ f SW.runWriterT (AddIG (,mempty) first (const (. fst)))++-- -----------------------------------------------------------------------------++class (MonadTower m, m ~ BaseMonad m, BaseMonad m ~ m) => IsBaseMonad m++instance (MonadTower m, m ~ BaseMonad m, BaseMonad m ~ m) => IsBaseMonad m++type family SameMonad (m :: * -> *) (n :: * -> *) where+ SameMonad m m = True+ SameMonad m n = False++-- -----------------------------------------------------------------------------++-- | When considering whether a particular monad within a 'MonadTower'+-- stack satisfies a constraint, we need to be able to determine+-- this at the type level.+--+-- This is achieved with the 'ConstraintSatisfied' associated type:+-- it should be equated to a closed type family with the result+-- being 'True' for all monads for which the constraint is satisfied+-- and 'False' for all others.+--+-- (This is defined as a type class rather than just a type family+-- so that we can explicitly state that this needs to be defined.)+class ValidConstraint (c :: (* -> *) -> Constraint) where+ type ConstraintSatisfied c (m :: * -> *) :: Bool++instance ValidConstraint IsBaseMonad where+ type ConstraintSatisfied IsBaseMonad m = SameMonad (BaseMonad m) m
+ Control/Monad/Levels/Except.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}++-- unsafeCoerceConstraint is used to prevent the need for a complex+-- induction proof (which I'm not sure can actually be achieved).+{-# LANGUAGE Trustworthy #-}++{- |+ Module : Control.Monad.Levels.Except+ Description : Error-handling monadic computations+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Computations which may fail or throw exceptions.++ -}+module Control.Monad.Levels.Except+ ( throwError+ , catchError+ , ExceptT(..)+ , HasError+ , IsError+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints++import Data.Constraint++import Control.Exception (IOException, catch)+import Control.Monad.Trans.Except (ExceptT (..))+import qualified Control.Monad.Trans.Except as E++import Control.Monad.Trans.List (ListT)++-- -----------------------------------------------------------------------------++-- | Constraint for monads that can throw and handle exceptions.+class (MonadTower m) => IsError e m where++ _throwError :: e -> m a++ _catchError :: VarFunction (CatchFn e) m a++instance IsError IOException IO where++ _throwError = ioError++ _catchError = catch++instance IsError e (Either e) where++ _throwError = Left++ _catchError e f = either f Right e++instance (MonadTower m) => IsError e (ExceptT e m) where++ _throwError = E.throwE++ _catchError = E.catchE++instance ValidConstraint (IsError e) where+ type ConstraintSatisfied (IsError e) m = SameError e m++type family SameError e m where+ SameError IOException IO = True+ SameError e (Either e) = True+ SameError e (ExceptT e m) = True+ SameError e m = False++-- | A monad stack that can throw and handle exceptions of type @e@.+type HasError e m = SatisfyConstraint (IsError e) m++-- | Begin exception processing.+throwError :: forall e m a. (HasError e m) => e -> m a+throwError = liftSat (Proxy :: Proxy (IsError e)) . _throwError++type CatchFn e = Func MonadicValue (MkVarFn (Func (Const e) MonadicValue))++-- | Handle exception processing.+catchError :: forall e m a. (HasError e m) => m a -> (e -> m a) -> m a+catchError = lowerSat' c vf m a (Sub Dict) _catchError+ where+ c :: Proxy (IsError e)+ c = Proxy++ vf :: Proxy (CatchFn e)+ vf = Proxy++ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy++-- -----------------------------------------------------------------------------++instance (MonadTower m) => ConstraintPassThrough (IsError e) (ListT m) True
+ Control/Monad/Levels/RWS.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, TypeFamilies #-}++{- |+ Module : Control.Monad.Levels.RWS+ Description : Monads with reader, writer and state abilities+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Note that the original definitions are used for the various reader,+writer and state computations: as such, if there is (for example)+another level that satisfies 'IsReader r' above the one that satisfies+'IsRWS r w s' in the stack, then calling 'ask' will use the higher+level.++ -}+module Control.Monad.Levels.RWS+ ( HasRWS+ , IsRWS+ , module Control.Monad.Levels.Reader+ , module Control.Monad.Levels.Writer+ , module Control.Monad.Levels.State+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints+import Control.Monad.Levels.Reader+import Control.Monad.Levels.State+import Control.Monad.Levels.Writer++import Data.Monoid (Monoid)++import qualified Control.Monad.Trans.RWS.Lazy as L+import qualified Control.Monad.Trans.RWS.Strict as S++-- -----------------------------------------------------------------------------++-- | Defined as another class rather than an alias in case you need to+-- ensure the same level satisfies all three constraints (and to+-- have a specific 'ValidConstraint' instance).+class (IsReader r m, IsWriter w m, IsState s m) => IsRWS r w s m++instance (MonadTower m, Monoid w) => IsRWS r w s (L.RWST r w s m)++instance (MonadTower m, Monoid w) => IsRWS r w s (S.RWST r w s m)++instance (Monoid w) => ValidConstraint (IsRWS r w s) where+ type ConstraintSatisfied (IsRWS r w s) m = SameRWS r w s m++type family SameRWS r w s m where+ SameRWS r w s (L.RWST r w s m) = True+ SameRWS r w s (S.RWST r w s m) = True+ SameRWS r w s m = False++type HasRWS r w s m = SatisfyConstraint (IsRWS r w s) m
+ Control/Monad/Levels/RWS/Lazy.hs view
@@ -0,0 +1,22 @@+{- |+ Module : Control.Monad.Levels.RWS.Lazy+ Description : Lazy monad with reader, writer and state abilities+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Note that the original definitions are used for the various reader,+writer and state computations: as such, if there is (for example)+another level that satisfies 'IsReader r' above the one that satisfies+'IsRWS r w s' in the stack, then calling 'ask' will use the higher+level.++ -}+module Control.Monad.Levels.RWS.Lazy+ ( RWST(..)+ , module Control.Monad.Levels.RWS+ ) where++import Control.Monad.Levels.RWS++import Control.Monad.Trans.RWS.Lazy
+ Control/Monad/Levels/RWS/Strict.hs view
@@ -0,0 +1,22 @@+{- |+ Module : Control.Monad.Levels.RWS.Strict+ Description : Strict monad with reader, writer and state abilities+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Note that the original definitions are used for the various reader,+writer and state computations: as such, if there is (for example)+another level that satisfies 'IsReader r' above the one that satisfies+'IsRWS r w s' in the stack, then calling 'ask' will use the higher+level.++ -}+module Control.Monad.Levels.RWS.Strict+ ( RWST(..)+ , module Control.Monad.Levels.RWS+ ) where++import Control.Monad.Levels.RWS++import Control.Monad.Trans.RWS.Strict
+ Control/Monad/Levels/Reader.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, PolyKinds, ScopedTypeVariables, TypeFamilies+ #-}++{- |+ Module : Control.Monad.Levels.Reader+ Description : Dealing with Reader+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Provides a shared environment for reading values and executing+sub-computations in a modified environment.++ -}+module Control.Monad.Levels.Reader+ ( ask+ , asks+ , reader+ , local+ , ReaderT(..)+ , HasReader+ , IsReader+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints++import Control.Monad.Trans.Cont (ContT)+import Control.Monad.Trans.List (ListT)+import Control.Monad.Trans.Reader (ReaderT (..))+import qualified Control.Monad.Trans.Reader as R+import qualified Control.Monad.Trans.RWS.Lazy as LRWS+import qualified Control.Monad.Trans.RWS.Strict as SRWS+import Data.Monoid++-- -----------------------------------------------------------------------------++-- | The minimal definitions needed by a monad providing a Reader+-- environment.+class (MonadTower m) => IsReader r m where++ _local :: (r -> r) -> m a -> m a++ _reader :: (r -> a) -> m a++instance ValidConstraint (IsReader r) where+ type ConstraintSatisfied (IsReader r) m = SameReader r m++type family SameReader r m where+ SameReader r ((->) r) = True+ SameReader r (ReaderT r m) = True+ SameReader r (LRWS.RWST r w s m) = True+ SameReader r (SRWS.RWST r w s m) = True+ SameReader r m = False++-- | A monad stack containing a Reader environment of type @r@.+type HasReader r m = SatisfyConstraint (IsReader r) m++-- | Execute a computation in a modified environment.+local :: forall r m a. (HasReader r m) => (r -> r) -> m a -> m a+local = lowerFunction (Proxy :: Proxy (IsReader r)) . _local++-- | Retrieve a function of the current environment.+reader :: forall r m a. (HasReader r m) => (r -> a) -> m a+reader = liftSat (Proxy :: Proxy (IsReader r)) . _reader++-- | Obtain the reader environment.+ask :: (HasReader r m) => m r+ask = reader id++-- | Retrieve a function of the current environment. An alias of+-- 'reader'.+asks :: (HasReader r m) => (r -> a) -> m a+asks = reader++-- -----------------------------------------------------------------------------++instance (MonadTower m) => IsReader r (ReaderT r m) where++ _local = R.local++ _reader = R.reader++instance IsReader r ((->) r) where++ _local f m = m . f++ _reader = id++instance (MonadTower m, Monoid w) => IsReader r (LRWS.RWST r w s m) where++ _local = LRWS.local++ _reader = LRWS.reader++instance (MonadTower m, Monoid w) => IsReader r (SRWS.RWST r w s m) where++ _local = SRWS.local++ _reader = SRWS.reader++-- -----------------------------------------------------------------------------+-- Dealing with ContT and ListT++instance (MonadTower m) => ConstraintPassThrough (IsReader r) (ContT c m) True+instance (MonadTower m) => ConstraintPassThrough (IsReader r) (ListT m) True
+ Control/Monad/Levels/State.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}++{- |+ Module : Control.Monad.Levels.State+ Description : Dealing with State+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Monad environments for stateful computations.++ -}+module Control.Monad.Levels.State+ ( state+ , get+ , gets+ , put+ , modify+ , modify'+ , HasState+ , IsState+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints++import Control.Monad.Trans.Cont (ContT)+import Control.Monad.Trans.List (ListT)+import qualified Control.Monad.Trans.RWS.Lazy as LRWS+import qualified Control.Monad.Trans.RWS.Strict as SRWS+import qualified Control.Monad.Trans.State.Lazy as LSt+import qualified Control.Monad.Trans.State.Strict as SSt+import Data.Monoid (Monoid)++-- -----------------------------------------------------------------------------++-- | The minimal definition needed for a monad providing a stateful+-- environment.+class (MonadTower m) => IsState s m where++ _state :: (s -> (a,s)) -> m a++instance ValidConstraint (IsState s) where+ type ConstraintSatisfied (IsState s) m = SameState s m++type family SameState s m where+ SameState s (LSt.StateT s m) = True+ SameState s (SSt.StateT s m) = True+ SameState s (LRWS.RWST r w s m) = True+ SameState s (SRWS.RWST r w s m) = True+ SameState s m = False++-- | A monad stack containing a stateful environment of type @s@.+type HasState s m = SatisfyConstraint (IsState s) m++-- | Embed a simple state action into the monad stack.+state :: forall m s a. (HasState s m) => (s -> (a,s)) -> m a+state = liftSat (Proxy :: Proxy (IsState s)) . _state++-- | Obtain the state environment.+get :: (HasState s m) => m s+get = state (\s -> (s,s))++-- | Apply a function to the stateful environment. Equivalent to+-- @fmap f 'get'@.+gets :: (HasState s m) => (s -> a) -> m a+gets f = state (\s -> (f s, s))++-- | Replace the stateful environment.+put :: (HasState s m) => s -> m ()+put s = state (const ((),s))++-- | Map the old state to a new state, and discard the old one.+-- Equivalent to @'gets' f >>= 'put'@.+modify :: (HasState s m) => (s -> s) -> m ()+modify f = state (\ s -> ((), f s))++-- | A variant of 'modify' in which the computation is strict in the+-- new state.+modify' :: (HasState s m) => (s -> s) -> m ()+modify' f = state (\ s -> let s' = f s in s' `seq` ((), s'))++-- -----------------------------------------------------------------------------++instance (MonadTower m) => IsState s (LSt.StateT s m) where++ _state = LSt.state++instance (MonadTower m) => IsState s (SSt.StateT s m) where++ _state = SSt.state++instance (MonadTower m, Monoid w) => IsState s (LRWS.RWST r w s m) where++ _state = LRWS.state++instance (MonadTower m, Monoid w) => IsState s (SRWS.RWST r w s m) where++ _state = SRWS.state++-- -----------------------------------------------------------------------------+-- Dealing with ContT and ListT++instance (MonadTower m) => ConstraintPassThrough (IsState s) (ContT r m) True+instance (MonadTower m) => ConstraintPassThrough (IsState s) (ListT m) True
+ Control/Monad/Levels/State/Lazy.hs view
@@ -0,0 +1,25 @@+{- |+ Module : Control.Monad.Levels.State.Lazy+ Description : Lazy stateful computations+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Lazy stateful computations.++ -}+module Control.Monad.Levels.State.Lazy+ ( state+ , get+ , gets+ , put+ , modify+ , modify'+ , StateT(..)+ , HasState+ , IsState+ ) where++import Control.Monad.Levels.State++import Control.Monad.Trans.State.Lazy (StateT (..))
+ Control/Monad/Levels/State/Strict.hs view
@@ -0,0 +1,25 @@+{- |+ Module : Control.Monad.Levels.State.Strict+ Description : Strict stateful computations+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++Strict stateful computations.++ -}+module Control.Monad.Levels.State.Strict+ ( state+ , get+ , gets+ , put+ , modify+ , modify'+ , StateT(..)+ , HasState+ , IsState+ ) where++import Control.Monad.Levels.State++import Control.Monad.Trans.State.Strict (StateT (..))
+ Control/Monad/Levels/Transformers.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies,+ UndecidableInstances #-}++{- |+ Module : Control.Monad.Levels.Transformers+ Description : Lower down to a specific transformer+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Transformers+ ( HasTransformer+ , TransformedMonad+ , liftT+ -- * Exported for use with custom instances+ , IsTransformer+ ) where++import Control.Monad.Levels.Constraints+import Control.Monad.Levels.Definitions++import Control.Monad.Trans.Cont (ContT)+import Control.Monad.Trans.Except (ExceptT)+import Control.Monad.Trans.List (ListT)+import Control.Monad.Trans.Reader+import qualified Control.Monad.Trans.State.Lazy as LSt+import qualified Control.Monad.Trans.State.Strict as SSt++-- -----------------------------------------------------------------------------++-- | Unlike 'HasBaseMonad', this is not a universal constraint+-- applicable to all 'MonadLevel' instances, as otherwise it can be+-- used to bypass the lack of an allowed constraint.+type HasTransformer t m = ( SatisfyConstraint (IsTransformer t) m+ , MonadLevel (TransformedMonad t m)+ , TransformedMonad t m ~ t (LowerMonad (TransformedMonad t m)))++-- | The sub-part of the monadic stack where the requested transformer+-- is on top.+type TransformedMonad t m = SatMonad (IsTransformer t) m++class (MonadLevel m, m ~ t (LowerMonad m), t (LowerMonad m) ~ m) => IsTransformer t m++instance (MonadLevel m, m ~ t (LowerMonad m), t (LowerMonad m) ~ m) => IsTransformer t m++instance ValidConstraint (IsTransformer t) where+ type ConstraintSatisfied (IsTransformer t) m = SameTransformer t m++type family SameTransformer (t :: (* -> *) -> * -> *) (m :: * -> *) where+ SameTransformer t (t m) = True+ SameTransformer t m = False++liftT :: (HasTransformer t m) => TransformedMonad t m a -> m a+liftT m = liftSat (Proxy :: Proxy (IsTransformer t)) m++-- -----------------------------------------------------------------------------+-- ContT and ListT instances++-- Note: RWS transformers aren't allowed for ContT and ListT as they+-- don't allow passing through of Writer manipulations.++instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (ContT r)) (ListT m) True++instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (ExceptT e)) (ListT m) True++instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (ReaderT r)) (ContT c m) True+instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (ReaderT r)) (ListT m) True++instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (LSt.StateT s)) (ContT r m) True+instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (LSt.StateT s)) (ListT m) True++instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (SSt.StateT s)) (ContT r m) True+instance (MonadLevel m) => ConstraintPassThrough (IsTransformer (SSt.StateT s)) (ListT m) True
+ Control/Monad/Levels/Writer.hs view
@@ -0,0 +1,143 @@+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,+ MultiParamTypeClasses, ScopedTypeVariables, TupleSections,+ TypeFamilies #-}++{- |+ Module : Control.Monad.Levels.Writer+ Description : Writer/logging monads+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Writer+ ( writer+ , tell+ , HasWriter+ , listen+ , CanListen+ , ListenFn+ , pass+ , CanPass+ , PassFn+ , IsWriter+ ) where++import Control.Monad.Levels+import Control.Monad.Levels.Constraints++import Control.Arrow (second)+import Data.Monoid (Endo (..), Monoid (..))++import qualified Control.Monad.Trans.RWS.Lazy as LRWS+import qualified Control.Monad.Trans.RWS.Strict as SRWS+import qualified Control.Monad.Trans.Writer.Lazy as LW+import qualified Control.Monad.Trans.Writer.Strict as SW++-- -----------------------------------------------------------------------------++-- | The minimal definition needed for a monad providing a writer+-- environment.+class (Monoid w, MonadTower m) => IsWriter w m where++ _writer :: (a,w) -> m a++ _listen :: m a -> m (a,w)++ _pass :: m (a, w -> w) -> m a++instance (Monoid w, MonadTower m) => IsWriter w (LW.WriterT w m) where++ _writer = LW.writer++ _listen = LW.listen++ _pass = LW.pass++instance (Monoid w, MonadTower m) => IsWriter w (SW.WriterT w m) where++ _writer = SW.writer++ _listen = SW.listen++ _pass = SW.pass++instance (Monoid w, MonadTower m) => IsWriter w (LRWS.RWST r w s m) where++ _writer = LRWS.writer++ _listen = LRWS.listen++ _pass = LRWS.pass++instance (Monoid w, MonadTower m) => IsWriter w (SRWS.RWST r w s m) where++ _writer = SRWS.writer++ _listen = SRWS.listen++ _pass = SRWS.pass++instance (Monoid w) => ValidConstraint (IsWriter w) where+ type ConstraintSatisfied (IsWriter w) m = SameWriter w m++type family SameWriter w m where+ SameWriter w (LW.WriterT w m) = True+ SameWriter w (SW.WriterT w m) = True+ SameWriter w (LRWS.RWST r w s m) = True+ SameWriter w (SRWS.RWST r w s m) = True+ SameWriter w m = False++type HasWriter w m = (Monoid w, SatisfyConstraint (IsWriter w) m)++-- | Embed a simple writer action.+writer :: forall w m a. (HasWriter w m) => (a,w) -> m a+writer = liftSat (Proxy :: Proxy (IsWriter w)) . _writer++-- | An action that produces the output @w@.+tell :: (HasWriter w m) => w -> m ()+tell = writer . ((),)++type CanListen w m a = SatisfyConstraintF (IsWriter w) m a (ListenFn w)++type ListenFn w = Func MonadicValue (MkVarFnFrom (MonadicTuple w))++-- | Execute the action @m@ and add its output to the value of the+-- computation.+listen :: forall w m a. (CanListen w m a) => m a -> m (a,w)+listen = lowerSat c f m a _listen+ where+ c :: Proxy (IsWriter w)+ c = Proxy++ f :: Proxy (ListenFn w)+ f = Proxy++ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy++type CanPass w m a = SatisfyConstraintF (IsWriter w) m a (PassFn w)++type PassFn w = MkVarFn (MonadicTuple (Endo w))++-- | Execute the action @m@ (which returns a value and a function) and+-- returns the value, applying the function to the output.+pass :: forall w m a. (CanPass w m a) => m (a, w -> w) -> m a+pass = lowerSat c f m a (_pass . fmap (second appEndo)) . fmap (second Endo)+ where+ c :: Proxy (IsWriter w)+ c = Proxy++ f :: Proxy (PassFn w)+ f = Proxy++ m :: Proxy m+ m = Proxy++ a :: Proxy a+ a = Proxy
+ Control/Monad/Levels/Writer/Lazy.hs view
@@ -0,0 +1,26 @@+{- |+ Module : Control.Monad.Levels.Writer.Lazy+ Description : Lazy writer monad+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Writer.Lazy+ ( writer+ , tell+ , HasWriter+ , listen+ , CanListen+ , ListenFn+ , pass+ , CanPass+ , PassFn+ , WriterT(..)+ , IsWriter+ ) where++import Control.Monad.Levels.Writer+import Control.Monad.Trans.Writer.Lazy (WriterT (..))
+ Control/Monad/Levels/Writer/Strict.hs view
@@ -0,0 +1,26 @@+{- |+ Module : Control.Monad.Levels.Writer.Strict+ Description : Strict writer monad+ Copyright : (c) Ivan Lazar Miljenovic+ License : 3-Clause BSD-style+ Maintainer : Ivan.Miljenovic@gmail.com++++ -}+module Control.Monad.Levels.Writer.Strict+ ( writer+ , tell+ , HasWriter+ , listen+ , CanListen+ , ListenFn+ , pass+ , CanPass+ , PassFn+ , WriterT(..)+ , IsWriter+ ) where++import Control.Monad.Levels.Writer+import Control.Monad.Trans.Writer.Strict (WriterT (..))
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2014 Ivan Lazar Miljenovic++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,106 @@+`monad-levels`+==============++Why not mtl?+------------++The oft-spouted problem with the standard monad transformer library+[mtl] and similar libraries is that instances are quadratic: you need+a separate instance for each valid combination of transformer ++typeclass.++[mtl]: http://hackage.haskell.org/package/mtl++For end users, this isn't really a problem: after all, all the+required instances have already been written for you!++But what happens if you have a custom transformer, or a custom+typeclass?++What about if you want to have something like `MonadIO` but for a+different base monad?++Then you need to write all those extra instances.++What makes it more frustrating is that many of the instance+definitions are identical: typically for every transformer (using+`StateT s m` as an example) it becomes a matter of:++* Possibly unwrap the transformer from a monadic value to get the+ lower monad (e.g. `StateT s m a -> m (a,s)`);++* Possibly add internal values (e.g. `m a -> m (a,s)`);++* Wrap the lower monad from the result of the computation back up into+ the transformer (e.g. `m (a,s) -> StateT s m a`).++The solution+------------++Ideally, instead we'd have something along the lines of (simplified):++```haskell++class (Monad m) => MonadBase m where+ type BaseMonad m :: * -> *++ liftBase :: BaseMonad m a -> m a++class (MonadBase m) => MonadLevel m where++ type LowerMonad m :: * -> *++ type InnerValue m a :: *++ -- A continuation-based approach for how to lift/lower a monadic value.+ wrap :: ( (m a -> LowerMonad m (InnerValue m a) -- unwrap+ -> (LowerMonad m a -> LowerMonad m (InnerValue m a)) -- addInternal+ -> LowerMonad m (InnerValue m a)+ )+ -> m a+```++With these two classes, we could then use Advanced Type Hackery (TM)+to let us instead just specify instances for the transformers/monads+that *do* have direct implementations for a typeclass, and then have+the rest defined for us!++It turns out that this approach is even powerful enough to make+`liftBase` redundant, and it isn't limited to just lifting a monad but+can instead be used for arbitrary functions.++Advantages+----------++* Minimal specification required for adding new typeclasses: just+ specify the instances for monads that satisfy it, and then use the+ provided machinery to lift/lower methods to other transformers in+ the monadic stack.++* Works even for polyvariadic functions.++* Still allows specifying whether certain transformers do _not_ allow+ some constraints to pass through (e.g. `ContT` does not allow access+ to a `WriterT`).++Disadvantages+-------------++* Requires a _lot_ of GHC extensions.++* Requires usage of proxies when lifting/lowering typeclass methods.++* Large usage of associated types means type errors can be difficult+ to decipher.++* Due to usage of closed type-families, it is not possible to add+ extra instances to typeclasses (i.e. it is not possible to use a+ custom `State` monad/monad-transformer with+ `Control.Monad.Levels.State`).++* Currently un-benchmarked; as such, it's not known how much of a+ performance penalty this approach takes.++* Lowering polyvariadic functions requires specifying the type of the+ function using a specific grammar (though the common `m a -> m a`+ case is pre-defined).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TODO.md view
@@ -0,0 +1,27 @@+* Finish off re-implementing all mtl classes.++* Implement being able to change out the underlying stack from a+ transformer (e.g. `StateT s m a -> StateT s n a`).++* Clean up API.++ - Determine what needs to be exported+ - Should variadic-functions be exported from Levels.hs?+ - Change Constraint synonyms to type-classes for better error+ reporting?+ - Should VArgs be able to have different constraints for+ lifting/lowering?++* Documentation++ - Document modules+ - Add extra documentation modules:+ + How to use the library+ + How to add extra base monads+ + How to add extra levels+ + How to add a new transformer class+ + Dealing with variadic functions++* Test suite++* Benchmarking and performance enhancements
+ monad-levels.cabal view
@@ -0,0 +1,55 @@+-- Initial monad-levels.cabal generated by cabal init. For further+-- documentation, see http://haskell.org/cabal/users-guide/++name: monad-levels+version: 0.1.0.0+synopsis: Specific levels of monad transformers+description: An automatic way of adding instances to monad classes.+homepage: https://github.com/ivan-m/monad-levels+bug-reports: https://github.com/ivan-m/monad-levels/issues+license: MIT+license-file: LICENSE+author: Ivan Lazar Miljenovic+maintainer: Ivan.Miljenovic@gmail.com+-- copyright:+category: Control+build-type: Simple+extra-source-files: README.md+ CHANGELOG.md+ TODO.md+cabal-version: >=1.10++source-repository head+ type: git+ location: git://github.com/ivan-m/monad-levels.git++library+ exposed-modules: Control.Monad.Levels+ , Control.Monad.Levels.Constraints+ , Control.Monad.Levels.Transformers++ , Control.Monad.Levels.Cont+ , Control.Monad.Levels.Except+ , Control.Monad.Levels.Reader+ , Control.Monad.Levels.State+ , Control.Monad.Levels.State.Lazy+ , Control.Monad.Levels.State.Strict+ , Control.Monad.Levels.Writer+ , Control.Monad.Levels.Writer.Lazy+ , Control.Monad.Levels.Writer.Strict++ , Control.Monad.Levels.RWS+ , Control.Monad.Levels.RWS.Lazy+ , Control.Monad.Levels.RWS.Strict++ other-modules: Control.Monad.Levels.Definitions+ , Control.Monad.Levels.ConstraintPassing++ -- other-extensions:+ build-depends: base >=4.7 && <4.8+ , transformers == 0.4.*+ , constraints == 0.4.*+ -- hs-source-dirs:+ default-language: Haskell2010++ ghc-options: -Wall