Reference
/
Polar Syntax

Polar Syntax

Polar is a declarative logic programming language specialized for authorization logic. This guide is a brief description of the core syntax of Polar.

Each Polar file defines a set of rules. When a Polar file is loaded into the authorization engine, all rules are added to the engine's knowledge base, which can then be queried for authorization decisions.

Boolean

Polar parses the keywords true and false as boolean values.

String

Polar supports double-quoted (") strings, which can be used to represent any textual data. Quotes within strings can be escaped with a single backslash ("\""). Two strings are considered equal if they have the same length and each of their corresponding characters are equal.

The string type can be referenced as String for use as a specializer or with the matches operator:

is_string(_s: String);
is_string(s) if s matches String;

List

A list is an ordered sequence of values defined using square brackets: [v1, v2, ..., vN]. For example:

["polar", "lang", "oso"]
["oso", ["polar", "lang"]]

For lists of strings, membership can be determined using the in operator.

Rules

Rules are logical statements that may be conditional ("if this then that").

The simplest rule is the statement of a fact, such as:

is_bear("Yogi");

This rule is unconditional: it states that Yogi is a bear.

However, a rule can also be conditional. Consider the following:

is_person(x) if is_bear(x);

This rule states that x is a person if x is a bear. Given a policy consisting of the above pair of rules, Oso Cloud can infer that Yogi is a person because we've told it that Yogi is a bear and that if something is a bear then it is a person. Bears are people, too, y'know.

Variables

In Polar, a variable does not need a separate declaration; it is initialized the first time it is referenced in a rule. The following are all variables: foo, BAR, myVar123.

If a variable is unbound and unified with a value, the variable will be bound to that value for the remainder of the rule. If two bound variables are unified, their values will be unified. For example:

# Bind variable `x` -> "hello"
x = "hello"

# With `x` still bound to "hello", unifying it again with "hello" succeeds…
"hello" = x

# …but unifying `x` with "world" fails:
x = "world"

# With `x` still bound to "hello", binding `y` to "world" and then unifying `x`
# and `y` fails
y = "world" and x = y

Singletons

If a variable occurs only once, then its value can't be used for anything. Such variables are called singletons, and Polar will warn you if they occur in a rule. For example, if you try to load the rule…

user(first, last) if person("George", last);

…you'll see the following message:

Singleton variable first is unused or undefined
001: user(first, last) if person("George", last);
          ^

The reason these warnings are important is that, as in this case, they usually indicate logical errors. Here, the error is forgetting to use the first variable, and instead using a literal string ("George") in the call to the person rule.

Singleton variables can be seen as wildcards: their values depend on nothing else in the expression and therefore can be anything. In the example above, first matches any value as long as person("George", last) results in a match.

If you wish to keep an unused parameter in a rule, you can suppress the singleton variable warning by starting your variable's name with an _ (underscore), e.g., change first to _first in the example above. The underscore makes explicit that the variable can match any value.

Operators

Operators are used to combine terms in rule bodies into expressions.

Unification

Unification is the basic matching operation in Polar. Two values are said to unify if they are equal or if there is a consistent set of variable bindings that makes them equal. Unification is defined recursively over lists: two lists unify if all of their corresponding elements unify.

The unification operator (=) checks if its left and right operands unify; for example, "a" = "a", x = "a", or ["a", "b"] = [x, "b"] where the variable x is either bound to "a" or unbound.

Conjunction (and)

The and operator is used to state that a pair of conditions in a rule's body must both hold. For example, the rule…

oso_employee(first, last) if
  is_user(first, last) and
  is_employee("Oso", first, last);

…will be satisfied if the person is a user and an Oso employee.

Disjunction (or)

The or operator will be true if either its left or its right operand is true. Disjunctions can always be replaced by multiple rules with identical heads but different bodies, but the or operator may help simplify writing rules with alternatives. For example:

is_user(first, last) if
  oso_employee(first, last) or
  is_guest(first, last);

# The `or` can be rewritten as a pair of rules:
is_user(first, last) if oso_employee(first, last);
is_user(first, last) if is_guest(first, last);

List membership (in)

The in operator can be used to iterate over lists of strings. An in operation looks like this:

x in ["a", "b", "c"]

The left operand, x, is a variable that will be unified with each element in the list. If the right operand is not a list of strings, the in operation will fail.

In the following example, the variable x will be bound to "a", "b", and "c", in turn, and then the x = "a" check will evaluate. This expression will only succeed for the first item in the list, "a".

x in ["a", "b", "c"] and x = "a"

The left operand does not need to be a variable. For example, the following expression will succeed twice since "a" is in the first and fourth positions in the list:

"a" in ["a", "b", "c", "a"]

Patterns and Matching

Polar has powerful pattern matching facilities that can control which rules execute and act as type guards within rule bodies.

Specialization

Rule heads (the part of the rule before the if keyword) can contain specializers. A specializer is usually an application type, but there are also a couple built-in specializers. When Polar evaluates a query to see if it matches a rule head, the query will only match if the types of the query's arguments match the specializers in the rule head. For example, given the rule…

is_person(_person: Person);

…the lone argument in a query for is_person must be of type Person.

Multiple rules with the same name can be written with different specializers:

is_person(_person: Person);
is_person(_user: User);

Now, the is_person rule will match if the argument is a User or a Person.

matches operator

The matches operator can be used anywhere within a rule body to assert that a variable has a certain type. The semantics are identical to specialization; x matches Person will succeed if x is of type Person and fail otherwise.

Actor and Resource Specializers

Oso provides built-in specializers that will match any application type that has been declared via an actor or resource block.

The Actor specializer will match any application type that has been declared via an actor block, and Resource will match types declared via actor and resource blocks.

For example, the following is a valid head for an allow rule:

allow(actor: Actor, action, resource: Resource) if ...

The Actor and Resource specializers are used by Oso's resource blocks to simplify policies.