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

[Dan Weston]

Is this type-level design flexible enough for future requirement changes?

The best answer to "Why is this door locked?" may not be "You don't have 
permission to open it", but rather "What door?".

Suppose a client comes along later with a requirement that the 
permissions themselves are secret (e.g. I don't want you to know that I 
have permission to read your email). Now the permissions themselves have 
to be reflected somehow. And this reflection has permissions of its own. 
And permissions might have to nest not like locked doors but like trap 
doors. The most effective permission denial is the illusion that there 
is nothing there.

Also, doesn't the type-level correspond to an intuitionistic logic, so 
it is difficult to express the concept of not-having-permission (a Vice 
President has permission to nuke some defenseless country only if the 
President's permission has been revoked through impeachment).

Moreover, I see no way to have side effects (if someone peeks into your 
secret documents, let them look rather than tip them that you are on to 
them, but monitor their movements to see who they sell them to).

Finally, type checking always halts, but it may desirable (in a 
Kafkaesque way) simply not to answer, such as when a dissident applies 
for an exit visa she is entitled by law to receive.

Some many ways for a rigid design to fail.

Dan

David Roundy wrote:
> On Thu, Apr 03, 2008 at 05:31:16PM +0200, apfelmus wrote:
>> David Roundy wrote:
>>> Luke Palmer wrote:
>>>> porrifolius wrote:
>>>>>  (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?
>>>
>>> At the simplest (and stupidest) level, one could define
>>>
>>> data CanReadA
>>> data CanReadB
>>> -- etc
>>>
>>> data HavePermission perms where
>>>   HaveAPerm :: HavePermission CanReadA
>>>   HaveBPerm :: HavePermission CanReadB
>>>
>>> and if you then restricted access to the constructors of HavePermission,
>>> you could write code like
>>>
>>> data RestrictedData permrequired a = Data a
>>> -- constructor obviously not exported, or you'd lose any safety
>>>
>>> readRestrictedData :: HavePermission perm -> RestrictedData perm a -> a
>>>
>>> and now if you export readRestrictedData only, then only folks with the
>>> proper permissions could access the data (and this could be done at
>>> runtime).
>> At runtime, are you sure? I mean, if I want to use it like in
>>
>>   foo = ... readRestrictedData permission secret ...
>>
>> I must know that the type of my  permission  matches the the type of 
>> secret , either by knowing them in advance or by propagating this as 
>> type variable into the type of foo. In any case, I may only write  foo 
>> if I know statically that  permission  is going to match the  secret . 
>> No runtime involved?
>>
>> In other words, I fail to see how this GADT example is different from a 
>> normal phantom type (modulo different naming)
> 
> The difference is that I can inspect at runtime what permissions I have.  I
> see that I didn't demonstrate this.  You can introduce a function
> 
> checkPerms :: HavePermission p -> HavePermission p' -> EqCheck
> checkPerms HaveAPerm HaveAPerm = IsEq
> checkPerms HaveBPerm HaveBPerm = IsEq
> checkPerms _ _ = NotEq
> 
> data EqCheck a b where
>   IsEq :: EqCheck a a
>   NotEq :: EqCheck a b
> 
> which allows you to compare permissions at runtime and make use of them.