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

[David Roundy]

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.
-- 
David Roundy
Department of Physics
Oregon State University