Type Level Permission Checking

Few days ago I was working on some API handlers in our server written in Haskell with the framework Yesod. There was a mistake, some secret data was accessible to normal users because we forgot to check the user’s type, luckily it’s not on production yet. The fix is simple, just a line of if (userType user) /= Admin then ... but that doesn’t seems to solve the problem fundamentally, it’s simply so easy to forget to check for permission in various cases. Well, this is Haskell, wouldn’t it be possible to make it a compile time error if we forget to check it?

Modelling the problem

The handler looks like this.

getFooR = do
    post   <- get (PostKey aPostId)      -- This line is ok
    secret <- get (SecretKey aSecretId)  -- This isn't. Secret is accessible for Admin only.

There is no different between getting a post and a secret, which means the compiler has no information to know whether is this allowed or not. In order to make things simpler, I’d like to simplified it into something like this first:

-- Lets say all the operations are IO String
operation :: IO String
operation = do
  guestStr <- guestOperation
  userStr  <- userOperation
  adminStr <- adminOperation
  pure $ guestStr <> userStr <> adminStr

In the above example, I would like to have the compiler giving me an error for a certain operation. E.g. something like this:

operation :: IO String
operation = checkPermission @User $ do
  guestStr <- guestOperation
  userStr  <- userOperation
  adminStr <- adminOperation    -- Some kind of error on this line
  pure $ guestStr <> userStr <> adminStr

So here is the plan.

  1. Add a type level list (of permissions) somewhere into the monad.
  2. A type level function (used to check permission) should create a list of permissions available by a given user type.
  3. Each operation should assert “which permission should be in the list”.
  4. If the list does not contains the required permission, type check should fail.

Creating a list of permissions

To create a type level list, we have to enable the some extensions.

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

data UserType = Admin | User | Guest

-- The DataKinds extension turns "data and types" into "types and kinds"
data List a = Nil | a :> (List a)
infixr 5 :>

-- With the above definition, we can write a list like this:
type PermissionDef = Admin :> User :> Guest :> Nil

-- And we can also write some type level functions that would be helpful later

-- `After` is a type level function that returns the rest of the list after a certain element
type family After (a :: k) (i :: List k) where
  -- If the first element matches, return the rest of the elements
  After a (a :> rest) = rest
  -- If the first element does not match, try to find from the rest of the elements
  After a (b :> rest) = After a rest
  -- If the list is empty, return an empty list.
  After _ Nil         = Nil

-- Example usage:
-- `After B (A :> B :> C :> Nil)` would have the same type as `C :> Nil`

With the above code, we can write a function that generates a list of available permission when given a user type.

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
type AvailablePermissions a = a :> (After a PermissionDef)

permissionsOf :: forall p. Proxy (AvailablePermissions p)
permissionsOf = Proxy

Example: Example usage of permissionsOf

Assert the required permission

While we can calculate a list of permission, we need somewhere to put them. So lets create a monad transformer to add the list to the base monad.

-- Nothing really interesting
data PermissionT :: List UserType -> (* -> *) -> * -> * where
  PermissionT :: m a -> PermissionT l m a

instance Functor m => Functor (PermissionT l m) where
  fmap f (PermissionT io) = PermissionT (fmap f io)
instance Applicative m => Applicative (PermissionT l m) where
  (PermissionT f) <*> (PermissionT v) = (PermissionT $ f <*> v)
  pure = PermissionT . pure

instance Monad m => Monad (PermissionT l m) where
  (PermissionT m) >>= f = PermissionT
    (m >>= \x-> let (PermissionT p) = f x in p)
instance MonadTrans (PermissionT l) where
  lift = PermissionT

instance MonadIO m => MonadIO (PermissionT l m) where
  liftIO = PermissionT . liftIO

And we want a type level function that checks if an element is in the list.

type family InList (a :: k) (l :: List k) :: Bool where
  InList _ Nil         = False
  InList a (a :> rest) = True
  InList a (_ :> rest) = InList a rest

Such that, finally, we can describe the required permission! The function body doesn’t matter, just for demonstration.

-- This operation does not require any permission
safeOperation :: PermissionT l IO String
safeOperation = lift readLn

-- Assert that `Guest` is in the list `l`
guestOperation :: (InList Guest l ~ True) => PermissionT l IO String
guestOperation = lift readLn

-- Assert that `User` is in the list `l`
userOperation :: (InList User l ~ True) => PermissionT l IO String
userOperation = lift readLn

-- Assert that `Admin` is in the list `l`
adminOperation :: (InList Admin l ~ True) => PermissionT l IO String
adminOperation = lift readLn

Satisfying the constraints

Instead of just asserting the permissions, we also want to have a “checking function” that is responsible to check the permissions, and therefore remove the constraints on the list after the check. This is very similar to the previous permissionsOf function.

checkPermission :: forall p a l m. PermissionT (AvailablePermissions p) m a -> PermissionT l m a
checkPermission (PermissionT m) = PermissionT m

Available permissions are calculated by the provided user type. While the constraints on the calculated list is determined by the operations. Operations that failed to have it’s constraint fulfilled would have errors like this:

Permission checked

Finally, we need a way to “exit” the monad transformer.

runPermissionT :: PermissionT Nil m a -> m a
runPermissionT (PermissionT m) = m

Here is the key, by asserting the final list of permission to be Nil, we are forcing the user to create operations that does not ask for any permission. And if any permission is needed, they have to check it.

Permission checking

Constraint depends on type variable

So, the simplified operations checking is working pretty nice. Let’s try to have it solving the original issue. The library used in Yesod is called yesod-persistent, here is a simplified version of its model types:

data Secret = Secret String
data Post = Post Int

class PersistEntity record where
  data Key record :: * -> *
  get :: Key record k -> IO record

-- Lets say the Secret model has a unique string as id
instance PersistEntity Secret where
  data Key Secret k = SecretKey String
  get (SecretKey str) = pure $ Secret str

-- And the Post model has a unique int as id
instance PersistEntity Post where
  data Key Post k = PostKey Int
  get (PostKey n) = pure $ Post n

Models can be accessed like this:

post :: IO Post
post = get (PostKey 1)
secret :: IO Secret
secret = get (SecretKey "hi")

Um… the function is used to get multiple types of model, how can we integrate the permission model we have? We need a way to transform the model into its required permission, and then assert with that permission. Lets describe the “model-permission-relationship”.

type family PermissionNeeded a :: UserType where
  PermissionNeeded Secret = Admin
  PermissionNeeded Post   = User
  PermissionNeeded _      = Guest

Instead of the normal get, we have to create a version of get that understand the permission, and therefore returns in the context of PermissionT.

  :: ( PersistEntity record
     , InList l (PermissionNeeded record) ~ True
  => Key record k
  -> PermissionT l IO record
safeGet = PermissionT . get

Which is integrated nicely with other operations!

Everything is well checked!


In the above examples, I did nothing much except from checking for permissions, but it can be very powerful depends on how you implement the functions. This kind of checking is not difficult, but just easy to forget, especially when nested inside functions. By putting permission checking into type level, the type checker can help to make a more secure program.

The implementation idea is based on a paper about implementing type-safe, explicit exceptions.


I work at HERP and we are hiring. We mostly write Typescript but we do use some Haskell.