David Roundy wrote:
apfelmus wrote:
David Roundy 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
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.
Ah, so you are able to use case expressions casePerm :: (Permission Low -> a) -> (Permission High -> a) -> Permission any -> a which is not possible with a plain phantom type approach. One example use would be foo :: Permission p -> Either String Bar foo = casePerm (const $ Left "foo: permission too low") (\p -> readRestricted p ... ) Of course, you may not export HaveAPerm and HaveBPerm (at least not for construction, only for pattern matching), so you probably need such a special function casePerm anyway. Regards, apfelmus