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

[apfelmus]

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)

     data Permission p = Permitted -- not exported

     low  :: Permission Low  -- same role as HaveAPerm
     high :: Permission High -- a module which knows these constants has
                             -- corresponding permissions

     data Restricted p a = Restricted a

     readRestricted :: Permission p -> Restricted p a -> a


Regards,
apfelmus