diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +0.1.0.0 +------- +* Initial release diff --git a/Control/Monad/Levels.hs b/Control/Monad/Levels.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels.hs @@ -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 diff --git a/Control/Monad/Levels/ConstraintPassing.hs b/Control/Monad/Levels/ConstraintPassing.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/ConstraintPassing.hs @@ -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 diff --git a/Control/Monad/Levels/Constraints.hs b/Control/Monad/Levels/Constraints.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Constraints.hs @@ -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)) + +-- ----------------------------------------------------------------------------- diff --git a/Control/Monad/Levels/Cont.hs b/Control/Monad/Levels/Cont.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Cont.hs @@ -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 + handles them. For +example, with a lazy state transformer, using this module results in +, +whereas @mtl@ uses +. + + -} +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 +-- +-- 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 diff --git a/Control/Monad/Levels/Definitions.hs b/Control/Monad/Levels/Definitions.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Definitions.hs @@ -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 diff --git a/Control/Monad/Levels/Except.hs b/Control/Monad/Levels/Except.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Except.hs @@ -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 diff --git a/Control/Monad/Levels/RWS.hs b/Control/Monad/Levels/RWS.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/RWS.hs @@ -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 diff --git a/Control/Monad/Levels/RWS/Lazy.hs b/Control/Monad/Levels/RWS/Lazy.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/RWS/Lazy.hs @@ -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 diff --git a/Control/Monad/Levels/RWS/Strict.hs b/Control/Monad/Levels/RWS/Strict.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/RWS/Strict.hs @@ -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 diff --git a/Control/Monad/Levels/Reader.hs b/Control/Monad/Levels/Reader.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Reader.hs @@ -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 diff --git a/Control/Monad/Levels/State.hs b/Control/Monad/Levels/State.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/State.hs @@ -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 diff --git a/Control/Monad/Levels/State/Lazy.hs b/Control/Monad/Levels/State/Lazy.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/State/Lazy.hs @@ -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 (..)) diff --git a/Control/Monad/Levels/State/Strict.hs b/Control/Monad/Levels/State/Strict.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/State/Strict.hs @@ -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 (..)) diff --git a/Control/Monad/Levels/Transformers.hs b/Control/Monad/Levels/Transformers.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Transformers.hs @@ -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 diff --git a/Control/Monad/Levels/Writer.hs b/Control/Monad/Levels/Writer.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Writer.hs @@ -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 diff --git a/Control/Monad/Levels/Writer/Lazy.hs b/Control/Monad/Levels/Writer/Lazy.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Writer/Lazy.hs @@ -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 (..)) diff --git a/Control/Monad/Levels/Writer/Strict.hs b/Control/Monad/Levels/Writer/Strict.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/Levels/Writer/Strict.hs @@ -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 (..)) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/TODO.md b/TODO.md new file mode 100644 --- /dev/null +++ b/TODO.md @@ -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 diff --git a/monad-levels.cabal b/monad-levels.cabal new file mode 100644 --- /dev/null +++ b/monad-levels.cabal @@ -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