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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
