Definitions & Declarations

At the top level, a Par file consists of definitions, declarations, and type definitions.

These define global names that can be used throughout the file, an unlimited number of times.

Because of Par’s linear type system, local variables may be required to use exactly once. That is if they have a linear type. Global definitions can be used any number of times regardless of their type.

Par has a simple naming rule:

• Global names start with an upper-case letter. That is global types, functions, and so on.
• Local names start with lower-case letter, or _. That includes local variables, function parameters, and type variables in generic functions.

While global names can be used throughout the program, there is an important restriction!

❗ Cyclic usages are forbidden! Both in types, and in definitions.

That means that if a type Alice uses a type Bob, then Bob can’t use Alice. Same for functions, and other definitions. In fact, Alice can’t use Alice either!

This apparently mad restriction has important motivations, and innovative remedies.

The motivation is Par’s ambitious stride towards totality — which means preventing infinite loops.

Unrestricted recursion is a source of infinite loops, and while that can be partially remedied by totality checkers, such as in Agda, Par chooses a different approach. That is outlawing unrestricted recursion, and instead relying on more principled ways to achieve cyclic behavior, including what’s usually achieved by mutual recursion.

The remedies come in form of these more principled ways. Fortunately, they don’t just replace the familiar recursion by clunkier mechanisms, they bring their own perks.

Naive recursion on the term level (like in functions) is replaced by a powerful, universal looping mechanism, called begin/loop. It’s a single tool usable for:

• Recursive reduction. Analyzing lists, trees, or even files.
• Iterative construction. Those are objects that can be interacted with repeatedly.
• Imperative-looking loops in process syntax.

Naive recursion in types is replaced by anonymous recursive and iterative (corecursive) types.

Definitions

Global values (including functions) are defined at the top level starting with the keyword def, followed by an upper-case name, an = sign, and an expression computing the value.

def MyNumber = 7

In this case, Par is able to infer the type of MyNumber as Nat (a natural number), so no type annotation is needed. Often, a type annotation is needed, or wanted. In those cases, we can add it using a colon after the name:

def MyName: String = "Michal"

Declarations

Sometimes a type is longer and a definition becomes busy and hard to read with it.

For example, here’s a simple function adding up all the numbers in a list:

def SumList: [List<Int>] Int = [list] list.begin.case {
  .end!       => 0,
  .item(x) xs => Int.Add(x, xs.loop),
}

The code uses many concepts that will be covered later, so only focus on the parts you know: def, :, and =. (You can run it in the playground, though!)

In such a case, the type annotation can be extracted into a separate declaration. A declaration starts with the keyword dec, followed by the name we want to annotate, a colon, and a type.

dec SumList : [List<Int>] Int

def SumList = [list] list.begin.case {
  .end!       => 0,
  .item(x) xs => Int.Add(x, xs.loop),
}

That’s much better!

Declarations may be placed anywhere in a file, so feel free to put them all on top, or keep them close to their corresponding definitions.

Type Definitions

Par has a structural type system. While many languages offer multiple forms of type definitions — for example, Rust has struct, enum, and more — Par only has one: type aliases.

With recursive and iterative types being anonymous, Par has no issue treating types as their shapes, instead of their names. In fact, type definitions are completely redundant in Par. Every usage of a global type (with the exception of the primitives) can be replaced by its definition, until no definitions are used.

Actually, all definitions are redundant in Par. However, programming without them would be quite tedious.

To give a name to a type, use the type keyword at the top level, followed by an upper-case name, an = sign, and a type to assign to it.

type MyString = String

MyString is now equal to String and can be used wherever String can.

A more useful example:

type StringBuilder = iterative choice {
  .build => String,
  .add(String) => self,
}

This particular type is a part of the built-in functionality, under the name String.Builder.

That’s an iterative choice type, something we will learn later. It’s an object that can be interacted with repeatedly, choosing a branch (a method) every time.

While we could paste the entire definition every time we would use this StringBuilder, it’s quite clear why we wouldn’t want to do that.

Generic types

A type definition may include generic type parameters, turning it into a formula that can be instantiated with any types substituted for the parameters.

The type parameters are specified in a comma-separated list inside angle brackets right after the type name. The parameters are local names, so they must be lower-case.

For example, the built-in List type has one type parameter:

type List<a> = recursive either {
  .end!,
  .item(a) self,
}

That’s a recursive either type, also something we will learn later. In this case, it defines a finite, singly-linked list of items of type a.

To use a generic type, we append a comma-separated list of specific type arguments enclosed in angle brackets after the type’s name.

type IntList = List<Int>

The resulting type is obtained by replacing each occurrence of each type variable by its corresponding type argument. So, the above is equal to:

type IntListExpanded = recursive either {
  .end!,
  .item(Int) self,
}