2008/4/2 porrifolius
(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