不同种类的ReaderT?

本文介绍了不同种类的ReaderT?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

冒着成为 XY问题的风险，是否可能会出现ReaderT在不同种类的环境中?我正在尝试类似...

At the risk of this becoming an XY Problem, is it possible to have a ReaderT with a differently kinded environment? I'm trying something like...

type AppM (perms :: [*]) = ReaderT (perms :: [*]) IO

...但是编译器抱怨...

...but the compiler complains with...

Expected a type, but ‘(perms :: [*])’ has kind ‘[*]’

...大概是因为ReaderT被定义为...

...presumably because ReaderT is defined as...

newtype ReaderT r (m :: k -> *) (a :: k) = ReaderT {runReaderT :: r -> m a}

...其中r是*

我正在尝试在类型级别上跟踪权限/角色，而我的最终目标是编写类似...的功能

I'm trying to track permissions/roles at a type-level, and my ultimate goal is to write functions like...

ensurePermission :: (p :: Permission) -> AppM (p :. ps) ()

...，其中每个对ensurePermission的调用都会在monad的权限列表(类型级别)上追加/添加新的权限.

... where every call to ensurePermission appends/prepends a new permission to the monad's permission list (at the type-level).

我尝试了以下操作，并且似乎可以编译，但是我不确定发生了什么.从概念上讲，perms仍然不是[*]类型.这段代码如何被编译器接受，但原始代码却不可接受?

I tried the following, and it seems to compile, but I'm not sure what's going on. Conceptually isn't perms still of kind [*]. How is this snippet acceptable to the compiler, but the original one isn't?

