52 Static vs dynamic typing

Static typing

The keyword var introduces a statically typed variable. The element type of the variable is either supplied by an explicit type annotation or determined by static type deduction applied to the expression used to assign its initial value. Subsequent assignments must be compatible with this static element type; otherwise a static type error is reported.

A variable declaration may also include a cardinality qualifier, such as * or ?. That qualifier is a constraint on the variable location, not part of the element type. Assignment to the variable must satisfy both the static element type and the location's cardinality constraint.

For example, var Integer id* = {}; declares a location named id whose extension contains zero or more Integer values. The element type is still Integer, not Set<Integer>.

These are separate static checks. Assigning a String expression to an Integer variable is a static type check failure. Assigning an expression whose static cardinality may be many to a cardinality-one variable is a static cardinality constraint check failure.

// Introduces a statically typed variable named x. Its static type is Integer.
var x = 10;

// Gives an empty multi-valued variable an explicit element type.
var Integer id* = {};

// Static type check failure: String is not assignable to Integer.
x := "hello";

Cardinality flow

A common case is an optional path that has been tested before it is used:

value List
{
    Integer head;
    List tail?;
}

func Boolean memberOf(List list, Integer value)
{
    if list.head = value {
        return true;
    }

    if list.tail = none {
        return false;
    }

    return list.tail.memberOf(value);
}

The attribute tail? makes list.tail optional, so the expression has static cardinality zero or one. The final statement passes list.tail as the receiver argument to memberOf, whose first parameter requires a single List.

The call is valid because the preceding test has refined the cardinality. The test list.tail = none proves that the extension is empty in the guarded block. Because that block returns, the following statements are checked in the remaining case, where list.tail is non-empty. Since the original cardinality was at most one, the remaining cardinality is exactly one.

This is cardinality flow. Static checking tracks both an expression's element type and its static cardinality. Flow-sensitive checks may refine cardinality in guarded scopes, just as a positive type test may refine the static type of an expression.

Similarly, inside the then-branch of if E ≠ none { ... }, an expression E whose static cardinality is zero or one is narrowed to cardinality one. For an expression whose static cardinality may be many, E ≠ none proves only that the extension is non-empty; it does not make the expression single-valued.

Cardinality flow is a static analysis rule. It does not execute a query while checking the program. If a required cardinality fact cannot be proved from the static expression shape and the enclosing guards, the use is rejected as a static cardinality constraint check failure.

Dynamic typing

Dynamic variables are disabled by default. A file with no @dynamic directive is in strict mode, so assigning to a name that has not been declared with var is a static error.

A script or interactive file may opt into dynamic variables by putting @dynamic = true; in the source-file prologue: after any component declaration and before any using declaration, ordinary declaration, or statement. In a script with no component declaration, this is the first non-comment item in the file. In that mode, assigning to an undeclared name introduces a dynamically typed variable. A dynamically typed variable can later be assigned values of any type. This mode is intended for exploratory, interactive, or script-like code.

@dynamic = true;

// First assignment introduces a dynamic variable named y.
y := 10;

// y can be freely reassigned a value of any type.
y := "hello";

Default strict mode

Reusable component source must use the default strict mode and must not enable dynamic variables. In strict mode, dynamic variables are not permitted and every variable must be introduced explicitly using var. Because strict mode is the default, source normally omits the directive; @dynamic = false; is allowed as an explicit spelling of the default.

@dynamic = false;

// Static error: dynamic variables are disabled.
y := 10;

Rationale

Predica is fundamentally a statically typed language designed for clarity, safety, and formal reasoning. Static typing ensures that errors are detected early and that programs remain predictable and analyzable.

However, practical development workflows also benefit from a lightweight, flexible mechanism for experimentation, scripting, and interactive exploration. Dynamic variables provide this flexibility without weakening the core type system, because they are introduced only when the programmer omits var in a file that explicitly enables dynamic mode.

This design keeps the language mathematically disciplined while still supporting rapid prototyping and REPL-style usage.