В отдельной Gist вы прокомментировали:
@K.A.Buhr, вау! Спасибо за такой подробный ответ. Вы правы, что это проблема XY, и вы в значительной степени прибили реальную проблему, которую я пытаюсь решить. Еще одна важная часть контекста заключается в том, что в какой-то момент эти разрешения на уровне типов должны быть «реализованы» на уровне значений. Это связано с тем, что последняя проверка сопоставлена с разрешениями, предоставленными текущему вошедшему в систему пользователю, которые хранятся в БД.
Учитывая это, я планирую иметь две "общие" функции, скажем:
requiredPermission :: (RequiredPermission p ps) => Proxy p -> AppM ps ()
optionalPermission :: (OptionalPermission p ps) => Proxy p -> AppM ps ()
Вот разница:
requiredPermission просто добавит разрешение в список уровня типа и будет проверено при вызове runAppM. Если текущий пользователь не имеет ВСЕХ требуемых разрешений, runAppM немедленно выдаст ошибку 401 в пользовательский интерфейс. - С другой стороны,
optionalPermission извлечет пользователя из среды Reader, проверит разрешение и вернет True / False. runAppM ничего не сделает с OptionalPermissions. Это будет в тех случаях, когда отсутствие разрешения НЕ должно проваливать все действие, но пропустить определенный шаг в действии.
Учитывая этот контекст, я не уверен, что в конечном итоге я получу такие функции, как grantA или grantB. «Развертывание» ВСЕХ RequestPermissions в конструкторе AppM будет выполнено 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 символов на проверку разрешения. Тем не менее, ни одно из этих улучшений не является необходимым, и они могут добавить существенную сложность, которой следует избегать, если это вообще возможно до тех пор, пока после не получится работающий прототип. Другими словами, элегантный код, который не работает, не так уж и элегантен.
В этом духе, вот как я мог бы адаптировать свое исходное решение для поддержки набора «требуемых» разрешений, которые должны быть удовлетворены в определенных «точках входа» (например, в определенных перенаправленных веб-запросах), и для выполнения проверки разрешений во время выполнения к базе данных пользователей.
Во-первых, у нас есть набор разрешений:
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 для одновременного определения обеих функций, но пока давайте сделаем это без синглетонов.)
Как и раньше, у нас будет монада, которая содержит список разрешений. Вы можете думать об этом как о списке разрешений, которые были проверены и проверены на данный момент в коде. Мы сделаем это монадным трансформатором для общего m с компонентом ReaderT Env:
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
newtype AppT (perms :: [Permission]) m a = AppT (ReaderT Env m a)
deriving (Functor, Applicative, Monad, MonadReader Env, MonadIO)
Теперь мы можем определить действия в этой монаде, которые формируют строительные блоки для нашего приложения:
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 может автоматически определить сигнатуру этого типа, определив, что требуются разрешения ReadP и MetaP. Если бы мы хотели сделать разрешение MetaP необязательным, мы могли бы написать:
readPageWithOptionalMeta :: ( Allowed 'ReadP perms ~ 'True
, MonadIO m) => Int -> AppT perms m ()
readPageWithOptionalMeta n = do
readPage n
whenMeta $ metaPage n
, где whenMeta допускает необязательные действия в зависимости от доступных разрешений. (См. Ниже.) Опять же, эта подпись может быть выведена автоматически.
Пока что мы допустили необязательные разрешения, мы явно не имели дело с «необходимыми» разрешениями. Они будут определены в точках входа , которые будут определены с использованием отдельной монады:
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
Обратите внимание, что у нас есть блок do, построенный из AppT строительных блоков. Фактически, это эквивалентно readPageWithOptionalMeta выше и имеет тип:
(Allowed 'ReadP perms ~ 'True, MonadIO m) => Int -> AppT perms m ()
Здесь _somethingspecial_ необходимо адаптировать это AppT (чей список разрешений требует проверки и проверки ReadP до его запуска) для точки входа, чьи списки требуемых и (статически) проверенных разрешений [ReadP]. Мы сделаем это, используя набор функций для проверки фактических прав доступа во время выполнения:
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