data HList (l :: [*]) where
  HNil :: HList '[]
  HCons :: e -> HList l -> HList (e ': l)

type AppM (perms :: [*]) = ReaderT (HList perms) IO

编辑#2

我尝试发展自己的代码段以进一步匹配最终目标，但又因另一个种类"问题而陷入困境:

Edit #2

I tried evolving my code snippet to further match my end-goal, but I'm stuck again with a different "kind" problem:

编译器不接受以下代码:

The compiler doesn't accept the following code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data Permission = PermissionA
                | PermissionB

$(genSingletons [''Permission])

data PList (perms :: [Permission]) where
  PNil :: PList '[]
  PCons :: p -> PList perms -> PList (p ': perms)

--     • Expected kind ‘[Permission]’, but ‘p : perms’ has kind ‘[*]’
--     • In the first argument of ‘PList’, namely ‘(p : perms)’
--       In the type ‘PList (p : perms)’
--       In the definition of data constructor ‘PCons’
--    |
-- 26 |   PCons :: p -> PList perms -> PList (p ': perms)
--    |                                       ^^^^^^^^^^

它也不接受以下变化...

Neither does it accept the following variation...

data PList (perms :: [Permission]) where
  PNil :: PList '[]
  PCons :: (p :: Permission) -> PList perms -> PList (p ': perms)


--     • Expected a type, but ‘(p :: Permission)’ has kind ‘Permission’
--     • In the type ‘(p :: Permission)’
--       In the definition of data constructor ‘PCons’
--       In the data declaration for ‘PList’
--    |
-- 26 |   PCons :: (p :: Permission) -> PList perms -> PList (p ': perms)
--    |            ^^^^^^^^^^^^^^^^^

推荐答案

在单独的摘要中，您评论了:

In a separate Gist, you commented:

考虑到这一点，我计划具有两个常规"功能，例如:

Taking this into account, I'm planning to have two "general" functions, say:

requiredPermission :: (RequiredPermission p ps) => Proxy p -> AppM ps ()
optionalPermission :: (OptionalPermission p ps) => Proxy p -> AppM ps ()

区别在于:

requiredPermission只会将权限添加到类型级别列表中，并且在调用runAppM时将对其进行验证.如果当前用户没有所有必需的权限，则runAppM将立即向UI抛出401错误.
另一方面，optionalPermission将从Reader环境中提取用户，检查权限，并返回True/False. runAppM对OptionalPermissions无效.这些情况适用于在没有权限的情况下不应使整个操作失败，而应跳过操作中的特定步骤的情况.

requiredPermission will simply add the permission to the type-level list and it will be verified when runAppM is called. If the current user does not have ALL the required permissions, then runAppM will immediately throw a 401 error to the UI.
On the other hand, optionalPermission will extract the user from the Reader environment, check the permission, and return a True / False. runAppM will do nothing with OptionalPermissions. These will be for cases where the absence of a permission should NOT fail the entire action, but skip a specific step in the action.

在这种情况下，我不确定是否最终会使用GrantA或GrantB之类的函数. AppM构造函数中所有RequestPermissions的解包"将由runAppM完成，这还将确保当前登录的用户实际上具有这些权限.

Given this context, I'm not sure if I would end-up with functions, like grantA or grantB. The "unwrapping" of ALL the RequestPermissions in the AppM constructor will be done by runAppM, which will also ensure that the currently sign-in user actually has these permissions.

请注意，有多种方法可以验证"类型.例如，下面的程序-通过狡猾的黑魔术-设法在不使用代理或单例的情况下实现了对运行时类型的验证！

Note that there's more than one way to "reify" types. For example, the following program -- through devious black magic trickery -- manages to reify a runtime type without the use of proxies or singletons!

main = do
  putStr "Enter \"Int\" or \"String\": "
  s <- getLine
  putStrLn $ case s of "Int" ->    "Here is an integer: " ++ show (42 :: Int)
                       "String" -> "Here is a string: " ++ show ("hello" :: String)

类似地，grantA的以下变体设法将仅在运行时已知的用户权限提升为类型级别:

Similarly, the following variant of grantA manages to lift user permissions known only at runtime to the type-level:

whenA :: M (PermissionA:ps) () -> M ps ()
whenA act = do
  perms <- asks userPermissions  -- get perms from environment
  if PermissionA `elem` perms
    then act
    else notAuthenticated

此处可以使用字母来避免获得不同权限的样板并提高此受信任代码段的类型安全性(即，使得PermissionA的两次出现都必须匹配).同样，约束类型可能会在每个权限检查中节省5或6个字符.但是，这些改进都不是必需的，并且它们可能会增加相当大的复杂性，在之后获得工作原型之前，应尽可能避免这种复杂性.换句话说，优雅的代码行不通.

Singletons could be used here to avoid boilerplate for different permissions and to improve type safety in this trusted piece of code (i.e., so that the two occurrences of PermissionA are forced to match). Similarly, constraint kinds might save 5 or 6 characters per permission check. However, neither of these improvements is necessary, and they may add substantial complexity that should be avoided if at all possible until after you get a working prototype. In other words, elegant code that doesn't work isn't all that elegant.

本着这种精神，这就是我如何调整原始解决方案以支持一组在特定入口点"(例如，特定的路由Web请求)必须满足的必需"权限，并执行运行时权限检查的方法针对用户数据库.

In that spirit, here is how I might adapt my original solution to support a set of "required" permissions that must be satisfied at specific "entry points" (e.g., specific routed web requests), and to perform runtime permission checking against a user database.

首先，我们有一组权限:

First, we have a set of permissions:

data Permission
  = ReadP            -- read content
  | MetaP            -- view (private) metadata
  | WriteP           -- write content
  | AdminP           -- all permissions
  deriving (Show, Eq)

和用户数据库:

type User = String
userDB :: [(User, [Permission])]
userDB
  = [ ("alice", [ReadP, WriteP])
    , ("bob",   [ReadP])
    , ("carl",  [AdminP])
    ]

以及包含用户权限以及您希望在阅读器中随身携带的其他内容的环境:

as well as an environment that includes user permissions and whatever else you want to carry around in a reader:

data Env = Env
  { uperms :: [Permission]   -- user's actual permissions
  , user :: String           -- other Env stuff
  } deriving (Show)

我们还希望类型和术语级别的函数检查权限列表:

We'll also want functions at the type and term level to check permission lists:

type family Allowed (p :: Permission) ps where
  Allowed p (AdminP:ps) = True   -- admins can do anything
  Allowed p '[] = False
  Allowed p (p:ps) = True
  Allowed p (q:ps) = Allowed p ps
allowed :: Permission -> [Permission] -> Bool
allowed p (AdminP:ps) = True
allowed p (q:ps) | p == q = True
                 | otherwise = allowed p ps
allowed p [] = False

(是的，您可以使用singletons库同时定义这两个函数，但是现在不使用单例功能就可以做到这一点.)

(Yes, you could use the singletons library to define both functions simultaneously, but let's do this without singletons for now.)

和以前一样，我们将有一个monad，其中包含权限列表.您可以将其视为代码中目前已检查和验证的权限列表.我们将其作为具有ReaderT Env组件的常规m的单子转换器:

As before, we'll have a monad that carries around a list of permissions. You can think of it as the list of permissions that have been checked and verified at this point in the code. We'll make this a monad transformer for a general m with a ReaderT Env component:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
newtype AppT (perms :: [Permission]) m a = AppT (ReaderT Env m a)
  deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)

现在，我们可以在此monad中定义构成应用程序构建块的动作:

Now, we can define actions in this monad that form the building blocks for our application:

readPage :: (Allowed ReadP perms ~ True, MonadIO m) => Int -> AppT perms m ()
readPage n = say $ "Read page " ++ show n

metaPage :: (Allowed ReadP perms ~ True, MonadIO m) => Int -> AppT perms m ()
metaPage n = say $ "Secret metadata " ++ show (n^2)

editPage :: (Allowed ReadP perms ~ True, Allowed WriteP perms ~ True, MonadIO m) => Int -> AppT perms m ()
editPage n = say $ "Edit page " ++ show n

say :: MonadIO m => String -> m ()
say = liftIO . putStrLn

在每种情况下，在已检查和验证的权限列表包括类型签名中列出的所需权限的任何情况下，都可以执行该操作. (是的，约束种类在这里可以很好地工作，但让我们保持简单.)

In each case, the action is allowed in any context where the list of permissions that have been checked and verified includes the needed permissions listed in the type signature. (Yes, constraint kinds would work fine here, but let's keep it simple.)

我们可以像在其他答案中所做的那样，从中构造出更复杂的动作

We can build more complicated actions out of these, as we did in my other answer:

readPageWithMeta :: ( Allowed 'ReadP perms ~ 'True, Allowed 'MetaP perms ~ 'True
    , MonadIO m) => Int -> AppT perms m ()
readPageWithMeta n = do
  readPage n
  metaPage n

请注意，GHC实际上可以自动推断出此类型签名，从而确定需要ReadP和MetaP权限.如果要使MetaP权限为可选，我们可以编写:

Note that GHC can actually infer this type signature automatically, determining that ReadP and MetaP permissions are required. If we wanted to make the MetaP permission optional, we could write:

readPageWithOptionalMeta :: ( Allowed 'ReadP perms ~ 'True
    , MonadIO m) => Int -> AppT perms m ()
readPageWithOptionalMeta n = do
  readPage n
  whenMeta $ metaPage n

其中，whenMeta允许根据可用权限执行可选操作. (请参见下文.)再次可以自动推断出此签名.

where the whenMeta allows an optional action depending on available permissions. (See below.) Again, this signature can be inferred automatically.

到目前为止，虽然我们已经允许了可选权限，但是我们还没有明确处理必需"权限.这些将在进入点中指定，这些入口将使用单独的monad进行定义:

So far, while we've allowed for optional permissions, we haven't explicitly dealt with "required" permissions. Those are going to be specified at entry points which will be defined using a separate monad:

newtype EntryT' (reqP :: [Permission]) (checkedP :: [Permission]) m a
  = EntryT (ReaderT Env m a)
  deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)
type EntryT reqP = EntryT' reqP reqP

这需要一些解释. EntryT'(带有勾号)具有两个权限列表.第一个是入口点所需权限的完整列表，并且对于每个特定入口点都有一个固定值.第二个是已经检查"的那些权限的子集(从静态的意义上说，有一个函数调用来检查和验证用户是否具有所需的权限).当我们定义入口点时，它将从空白列表到所需权限的完整列表.我们将其用作类型级别的机制，以确保正确设置了一组权限检查函数调用. EntryT(不打勾)的(静态)检查权限等于其所需的权限，这就是我们所知的安全运行方式(针对特定用户的动态确定的权限集，所有这些都将由类型).

This requires some explanation. An EntryT' (with the tick mark) has two lists of permissions. The first is the full list of required permissions for the entry point and has a fixed value for each particular entry point. The second is the subset of those permissions that have been "checked" (in the static sense that a function call is in place to check and verify the user has the required permission). It will be built up from the empty list to the full list of required permissions when we define entry points. We'll use it as a type-level mechanism to ensure that the correct set of permission checking function calls is in place. An EntryT (no tick) has its (statically) checked permissions equal to its required permissions, and that's how we know it's safe to run (against a particular user's dynamically determined set of permissions, which will all be checked as guaranteed by the type).

runEntryT :: MonadIO m => User -> EntryT req m () -> m ()
runEntryT u (EntryT act)
  = case lookup u userDB of
      Nothing   -> say $ "error 401: no such user '" ++ u ++ "'"
      Just perms -> runReaderT act (Env perms u)

要定义一个切入点，我们将使用以下内容:

To define an entry point, we'll use something like this:

entryReadPage :: MonadIO m => Int -> EntryT '[ReadP] m ()
entryReadPage n = _somethingspecial_ $ do
  readPage n
  whenMeta $ metaPage n

请注意，这里我们有一个do块是基于AppT构造块构建的.实际上，它等效于上面的readPageWithOptionalMeta，因此具有类型:

Note that we have a do block here built out of AppT building blocks. In fact, it's equivalent to readPageWithOptionalMeta above and so has type:

(Allowed 'ReadP perms ~ 'True, MonadIO m) => Int -> AppT perms m ()

此处的_somethingspecial_需要使此AppT(其权限列表要求在运行ReadP之前检查并验证其权限)适应于其必需和(静态)已检查权限列表为[ReadP].我们将使用一组函数来检查实际的运行时权限:

The _somethingspecial_ here needs to adapt this AppT (whose list of permissions requires that ReadP be checked and verified before it is run) to an entry point whose lists of required and (statically) checked permissions is [ReadP]. We'll do this using a set of functions to check actual runtime permissions:

requireRead :: MonadIO m => EntryT' r c m () -> EntryT' r (ReadP:c) m ()
requireRead = unsafeRequire ReadP
requireWrite :: MonadIO m => EntryT' r c m () -> EntryT' r (WriteP:c) m ()
requireWrite = unsafeRequire WriteP
-- plus functions for the rest of the permissions

所有定义如下:

unsafeRequire :: MonadIO m => Permission -> EntryT' r c m () -> EntryT' r c' m ()
unsafeRequire p act = do
  ps <- asks uperms
  if allowed p ps
    then coerce act
    else say $ "error 403: requires permission " ++ show p

现在，当我们写:

entryReadPage :: MonadIO m => Int -> EntryT '[ReadP] m ()
entryReadPage n = requireRead . _ $ do
  readPage n
  whenMeta $ metaPage n

外部类型正确，反映了requireXXX函数列表与类型签名中所需权限列表匹配的事实.其余孔的类型为:

the outer type is correct, reflecting the fact that the list of requireXXX functions matches the list of required permissions in the type signature. The remaining hole has type:

AppT perms0 m0 () -> EntryT' '[ReadP] '[] m ()

由于我们构造权限检查的方式，这是安全转换的一种特殊情况:

Because of the way we've structured our permission checking, this is a special case of the safe transformation:

toRunAppT :: MonadIO m => AppT r m a -> EntryT' r '[] m a
toRunAppT = coerce

换句话说，我们可以使用相当不错的语法编写最终的入口点定义，该语法从字面上说我们需要Read来运行此AppT":

In other words, we can write our final entry point definition using a fairly nice syntax which literally says that we "require Read to run this AppT":

entryReadPage :: MonadIO m => Int -> EntryT '[ReadP] m ()
entryReadPage n = requireRead . toRunAppT $ do
  readPage n
  whenMeta $ metaPage n

并类似地:

entryEditPage :: MonadIO m => Int -> EntryT '[ReadP, WriteP] m ()
entryEditPage n = requireRead . requireWrite . toRunAppT $ do
  editPage n
  whenMeta $ metaPage n

请注意，所需的权限列表已明确包含在入口点的类型中，并且执行这些权限的运行时检查的requireXXX函数的组合列表必须以相同的顺序与这些相同的权限完全匹配.键入检查.

Observe that the list of required permissions is included explicitly in the entry point's type, and the composed list of requireXXX functions that perform runtime checking of those permissions must exactly match those same permissions, in the same order, for it to type check.

最后一个难题是whenMeta的实现，该实现执行运行时权限检查，并在权限可用时执行可选操作.

The last piece of the puzzle is the implementation of whenMeta, which performs a runtime permission check and executes an optional action if the permission is available.

whenMeta :: Monad m => AppT (MetaP:perms) m () -> AppT perms m ()
whenMeta = unsafeWhen MetaP
-- and similar functions for other permissions

unsafeWhen :: Monad m => Permission -> AppT perms m () -> AppT perms' m ()
unsafeWhen p act = do
  ps <- asks uperms
  if allowed p ps
    then coerce act
    else return ()

这是带有测试harnass的完整程序.您可以看到:

Here's the full program with a test harnass. You can see that:

Username/Req (e.g., "alice Read 5"): alice Read 5    -- Alice...
Read page 5
Username/Req (e.g., "alice Read 5"): bob Read 5      -- and Bob can read.
Read page 5
Username/Req (e.g., "alice Read 5"): carl Read 5     -- Carl gets the metadata, too
Read page 5
Secret metadata 25
Username/Req (e.g., "alice Read 5"): bob Edit 3      -- Bob can't edit...
error 403: requires permission WriteP
Username/Req (e.g., "alice Read 5"): alice Edit 3    -- but Alice can.
Edit page 3
Username/Req (e.g., "alice Read 5"):

来源:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Realistic where

import Control.Monad.Reader
import Data.Coerce

-- |Set of permissions
data Permission
  = ReadP            -- read content
  | MetaP            -- view (private) metadata
  | WriteP           -- write content
  | AdminP           -- all permissions
  deriving (Show, Eq)

type User = String
-- |User database
userDB :: [(User, [Permission])]
userDB
  = [ ("alice", [ReadP, WriteP])
    , ("bob",   [ReadP])
    , ("carl",  [AdminP])
    ]

-- |Environment with 'uperms' and whatever else is needed
data Env = Env
  { uperms :: [Permission]   -- user's actual permissions
  , user :: String           -- other Env stuff
  } deriving (Show)

-- |Check for permission in type-level and term-level lists
type family Allowed (p :: Permission) ps where
  Allowed p (AdminP:ps) = True   -- admins can do anything
  Allowed p '[] = False
  Allowed p (p:ps) = True
  Allowed p (q:ps) = Allowed p ps
allowed :: Permission -> [Permission] -> Bool
allowed p (AdminP:ps) = True
allowed p (q:ps) | p == q = True
                 | otherwise = allowed p ps
allowed p [] = False

-- |An application action running with a given list of checked permissions.
newtype AppT (perms :: [Permission]) m a = AppT (ReaderT Env m a)
  deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)

-- Optional actions run if permissions are available at runtime.
whenRead :: Monad m => AppT (ReadP:perms) m () -> AppT perms m ()
whenRead = unsafeWhen ReadP
whenMeta :: Monad m => AppT (MetaP:perms) m () -> AppT perms m ()
whenMeta = unsafeWhen MetaP
whenWrite :: Monad m => AppT (WriteP:perms) m () -> AppT perms m ()
whenWrite = unsafeWhen WriteP
whenAdmin :: Monad m => AppT (AdminP:perms) m () -> AppT perms m ()
whenAdmin = unsafeWhen AdminP
unsafeWhen :: Monad m => Permission -> AppT perms m () -> AppT perms' m ()
unsafeWhen p act = do
  ps <- asks uperms
  if allowed p ps
    then coerce act
    else return ()

-- |An entry point, requiring a list of permissions
newtype EntryT' (reqP :: [Permission]) (checkedP :: [Permission]) m a
  = EntryT (ReaderT Env m a)
  deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)
-- |An entry point whose full list of required permission has been (statically) checked).
type EntryT reqP = EntryT' reqP reqP

-- |Run an entry point whose required permissions have been checked.
runEntryT :: MonadIO m => User -> EntryT req m () -> m ()
runEntryT u (EntryT act)
  = case lookup u userDB of
      Nothing   -> say $ "error 401: no such user '" ++ u ++ "'"
      Just perms -> runReaderT act (Env perms u)

-- Functions to build the list of required permissions for an entry point.
requireRead :: MonadIO m => EntryT' r c m () -> EntryT' r (ReadP:c) m ()
requireRead = unsafeRequire ReadP
requireMeta :: MonadIO m => EntryT' r c m () -> EntryT' r (MetaP:c) m ()
requireMeta = unsafeRequire MetaP
requireWrite :: MonadIO m => EntryT' r c m () -> EntryT' r (WriteP:c) m ()
requireWrite = unsafeRequire WriteP
requireAdmin :: MonadIO m => EntryT' r c m () -> EntryT' r (AdminP:c) m ()
requireAdmin = unsafeRequire AdminP
unsafeRequire :: MonadIO m => Permission -> EntryT' r c m () -> EntryT' r c' m ()
unsafeRequire p act = do
  ps <- asks uperms
  if allowed p ps
    then coerce act
    else say $ "error 403: requires permission " ++ show p

-- Adapt an entry point w/ all static checks to an underlying application action.
toRunAppT :: MonadIO m => AppT r m a -> EntryT' r '[] m a
toRunAppT = coerce

-- Example application actions
readPage :: (Allowed ReadP perms ~ True, MonadIO m) => Int -> AppT perms m ()
readPage n = say $ "Read page " ++ show n
metaPage :: (Allowed ReadP perms ~ True, MonadIO m) => Int -> AppT perms m ()
metaPage n = say $ "Secret metadata " ++ show (n^2)
editPage :: (Allowed ReadP perms ~ True, Allowed WriteP perms ~ True, MonadIO m) => Int -> AppT perms m ()
editPage n = say $ "Edit page " ++ show n

say :: MonadIO m => String -> m ()
say = liftIO . putStrLn

-- Example entry points
entryReadPage :: MonadIO m => Int -> EntryT '[ReadP] m ()
entryReadPage n = requireRead . toRunAppT $ do
  readPage n
  whenMeta $ metaPage n
entryEditPage :: MonadIO m => Int -> EntryT '[ReadP, WriteP] m ()
entryEditPage n = requireRead . requireWrite . toRunAppT $ do
  editPage n
  whenMeta $ metaPage n

-- Test harnass
data Req = Read Int
         | Edit Int
         deriving (Read)
main :: IO ()
main = do
  putStr "Username/Req (e.g., \"alice Read 5\"): "
  ln <- getLine
  case break (==' ') ln of
    (user, ' ':rest) -> case read rest of
      Read n -> runEntryT user $ entryReadPage n
      Edit n -> runEntryT user $ entryEditPage n
  main

这篇关于不同种类的ReaderT?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！