diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/bookkeeper-permissions.cabal b/bookkeeper-permissions.cabal new file mode 100644 --- /dev/null +++ b/bookkeeper-permissions.cabal @@ -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 diff --git a/src/Bookkeeper/Permissions.hs b/src/Bookkeeper/Permissions.hs new file mode 100644 --- /dev/null +++ b/src/Bookkeeper/Permissions.hs @@ -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 +-- 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 +-- for the sake of simplicity, but porting it to another record library like +-- 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 diff --git a/src/Bookkeeper/Permissions/Examples.hs b/src/Bookkeeper/Permissions/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Bookkeeper/Permissions/Examples.hs @@ -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