Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Permission pr a
- data a :|: b
- data a :&: b
- read :: ElimList "read" prf a => Set prf -> a -> ElimListM "read" prf a
- modify :: ElimList "modify" prf a => Set prf -> (ElimListM "modify" prf a -> ElimListM "modify" prf a) -> a -> a
- insert :: ElimList "insert" prf a => Set prf -> ElimListM "insert" prf a -> a
- unsafePermission :: a -> Permission prf a
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 Source #
An opaque data type used for protecting record fields.
Show a => Show (Permission k pr a) Source # | |
Reading
read :: ElimList "read" prf a => Set prf -> a -> ElimListM "read" prf a Source #
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 Source #
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 Source #
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 Source #
Used to create protected values. Shouldn't be called from user code.