[Haskell-cafe] Role based access control via monads or arrows or... something

[Luke Palmer]

2008/4/2 porrifolius <porrifolius at gmail.com>:
>   (7) ideally required permissions would appear (and accumulate) in type
>  signatures via inference so application code knows which are required and
>  type checker can reject static/dynamic role constraint violations

If you mean what I think you mean by "dynamic", that these are runtime
permissions,
then you're not going to get the type checker to check them... of course.  What
did you mean by dynamic?

>  I've attempted a solution using arrows based loosely upon ideas in [1] and
>  [2].  I can't figure out how to make it work, even if I did get it working I
>  now suspect it can be done far more simply, and I don't think it could ever
>  provide feature (7).  For what it's worth it's attached.
>
>  Ideally you kind folk could help me come up with a type-level solution to
>  satisfy (7), so you could have something like:
>  deptAveSal :: (HasPerms subject? Read Salary [person]?, HasPerm subject? Read
>  Employees dept?, HasRole subject? Manager dept?) => Department -> Salary

What comes to mind is that you could pass proofs around which
represent required permissions.  The hard part is coming up with a
data type algebra for expressing your "theorems" (permission
requirements).   If you want a rich system of permissions, it's pretty
unlikely that you'll get inference.

    data HasRole role dept     = HasRole -- do not expose this constructor
    data HasPerm perm obj dept = HasPerm -- nor this one

    class Department d where

    deptAveSal :: (Department dept)
               => HasPerm ReadPerm Employees dept
               -> HasRole ManagerRole dept
               -> dept
               -> Salary

And then dole out HasRoles and HasPerms through your module interface.

However, I'm pretty sure any solution to (7) will be unsatisfactory to
you, considering your long list of requirements.  Haskell's type
system is not SQL, it will have a hard time supporting these things.
If you're interested in programming with type-safe permissions you
might want to look into dependent types (Epigram, Agda 2), but those
languages are not what you would consider "mature" or "fast"  (it
takes 1 second to verify that 113 is prime in Agda 2... now you see
what I mean?).  It would be an academic exercise.

Here's my ill-informed advice (since I don't know what problem you're
trying to solve, only what solution you want to have):  Forget (7),
stay away from arrows for this, and avoid overengineering (this kind
of problem especially likes to attract overengineers).

My hunch is that you only need two things:  a data type witnessing a
permission.  That is, don't worry about the subject? stuff; if the
program can get its hands on a witness of a permission, then it has
that permission.   I would start with KISS, just a plain
unparameterized data type:

    -- keep this type abstract and do not expose the constructors
    data Perm = ReadSalaryPermission Employee
              | ...

And then maybe introduce separation and type parameters as you start
to use them and see where the logical boundaries are.

Of the possible ways you can put this into a monad, I would say
"Access t" is a computation which results in a value of type t after
receiving witnesses of required permissions.  I considered:

    data Access a = Access { value :: a, required :: Set Perm }

But I like to avoid ad-hoc checks like this and actually put the
checks right in the code.

    newtype Access' a = Access' (Set Perm -> Maybe a)

Or:

    data Access'' a
        = Result a
        | NeedPermissions (Set PermSpec) (Set Perm -> Access'' a)

Or something like that.  Let the computation figure out how to verify
the permissions.  Notice how Perm and PermSpec are different in the
last example, because of the witness model.  You don't want to give
someone the permissions to do something when you're just trying to
tell them what permissions they need.

In particular, though, there is nothing arrow-like about this problem.
 Arrows abstract the notion of function, and this problem is all about
values.

Luke