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

Reply via email to