A generic transformation of a DepT-effectful function of any number of arguments, provided the function satisfies certain constraints on the arguments, the environment type constructor and base monad, and the return type.

It is parameterized by three constraints:

• ca of kind Type -> Constraint, the constraint required of each argument (usually something like Show).
• cem of kind ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint, a two-place constraint required of the environment type constructor / base monad combination. Note that the environment type constructor remains unapplied. That is, for a given cem, cem NilEnv IO kind-checks but cem (NilEnv IO) IO doesn't. See also Ensure.
• cr of kind Type -> Constraint, the constraint required of the return type.

We can define Advices that work with concrete types by using MustBe in the case of ca and cr, and MustBe2 in the case of cem.

Advices that don't care about a particular constraint can leave it polymorphic, and this facilitates composition, but the constraint must be given some concrete value (Top in the case of ca and cr, Top2 in the case of cem) through type application at the moment of calling advise.

See Control.Monad.Dep.Advice.Basic for examples.

The most general (and complex) way of constructing Advices.

Advices work in two phases. First, the arguments of the transformed function are collected into an n-ary product NP, and passed to the first argument of makeAdvice, which produces a (possibly transformed) product of arguments, along with some summary value of type u. Use () as the summary value if you don't care about it.

In the second phase, the monadic action produced by the function once all arguments have been given is transformed using the second argument of makeAdvice. This second argument also receives the summary value of type u calculated earlier.

>>> :{
 doesNothing :: forall ca cem cr. Advice ca cem cr
 doesNothing = makeAdvice @() (\args -> pure (pure args)) (\() action -> action)
:}

IMPORTANT! When invoking makeAdvice, you must always give the type of the existential u through a type application. Otherwise you'll get weird "u is untouchable" errors.

Create an advice which only tweaks and/or analyzes the function arguments.

Notice that there's no u parameter, unlike with makeAdvice.

>>> :{
 doesNothing :: forall ca cem cr. Advice ca cem cr
 doesNothing = makeArgsAdvice pure
:}

Create an advice which only tweaks the execution of the final monadic action.

Notice that there's no u parameter, unlike with makeAdvice.

>>> :{
 doesNothing :: forall ca cem cr. Advice ca cem cr
 doesNothing = makeExecutionAdvice id
:}

Apply an Advice to some compatible function. The function must have its effects in DepT, and satisfy the constraints required by the Advice.

IMPORTANT! If the ca, cem or cr constraints of the supplied Advice remain polymorphic, they must be given types by means of type applications:

>>> :{
 foo :: Int -> DepT NilEnv IO String
 foo _ = pure "foo"
 advisedFoo1 = advise (returnMempty @Top @Top2) foo
 advisedFoo2 = advise @Top @Top2 returnMempty foo
 advisedFoo3 = advise (printArgs @Top stdout "args: ") foo
 advisedFoo4 = advise @_ @_ @Top (printArgs stdout "args: ") foo
:}

Ensure is a helper for lifting typeclass definitions of the form:

>>> :{
 type HasLogger :: Type -> (Type -> Type) -> Constraint
 class HasLogger em m | em -> m where
   logger :: em -> String -> m ()
:}

To work as the cem constraint, like this:

>>> type FooAdvice = Advice Top (Ensure HasLogger) Top

Why is it necessary? Two-place HasX-style constraints receive the "fully applied" type of the record-of-functions. That is: NilEnv IO instead of simply NilEnv. This allows them to also work with monomorphic environments (like those in RIO) whose type isn't parameterized by any monad.

But the cem constraint works with the type constructor of the environment record, of kind (Type -> Type) -> Type, and not with the fully applied type of kind Type.

A two-place constraint which requires nothing of the environment and the base monad.

Useful as the cem type application argument of advise and restrictEnv.

For similar behavior with the ar and cr type arguments of advise and restrictEnv, use Top from "sop-core".

>>> type UselessAdvice = Advice Top Top2 Top

Combines two two-place constraints on the environment / monad pair.

For example, an advice which requires both Ensure HasLogger and Ensure HasRepository might use this.

Useful to build the cem type application argument of advise and restrictEnv.

For similar behavior with the ar and cr type arguments of advise and restrictEnv, use And from "sop-core".

Require a constraint only on the base monad, for example a base moonad with MonadIO.

Useful to build cem type application argument of advise and restrictEnv.

>>> type FooAdvice = Advice Top (MonadConstraint MonadIO) Top

>>> type FooAdvice = Advice Top (MonadConstraint (MonadReader Int)) Top

Require a constraint only on the unapplied environment type constructor, which has kind (Type -> Type) -> Type.

Can be used to build cem type application argument of advise and restrictEnv.

Most of the time this is not what you want. One exception is when pinning the environment with a MustBe equality constraint, while leaving the base monad free:

>>> type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top

If what you want is to lift a two-parameter HasX-style typeclass to cem, use Ensure instead.

A class synonym for (~), the type equality constraint.

