【问题标题】:Differently kinded ReaderT?不同想法的读者?
【发布时间】:2019-06-29 05:42:46
【问题描述】:

冒着成为XY Problem 的风险,是否有可能拥有一个具有不同类型环境的ReaderT?我正在尝试类似...

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

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

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

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

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

...其中r 是一种*

我正在尝试在类型级别跟踪权限/角色,我的最终目标是编写类似...的函数

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

... 每次调用 ensurePermission 都会在 monad 的权限列表(在类型级别)中附加/前置一个新权限。

编辑

我尝试了以下,它似乎可以编译,但我不确定发生了什么。从概念上讲,perms 仍然不是 [*]。这个 sn-p 如何被编译器接受,而原来的不是?

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

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

编辑#2

我尝试改进我的代码 sn-p 以进一步匹配我的最终目标,但我又遇到了一个不同的“种类”问题:

编译器不接受以下代码:

{-# 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)
--    |                                       ^^^^^^^^^^

也不接受以下变体...

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)
--    |            ^^^^^^^^^^^^^^^^^

【问题讨论】:

  • 部分问题在于[*] 类型没有任何具有值的类型。类型检查器将因此拒绝您的ensurePermission。如果有意义的话,你只能在你有价值观的地方拥有*(或#)的类型。你需要像Proxy 这样的东西。
  • 您确定不想要type AppM (perms :: [*]) = ReaderT (Hlist perms) IO 吗?即,读取器访问类型列表中任何类型的值?
  • @David 我不确定我是否完全理解你。更是如此,因为我从 Servant 的 Context 类型和 HasContextEntry 类型类中汲取灵感 - stackage.org/haddock/lts-12.1/servant-server-0.14.1/…
  • @chi 可能你是对的。我假设HList 是一个异构列表,对吗?哪个(维护良好的)库提供了这个?我尝试搜索 stackage/hackage 并找到了很多。事实上Servant本身提供了一个HList类型,但它只针对HTTP头。
  • @chi 我试过你的建议,它似乎可以编译。但我不确定为什么。我已经编辑了问题。

标签: haskell higher-kinded-types data-kinds


【解决方案1】:

是的,我认为我们这里有一个 XY 问题,所以让我们退后一步。

Reader 是一个 monad,用于携带便于阅读的 。你没有价值——你有一个想要在类型级别强制执行的权限列表——所以我认为你不需要或想要一个阅读器、一个异构列表或其他类似的东西。

相反,给定一个布尔权限列表:

data Permission = PermissionA | PermissionB deriving (Show)

您想在类型级别定义一个参数化的 monad,并列出其授予的权限。围绕底层 IO monad 的新类型包装器可以:

{-# LANGUAGE DataKinds, KindSignatures, GeneralizedNewtypeDeriving #-}
newtype M (ps :: [Permission]) a = M (IO a) deriving (Functor, Applicative, Monad)

您还需要一个类型函数(AKA 类型族)来确定权限是否在权限列表中:

{-# LANGUAGE TypeFamilies, TypeOperators #-}
type family Allowed (p :: Permission) ps where
  Allowed p '[] = False
  Allowed p (p:ps) = True
  Allowed p (q:ps) = Allowed p ps

现在,如果您想编写需要某些权限的函数,您可以编写如下内容:

deleteA :: (Allowed PermissionA ps ~ True) => M ps ()
deleteA = M $ print "Deleted A"

readB :: (Allowed PermissionB ps ~ True) => M ps ()
readB = M $ print "Read B"

copyBtoA :: ( Allowed PermissionA ps ~ True
            , Allowed PermissionB ps ~ True) => M ps ()
copyBtoA = M $ print "Copied B to A"

为了运行M 操作,我们引入了一个在没有权限的情况下运行的函数:

-- runM with no permissions
runM :: M '[] a -> IO a
runM (M act) = act

请注意,如果您尝试runM readB,您将收到类型错误(无法将FalseTrue 匹配——这不是最大的错误消息,但是...)。

为了授予权限,我们介绍一下函数:

-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA (M act) = M act
grantB :: M (PermissionB:ps) a -> M ps a
grantB (M act) = M act

这些函数本质上是术语级别的标识函数——它们只是打开并重新包装M 构造函数。但是,它们在类型级别的操作是为其输入参数添加权限。这意味着:

runM $ grantB $ readB

现在进行类型检查。这样做:

runM $ grantA . grantB $ readB
runM $ grantB . grantA $ readB
runM $ grantB . grantA . grantB $ readB
etc.

然后你可以编写如下程序:

program :: IO ()
program = runM $ do
  grantA $ do
    deleteA
    grantB $ do
      readB
      copyBtoA

同时拒绝以下程序:

program1 :: IO ()
program1 = runM $ do
  grantA $ do
    deleteA
    grantB $ do
      readB
    copyBtoA    -- error, needs PermissionB

这个基础设施可能有点难看,但它应该是您进行基于类型、完全编译时权限检查所需的全部。

也许可以尝试一下这个版本,看看它是否满足您的需求。完整代码为:

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

data Permission = PermissionA | PermissionB deriving (Show)

newtype M (ps :: [Permission]) a = M (IO a) deriving (Functor, Applicative, Monad)

type family Allowed (p :: Permission) ps where
  Allowed p '[] = False
  Allowed p (p:ps) = True
  Allowed p (q:ps) = Allowed p ps

-- runM with no permissions
runM :: M '[] a -> IO a
runM (M act) = act

-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA (M act) = M act
grantB :: M (PermissionB:ps) a -> M ps a
grantB (M act) = M act

deleteA :: (Allowed PermissionA ps ~ True) => M ps ()
deleteA = M $ print "Deleted A"

readB :: (Allowed PermissionB ps ~ True) => M ps ()
readB = M $ print "Read B"

copyBtoA :: ( Allowed PermissionA ps ~ True
            , Allowed PermissionB ps ~ True) => M ps ()
copyBtoA = M $ print "Copied B to A"

program :: IO ()
program = runM $ do
  grantA $ do
    deleteA
    grantB $ do
      readB
      copyBtoA

基于@dfeuer 评论的两个附加说明。首先,它提醒我grantAgrantB 可以同样使用Data.Coerce 中的“安全”coerce 函数来编写,如下所示。这个版本和上面的版本生成的代码没什么区别,看个人口味吧:

import Data.Coerce

-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA = coerce
grantB :: M (PermissionB:ps) a -> M ps a
grantB = coerce

其次,@dfeuer 所说的是,在用于控制权限的可信代码库和依赖于类型系统来强制执行权限系统的代码的“其余部分”之间没有明确的区别。例如,M 构造函数上的模式匹配本质上是危险的,因为您可以从一个权限上下文中提取 IO a 并在另一个权限上下文中重构它。 (这基本上是grantAgrantB 无条件提升特权所做的事情。)如果您在受信任的代码库之外“意外”执行此操作,您最终可能会绕过权限系统。在许多应用程序中,这没什么大不了的。

但是,如果您试图证明系统安全,您可能需要一个小型可信代码库,该代码库与危险的 M 构造函数一起使用,并且仅导出一个“安全”API,以确保通过类型系统的安全性。在这种情况下,您将拥有一个导出类型M 的模块,但不是其构造函数M(..)。相反,您将导出智能构造函数以创建具有适当权限的 M 操作。

此外,出于晦涩的技术原因,即使不导出 M 构造函数,“不受信任”代码仍然可能在不同的权限上下文之间进行强制转换:

stealPermission :: M (PermissionA:ps) a -> M ps a
stealPermission = coerce

因为M 类型构造函数的第一个参数有一个所谓的“角色”,默认为“幻影”而不是“名义”。如果你覆盖它:

{-# LANGUAGE RoleAnnotations #-}
type role M nominal _

那么coerce只能在构造函数在作用域内的地方使用,这就堵住了这个漏洞。不受信任的代码仍然可以使用unsafeCoerce,但有一些机制(谷歌的“Safe Haskell”)可以防止这种情况发生。

【讨论】:

  • 应该有角色注解保护幻象,不应该导出newtype构造函数。
  • 好的,我在最后添加了一条注释,我认为可以解决这个问题。
  • @K.A.Buhr,哇!谢谢你这么详细的回复。你说得对,这是一个 XY 问题,而且你几乎已经解决了我要解决的实际问题。我最终写了一个很长的回复,超过了 StackOverflow 的评论限制。请看能不能看懂gist.github.com/saurabhnanda/b783c4a99d56c527613cf6cb3febce4c
  • @K.A.Buhr 我是否需要启用AllowAmbiguousTypes 才能编写readAdeleteB 之类的函数。我尝试了gist.github.com/saurabhnanda/… 之类的东西,编译器最终得到了模棱两可的类型变量。
  • @K.A.Buhr 有没有办法让这种技术与完全多态的 monad m 一起工作?为了进行测试,我们所有的代码在m 中都是多态的,并且仅由runAppM 函数具体化。我尝试编写一个类似于 type (HasApp p m) = (RequiredPermission p ps ~ True, m ps) 的 ConstraintKind,但由于 Not in scope: type variable ‘ps’ 而无法正常工作
【解决方案2】:

在单独的 Gist 中,您评论道:

@K.A.Buhr,哇!谢谢你这么详细的回复。你说得对,这是一个 XY 问题,而且你几乎已经解决了我要解决的实际问题。另一个重要的背景是,在某些时候,这些类型级别的权限必须在值级别“具体化”。这是因为最终检查是针对授予当前登录用户的权限,这些权限存储在数据库中。

考虑到这一点,我打算有两个“通用”功能,比如:

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 做任何事情。这些将适用于缺少权限不应导致整个操作失败,而是跳过操作中的特定步骤的情况。

在这种情况下,我不确定我是否会最终得到一些函数,比如grantA 或grantB。 AppM 构造函数中所有 RequestPermissions 的“解包”将由 runAppM 完成,这也将确保当前登录的用户实际上拥有这些权限。

请注意,“具体化”类型的方法不止一种。例如,下面的程序——通过狡猾的黑魔法——设法在不使用代理或单例的情况下具体化运行时类型!

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 的以下变体设法将仅在运行时已知的用户权限提升到类型级别:

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 个字符。但是,这些改进都不是必需的,而且它们可能会增加相当大的复杂性,如果可能的话,应该避免这种情况,直到你得到一个工作原型之后。换句话说,优雅但不起作用的代码并不是那么优雅。

本着这种精神,我可以通过以下方式调整我的原始解决方案以支持一组必须在特定“入口点”(例如,特定路由的 Web 请求)满足的“必需”权限,并执行运行时权限检查针对用户数据库。

首先,我们有一组权限:

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])
    ]

以及包含用户权限的环境以及您想在阅读器中携带的任何其他内容:

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

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

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 库来同时定义这两个函数,但我们现在不使用单例。)

