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 ‘[*]’
...presumably because ReaderT is defined as...
newtype ReaderT r (m :: k -> *) (a :: k) = ReaderT {runReaderT :: r -> m a}
...where r is of kind *
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) ()
... where every call to ensurePermission appends/prepends a new permission to the monad's permission list (at the type-level).
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
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:
@K.A.Buhr, wow! Thank you for such a detailed reply. You are correct that this is an XY problem, and you've pretty-much nailed the actual problem that I'm trying to solve. Another important piece of context is that, at some point these type-level permissions will have to be "reified" at the value-level. This is because the final check is against the permissions granted to the currently signed-in user, which are stored in the DB.
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 ()Here's the difference:
requiredPermissionwill simply add the permission to the type-level list and it will be verified whenrunAppMis called. If the current user does not have ALL the required permissions, thenrunAppMwill immediately throw a 401 error to the UI.- On the other hand,
optionalPermissionwill extract the user from theReaderenvironment, check the permission, and return a True / False.runAppMwill do nothing withOptionalPermissions. 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.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)
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
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.
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)
and a user databsae:
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
(Yes, you could use the singletons library to define both functions simultaneously, but let's do this without singletons for now.)
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)
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
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
where the whenMeta allows an optional action depending on available permissions. (See below.) Again, this signature can be inferred automatically.
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
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
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 ()
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
all defined in terms of:
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
Now, when we write:
entryReadPage :: MonadIO m => Int -> EntryT '[ReadP] m ()
entryReadPage n = requireRead . _ $ do
readPage n
whenMeta $ metaPage n
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
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
and similarly:
entryEditPage :: MonadIO m => Int -> EntryT '[ReadP, WriteP] m ()
entryEditPage n = requireRead . requireWrite . toRunAppT $ do
editPage n
whenMeta $ metaPage n
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.
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 ()
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"):
The source:
{-# 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