Разновидность ReaderT?

В отдельном 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

Да, я думаю, что у нас здесь проблема XY, так что давайте сделаем шаг назад.

Reader – это монада для переноса значения, которое удобно читать. У вас нет значения — у вас есть список разрешений, которые вы хотите применить на уровне типа — так что я не думаю, что вам нужен или нужен читатель, разнородный список или что-то в этом роде.

Вместо этого, учитывая список логических разрешений:

data Permission = PermissionA | PermissionB deriving (Show)

вы хотите определить монаду, параметризованную на уровне типа со списком предоставленных разрешений. Обертка newtype вокруг вашей основной монады IO подойдет:

{-# 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, вы получите ошибку типа (не удалось сопоставить False с True - не самое большое сообщение об ошибке, но...).

Для предоставления разрешений введем функции:

-- 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. Во-первых, это напомнило мне, что grantA и grantB можно с одинаковым успехом записать с помощью "безопасной" функции coerce из Data.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 из одного контекста разрешений и реконструировать его в другом. (В основном это то, что grantA и grantB делают для безусловного повышения привилегий.) Если вы сделаете это «случайно» за пределами доверенной кодовой базы, вы можете в конечном итоге обойти систему разрешений. Во многих приложениях это не имеет большого значения.

Однако, если вы пытаетесь доказать безопасность системы, вам может понадобиться небольшая доверенная база кода, которая работает с опасным конструктором 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, но есть механизмы (Google для «Safe Haskell»), чтобы предотвратить это.