和以前一样,我们将有一个带有权限列表的 monad。您可以将其视为代码中此时已检查和验证的权限列表。我们将使它成为带有ReaderT Env 组件的通用m 的monad 转换器:

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

现在,我们可以在这个 monad 中定义构成我们应用程序构建块的操作:

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

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

我们可以从中构建更复杂的操作,就像我们在其他答案中所做的那样:

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

请注意,GHC 实际上可以自动推断此类型签名,确定需要 ReadPMetaP 权限。如果我们想让MetaP 权限可选,我们可以这样写:

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

whenMeta 允许根据可用权限执行可选操作。 (见下文。)同样,可以自动推断此签名。

到目前为止,虽然我们允许可选权限,但我们还没有明确处理“必需”权限。这些将在 入口点 中指定,这些入口点将使用单独的 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(不打勾)的(静态)检查权限等于其所需权限,这就是我们知道它可以安全运行的方式(针对特定用户的动态确定的权限集,所有这些都将由类型)。

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)

要定义一个入口点,我们将使用如下内容:

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

请注意,我们这里有一个由AppT 构建块构建的do 块。事实上,它等价于上面的readPageWithOptionalMeta,所以有type:

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

这里的_somethingspecial_ 需要将此AppT(其权限列表要求在运行之前检查和验证ReadP)适应其所需和(静态)检查权限列表为@的入口点987654361@。我们将使用一组函数来检查实际的运行时权限:

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 函数列表与类型签名中所需权限列表相匹配的事实。剩下的洞有类型:

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

