[Haskell-cafe] Synthetic values?
Alexey Khudyakov
alexey.skladnoy at gmail.com
Wed Feb 9 20:14:44 CET 2011
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
More information about the Haskell-Cafe
mailing list