Poly-kinded, so it can be applied both to type constructors (like monads) and to concrete types.

It this library it will be used partially applied:

>>> type FooAdvice = Advice Top (MonadConstraint (MustBe IO)) Top

>>> type FooAdvice = Advice Top Top2 (MustBe String)

Pins both the environment type constructor and the base monad. Sometimes we don't want to advise functions in some generic environment, but in a concrete environment having access to all the fields, and in a concrete base monad.

Useful to build the cem type application argument of advise and restricEnv.

For similar behavior with the ar and cr type arguments of advise and restrictEnv, use MustBe.

It this library it will be used partially applied:

>>> type FooAdvice = Advice Top (MustBe2 NilEnv IO) Top

Makes the constraint on the arguments more restrictive.

Makes the constraint on the environment / monad more restrictive.

Makes the constraint on the result more restrictive.

Given a base monad m action that gets hold of the DepT environment, run the DepT transformer at the tip of a curried function.

>>> :{
 foo :: Int -> Int -> Int -> DepT NilEnv IO ()
 foo _ _ _ = pure ()
:}

>>> runFinalDepT (pure NilEnv) foo 1 2 3 :: IO ()

Given a base monad m action that gets hold of the DepT environment, and a function capable of extracting a curried function from the environment, run the DepT transformer at the tip of the resulting curried function.

Why put the environment behind the m action? Well, since getting to the end of the curried function takes some work, it's a good idea to have some flexibility once we arrive there. For example, the environment could be stored in a Data.IORef and change in response to events, perhaps with advices being added or removed.

>>> :{
  type MutableEnv :: (Type -> Type) -> Type
  data MutableEnv m = MutableEnv { _foo :: Int -> m (Sum Int) }
  :}

>>> :{
  do envRef <- newIORef (MutableEnv (pure . Sum))
     let foo' = runFromEnv (readIORef envRef) _foo
     do r <- foo' 7
        print r
     modifyIORef envRef (\e -> e { _foo = advise @Top @Top2 returnMempty (_foo e) })
     do r <- foo' 7
        print r
:}
Sum {getSum = 7}
Sum {getSum = 0}

A constraint that can always be satisfied.

Since: sop-core-0.2

Pairing of constraints.

Since: sop-core-0.2

Require a constraint for every element of a list.

If you have a datatype that is indexed over a type-level list, then you can use All to indicate that all elements of that type-level list must satisfy a given constraint.

Example: The constraint

All Eq '[ Int, Bool, Char ]

is equivalent to the constraint

(Eq Int, Eq Bool, Eq Char)

Example: A type signature such as

f :: All Eq xs => NP I xs -> ...

means that f can assume that all elements of the n-ary product satisfy Eq.

Note on superclasses: ghc cannot deduce superclasses from All constraints. You might expect the following to compile

class (Eq a) => MyClass a

foo :: (All Eq xs) => NP f xs -> z
foo = [..]

bar :: (All MyClass xs) => NP f xs -> x
bar = foo

but it will fail with an error saying that it was unable to deduce the class constraint AllF Eq xs (or similar) in the definition of bar. In cases like this you can use Dict from Data.SOP.Dict to prove conversions between constraints. See this answer on SO for more details.

An n-ary product.

The product is parameterized by a type constructor f and indexed by a type-level list xs. The length of the list determines the number of elements in the product, and if the i-th element of the list is of type x, then the i-th element of the product is of type f x.

The constructor names are chosen to resemble the names of the list constructors.

Two common instantiations of f are the identity functor I and the constant functor K. For I, the product becomes a heterogeneous list, where the type-level list describes the types of its components. For K a, the product becomes a homogeneous list, where the contents of the type-level list are ignored, but its length still specifies the number of elements.

In the context of the SOP approach to generic programming, an n-ary product describes the structure of the arguments of a single data constructor.

Examples:

I 'x'    :* I True  :* Nil  ::  NP I       '[ Char, Bool ]
K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]

The identity type functor.

Like Identity, but with a shorter name.

Specialization of hcfoldMap.

Since: sop-core-0.3.2.0

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only became sufficiently general to support this instance in GHC 7.8, so prior to 7.8 this instance is unavailable.

But due to the coherence of instance resolution in Haskell, this Category has some very interesting properties. Notably, in the absence of IncoherentInstances, this category is "thin", which is to say that between any two objects (constraints) there is at most one distinguishable arrow.

This means that for instance, even though there are two ways to derive Ord a :- Eq [a], the answers from these two paths _must_ by construction be equal. This is a property that Haskell offers that is pretty much unique in the space of languages with things they call "type classes".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and then from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

Diagrammatically,

                   Ord a
               ins /     \ cls
                  v       v
            Ord [a]     Eq a
               cls \     / ins
                    v   v
                   Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

Values of type Dict p capture a dictionary for a constraint of type p.

e.g.

Dict :: Dict (Eq Int)

captures a dictionary that proves we have an:

instance Eq 'Int

Pattern matching on the Dict constructor will bring this instance into scope.