由于我们构建权限检查的方式,这是安全转换的一个特例:

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

换句话说,我们可以使用相当不错的语法来编写我们的最终入口点定义,它的字面意思是“需要Read 来运行这个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 函数的组合列表必须以相同的顺序完全匹配这些相同的权限,以便它能够类型检查。

最后一个难题是whenMeta 的实现,它执行运行时权限检查,如果权限可用,则执行可选操作。

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 ()

这是带有测试工具的完整程序。你可以看到:

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

【讨论】:

  • 再次感谢您的迷你博客文章 :) 当我在笔记本电脑上时,我会尝试摆弄您的代码示例,但首先跳出来的是需要显式转换使用机械requireX . toRunAppT 转换将(Allowed p perms) =&gt; AppT pems m 转换为更具体的形式。有没有办法使用AppT perms m 上的约束来自动具体化 monad? requiredX 正在构建的类型级列表,在调用readPage / writePage 时不能构建它。顺便说一句,这就是我进入原始 ReaderT / HList 兔子洞的方式。
  • 是的,这是可能的。我故意避开它,因为它是一个糟糕的设计。您认为您希望将所需权限冒泡到入口点,然后在顶层以某种不透明的方式进行检查,但随后 (1) 您可以更轻松地更改应用程序内部的代码在运行时将用户锁定在入口点之外; (2) 您丢失了入口点签名提供的显式应用安全规范。
  • 我花了很多时间摆弄代码来了解使用通用/单一功能进行权限检查的缺点,但无法弄清楚。您能否详细说明您的评论:(1) you make it easier for code changes in the guts of the app to lock users out of entry points at runtime; and (2) you lose the explicit app security specification provided by the entry point signatures.
  • (1) 如果重构多个入口点使用的低级代码,很容易意外引入新的权限要求。如果权限溢出,则没有类型错误,但突然访问主页需要CommentEditP。 (2) 与 (1) 相关的是,入口点类型签名为您的应用程序的安全保证提供了文档化规范。运行entryX 需要什么权限?检查签名。代码更改需要规范更改?应该由人而不是编译器来监督这些变化。
  • 感谢您的澄清 - 现在对我来说很有意义。顺便说一句,我从您的解决方案中获取了提示,并在gist.github.com/saurabhnanda/… 为我的应用程序尝试了 PoC - 现在它是针对每个客户启用的某些功能标志,而不是权限。我有一个多态 requireFeature 函数,它可以为传递给它的任何特征标志引入类型级约束。同样,有一个多态 runAction 需要您将特征标志列表作为代理传递(续......)
猜你喜欢
  • 2014-01-19
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 2019-10-13
  • 1970-01-01
  • 1970-01-01
  • 2020-08-13
  • 1970-01-01
相关资源
最近更新 更多