bookkeeper-permissions (empty) → 0.1.0.0
raw patch · 5 files changed
+439/−0 lines, 5 filesdep +basedep +bookkeeperdep +type-level-setssetup-changed
Dependencies added: base, bookkeeper, type-level-sets
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- bookkeeper-permissions.cabal +26/−0
- src/Bookkeeper/Permissions.hs +311/−0
- src/Bookkeeper/Permissions/Examples.hs +70/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Philip Kamenarsky (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Author name here nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ bookkeeper-permissions.cabal view
@@ -0,0 +1,26 @@+name: bookkeeper-permissions+version: 0.1.0.0+synopsis: Permissions for bookkeeper records+description: Please see README.md+homepage: https://github.com/pkamenarsky/bookkeeper-permissions+bug-reports: https://github.com/pkamenarsky/bookkeeper-permissions/issues+license: BSD3+license-file: LICENSE+author: Philip Kamenarsky+maintainer: p.kamenarsky@gmail.com+copyright: 2016 Philip Kamenarsky+category: Data Structures, Records+tested-with: GHC == 8.0.1+build-type: Simple+cabal-version: >=1.10++library+ hs-source-dirs: src+ exposed-modules: Bookkeeper.Permissions,+ Bookkeeper.Permissions.Examples+ default-language: Haskell2010+ build-depends: base >= 4.9 && < 4.10,+ bookkeeper,+ type-level-sets+ ghc-options: -Wall+ default-language: Haskell2010
+ src/Bookkeeper/Permissions.hs view
@@ -0,0 +1,311 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Bookkeeper.Permissions+ (+-- * Introduction+--+-- | This experimental library adds permissions to+-- <https://hackage.haskell.org/package/bookkeeper bookkeeper> records. Its+-- intended purpose is to be used as a building block in other libraries+-- providing general access to data in some form or other (database bindings,+-- web servers etc).+--+-- A common pattern in user facing programs is the following:+--+-- > doAdminStuff admin = do+-- > when admin $ do+-- > ...+--+-- But this is not enforced by the type system and can thus easily be forgotten+-- or gotten wrong. The approach that this library takes to getting the type+-- system work for us is to protect /data/ by requiring that record fields are+-- marked with specific /permissions/ that need to be provided when accessing+-- said fields.+--+-- This library uses <https://hackage.haskell.org/package/bookkeeper bookkeeper>+-- for the sake of simplicity, but porting it to another record library like+-- <http://hackage.haskell.org/package/rawr rawr> shouldn't be too much work.+-- The aim is to see if the approach taken is generally useful and generalizes+-- well.+--+-- Let's start by defining some custom permissions:+--+-- > data Admin = Admin+-- > data Auth = Auth+--+-- And a record with protected fields:+--+-- > type Person = Book+-- > '[ "name" :=> Permission+-- > '[ "modify" :=> (Admin :&: Auth)+-- > , "insert" :=> Auth+-- > ] String+-- > , "age" :=> Permission+-- > '[ "modify" :=> Auth+-- > , "insert" :=> Auth+-- > ] Int+-- > ]+--+-- /Note:/ 'unsafePermission' shouldn't be called from user code. It is intended+-- to be called by other libraries only (i.e. database access layer). It's+-- only used here to easily create a value with protected fields.+--+-- > person :: Person+-- > person = emptyBook+-- > & #name =: unsafePermission "person"+-- > & #age =: unsafePermission 6+--+-- This is a normal 'Book', except that its fields are protected by the+-- opaque data type 'Permission'. A 'Permission' takes the following form:+--+-- > Permission [ mode :=> permissions, mode2 :=> permissions2 ] type+--+-- /Modes/ help define permissions for different purposes, i.e. reading or+-- modifying. Modes can be arbitrary, but certain functions like 'modify' or+-- 'insert' expect certain modes to be present.+--+-- Different permissions can be mixed with the ':|:' (/boolean or/) and ':&:'+-- (/boolean and/) operators, i.e:+--+-- > Permission [ "modify" :=> (Admin :&: Auth)] String+--+-- This means that the field can be accessed only when /both/ permissions+-- 'Admin' and 'Auth' are provided. Contrast this with:+--+-- > Permission [ "modify" :=> (Admin :|: Auth)] String+--+-- which means that access is granted by providing at least one of the+-- required permissions.+--+-- ':|:' and ':&:' can be nested arbitrarily.+--+-- Now, the general idea is to provide a list of permissions when+-- accessing protected data:+--+-- > modify (Auth `Set.Ext` Set.Empty) f person+-- > where f = ...+--+-- The provided list of permissions is used to /eliminate/ the 'Permission'+-- constructor from all fields that require less or equal permissions to those+-- provided in the permissions list. The above would eliminate the 'Permission'+-- constructor from the field "age", but would leave the type of "name" as:+--+-- > Permission [ "modify" :=> Admin ] String+--+-- meaning that it can't be accessed without providing the permission 'Admin'.+-- The whole type of 'f' would be:+--+-- > f :: Book' '[ "age" :=> Int+-- > , "name" :=> Permission '["modify" :=> Admin] String+-- > ]+-- > -> Book' '[ "age" :=> Int+-- > , "name" :=> Permission '["modify" :=> Admin] String+-- > ]+--+-- In constrast, the following:+--+-- > modify (Admin `Set.Ext` (Auth `Set.Ext` Set.Empty)) f person+-- > where f = ...+--+-- would provide access to all fields.++-- * Permissions+ Permission+ , (:|:), (:&:)++-- * Reading+ , Bookkeeper.Permissions.read++-- * Modification+ , modify++-- * Insertion+ , insert++-- * Unsafe+ , unsafePermission+ ) where++import Prelude hiding (and)++import GHC.TypeLits+import GHC.OverloadedLabels++import Data.Proxy++import Bookkeeper hiding (modify)+import Bookkeeper.Internal hiding (modify)++import qualified Data.Type.Map as Map+import qualified Data.Type.Set as Set++--------------------------------------------------------------------------------++type Iso a b = (a -> b, b -> a)++iso :: (a -> b) -> (b -> a) -> Iso a b+iso = (,)++data Star++-- | Type level boolean /or/.+data a :|: b++-- | Type level boolean /and/.+data a :&: b++-- | An opaque data type used for protecting record fields.+data Permission pr a = Permission a deriving Show++cnvPermission :: Permission prf a -> Permission prf' a+cnvPermission (Permission a) = Permission a++-- | Used to create protected values. Shouldn't be called from user code.+unsafePermission :: a -> Permission prf a+unsafePermission = Permission++type family ElimTerm1M prf x where+ ElimTerm1M prf (op () x) = ElimTerm1M prf x+ ElimTerm1M prf (op x ()) = ElimTerm1M prf x+ ElimTerm1M prf (prf :&: x) = ElimTerm1M prf x+ ElimTerm1M prf (x :&: prf) = ElimTerm1M prf x+ ElimTerm1M prf (op prf prf) = ()+ ElimTerm1M prf (prf :|: x) = ()+ ElimTerm1M prf (x :|: prf) = ()+ ElimTerm1M prf prf = ()+ ElimTerm1M prf x = x++data ModeNotFound++type family ElimTermM prf x where+ ElimTermM Star x = ()+ ElimTermM prf ('Just (op x y)) = ElimTerm1M prf (op (ElimTermM prf ('Just x)) (ElimTermM prf ('Just y)))+ ElimTermM prf ('Just x) = ElimTerm1M prf x+ ElimTermM prf 'Nothing = ModeNotFound++--------------------------------------------------------------------------------++type family UnpackPermissionM mode prf a where+ UnpackPermissionM mode prf (Permission '[mode :=> ()] a) = ElimM mode prf a+ UnpackPermissionM mode prf (Permission '[mode :=> ModeNotFound] a) = TypeError ('Text "Mode " ':<>: 'ShowType mode ':<>: 'Text " isn't defined for all fields")+ UnpackPermissionM mode prf (Permission prf' a) = Permission prf' a++class UnpackPermission mode prf a where+ unpackPermission :: Proxy mode -> Proxy prf -> Iso a (UnpackPermissionM mode prf a)++instance ( Elim mode prf a+ , UnpackPermissionM mode prf (Permission '[mode :=> ()] a) ~ (ElimM mode prf a)+ ) => UnpackPermission mode prf (Permission '[mode :=> ()] a) where+ unpackPermission mode prf = iso (\(Permission a) -> fst (elim mode prf) a) (\a -> Permission (snd (elim mode prf) a))++instance {-# OVERLAPPABLE #-} (UnpackPermissionM mode prf (Permission prf' a) ~ Permission prf' a) => UnpackPermission mode prf (Permission prf' a) where+ unpackPermission _ _ = iso id id++type family ElimM mode prf a where+ ElimM mode prf (Book' kvs) = Book' (ElimBookM mode prf kvs)+ ElimM mode prf x = x++class Elim mode prf a where+ elim :: Proxy mode -> Proxy prf -> Iso a (ElimM mode prf a)++instance (ElimBook mode prf kvs) => Elim mode prf (Book' kvs) where+ elim mode prf = iso (\a -> (fst (elimBook mode prf) a)) (\a -> (snd (elimBook mode prf) a))++instance {-# OVERLAPPABLE #-} (ElimM mode prf a ~ a) => Elim mode prf a where+ elim _ _ = iso id id++type family ElimBookM mode prf a where+ ElimBookM mode prf '[] = '[]+ ElimBookM mode prf ((k :=> Permission prf' v) ': m) = (k :=> UnpackPermissionM mode prf (Permission '[mode :=> (ElimTermM prf (Map.Lookup prf' mode))] v)) ': ElimBookM mode prf m+ ElimBookM mode prf ((k :=> v) ': m) = (k :=> ElimM mode prf v) ': ElimBookM mode prf m++class ElimBook mode prf a where+ elimBook :: Proxy mode -> Proxy prf -> Iso (Book' a) (Book' (ElimBookM mode prf a))++instance (ElimBookM mode prf '[] ~ '[]) => ElimBook mode prf '[] where+ elimBook _ _ = iso id id++instance {-# OVERLAPPABLE #-}+ ( UnpackPermission mode prf (Permission '[mode :=> (ElimTermM prf (Map.Lookup prf' mode))] v)+ , ElimBook mode prf m+ ) => ElimBook mode prf ((k :=> Permission prf' v) ': m) where+ elimBook mode prf = iso+ (\(Book (Map.Ext k v m)) -> Book (Map.Ext k (fst (unpackPermission mode prf) (cnvPermission v :: (Permission '[mode :=> (ElimTermM prf (Map.Lookup prf' mode))] v))) (getBook (fst (elimBook mode prf) (Book m)))))+ (\(Book (Map.Ext k v m)) -> Book (Map.Ext k (cnvPermission (snd (unpackPermission mode prf) v :: Permission '[mode :=> (ElimTermM prf (Map.Lookup prf' mode))] v)) (getBook (snd (elimBook mode prf) (Book m)))))++instance {-# OVERLAPPABLE #-}+ ( Elim mode prf v+ , ElimBook mode prf m+ , ElimBookM mode prf ((k :=> v) ': m) ~ ((k :=> ElimM mode prf v) ': ElimBookM mode prf m)+ ) => ElimBook mode prf ((k :=> v) ': m) where+ elimBook mode prf = iso+ (\(Book (Map.Ext k v m)) -> (Book (Map.Ext k (fst (elim mode prf) v) (getBook (fst (elim mode prf) (Book m))))))+ (\(Book (Map.Ext k v m)) -> (Book (Map.Ext k (snd (elim mode prf) v) (getBook (snd (elim mode prf) (Book m))))))++type family ElimListM mode lst a where+ ElimListM mode '[] a = a+ ElimListM mode (x:xs) a = ElimListM mode xs (ElimM mode x a)++class ElimList mode t a where+ elimList :: Proxy mode -> Set.Set t -> Iso a (ElimListM mode t a)++instance ElimList mode '[] a where+ elimList _ _ = iso id id++instance (Elim mode x a, ElimList mode xs (ElimM mode x a)) => ElimList mode (x : xs) a where+ elimList mode (Set.Ext _ xs) = iso+ ((fst (elimList mode xs)) . (fst (elim mode (Proxy :: Proxy x))))+ ((snd (elim mode (Proxy :: Proxy x))) . (snd (elimList mode xs)))++--------------------------------------------------------------------------------++data Mode (m :: Symbol) = Mode++instance (s ~ s') => IsLabel s (Mode s') where+ fromLabel _ = Mode++-- | Read a protected value.+--+-- The purpose of this library is to be integrated in other libraries that+-- provide access to data in some form. For that purpose, functions like+-- 'read', 'modify' and 'insert' are provided. These functions expect a+-- type level list of permissions in order to infer a type containing+-- fields with possibly eliminated 'Permission' constructors. How this list+-- is generated is up to the calling library.+read :: (ElimList "read" prf a) => Set.Set prf -> a -> (ElimListM "read" prf a)+read prf a = from a+ where (from, _) = elimList (Proxy :: Proxy "read") prf++-- | Modify a protected value.+--+-- The purpose of this library is to be integrated in other libraries that+-- provide access to data in some form. For that purpose, functions like+-- 'read', 'modify' and 'insert' are provided. These functions expect a+-- type level list of permissions in order to infer a type containing+-- fields with possibly eliminated 'Permission' constructors. How this list+-- is generated is up to the calling library.+modify :: (ElimList "modify" prf a) => Set.Set prf -> (ElimListM "modify" prf a -> ElimListM "modify" prf a) -> a -> a+modify prf f = to . f . from+ where (from, to) = elimList (Proxy :: Proxy "modify") prf++-- | Create a protected value.+--+-- The purpose of this library is to be integrated in other libraries that+-- provide access to data in some form. For that purpose, functions like+-- 'read', 'modify' and 'insert' are provided. These functions expect a+-- type level list of permissions in order to infer a type containing+-- fields with possibly eliminated 'Permission' constructors. How this list+-- is generated is up to the calling library.+insert :: (ElimList "insert" prf a) => Set.Set prf -> (ElimListM "insert" prf a) -> a+insert prf a = to a+ where (_, to) = elimList (Proxy :: Proxy "insert") prf
+ src/Bookkeeper/Permissions/Examples.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}++module Bookkeeper.Permissions.Examples where++import Bookkeeper+import Bookkeeper.Internal+import Bookkeeper.Permissions as P++import qualified Data.Type.Map as Map+import qualified Data.Type.Set as Set++data Admin = Admin+data Auth = Auth++type Person = Book+ '[ "name" :=> Permission+ '[ "modify" :=> (Admin :&: Auth)+ , "insert" :=> Auth+ ] String+ , "age" :=> Permission+ '[ "modify" :=> Auth+ , "insert" :=> Auth+ ] Int+ , "bff" :=> Permission+ '[ "modify" :=> Admin+ , "insert" :=> Auth+ ] (Book+ '[ "forever" :=> Permission+ '[ "modify" :=> Admin+ , "insert" :=> Auth+ ] Bool+ ])+ , "key" :=> Permission+ '[ "read" :=> Admin+ , "modify" :=> Admin+ , "insert" :=> Auth+ ] String+ ]++person :: Person+person = emptyBook+ & #name =: unsafePermission "person"+ & #age =: unsafePermission 6+ & #bff =: unsafePermission (emptyBook & #forever =: unsafePermission True)+ & #key =: unsafePermission "key"++test_insert :: Person+test_insert = insert (Auth `Set.Ext` Set.Empty) $ emptyBook+ & #name =: "person"+ & #age =: 6+ & #bff =: (emptyBook & #forever =: True)+ & #key =: "key"++insertKey :: Book' (old Map.:\ "key") -> Book' old+insertKey = undefined++test_insert' :: Person+test_insert' = insertKey $ insert (Auth `Set.Ext` Set.Empty) $ emptyBook+ & #name =: "person"+ & #age =: 6+ & #bff =: (emptyBook & #forever =: True)++test_modify :: Person+test_modify = P.modify (Auth `Set.Ext` Set.Empty) f person+ where f p = p & #age =: 6