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