为一个类似ReaderT的monad转换器编写一个“缩放”函数

Question

我有这个ReaderT-like monad转换器(灵感来自this answer)：

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Control.Monad.Reader -- from "mtl"
import Data.Kind (Type)

type DepT :: ((Type -> Type) -> Type) -> (Type -> Type) -> Type -> Type
newtype DepT env m r = DepT {toReaderT :: ReaderT (env (DepT env m)) m r}
  deriving (Functor, Applicative, Monad, MonadReader (env (DepT env m)))

instance MonadTrans (DepT env) where
  lift = DepT . lift

和这两个参数化记录，我给它们提供了"rank-2 functor"实例：

{-# LANGUAGE TemplateHaskell #-}
import qualified Rank2 -- form rank2classes
import qualified Rank2.TH

type Env :: (Type -> Type) -> Type
data Env m = Env
  { logger :: String -> m (),
    logic :: Int -> m Int
  }
$(Rank2.TH.deriveFunctor ''Env)

type BiggerEnv :: (Type -> Type) -> Type
data BiggerEnv m = BiggerEnv
  { inner :: Env m,
    extra :: Int -> m Int
  }
$(Rank2.TH.deriveFunctor ''BiggerEnv)

直观地说，我希望能够用以下类型编写一个转换函数：

zoom :: forall a. DepT Env IO a -> DepT BiggerEnv IO a

这是因为与DepT BiggerEnv IO a相比，DepT Env IO a使用的“信息”更少。

但是我被卡住了。有没有一种方法可以编写zoom

Answer 1

一般的解决方案是这样的函数：

withDepT ::
  forall small big m a.
  Monad m =>
  ( forall p q.
    (forall x. p x -> q x) ->
    small p ->
    small q
  ) ->
  (forall t. big t -> small t) ->
  DepT small m a ->
  DepT big m a
withDepT mapEnv inner (DepT (ReaderT f)) =
  DepT
    ( ReaderT
        ( \big ->
            let small :: small (DepT small m)
                -- we have a big environment at hand, so let's extract the
                -- small environment, transform every function in the small
                -- environment by supplying the big environment and, as a
                -- finishing touch, lift from the base monad m so that it
                -- matches the monad expected by f.
                small = mapEnv (lift . flip runDepT big) (inner big)
             in f small
        )
    )

其中，第一个参数是，在Env的情况下，函数如下

mapEnv :: (forall x. n x -> m x) -> Env n -> Env m
mapEnv f (Env {logger,logic}) =
    Env { logger = f . logger, logic = f . logic }

它改变了环境的单元体。mapEnv对应于rank2classes中的Rank2.<$>。

Answer 2

首先，我们可以创建一个类似于withReaderT函数的更通用的函数withDepT。

withDepT :: forall env env' m a.
            (env' (DepT env' m) -> env (DepT env m))
            -> DepT env m a
            -> DepT env' m a
withDepT f (DepT m) = DepT (withReaderT f m)

然后，我们可以使用它通过提供如下函数来实现zoom：

biggerEnvToEnv :: BiggerEnv (DepT BiggerEnv IO) -> Env (DepT Env IO)
biggerEnvToEnv (BiggerEnv (Env logger logic) _) = Env logger' logic'
  where
    logger' = mystery . logger
    logic' = mystery . logic

zoom = withDepT biggerEnvToEnv

但接下来我们需要实现mystery。让我们看一下它的类型：

mystery :: forall a. DepT BiggerEnv IO a -> DepT Env IO a

现在我们可以看到，mystery与我们想要的zoom函数相反：

zoom :: forall a. DepT Env IO a -> DepT BiggerEnv IO a

因此我们可以得出结论，除非BiggerEnv和Env是同构的，否则不可能自然地派生出zoom，这是因为BiggerEnv中的extra值不同。