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