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.
> instance PRead (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
