Polar: Types

Polar's type system lets you write flexible and expressive policies. In this guide, we'll cover Polar's type system and how it affects rule evaluation and, as a result, authorization.

Note that this guide assumes you have gone over:

• Polar: Introduction
• Polar: Testing and Policy Iteration

Overview

Logical programming lets you describe rules that are true under certain conditions, which you can think of as the rule's constraints. For example, this rule:

...is considered true only when Polar can find a set of values such that each inner expression is true.

Polar's type system lets you apply an additional class of constraint on your rules by stating that the rule is satisfied only by values of the specified type.

For example:

Though this is a toy example that only ensures bears and birds never appear related, Polar's type system confers more serious benefits:

• Application modeling to mirror your application's relationships in your policy.
• Expressive constraints to precisely define complex rules.
• Polymorphism to write rules that can apply to multiple types of resources, enhancing code reusability and simplifying your policy.

Using types

Polar supports the following types:

• Primitive types
• Resources you define in your policy

Polar then uses types for:

• Value typing, which lets you declare values' types.
• Variable binding, which lets you declare that a variable may only be bound to values of a specific type.
• Unification + inference, where Polar uses value types, variable binding, and equality (unification) to draw inferences.

Value typing

Polar values have a declared type. In many cases, you will explicitly declare the type. However, Polar typically infers that string literals (e.g. "admin") are of the primitive String type.

How you specify a value's type depends on where the value is used:

Variable binding

Polar lets you declare that a variable may only be bound to values of a specific type. This can be done in a rule's...

• Head by typing a parameter. For example:

  
  

  has_permission(user: User, "edit", organization: Organization) if

  has_role(user, "admin", organization);

  
  

• Body using the matches operator on an otherwise untyped variable. For example:

  
  

  has_permission(actor: Actor, "view", account: Account) if

  organization matches Organization and

  has_relation(account, "parent", organization) and

  has_role(actor, "member", organization);

  
  

Binding + unification

When you query Oso, Polar uses types to determine which values that satisfy the query. To do this, Polar ensures:

• All values bound to a variable are of the variable's declared type.
• All objects literals unify with facts that are present in your authorization data or are inferrable from your policy.

Simple example

Consider this rule:

This rule can be satisfied where Polar can find valid bindings for user and organization that are of type User and Organization, whose second parameter is exactly the string "admin".

Complex example

For instance, consider the following policy that defines multiple actors: User and Bot.

The check for Bot{"alice"}'s ability to "edit" Organization{"acme"} fails because there is no has_permission rule defined whose first parameter is Bot and whose second parameter is exactly "edit".

This policy is self-contained, so you can place it in your rules editor, and then run the tests.

As a challenge, manipulate the policy to change the assert_not into an assert.

Polymorphism

Not only is Polar a typed language, it is also polymorphic. For most users, this just means that parameters whose type is Actor can accept any resource type declared as an actor, and likewise for Resource and resource.

Don't worry too much, though––polymorphism is an advanced feature and many users never need to use it directly.

Example

Below, by simply changing the has_permission rule's first parameter from user: User to actor: Actor, we can generalize the rule to automatically work for all actor resources, i.e. both User and Bot.

The check for Bot{"alice"}'s ability to "edit" Organization{"acme"} now succeeds because:

• There is a has_permission statement whose first parameter can be bound to Bot values, and whose second parameter is exactly "edit".
• The has_permission rule is satisfied because there is also authorization data of the form has_role(bot: Bot, "admin", organization: Organization) whose variables can be consistently bound to the query's values.