packages feed

dep-t-advice (empty) → 0.1.0.0

raw patch · 9 files changed

+1497/−0 lines, 9 filesdep +basedep +constraintsdep +dep-tsetup-changed

Dependencies added: base, constraints, dep-t, dep-t-advice, doctest, mtl, rank2classes, sop-core, tasty, tasty-hunit, template-haskell, transformers

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for dep-t-advice
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2021, Daniel Diaz
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Daniel Diaz nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,137 @@+# dep-t-advice
+
+This package is a companion to
+[dep-t](http://hackage.haskell.org/package/dep-t). It provides a mechanism for
+handling cross-cutting concerns in your application by adding "advices" to the
+functions in your record-of-functions, in a way that is composable and
+independent of each function's particular number of arguments.
+
+## Rationale
+
+So, you have decided to structure your program in a record-of-functions style,
+using [dep-t](http://hackage.haskell.org/package/dep-t). Good choice!
+
+You have already selected your functions, decided which base monad use for
+`DepT`, and now you are ready to construct the environment record, which serves
+as your [composition
+root](https://stackoverflow.com/questions/6277771/what-is-a-composition-root-in-the-context-of-dependency-injection).
+
+Now seems like a good moment to handle some of those pesky ["croscutting
+concerns"](https://en.wikipedia.org/wiki/Cross-cutting_concern), don't you
+think?
+
+Stuff like:
+
+- Logging
+- Caching
+- Monitoring
+- Validation
+- Setting up transaction boundaries.
+- Setting up exception handlers for uncaught exceptions.
+
+But how will you go about it?
+
+### A perfectly simple and reasonable solution
+
+Imagine that you want to make this function print its argument to stdout:
+
+    foo :: Int -> DepT e IO () 
+
+Easy enough:
+
+    foo' :: Int -> DepT e IO ()
+    foo' arg1 = do
+        liftIO $ putStrLn (show arg1)
+        foo arg1
+
+You can even write your own general "printArgs" combinator:
+
+    printArgs :: Show a => (a -> DepT e IO ()) -> (a -> DepT e IO ())
+    printArgs f arg1 = do
+        liftIO $ putStrLn (show arg1)
+        f arg1
+
+You could wrap `foo` in `printArgs` when constructing the record-of-functions,
+or perhaps you could modify the corresponding field after the record had been
+constructed.
+
+This solution works, and is easy to understand. There's an annoyance though:
+you need a different version of `printArgs` for each number of arguments a
+function might have.
+
+And if you want to compose different combinators (say, `printArgs` and
+`printResult`) before applying them to functions, you need a composition
+combinator specific for each number of arguments.
+
+### The solution using "advices"
+
+The `Advice` datatype provided by this package encapsulates a transformation on
+`DepT`-effectful functions, *in a way that is polymorphic over the number of
+arguments*. The same advice will work for functions with `0`, `1` or `N`
+arguments.
+
+Advices are parameterized by the constraints they require of the function:
+
+- The function arguments. "All the arguments must be showable".
+- The `DepT` environment and the base monad. "The environment must have a
+  logger, and the base monad must have a `MonadIO` instance."
+- The function return type. "The function must return a type that is a
+  `Monoid`."
+
+Here's how a `printArgs` advice might be defined:
+
+    printArgs :: forall cr. Handle -> String -> Advice Show (BaseConstraint MonadIO) cr
+    printArgs h prefix =
+      makeArgsAdvice
+        ( \args -> do
+            liftIO $ hPutStr h $ prefix ++ ":"
+            hctraverse_ (Proxy @Show) (\(I a) -> liftIO (hPutStr h (" " ++ show a))) args
+            liftIO $ hPutStrLn h "\n"
+            liftIO $ hFlush h
+            pure args
+        )
+
+The advice receives the arguments of the function in the form of an [n-ary
+product](http://hackage.haskell.org/package/sop-core-0.5.0.1/docs/Data-SOP-NP.html#t:NP)
+from [sop-core](http://hackage.haskell.org/package/sop-core-0.5.0.1). But it
+must be polymorphic on the shape of the type-level list which indexes the
+product. This makes the advice work for any number of parameters.
+
+The advice would be applied like this:
+
+    advise (printArgs @Top stdout "foo args: ") foo
+
+The `@Top` type application is necessary because `printArgs` is polymorphic on
+the `cr` constraint on the function results, and the `advise` function requires
+all the constraints to be "concrete" in order to apply the advice. 
+
+## Advices should be applied at the composition root
+
+It's worth emphasizing that advices should be applied at the ["composition
+root"](https://stackoverflow.com/questions/6277771/what-is-a-composition-root-in-the-context-of-dependency-injection),
+the place in our application in which all the disparate functions are assembled
+and we commit to a concrete monad, namely `DepT`.
+
+Before being brought into the composition root, the functions need not be aware
+that `DepT` exists. They might be working in some generic `MonadReader`
+environment, plus some constraints on that environment.
+
+Once we decide to use `DepT`, we can apply the advice, because advice only
+works on functions that end on a `DepT` action. Also, advice might depend on
+the full gamut of functionality stored in the environment.
+
+## Links
+
+- [Aspect Oriented Programming with
+  Spring](https://docs.spring.io/spring-framework/docs/current/reference/html/core.html#aop)
+  and [Spring AOP
+  APIs](https://docs.spring.io/spring-framework/docs/current/reference/html/core.html#aop-api).
+
+- [Using the “constraints” package to make a wrapped function less
+  polymorphic](https://stackoverflow.com/questions/65800809/using-the-constraints-package-to-make-a-wrapped-function-less-polymorphic)
+
+- [Dependency Injection Principles, Practices, and
+  Patterns](https://www.goodreads.com/book/show/44416307-dependency-injection-principles-practices-and-patterns)
+  This is a good book on the general princples of DI. 
+
+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain
+ dep-t-advice.cabal view
@@ -0,0 +1,64 @@+cabal-version:       3.0
+
+name:                dep-t-advice
+version:             0.1.0.0
+synopsis:            Giving good advice to functions in a DepT environment.
+description:         Companion to the dep-t package. Easily add behaviour to functions living in a DepT environment, 
+                     whatever the number of arguments they might have.
+                     
+                     In other words: something like the "advices" of
+                     aspect-oriented programming.
+-- bug-reports:
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Daniel Diaz
+maintainer:          diaz_carrete@yahoo.com
+category:            Control
+extra-source-files:  CHANGELOG.md, README.md
+
+source-repository    head
+  type:     git
+  location: https://github.com/danidiaz/dep-t-advice.git
+
+common common
+  build-depends:       base >=4.10.0.0 && < 5,
+                       sop-core ^>= 0.5.0.0,
+                       constraints ^>= 0.12,
+                       dep-t ^>= 0.1.3.0,
+  default-language:    Haskell2010
+
+common common-tests
+  import:              common
+  build-depends:       
+                       dep-t-advice, 
+                       rank2classes       ^>= 1.4.1,
+                       transformers       ^>= 0.5.0.0,
+                       mtl                ^>= 2.2,
+                       template-haskell,
+
+library
+  import: common
+  exposed-modules:     Control.Monad.Dep.Advice
+                       Control.Monad.Dep.Advice.Basic
+  hs-source-dirs:      lib 
+
+test-suite tests
+  import:              common-tests
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             tests.hs
+  build-depends:       
+                       tasty              >= 1.3.1,
+                       tasty-hunit        >= 0.10.0.2,
+
+-- VERY IMPORTANT for doctests to work: https://stackoverflow.com/a/58027909/1364288
+-- http://hackage.haskell.org/package/cabal-doctest
+test-suite doctests
+  import:              common-tests
+  ghc-options:         -threaded
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             doctests.hs
+  build-depends:       
+                       doctest            ^>= 0.17 
+                       
+ lib/Control/Monad/Dep/Advice.hs view
@@ -0,0 +1,795 @@+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+-- |
+--    This package provices the 'Advice' datatype, along for functions for creating,
+--    manipulating, composing and applying values of that type.
+--
+--    'Advice's represent generic transformations on 'DepT'-effectful functions of
+--    any number of arguments.
+--
+-- >>> :{
+--    foo0 :: DepT NilEnv IO (Sum Int)
+--    foo0 = pure (Sum 5)
+--    foo1 :: Bool -> DepT NilEnv IO (Sum Int)
+--    foo1 _ = foo0
+--    foo2 :: Char -> Bool -> DepT NilEnv IO (Sum Int)
+--    foo2 _ = foo1
+-- :}
+--
+-- They work for @DepT@-actions of zero arguments:
+--
+-- >>> advise (printArgs @Top stdout "foo0") foo0 `runDepT` NilEnv
+-- foo0:
+-- <BLANKLINE>
+-- Sum {getSum = 5}
+--
+-- And for functions of one or more arguments, provided they end on a @DepT@-action:
+--
+-- >>> advise (printArgs @Top stdout "foo1") foo1 False `runDepT` NilEnv
+-- foo1: False
+-- <BLANKLINE>
+-- Sum {getSum = 5}
+--
+-- >>> advise (printArgs @Top stdout "foo2") foo2 'd' False `runDepT` NilEnv
+-- foo2: 'd' False
+-- <BLANKLINE>
+-- Sum {getSum = 5}
+--
+-- 'Advice's can also tweak the result value of functions:
+--
+-- >>> advise (returnMempty @Top @Top2) foo2 'd' False `runDepT` NilEnv
+-- Sum {getSum = 0}
+--
+-- And they can be combined using @Advice@'s 'Monoid' instance before being applied
+-- (although that might require harmonizing their constraint parameters):
+--
+-- >>> advise (printArgs stdout "foo2" <> returnMempty) foo2 'd' False `runDepT` NilEnv
+-- foo2: 'd' False
+-- <BLANKLINE>
+-- Sum {getSum = 0}
+module Control.Monad.Dep.Advice
+  ( -- * The Advice type
+    Advice,
+
+    -- * Creating Advice values
+    makeAdvice,
+    makeArgsAdvice,
+    makeExecutionAdvice,
+
+    -- * Applying Advices
+    advise,
+
+    -- * Constraint helpers
+    -- $constrainthelpers
+    Ensure,
+    Top2,
+    And2,
+    MonadConstraint,
+    EnvConstraint,
+    MustBe,
+    MustBe2,
+
+    -- * Combining Advices by harmonizing their constraints
+    -- $restrict
+    restrictArgs,
+    restrictEnv,
+    restrictResult,
+
+    -- * Invocation helpers
+    -- $invocation
+    runFinalDepT,
+    runFromEnv,
+
+    -- * "sop-core" re-exports
+    -- $sop
+    Top,
+    And,
+    All,
+    NP (..),
+    I (..),
+    cfoldMap_NP,
+
+    -- * "constraints" re-exports
+    -- $constraints
+    type (:-) (..),
+    Dict (..),
+  )
+where
+
+import Control.Monad.Dep
+import Data.Constraint
+import Data.Kind
+import Data.SOP
+import Data.SOP.Dict qualified as SOP
+import Data.SOP.NP
+
+-- $setup
+--
+-- >>> :set -XTypeApplications
+-- >>> :set -XStandaloneKindSignatures
+-- >>> :set -XMultiParamTypeClasses
+-- >>> :set -XFunctionalDependencies
+-- >>> :set -XRankNTypes
+-- >>> :set -XTypeOperators
+-- >>> :set -XConstraintKinds
+-- >>> :set -XNamedFieldPuns
+-- >>> import Control.Monad
+-- >>> import Control.Monad.Dep
+-- >>> import Control.Monad.Dep.Advice
+-- >>> import Control.Monad.Dep.Advice.Basic (printArgs,returnMempty)
+-- >>> import Data.Constraint
+-- >>> import Data.Kind
+-- >>> import Data.SOP
+-- >>> import Data.SOP.NP
+-- >>> import Data.Monoid
+-- >>> import System.IO
+-- >>> import Data.IORef
+
+-- | 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 'Advice's that work with concrete types by using 'MustBe' in
+-- the case of @ca@ and @cr@, and 'MustBe2' in the case of @cem@.
+--
+-- 'Advice's 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.
+type Advice ::
+  (Type -> Constraint) ->
+  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
+  (Type -> Constraint) ->
+  Type
+data Advice ca cem cr where
+  Advice ::
+    forall u ca cem cr.
+    Proxy u ->
+    ( forall as e m.
+      (All ca as, cem e m, Monad m) =>
+      NP I as ->
+      DepT e m (u, NP I as)
+    ) ->
+    ( forall e m r.
+      (cem e m, Monad m, cr r) =>
+      u ->
+      DepT e m r ->
+      DepT e m r
+    ) ->
+    Advice ca cem cr
+
+-- |
+--    Aspects compose \"sequentially\" when tweaking the arguments, and
+--    \"concentrically\" when tweaking the final 'DepT' action.
+--
+--    The first 'Advice' is the \"outer\" one. It tweaks the function arguments
+--    first, and wraps around the execution of the second, \"inner\" 'Advice'.
+instance Semigroup (Advice ca cem cr) where
+  Advice outer tweakArgsOuter tweakExecutionOuter <> Advice inner tweakArgsInner tweakExecutionInner =
+    let captureExistentials ::
+          forall ca cem cr outer inner.
+          Proxy outer ->
+          ( forall as e m.
+            (All ca as, cem e m, Monad m) =>
+            NP I as ->
+            DepT e m (outer, NP I as)
+          ) ->
+          ( forall e m r.
+            (cem e m, Monad m, cr r) =>
+            outer ->
+            DepT e m r ->
+            DepT e m r
+          ) ->
+          Proxy inner ->
+          ( forall as e m.
+            (All ca as, cem e m, Monad m) =>
+            NP I as ->
+            DepT e m (inner, NP I as)
+          ) ->
+          ( forall e m r.
+            (cem e m, Monad m, cr r) =>
+            inner ->
+            DepT e m r ->
+            DepT e m r
+          ) ->
+          Advice ca cem cr
+        captureExistentials _ tweakArgsOuter' tweakExecutionOuter' _ tweakArgsInner' tweakExecutionInner' =
+          Advice
+            (Proxy @(Pair outer inner))
+            ( let tweakArgs ::
+                    forall as e m.
+                    (All ca as, cem e m, Monad m) =>
+                    NP I as ->
+                    DepT e m (Pair outer inner, NP I as)
+                  tweakArgs args =
+                    do
+                      (uOuter, argsOuter) <- tweakArgsOuter' @as @e @m args
+                      (uInner, argsInner) <- tweakArgsInner' @as @e @m argsOuter
+                      pure (Pair uOuter uInner, argsInner)
+               in tweakArgs
+            )
+            ( let tweakExecution ::
+                    forall e m r.
+                    (cem e m, Monad m, cr r) =>
+                    Pair outer inner ->
+                    DepT e m r ->
+                    DepT e m r
+                  tweakExecution =
+                    ( \(Pair uOuter uInner) action ->
+                        tweakExecutionOuter' @e @m @r uOuter (tweakExecutionInner' @e @m @r uInner action)
+                    )
+               in tweakExecution
+            )
+     in captureExistentials @ca @cem @cr outer tweakArgsOuter tweakExecutionOuter inner tweakArgsInner tweakExecutionInner
+
+instance Monoid (Advice ca cem cr) where
+  mappend = (<>)
+  mempty = Advice (Proxy @()) (\args -> pure (pure args)) (const id)
+
+-- |
+--    The most general (and complex) way of constructing 'Advice's.
+--
+--    'Advice's 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.
+makeAdvice ::
+  forall u ca cem cr.
+  -- | The function that tweaks the arguments.
+  ( forall as e m.
+    (All ca as, cem e m, Monad m) =>
+    NP I as ->
+    DepT e m (u, NP I as)
+  ) ->
+  -- | The function that tweaks the execution.
+  ( forall e m r.
+    (cem e m, Monad m, cr r) =>
+    u ->
+    DepT e m r ->
+    DepT e m r
+  ) ->
+  Advice ca cem cr
+makeAdvice = Advice (Proxy @u)
+
+-- |
+--    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
+-- :}
+makeArgsAdvice ::
+  forall ca cem cr.
+  -- | The function that tweaks the arguments.
+  ( forall as e m.
+    (All ca as, cem e m, Monad m) =>
+    NP I as ->
+    DepT e m (NP I as)
+  ) ->
+  Advice ca cem cr
+makeArgsAdvice tweakArgs =
+  makeAdvice @()
+    ( \args -> do
+        args <- tweakArgs args
+        pure ((), args)
+    )
+    (const id)
+
+-- |
+--    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
+-- :}
+makeExecutionAdvice ::
+  forall ca cem cr.
+  -- | The function that tweaks the execution.
+  ( forall e m r.
+    (cem e m, Monad m, cr r) =>
+    DepT e m r ->
+    DepT e m r
+  ) ->
+  Advice ca cem cr
+makeExecutionAdvice tweakExecution = makeAdvice @() (\args -> pure (pure args)) (\() action -> tweakExecution action)
+
+data Pair a b = Pair !a !b
+
+-- |
+-- '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 <http://hackage.haskell.org/package/rio 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@.
+type Ensure :: (Type -> (Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+class c (e (DepT e m)) (DepT e m) => Ensure c e m
+
+instance c (e (DepT e m)) (DepT e m) => Ensure c e m
+
+-- | 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
+-- :}
+advise ::
+  forall ca cem cr as e m r advisee.
+  (Multicurryable as e m r advisee, All ca as, cem e m, Monad m, cr r) =>
+  -- | The advice to apply.
+  Advice ca cem cr ->
+  -- | A function to be adviced.
+  advisee ->
+  advisee
+advise (Advice _ tweakArgs tweakExecution) advisee = do
+  let uncurried = multiuncurry @as @e @m @r advisee
+      uncurried' args = do
+        (u, args') <- tweakArgs args
+        tweakExecution u (uncurried args')
+   in multicurry @as @e @m @r uncurried'
+
+type Multicurryable ::
+  [Type] ->
+  ((Type -> Type) -> Type) ->
+  (Type -> Type) ->
+  Type ->
+  Type ->
+  Constraint
+class Multicurryable as e m r curried | curried -> as e m r where
+  type BaseMonadAtTheTip as e m r curried :: Type
+  multiuncurry :: curried -> NP I as -> DepT e m r
+  multicurry :: (NP I as -> DepT e m r) -> curried
+  _runFromEnv :: m (e (DepT e m)) -> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
+
+instance Monad m => Multicurryable '[] e m r (DepT e m r) where
+  type BaseMonadAtTheTip '[] e m r (DepT e m r) = m r
+  multiuncurry action Nil = action
+  multicurry f = f Nil
+  _runFromEnv producer extractor = do
+    e <- producer
+    runDepT (extractor e) e
+
+instance Multicurryable as e m r curried => Multicurryable (a ': as) e m r (a -> curried) where
+  type BaseMonadAtTheTip (a ': as) e m r (a -> curried) = a -> BaseMonadAtTheTip as e m r curried
+  multiuncurry f (I a :* as) = multiuncurry @as @e @m @r @curried (f a) as
+  multicurry f a = multicurry @as @e @m @r @curried (f . (:*) (I a))
+  _runFromEnv producer extractor a = _runFromEnv @as @e @m @r @curried producer (\f -> extractor f a)
+
+-- | 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 ()
+runFinalDepT ::
+  forall as e m r curried.
+  Multicurryable as e m r curried =>
+  -- | action that gets hold of the environment
+  m (e (DepT e m)) ->
+  -- | function to invoke with effects in 'DepT'
+  curried ->
+  -- | a new function with effects in the base monad
+  BaseMonadAtTheTip as e m r curried
+runFinalDepT producer extractor = _runFromEnv producer (const extractor)
+
+-- | 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}
+runFromEnv ::
+  forall as e m r curried.
+  (Multicurryable as e m r curried, Monad m) =>
+  -- | action that gets hold of the environment
+  m (e (DepT e m)) ->
+  -- | gets a function from the environment with effects in 'DepT'
+  (e (DepT e m) -> curried) ->
+  -- | a new function with effects in the base monad
+  BaseMonadAtTheTip as e m r curried
+runFromEnv = _runFromEnv
+
+-- |
+--    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
+type Top2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+class Top2 e m
+
+instance Top2 e m
+
+-- |
+--    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\".
+type And2 ::
+  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
+  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
+  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint)
+class (f e m, g e m) => (f `And2` g) e m
+
+instance (f e m, g e m) => (f `And2` g) e m
+
+infixl 7 `And2`
+
+-- | 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)
+type MustBe :: forall k. k -> k -> Constraint
+class x ~ y => MustBe x y
+
+instance x ~ y => MustBe x y
+
+-- |
+-- 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
+type MustBe2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+class (e' ~ e, m' ~ m) => MustBe2 e' m' e m
+
+instance (e' ~ e, m' ~ m) => MustBe2 e' m' e m
+
+-- |
+--    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.
+type EnvConstraint :: (((Type -> Type) -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+class c e => EnvConstraint c e m
+
+instance c e => EnvConstraint c e m
+
+-- |
+--    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
+type MonadConstraint :: ((Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+class c m => MonadConstraint c e m
+
+instance c m => MonadConstraint c e m
+
+-- $restrict
+--
+--    'Advice' values can be composed using the 'Monoid' instance, but only if
+--    the have the same constraint parameters. It's unfortunate that—unlike with
+--    normal functions—'Advice' constaints aren't automatically "collected"
+--    during composition.
+--
+--    We need to harmonize the constraints on each 'Advice' by turning them
+--    into the combination of all constraints. The functions in this section
+--    help with that.
+--
+--    These functions take as parameter evidence of entailment between
+--    constraints, using the type '(:-)' from the \"constraints\" package.  But
+--    how to construct such evidence? By using the 'Sub' and the 'Dict'
+--    constructors, with either an explicit type signature:
+--
+-- >>> :{
+-- returnMempty' :: Advice ca cem (Monoid `And` Show)
+-- returnMempty' = restrictResult (Sub Dict) returnMempty
+-- :}
+--
+-- or with a type application to the restriction function:
+--
+-- >>> :{
+-- returnMempty'' :: Advice ca cem (Monoid `And` Show)
+-- returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty
+-- :}
+--
+-- Another example:
+--
+-- >>> :{
+--  type HasLogger :: Type -> (Type -> Type) -> Constraint
+--  class HasLogger em m | em -> m where
+--    logger :: em -> String -> m ()
+--  doLogging :: Advice Show (Ensure HasLogger) cr
+--  doLogging = undefined
+--  type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+--  type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint MonadIO
+--  doLogging':: Advice Show EnsureLoggerAndWriter cr
+--  doLogging'= restrictEnv (Sub Dict) doLogging
+--  doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging
+-- :}
+
+-- | Makes the constraint on the arguments more restrictive.
+restrictArgs ::
+  forall more less cem cr.
+  -- | Evidence that one constraint implies the other.
+  (forall r. more r :- less r) ->
+  -- | Advice with less restrictive constraint on the args.
+  Advice less cem cr ->
+  -- | Advice with more restrictive constraint on the args.
+  Advice more cem cr
+-- about the order of the type parameters... which is more useful?
+-- A possible principle to follow:
+-- We are likely to know the "less" constraint, because advices are likely to
+-- come pre-packaged and having a type signature.
+-- We arent' so sure about having a signature for a whole composed Advice,
+-- because the composition might be done
+-- on the fly, while constructing a record, without a top-level binding with a
+-- type signature.  This seems to favor putting "more" first.
+restrictArgs evidence (Advice proxy tweakArgs tweakExecution) =
+  let captureExistential ::
+        forall more less cem cr u.
+        (forall r. more r :- less r) ->
+        Proxy u ->
+        ( forall as e m.
+          (All less as, cem e m, Monad m) =>
+          NP I as ->
+          DepT e m (u, NP I as)
+        ) ->
+        ( forall e m r.
+          (cem e m, Monad m, cr r) =>
+          u ->
+          DepT e m r ->
+          DepT e m r
+        ) ->
+        Advice more cem cr
+      captureExistential evidence' _ tweakArgs' tweakExecution' =
+        Advice
+          (Proxy @u)
+          ( let tweakArgs'' :: forall as e m. (All more as, cem e m, Monad m) => NP I as -> DepT e m (u, NP I as)
+                tweakArgs'' = case SOP.mapAll @more @less (translateEvidence @more @less evidence') of
+                  f -> case f (SOP.Dict @(All more) @as) of
+                    SOP.Dict -> \args -> tweakArgs' @as @e @m args
+             in tweakArgs''
+          )
+          tweakExecution'
+   in captureExistential evidence proxy tweakArgs tweakExecution
+
+-- |
+--    Makes the constraint on the environment / monad more restrictive.
+restrictEnv ::
+  forall more ca less cr.
+  -- | Evidence that one constraint implies the other.
+  (forall e m. more e m :- less e m) ->
+  -- | Advice with less restrictive constraint on the environment and base monad.
+  Advice ca less cr ->
+  -- | Advice with more restrictive constraint on the environment and base monad.
+  Advice ca more cr
+restrictEnv evidence (Advice proxy tweakArgs tweakExecution) =
+  let captureExistential ::
+        forall more ca less cr u.
+        (forall e m. more e m :- less e m) ->
+        Proxy u ->
+        ( forall as e m.
+          (All ca as, less e m, Monad m) =>
+          NP I as ->
+          DepT e m (u, NP I as)
+        ) ->
+        ( forall e m r.
+          (less e m, Monad m, cr r) =>
+          u ->
+          DepT e m r ->
+          DepT e m r
+        ) ->
+        Advice ca more cr
+      captureExistential evidence' _ tweakArgs' tweakExecution' =
+        Advice
+          (Proxy @u)
+          ( let tweakArgs'' :: forall as e m. (All ca as, more e m, Monad m) => NP I as -> DepT e m (u, NP I as)
+                tweakArgs'' = case evidence' @e @m of Sub Dict -> \args -> tweakArgs' @as @e @m args
+             in tweakArgs''
+          )
+          ( let tweakExecution'' :: forall e m r. (more e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r
+                tweakExecution'' = case evidence' @e @m of Sub Dict -> \u action -> tweakExecution' @e @m @r u action
+             in tweakExecution''
+          )
+   in captureExistential evidence proxy tweakArgs tweakExecution
+
+-- |
+--    Makes the constraint on the result more restrictive.
+restrictResult ::
+  forall more ca cem less.
+  -- | Evidence that one constraint implies the other.
+  (forall r. more r :- less r) ->
+  -- | Advice with less restrictive constraint on the result.
+  Advice ca cem less ->
+  -- | Advice with more restrictive constraint on the result.
+  Advice ca cem more
+restrictResult evidence (Advice proxy tweakArgs tweakExecution) =
+  let captureExistential ::
+        forall more ca cem less u.
+        (forall r. more r :- less r) ->
+        Proxy u ->
+        ( forall as e m.
+          (All ca as, cem e m, Monad m) =>
+          NP I as ->
+          DepT e m (u, NP I as)
+        ) ->
+        ( forall e m r.
+          (cem e m, Monad m, less r) =>
+          u ->
+          DepT e m r ->
+          DepT e m r
+        ) ->
+        Advice ca cem more
+      captureExistential evidence' _ tweakArgs' tweakExecution' =
+        Advice
+          (Proxy @u)
+          tweakArgs'
+          ( let tweakExecution'' :: forall e m r. (cem e m, Monad m, more r) => u -> DepT e m r -> DepT e m r
+                tweakExecution'' = case evidence' @r of Sub Dict -> \u action -> tweakExecution' @e @m @r u action
+             in tweakExecution''
+          )
+   in captureExistential evidence proxy tweakArgs tweakExecution
+
+translateEvidence :: forall more less a. (forall x. more x :- less x) -> SOP.Dict more a -> SOP.Dict less a
+translateEvidence evidence SOP.Dict =
+  case evidence @a of
+    Sub Dict -> SOP.Dict @less @a
+
+-- $sop
+-- Some useful definitions re-exported the from \"sop-core\" package.
+--
+-- 'NP' is an n-ary product used to represent the arguments of advised functions.
+--
+-- 'I' is an identity functor. The arguments processed by an 'Advice' come wrapped in it.
+--
+-- 'cfoldMap_NP' is useful to construct homogeneous lists out of the 'NP' product, for example:
+--
+-- >>> cfoldMap_NP (Proxy @Show) (\(I a) -> [show a]) (I False :* I (1::Int) :* Nil)
+-- ["False","1"]
+
+-- $constraints
+--
+-- Some useful definitions re-exported the from \"constraints\" package.
+--
+-- 'Dict' and '(:-)' are GADTs used to capture and transform constraints. Used in the 'restrictArgs', 'restrictEnv' and 'restrictResult' functions.
+
+-- $constrainthelpers
+-- Some  <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ class synonyms>
+-- to help create the constraints that parameterize the 'Advice' type.
+--
+-- This library also re-exports the 'Top', 'And' and 'All' helpers from \"sop-core\":
+--
+-- * 'Top' is the \"always satisfied\" constraint, useful when whe don't want to require anything specific in @ca@ or @cr@ (@cem@ requires 'Top2').
+--
+-- * 'And' combines constraints for @ca@ or @cr@ (@cem@ requires 'And2').
+--
+-- * 'All' says that some constraint is satisfied by all the components of an 'NP'
+-- product. In this library, it's used to stipulate constraints on the
+-- arguments of advised functions.
+
+-- $invocation
+-- There functions are helpers for running 'DepT' computations, beyond what 'runDepT' provides.
+--
+-- They aren't directly related to 'Advice's, but they require some of the same machinery, and that's why they are here.
+ lib/Control/Monad/Dep/Advice/Basic.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+
+-- |
+-- This module contains examples of simple advices.
+--
+-- __/BEWARE!/__ These are provided for illustrative purposes only, they
+-- strive for simplicity and not robustness or efficiency.
+module Control.Monad.Dep.Advice.Basic
+  ( -- * Basic advices
+    returnMempty,
+    printArgs,
+    AnyEq (..),
+    doCachingBadly,
+    doAsyncBadly
+  )
+where
+
+import Control.Monad.Dep
+import Control.Monad.Dep.Advice
+import Data.Proxy
+import Data.SOP
+import Data.SOP (hctraverse_)
+import Data.SOP.NP
+import Data.Type.Equality
+import System.IO
+import Type.Reflection
+import Control.Concurrent
+
+-- | Makes functions discard their result and always return 'mempty'.
+--
+-- Because it doesn't touch the arguments or require some effect from the
+-- environment, this 'Advice' is polymorphic on @ca@ and @cem@.
+returnMempty :: forall ca cem. Advice ca cem Monoid
+returnMempty =
+  makeExecutionAdvice
+    ( \action -> do
+        _ <- action
+        pure mempty
+    )
+
+-- | Given a 'Handle' and a prefix string, makes functions print their
+-- arguments to the 'Handle'.
+--
+-- This advice uses 'MonadConstraint' to lift the 'MonadIO' constraint that
+-- applies only to the monad.
+--
+-- Because it doesn't touch the return value of the advised function, this
+-- 'Advice' is polymorphic on @cr@.
+printArgs :: forall cr. Handle -> String -> Advice Show (MonadConstraint MonadIO) cr
+printArgs h prefix =
+  makeArgsAdvice
+    ( \args -> do
+        liftIO $ hPutStr h $ prefix ++ ":"
+        hctraverse_ (Proxy @Show) (\(I a) -> liftIO (hPutStr h (" " ++ show a))) args
+        liftIO $ hPutStrLn h "\n"
+        liftIO $ hFlush h
+        pure args
+    )
+
+-- | A helper datatype for universal equality comparisons of existentialized values, used by 'doCachingBadly'.
+--
+-- For a more complete elaboration of this idea, see the the \"exinst\" package.
+data AnyEq where
+  AnyEq :: forall a. (Typeable a, Eq a) => a -> AnyEq
+
+instance Eq AnyEq where
+  AnyEq any1 == AnyEq any2 =
+    case testEquality (typeOf any1) (typeOf any2) of
+      Nothing -> False
+      Just Refl -> any1 == any2
+
+-- | 
+-- Given the means for looking up and storing values in the underlying monad
+-- @m@, makes functions (inefficiently) cache their results.
+--
+-- Notice the equality constraints on the 'Advice'. This means that the monad
+-- @m@ and the result type @r@ are known and fixed before building the advice.
+-- Once built, the 'Advice' won't be polymorphic over them.
+--
+-- The implementation of this function makes use of the existential type
+-- parameter @u@ of 'makeAdvice', because the phase that processes the function
+-- arguments needs to communicate the calculated `AnyEq` cache key to the phase
+-- that processes the function result.
+--
+-- A better implementation of this advice would likely use an @AnyHashable@
+-- helper datatype for the keys.
+doCachingBadly :: forall m r. (AnyEq -> m (Maybe r)) -> (AnyEq -> r -> m ()) -> Advice (Eq `And` Typeable) (MonadConstraint (MustBe m)) (MustBe r)
+doCachingBadly cacheLookup cachePut =
+  makeAdvice @AnyEq
+    ( \args ->
+        let key = AnyEq $ cfoldMap_NP (Proxy @(And Eq Typeable)) (\(I a) -> [AnyEq a]) $ args
+         in pure (key, args)
+    )
+    ( \key action -> do
+        mr <- lift $ cacheLookup key
+        case mr of
+          Nothing -> do
+            r <- action
+            lift $ cachePut key r
+            pure r
+          Just r ->
+            pure r
+    )
+
+-- | Makes functions that return `()` launch asynchronously.
+--
+-- A better implementation of this advice would likely use the \"async\"
+-- package instead of bare `forkIO`. 
+--
+-- And the @MustBe IO@ constraint could be relaxed to @MonadUnliftIO@.
+doAsyncBadly :: Advice ca (MonadConstraint (MustBe IO)) (MustBe ())
+doAsyncBadly = makeExecutionAdvice (\action -> do
+        e <- ask 
+        _ <- liftIO $ forkIO $ runDepT action e
+        pure ()
+    )
+
+ test/doctests.hs view
@@ -0,0 +1,10 @@+module Main (main) where
+
+import Test.DocTest
+
+main =
+  doctest
+    [ "-ilib",
+      "lib/Control/Monad/Dep/Advice.hs",
+      "lib/Control/Monad/Dep/Advice/Basic.hs"
+    ]
+ test/tests.hs view
@@ -0,0 +1,328 @@+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+module Main (main) where
+
+import Control.Monad.Dep
+import Control.Monad.Dep.Advice
+import Control.Monad.Dep.Advice.Basic
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Control.Monad.RWS
+import Data.Kind
+import Data.List (intercalate,lookup)
+import Rank2 qualified
+import Rank2.TH qualified
+import Test.Tasty
+import Test.Tasty.HUnit
+import Prelude hiding (log)
+import Data.Proxy
+
+-- Some helper typeclasses.
+--
+-- Has-style typeclasses can be provided to avoid depending on concrete
+-- environments.
+-- Note that the environment determines the monad.
+type HasLogger :: Type -> (Type -> Type) -> Constraint
+class HasLogger r m | r -> m where
+  logger :: r -> String -> m ()
+
+-- Possible convenience function to avoid having to use ask before logging
+-- Worth the extra boilerplate, or not?
+logger' :: (MonadReader e m, HasLogger e m) => String -> m ()
+logger' msg = asks logger >>= \f -> f msg
+
+type HasRepository :: Type -> (Type -> Type) -> Constraint
+class HasRepository r m | r -> m where
+  repository :: r -> Int -> m ()
+
+-- Some possible implementations.
+--
+-- An implementation of the controller, done programming against interfaces
+-- (well, against typeclasses).
+-- Polymorphic on the monad.
+mkController :: (MonadReader e m, HasLogger e m, HasRepository e m) => Int -> m String
+mkController x = do
+  e <- ask
+  logger e "I'm going to insert in the db!"
+  repository e x
+  return "view"
+
+-- A "real" logger implementation that interacts with the external world.
+mkStdoutLogger :: MonadIO m => String -> m ()
+mkStdoutLogger msg = liftIO (putStrLn msg)
+
+-- A "real" repository implementation
+mkStdoutRepository :: (MonadReader e m, HasLogger e m, MonadIO m) => Int -> m ()
+mkStdoutRepository entity = do
+  e <- ask
+  logger e "I'm going to write the entity!"
+  liftIO $ print entity
+
+-- The traces we accumulate from the fakes during tests
+type TestTrace = ([String], [Int])
+
+-- A "fake". A pure implementation for tests.
+mkFakeLogger :: Monoid x => MonadWriter ([String],x) m => String -> m ()
+mkFakeLogger msg = tell ([msg], mempty)
+
+-- Ditto.
+mkFakeRepository :: (MonadReader e m, HasLogger e m, MonadWriter TestTrace m) => Int -> m ()
+mkFakeRepository entity = do
+  e <- ask
+  logger e "I'm going to write the entity!"
+  tell ([], [entity])
+
+--
+--
+-- Here we define a monomorphic environment working on IO
+type EnvIO :: Type
+data EnvIO = EnvIO
+  { _loggerIO :: String -> IO (),
+    _repositoryIO :: Int -> IO ()
+  }
+
+instance HasLogger EnvIO IO where
+  logger = _loggerIO
+
+instance HasRepository EnvIO IO where
+  repository = _repositoryIO
+
+-- In the monomorphic environment, the controller function lives "separate",
+-- having access to the logger and the repository through the ReaderT
+-- environment.
+--
+-- The question is: the repository function *also* needs to know about the
+-- logger!  Shouldn't it be aware of the ReaderT environment as well? Why
+-- privilege the controller function in such a manner?
+--
+-- In a sufficiently complex app, the diverse functions will form a DAG of
+-- dependencies between each other. So it would be nice if the functions were
+-- treated uniformly, all having access to (views of) the environment record.
+mkControllerIO :: (HasLogger e IO, HasRepository e IO) => Int -> ReaderT e IO String
+mkControllerIO x = do
+  e <- ask
+  liftIO $ logger e "I'm going to insert in the db!"
+  liftIO $ repository e x
+  return "view"
+
+--
+--
+-- Here we define some polymorphic environments, which are basically
+-- records-of-functions parameterized by an effect monad.
+type Env :: (Type -> Type) -> Type
+data Env m = Env
+  { _logger :: String -> m (),
+    _repository :: Int -> m (),
+    _controller :: Int -> m String
+  }
+
+$(Rank2.TH.deriveFunctor ''Env)
+
+-- If our environment is parmeterized by the monad m, then logging is done in
+-- m.
+instance HasLogger (Env m) m where
+  logger = _logger
+
+instance HasRepository (Env m) m where
+  repository = _repository
+
+-- This bigger environment is for demonstrating how to "nest" environments.
+type BiggerEnv :: (Type -> Type) -> Type
+data BiggerEnv m = BiggerEnv
+  { _inner :: Env m,
+    _extra :: Int -> m Int
+  }
+
+$(Rank2.TH.deriveFunctor ''BiggerEnv)
+
+--
+--
+-- Creating environment values and commiting to a concrete monad.
+--
+-- This is the first time DepT is used in this module.
+-- Note that it is only here where we settle for a concrete monad for the
+-- polymorphic environments.
+env :: Env (DepT Env (Writer TestTrace))
+env =
+  let _logger = mkFakeLogger
+      _repository = mkFakeRepository
+      _controller = mkController
+   in Env {_logger, _repository, _controller}
+
+-- An IO variant
+envIO :: Env (DepT Env IO)
+envIO =
+  let _logger = mkStdoutLogger
+      _repository = mkStdoutRepository
+      _controller = mkController
+   in Env {_logger, _repository, _controller}
+
+biggerEnv :: BiggerEnv (DepT BiggerEnv (Writer TestTrace))
+biggerEnv =
+  let -- We embed the small environment into the bigger one using "zoomEnv"
+      -- and the rank-2 fmap that allows us to change the monad which
+      -- parameterized the environment.
+      --
+      -- _inner' = (Rank2.<$>) (withDepT (Rank2.<$>) inner) env,
+      _inner' = zoomEnv (Rank2.<$>) _inner env
+      _extra = pure
+   in BiggerEnv {_inner = _inner', _extra}
+
+biggerEnvIO :: BiggerEnv (DepT BiggerEnv IO)
+biggerEnvIO =
+  let _inner' = zoomEnv (Rank2.<$>) _inner envIO
+      _extra = pure
+   in BiggerEnv {_inner = _inner', _extra}
+
+expected :: TestTrace
+expected = (["I'm going to insert in the db!", "I'm going to write the entity!"], [7])
+
+--
+--
+-- Experiment about adding instrumetation
+
+emptyResult :: Advice ca cem Monoid
+emptyResult = makeAdvice @()
+    (\args -> pure ((), args))
+    (\() action -> do _ <- action
+                      pure mempty)
+
+doLogging :: Advice Show (Ensure HasLogger) cr
+doLogging = makeAdvice @()
+        (\args -> do
+            e <- ask
+            let args' = cfoldMap_NP (Proxy @Show) (\(I a) -> [show a]) args
+            logger e $ "advice before: " ++ intercalate "," args'
+            pure (pure args))
+        (\() action -> do 
+            e <- ask
+            r <- action
+            logger e $ "advice after"
+            pure r)
+
+advicedEnv :: Env (DepT Env (Writer TestTrace))
+advicedEnv =
+   env {
+         _controller = advise (doLogging @Top) (_controller env)
+       }
+
+expectedAdviced :: TestTrace
+expectedAdviced = (["advice before: 7", "I'm going to insert in the db!", "I'm going to write the entity!", "advice after"], [7])
+
+-- a small test of constraint composition
+weirdAdvicedEnv :: Env (DepT Env (Writer TestTrace))
+weirdAdvicedEnv =
+   env {
+         _controller = advise (doLogging <> emptyResult) (_controller env), --,
+         -- This advice below doesn't really do anything, I'm just experimenting with passing the constraints with type application
+         _logger = advise @(Show `And` Eq) @Top2 @Monoid (makeAdvice @() (\args -> pure (pure args)) (\_ -> id)) (_logger env)
+       }
+
+type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint (MonadWriter TestTrace)
+
+-- to ways to invoke restrict functions
+doLogging':: Advice Show EnsureLoggerAndWriter cr
+doLogging'= restrictEnv (Sub Dict) doLogging
+
+doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging
+
+returnMempty' :: Advice ca cem (Monoid `And` Show)
+returnMempty' = restrictResult (Sub Dict) returnMempty
+
+returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty
+
+-- does EnvConstraint compile?
+
+type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top
+
+
+--
+--
+-- environment for testing ba
+
+data CachingTestEnv m = CachingTestEnv { 
+    _cacheTestLogic :: m (),
+    _expensiveComputation :: Int -> Bool -> m String,
+    _logger2 :: String -> m ()
+    }
+
+instance HasLogger (CachingTestEnv m) m where
+  logger = _logger2
+
+type HasExpensiveComputation :: Type -> (Type -> Type) -> Constraint
+class HasExpensiveComputation r m | r -> m where
+  expensiveComputation :: r -> Int -> Bool -> m String
+instance HasExpensiveComputation (CachingTestEnv m) m where
+  expensiveComputation = _expensiveComputation 
+
+mkFakeExpensiveComputation :: (MonadReader e m, HasLogger e m) => Int -> Bool -> m String
+mkFakeExpensiveComputation i b = do
+    e <- ask
+    logger e "Doing expensive computation"
+    return $ (show i ++ show b)
+
+cacheTestLogic :: (MonadReader e m, HasLogger e m, HasExpensiveComputation e m) => m ()
+cacheTestLogic = do
+    e <- ask
+    expensiveComputation e 0 False >>= logger e
+    expensiveComputation e 1 True >>= logger e
+    expensiveComputation e 0 False >>= logger e
+    expensiveComputation e 1 True >>= logger e
+
+type ExpensiveComputationMonad = RWS () ([String],()) [(AnyEq,String)]
+
+cacheLookup :: AnyEq -> ExpensiveComputationMonad (Maybe String)
+cacheLookup key = do
+    cache <- get
+    pure $ lookup key cache
+
+cachePut :: AnyEq -> String -> ExpensiveComputationMonad ()
+cachePut key v = modify ((key,v) :)
+
+cacheTestEnv :: CachingTestEnv (DepT CachingTestEnv ExpensiveComputationMonad)
+cacheTestEnv = CachingTestEnv {
+        _cacheTestLogic = cacheTestLogic,
+        _expensiveComputation = advise (doCachingBadly cacheLookup cachePut) mkFakeExpensiveComputation,
+        _logger2 = mkFakeLogger
+    }
+
+expectedCached :: ([String],())
+expectedCached = (["Doing expensive computation","0False","Doing expensive computation","1True","0False","1True"],())
+
+--
+--
+--
+
+tests :: TestTree
+tests =
+  testGroup
+    "All"
+    [ testCase "hopeThisWorks" $
+        assertEqual "" expected $
+          execWriter $ runDepT (do e <- ask; (_controller . _inner) e 7) biggerEnv,
+      testCase "hopeAOPWorks" $
+        assertEqual "" expectedAdviced $
+          execWriter $ runDepT (do e <- ask; _controller e 7) advicedEnv,
+      testCase "hopeCachingWorks" $
+        assertEqual "" expectedCached $
+          let action = runFromEnv (pure cacheTestEnv) _cacheTestLogic 
+              (_,w) = execRWS action () mempty
+           in w
+    ]
+
+main :: IO ()
+main = defaultMain tests