Re: [Haskell-cafe] Synthetic values?
On 9 February 2011 19:33, Alexey Khudyakov wrote: > On 09.02.2011 20:57, Chris Smith wrote: >> >> On Wed, 2011-02-09 at 18:15 +0100, Cristiano Paris wrote: >>> >>> 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. >> >> If I'm understanding your high-level goals correctly, then you're going >> about things the wrong way. It looks like in your "Sealed" type, you're >> accumulating a list of type class constraints that are needed by a >> phantom type, in order to access the value. But type classes are open; >> anyone can make any new type an instance of the type class whenever they >> want. >> > > It's possible to have closed type classes. Trick consist in adding > unsatisfiable constraint. For example: > >> -- This type class is not exported >> class Private a >> class Private a => PRead a > > If Private is not exported one cannot add instances to PRead. > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > Indeed, this is exactly what I use in explicit-iomodes: http://hackage.haskell.org/packages/archive/explicit-iomodes/0.6.0.2/doc/html/System-IO-ExplicitIOModes.html#t:ReadModes Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On 09.02.2011 23:16, Cristiano Paris wrote: On Wed, Feb 9, 2011 at 19:33, Alexey Khudyakov wrote: ... If Private is not exported one cannot add instances to PRead. Nice trick. I would have thought of hiding the classes PRead and PWrite but I'm not sure if it could break the code. It shouldn't but it would be impossible to write signatures for polymorphic functions which use thoose type classes. foo :: PWrite p => Sealed p Int <-- impossible to write foo = ... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On Wed, Feb 9, 2011 at 20:14, Alexey Khudyakov wrote: > ... >> instance PRead (WRead ::: b) >> instance PRead b => PRead (a ::: b) > >> instance PWrite (WWrite ::: b) >> instance PWrite b => PWrite (a ::: b) Brilliant! I was thinking to something like this but as a replacement of the accumulation mechanism in the Monad. I didn't think of it in the permission checking part. Thanks a lot. Now I need to consolidate better my code for incorporating yours and other people contributions. Bye, -- Cristiano GPG Key: 4096R/C17E53C6 2010-02-22 Fingerprint = 4575 4FB5 DC8E 7641 D3D8 8EBE DF59 B4E9 C17E 53C6 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On Wed, Feb 9, 2011 at 20:14, Alexey Khudyakov wrote: > ... > My solution is based on heterogenous lists and require number of > language extensions. I'd recomend to read paper "Strongly typed > heterogeneous collections"[1] which describe this technique in detail Curious: I read the paper just because I had an idea about how to solve the problem but it led me to no solution even though it helped me a lot in understanding some advanced type mechanism. I'll read your solution later and come back to you with a comment. Thank you in the meantime. -- Cristiano GPG Key: 4096R/C17E53C6 2010-02-22 Fingerprint = 4575 4FB5 DC8E 7641 D3D8 8EBE DF59 B4E9 C17E 53C6 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On Wed, Feb 9, 2011 at 19:33, Alexey Khudyakov wrote: > ... > If Private is not exported one cannot add instances to PRead. Nice trick. I would have thought of hiding the classes PRead and PWrite but I'm not sure if it could break the code. Thank you! -- Cristiano GPG Key: 4096R/C17E53C6 2010-02-22 Fingerprint = 4575 4FB5 DC8E 7641 D3D8 8EBE DF59 B4E9 C17E 53C6 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On 09.02.2011 20:15, Cristiano Paris wrote:
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:
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.
Text below is literate haskell
My solution is based on heterogenous lists and require number of
language extensions. I'd recomend to read paper "Strongly typed
heterogeneous collections"[1] which describe this technique in detail
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE OverlappingInstances #-}
> {-# LANGUAGE FlexibleInstances #-}
So lets start with definition of type classes for permissions and data
types which represent such permissions.
> class PRead a
> class PWrite a
> data WRead = WRead
> data WWrite = WWrite
Now interestig part begins. We need to compose different permissons. I
define heterogenous list for that purpose. It's nothing more than a
nested tuple in disguise.
> data a ::: b = a ::: b
> infixr :::
List has instance for some permission if it has corresponding type in
it. Please note that I make use of overlapping here. You may need to
read about it.
Also list need some terminator. WRead is not instance of PRead whereas
WRead ::: () is. I will use () for that purpose. It's OK since all
type classes here are closed.
> instancePRead (WRead ::: b)
> instance PRead b => PRead (a ::: b)
> instance PWrite (WWrite ::: b)
> instance PWrite b => PWrite (a ::: b)
Here is function for checking that everything is working as expected
> withR :: PRead a => a -> ()
> withR _ = ()
> withW :: PWrite a => a -> ()
> withW _ = ()
> withWR :: (PRead a, PWrite a) => a -> ()
> withWR _ = ()
> r = WRead ::: ()
> w = WWrite ::: ()
> rw = WRead ::: WWrite ::: ()
[1] http://homepages.cwi.nl/~ralf/HList/
P.S. You can use phantom types to propagate type information. I feel
that carrying undefined is morally dubious practice.
> data T a = T
> newtype Sealed p a = Sealed a
> unseal :: T p -> Sealed p a -> a
> unseal _ (Sealed x) = x
> admin :: T (WRead ::: WWrite ::: ())
> admin = T
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On 09.02.2011 20:57, Chris Smith wrote: On Wed, 2011-02-09 at 18:15 +0100, Cristiano Paris wrote: 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. If I'm understanding your high-level goals correctly, then you're going about things the wrong way. It looks like in your "Sealed" type, you're accumulating a list of type class constraints that are needed by a phantom type, in order to access the value. But type classes are open; anyone can make any new type an instance of the type class whenever they want. It's possible to have closed type classes. Trick consist in adding unsatisfiable constraint. For example: > -- This type class is not exported > class Private a > class Private a => PRead a If Private is not exported one cannot add instances to PRead. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On Wed, 2011-02-09 at 18:15 +0100, Cristiano Paris wrote: > 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. If I'm understanding your high-level goals correctly, then you're going about things the wrong way. It looks like in your "Sealed" type, you're accumulating a list of type class constraints that are needed by a phantom type, in order to access the value. But type classes are open; anyone can make any new type an instance of the type class whenever they want. In particular, you say: > > 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. This is not true, though. One could just as easily write: data Dummy instance PRead Dummy instance PWrite Dummy unseal (undefined :: Dummy) $ appendLog "Foo" "Bar" and they've circumvented your security checks. I think you'll need to back up and rethink your base strategy. Without really understanding fully what you want, I'll still point out that there are tricks with existentials that work when you need someone to have an authentic token to do something; e.g., see the ST monad. -- Chris Smith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
On Wed, Feb 9, 2011 at 18:43, Steffen Schuldenzucker wrote: > ... let good = appendLog "Foo" "Bar" :: Sealed Admin String unseal (undefined :: Admin) good > "FooBar" That's true, but putting apart the problem I posed, in my construction I wouldn't expose unseal directly nor the Sealed constructor. This way, you should not be able to recreate the unseal function and you'd be given only specialized "unseal" functions for each role, like unsealAsAdmin, unsealAsUser and so on. Thank you for adding to the discussion. -- Cristiano GPG Key: 4096R/C17E53C6 2010-02-22 Fingerprint = 4575 4FB5 DC8E 7641 D3D8 8EBE DF59 B4E9 C17E 53C6 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Synthetic values?
In ghci I get
>>> let evil = appendLog "Foo" "Bar"
:1:11:
Ambiguous type variable `p' in the constraints:
`PRead p'
arising from a use of `appendLog' at :1:11-31
`PWrite p'
arising from a use of `appendLog' at :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"
:1:14:
No instance for (PWrite User)
arising from a use of `appendLog' at: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,
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Synthetic values?
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"
:1:14:
No instance for (PWrite User)
arising from a use of `appendLog' at :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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
