Bookkeeper.Permissions

Introduction

This experimental library adds permissions to 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 bookkeeper for the sake of simplicity, but porting it to another record library like 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

data Permission pr a

An opaque data type used for protecting record fields.

Instances

Show a => Show (Permission k pr a)

Methods

showsPrec :: Int -> Permission k pr a -> ShowS

show :: Permission k pr a -> String

showList :: [Permission k pr a] -> ShowS

data a :|: b

Type level boolean or.

data a :&: b

Type level boolean and.

Reading

read :: ElimList "read" prf a => Set prf -> a -> ElimListM "read" prf a

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.

Modification

modify :: ElimList "modify" prf a => Set prf -> (ElimListM "modify" prf a -> ElimListM "modify" prf a) -> a -> a

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.

Insertion

insert :: ElimList "insert" prf a => Set prf -> ElimListM "insert" prf a -> a

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.

Unsafe

unsafePermission :: a -> Permission prf a

Used to create protected values. Shouldn't be called from user code.