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.
Polar parses the keywords
false as boolean values.
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.
is_string(_s: String); is_string(s) if s matches String;
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
Rules are logical statements that may be conditional ("if this then that").
The simplest rule is the statement of a fact, such as:
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.
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:
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
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
variable, and instead using a literal string (
"George") in the call to the
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
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 in the example above. The
underscore makes explicit that the variable can match any value.
Operators are used to combine terms in rule bodies into expressions.
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
"a" = "a",
x = "a", or
["a", "b"] = [x, "b"] where the variable
x is either bound to
"a" or unbound.
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.
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);
in operator can be used to iterate over lists of strings. An
operation looks like this:
x in ["a", "b", "c"]
In the following example, the variable
x will be bound to
"c", in turn, and then the
x = "a" check will evaluate. This expression
will only succeed for the first item in the list,
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"]
Polar has powerful pattern matching facilities that can control which rules execute and act as type guards within rule bodies.
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…
…the lone argument in a query for
is_person must be of type
Multiple rules with the same name can be written with different specializers:
is_person(_person: Person); is_person(_user: User);
is_person rule will match if the argument is a
User or a
matches operator can be used anywhere within a rule body to assert that a
variable has a certain type. The semantics are identical to
x matches Person will succeed if
x is of
Person and fail otherwise.
Oso provides built-in specializers that will match any application type that has been declared via an actor or resource block.
Actor specializer will match any application type that has been declared
actor block, and
Resource will match types declared via
For example, the following is a valid head for an
allow(actor: Actor, action, resource: Resource) if ...
Resource specializers are used by Oso's
resource blocks to simplify policies.
Alongside your policy, Oso uses small pieces of authorization data called facts to make authorization decisions. Facts are concrete pieces of authorization-relevant information about the entities in your application, such as role assignments for specific users. Your application is responsible for providing these facts to Oso. You can learn more about facts here.
Oso infers type information about facts based on how the facts are used in your policy. For example, with a policy like this:
has_permission(user: User, "pet", dog: Dog) if are_friends(user, dog);
Oso infers that it should only accept
are_friends facts with two arguments,
where the first argument is a
User and the second is a
Oso uses these inferred fact types to prevent you from inserting invalid facts.
For example, with the above policy, if you attempted to tell
Oso the fact
are_friends(User:alice, Rabbit:peter), Oso would reject the
fact, because your policy doesn't use facts with the type
are_friends(User, Rabbit). Additionally, Oso prevents you from accidentally
omitting an argument-- Oso will reject
are_friends(User:alice), because the
Dog argument is missing.
Oso also uses these inferred types to prevent you from inserting facts that it
doesn't know about. This makes it impossible to accidentally insert a fact with
a misspelled predicate, like
What if you want Oso Cloud to store a fact that isn't used anywhere in your policy? For
instance, maybe you want to tag users by inserting
has_tag facts into Oso,
anticipating that you might use tags in your policy someday. Or maybe you
already tag users and use those in your policy, but you want to start tagging
In these cases, you can use the
declare statement to force Oso to accept a certain fact type:
declare has_tag(User, Tag);
This will make Oso accept facts like
has_tag(User:alice, Tag:is-cool), even
if your policy doesn't currently use facts like this.
You can have multiple
declare statements for a given fact predicate:
declare has_tag(User, Tag); declare has_tag(Dog, Tag); declare has_tag(Tag, Tag, Tag); # I heard you like tags.
declare statements form a union type-- as long as a fact matches
one of the declared or inferred types, Oso will accept it.
You never need to use a
declare statement for fact types that are used in
declare statements are only for making Oso accept fact types
that your policy never uses. Most policies will not use