[Haskell-cafe] Synthetic values?

[Steffen Schuldenzucker]

In ghci I get

 >>> let evil = appendLog "Foo" "Bar"
<interactive>:1:11:
     Ambiguous type variable `p' in the constraints:
       `PRead p'
         arising from a use of `appendLog' at <interactive>:1:11-31
       `PWrite p'
         arising from a use of `appendLog' at <interactive>:1:11-31
     Probable fix: add a type signature that fixes these type variable(s)

And then, specializing evil's type:

 >>> let good = appendLog "Foo" "Bar" :: Sealed Admin String
 >>> unseal (undefined :: Admin) good
"FooBar"

-- Steffen

On 02/09/2011 06:15 PM, Cristiano Paris wrote:
> 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,
>