101 Parameter Access and Ownership

Predica states parameter access directly. A plain parameter provides read-only access to a value. At a pass-by-reference or explicit pass-by-move call site, the caller uses an expression that denotes a location. & temporarily grants exclusive access to the denoted location, while ^ moves its value into an owned parameter.

Read-only parameters

func String identity(String x) =
    x;

A plain parameter is read-only and non-owning. The callee may read it and may copy its value into an owned variable, but it cannot update or consume the parameter. This is a source-language access rule, not a physical calling convention. An implementation may pass a cheap representation by value and an expensive representation by const reference.

Exclusive reference parameters

proc appendGreeting(&String x)
{
    x += "hi";
}

var String s = "hello";
appendGreeting(&s);

The & on the procedure parameter requires exclusive access, and the matching & at the call site explicitly grants that access. The argument expression must denote an initialised mutable location. For the duration of the call, no other code may read, update, or consume that location. The callee may read or update it but does not own it and cannot consume it.

Exclusive access to sublocations

A variable may contain sublocations. Attributes of a value held by a variable, and other mutable components selected from it, are locations in their own right. A caller may grant a callee exclusive access to such a sublocation by using an expression that denotes it:

value Point
{
    Integer x;
    Integer y;
}

proc increment(&Integer n)
{
    n++;
}

var Point p = Point { x = 1, y = 2 };
increment(&p.x);

The call grants increment exclusive access to the sublocation p.x, not to a copy of its value. The callee's update is therefore an update of p.x. During the call, the caller and other callees may not access p.x through that expression, through p, or through any other expression denoting an overlapping location. Access to a disjoint sublocation such as p.y does not conflict with the grant.

A reference exists only for the call. It cannot be stored, returned, captured, or otherwise used after the call finishes. Exclusive access may be passed on temporarily to another reference parameter:

proc inner(&String x)
{
    x += "b";
}

proc outer(&String x)
{
    x += "a";
    inner(&x);
    x += "c";
}

While inner is executing, outer has temporarily lent its exclusive access and cannot use x. It regains access when inner finishes. Reference parameters are permitted on procedures, where mutation of caller state is an explicit effect. They are not permitted on functions, folds, or external pure functions.

Owned parameters and moves

func String appendGreeting(^String x)
{
    x += "hi";
    return x;
}

The ^ on a parameter declares an owned variable in the callee. The callee may read, update, or consume it. An ordinary argument expression initialises the parameter by value. An explicit ^ argument moves the value from an initialised location owned by the caller. The call-site expression denotes that location; the callee receives the value in an owned parameter and the caller's location becomes uninitialised:

var String a = appendGreeting("a");  // constructs the owned parameter

var String s = "a";
var String b = appendGreeting(s);    // copies s; s remains initialised
var String c = appendGreeting(^s);   // moves s; s becomes uninitialised

A borrowed reference parameter cannot be moved because the current procedure does not own the referenced location. An explicit move may use any expression that denotes an initialised location owned by the caller, including an owned sublocation.

Moving, reinitialisation, and the requirement that every passed location be initialised are governed by Uninitialised Locations.

Exceptional exits

Once a call argument ^s transfers its value, s remains uninitialised if the call raises an exception. An exclusive reference granted by &s ends on every exit from the call, including an exceptional exit. Updates performed through the reference before the exception remain visible unless another specified mechanism, such as transaction rollback, reverses them.