Hi all, I've a type problem that I cannot solve and, before I keep banging my head against an unbreakable wall, I'd like to discuss it with the list. Consider the following code: ------------ module Main where class PRead p where {} class PWrite p where {} newtype Sealed p a = Sealed a instance Monad (Sealed p) where return = Sealed (Sealed x) >>= f = f x mustRead :: PRead p => a -> Sealed p a mustRead = Sealed mustWrite :: PWrite p => a -> Sealed p a mustWrite = Sealed readLog :: PRead p => String -> Sealed p String readLog = mustRead . id writeLog :: PWrite p => String -> Sealed p String writeLog = mustWrite . id appendLog l e = do l <- readLog l writeLog $ l ++ e ------------ The central type of this code is Sealed, which boxes a value inside a newtype with a phantom type which represents a "set of permissions". This set of permissions is implemented through a series of type classes (PRead and PWrite in this case) which are attached to the permission value p of the Sealed newtype. This way I can define which set of permissions I expect to be enforced when trying to peel off the Sealed value. The use of the Monad class and type classes as permissions behaves nicely when combining functions with different permission constraints, as it's the case of appendLog, whose type signature is: appendLog :: (PRead p, PWrite p) => String -> [Char] -> Sealed p String Very nice, the permissions accumulates as constraints over the p type. Now for the "peel-off" part: ------------ unseal :: p -> Sealed p a -> a unseal _ (Sealed x) = x ------------ Basically this function requires a witness value of the type p to peel-off the Sealed value. Notice that: ------------ unseal undefined $ appendLog "Foo" "Bar" ------------ won't work as the undefined value is unconstrained. That's good, because otherwise it'd very easy to circumvent the enforcing mechanism. So, I defined some "roles": ------------ data User = User data Admin = Admin instance PRead User where {} instance PRead Admin where {} instance PWrite Admin where {} ------------ If I try to unseal the Sealed value passing User, it won't succeed, as the type checker is expecting the value of a type which is also an instance of the PWrite class: ------------ *Main> unseal User $ appendLog "Foo" "Bar" <interactive>:1:14: No instance for (PWrite User) arising from a use of `appendLog' at <interactive>:1:14-34 ------------ while works perfectly if I pass Admin as a value: ------------ *Main> unseal Admin $ appendLog "Foo" "Bar" "FooBar" ------------ The idea is to hide the Admin and User constructor from the programmer and having two factory functions, checkAdmin and checkUser, which checks whether the current user has the named role, something like: ------------ checkAdmin :: IO Admin checkUser :: IO User ------------ where role checking happens in the IO Monad (or something similar), a-là trusted kernel. So far so good and I'm very happy with that. Now the problem. I would like to enforce permissions not at the role level, but at the permissions level. Let's say that I want to leave "unseal" unchanged, I'd like to "construct" a p-value for unseal "combining" functions checking for single permissions, that is, in pseudo-code: unseal (checkPRead .*. checkPWrite) $ appendLog "Foo" "Bar" where .*. is some kind of "type aggregation" operator. Or maybe something like: (checkPRead .*. checkPWrite) $ appendLog "Foo" "Bar" So far I got only frustration. In principle it seems possible to achieve this result because everything is known at compile time and the type-checked should have all the information available to enforce the security constraints. Anyhow, I couldn't write any usable code. Any help would be appreciated, even pointers to papers discussing this approach. Thank you, -- Cristiano GPG Key: 4096R/C17E53C6 2010-02-22 Fingerprint = 4575 4FB5 DC8E 7641 D3D8 8EBE DF59 B4E9 C17E 53C6