85 Folds

A fold reduces the values reached by a path to a single value. Common examples are counting the values, testing whether any value exists, summing numeric values, or collecting the reached values as a set.

Standard Library Folds

The standard library provides common folds:

Entries in this table may appear before every supporting declaration form or result type has been specified elsewhere in the language. Such entries are intentional specification todos, not permission to remove the fold from the standard vocabulary. A planned entry does not create a usable std declaration until the standard library chapter gives its declaration, typing, and definedness rules.

Query folds operate over the observed extension of a unary path frame. Relation-view or m-relation operations such as factorised collapse are implementation techniques, not standard library query folds.

The spelling E.Σname applies the fold named name to the observed extension of E. The collector E.Σ is primitive syntax and does not look up a fold name.

Standard folds are declared by the standard library component std. Every non-std component has an implicit dependency on std, and every source file has a standard prelude scope. The prelude makes common standard folds available unqualified and makes std available as an explicit component qualifier. Therefore E.Σcount means the fold declaration std.count. The explicit qualified form E.Σstd.count is also legal and denotes the same fold, but it is not the canonical spelling used by examples or renderers.

The std qualifier only selects declarations that are actually present in the standard library component. It is not legal to write E.Σstd.median or E.Σstd.collapse unless a future version of std declares folds named median or collapse. The unqualified forms E.Σmedian and E.Σcollapse are likewise not predefined standard folds; they are valid only when a visible user-defined or imported fold declaration with that local name is in scope.

Fold names from other components may be referenced unqualified only when that local name is not a standard prelude fold and the visible name is unambiguous. If a third-party component declares a fold with a standard name such as count, exists, or sum, the declaration is legal, but the third-party fold must be referenced with a component qualification or with an explicit local alias that does not use a standard fold name.

using vendor.Stats as stats;
using vendor.Stats { count as weightedCount };

items.Σcount          // std.count, even though vendor.Stats also declares count
items.Σstats.count    // vendor.Stats.count
items.ΣweightedCount  // vendor.Stats.count through an alias

A selected import that would bind a third-party fold to a standard fold name is invalid. For example, if count and mean are standard folds, then this import is rejected:

using vendor.Stats { count, avg as mean };

The import must use distinct aliases, or the third-party folds must be referenced through a component alias:

using vendor.Stats as stats;
using vendor.Stats { count as statsCount, avg as statsMean };

items.Σcount       // std.count
items.Σmean        // std.mean
items.Σstats.count // vendor.Stats.count
items.Σstats.avg   // vendor.Stats.avg
items.ΣstatsCount  // vendor.Stats.count
items.ΣstatsMean   // vendor.Stats.avg

If two non-standard components make the same unqualified fold name visible, an unqualified use of that fold name is ambiguous. The program must qualify the fold name with a component alias, or import one or both folds under distinct aliases.

For example, the following query is used to find the parts shipped by exactly one supplier:

s.part.[shipment.supplier.Σcount = 1]

Fold typing and definedness

For fold typing, the specification uses Extension<K,T> as metalanguage notation for an observed extension with element type T and order kind K. It is not source-level Predica syntax. The order kind is either unordered, for ordinary set-valued path observations, or ordered, for list-valued observations produced by operators such as orderBy.

If E has observed extension type Extension<K,T>, then a named fold application E.Σf<...>(args...) resolves the fold name f, instantiates the fold's generic parameters, checks its constraints, checks each ordinary argument against the corresponding fold parameter type, and gives the application the fold declaration's result type. The generic argument list and ordinary argument list are both optional. When the generic argument list is omitted, the generic parameters are inferred from the folded element type where possible; when it is present, the explicit generic arguments are checked against the declaration. A qualified fold name such as E.Σstats.count resolves through the component qualifier before the same instantiation and argument-checking rules are applied.

An unseeded inline fold E.Σ{ z ; a v ↦ step } is well-typed when z has some accumulator type A, a is bound as A, v is bound as T, and step has type A. The result type is A. On an empty input extension, the result is z.

A seeded inline fold E.Σ{ first v ↦ seed ; a v ↦ step } is well-typed when v in the seed clause has type T, seed has some accumulator type A, a is bound as A, the second v is bound as T, and step has type A. The result type is A.

Seeded folds and folds whose defined where guard is false have no result. This is the same no-result denotation used by none: it is not a marker value, and it is not a member of the fold's result type. In a query, a no-result fold contributes no output value for the surrounding scalar expression. A context that requires a total scalar value must either use a total fold or establish the fold's definedness before using the result.

In a declaration of the form fold R name<...>(params...) over input ..., the input binder has type Extension<K,T>, where T is the instantiated element type and K is the order kind of the fold operand. Ordinary parameters in params... are bound as values in the body and in any defined where guard. The body expression must have type R. The body may filter, order, and fold input; if it uses an order-sensitive operation, the usual order-kind rules still apply.

A fold application is well-typed only when the fold is defined for the operand's order kind. Order-insensitive folds may be applied to unordered or ordered extensions. Order-sensitive folds, such as Σconcat and Σlist, require an ordered input extension. Applying an order-sensitive fold directly to an unordered set extension is a compile-time error; use orderBy first.

For unordered input, the denotation of a fold must be independent of enumeration order and grouping. For an unseeded fold this requires the combining operation to be associative and order-insensitive with respect to the initial value. For a seeded fold it also requires independence from which element is chosen as the seed. Ordered input folds are evaluated in list order and may be order-sensitive.

General fold syntax

Predica supports both named fold declarations and inline fold expressions. This unifies standard aggregates and user-defined reductions while keeping the logic-frame denotation primary.

In the general case, a fold consumes the values in an observed unary extension, an initial value z, and a binary operation ⊕, where ⊕(a,v) combines an accumulated value a with the next value v.

The inline syntax for the general case is:

e.Σ{ z ; a v ↦ ⊕(a,v) }

The binder a names the accumulator and v names the current element from the observed extension. The element is not a normal function argument; it is supplied by the path on the left of .Σ.

Some folds, such as min and max, need the initial accumulator to be one of the input values rather than a fixed literal. A seeded general fold uses the first input value as the seed:

e.Σ{ first v ↦ seed(v) ; a v ↦ ⊕(a,v) }

The seeded form has no result on an empty input. For an ordered list input, the seed is the first list element. For unordered input, the seed choice is arbitrary, so the result must not depend on which element is chosen as the seed.

Named fold declarations

A component may introduce a reusable named fold with a top-level fold declaration:

fold ResultType name<GenericParams> where constraints =
    Σ{ initial ; accumulator element ↦ step };

The declaration name is written without the leading Σ. Applying the fold uses the name after Σ, as in E.Σname. A qualified application may put a component name or component alias before the fold name, as in E.Σstats.count, when disambiguation is needed. A fold declaration may also declare ordinary parameters after its generic parameter list:

fold ResultType name<GenericParams>(ParameterType parameter, ...) where constraints =
    Σ{ initial ; accumulator element ↦ step };

The folded input is still the observed unary extension on the left-hand side of the fold application. Ordinary parameters are additional scalar values supplied by the call site:

E.Σname(argument, ...)
E.Σname<ExplicitGenericArgs>(argument, ...)

Each argument is typed in the caller's context and must be assignable to the corresponding parameter type after generic instantiation. Inside the declaration body, the parameter names are ordinary local value names. They are distinct from the fold element and accumulator binders, and ordinary lexical scoping applies inside nested expressions.

A named fold may also be declared directly in terms of the whole observed input extension. The over binder introduces a local name for the extension being folded:

fold ResultType name<GenericParams>(params...) over input where constraints =
    expression;

Inside the declaration body, input denotes the same observed extension that appears on the left-hand side of the fold application. Ordinary parameters, if present, are also in scope in the body expression. The input may be folded again, filtered, or used in ordinary extension-valued expressions. This form is useful for folds defined from other folds, such as mean, which is sum / count, and for parameterized folds such as a shifted mean:

fold Real shiftedMean<Type T>(Real offset) over input where T isa Real =
    input.Σmean + offset;

items.ΣshiftedMean(2.5)

A fold parameter list may be empty or absent. When a parameter list is present, a fold application must supply the same number of ordinary arguments. The over binder name must not collide with an ordinary parameter name.

If a fold is only defined for some inputs, the declaration may include a defined where guard after the body expression:

fold Real mean<Type T> over input where T isa Real =
    input.Σsum / input.Σcount
    defined where input.Σcount > 0;

When the guard is false, the fold has no result for that input. For example, Σmean, Σmin, and Σmax have no result on an empty input.

The generic constraint ordered(T) requires the type argument T to have a standard order, as defined by the ordering rules for nominal and structural types.

Fold declarations belong to their declaring component, not to a single global fold namespace. A component may declare any local fold name, including a name also used by std or by another component. Name clashes are handled at reference sites: use the unqualified form for standard folds and unambiguous local folds, and use qualification or aliases for clashing third-party folds.

using vendor.Stats as stats;

items.Σmedian       // valid only if a visible declaration named median exists
items.Σstats.median // vendor.Stats.median, if that component declares it

The standard library folds are ordinary declarations in the component std. For example:

// Cardinality folds
fold Integer count<Type T> =
    Σ{ 0 ; n v ↦ n + 1 };

fold Boolean exists<Type T> =
    Σ{ false ; found v ↦ true };

fold Boolean empty<Type T> =
    Σ{ true ; empty v ↦ false };

// Boolean folds
fold Boolean all =
    Σ{ true ; result v ↦ result ∧ v };

fold Boolean any =
    Σ{ false ; result v ↦ result ∨ v };

// Numeric folds
fold T sum<Type T> where T isa Real =
    Σ{ 0 ; total v ↦ total + v };

fold T product<Type T> where T isa Real =
    Σ{ 1 ; total v ↦ total * v };

fold Real mean<Type T> over input where T isa Real =
    input.Σsum / input.Σcount
    defined where input.Σcount > 0;

fold Real variance<Type T> over input where T isa Real =
    ((input - input.Σmean)^2).Σmean
    defined where input.Σcount > 0;

fold Real stddev<Type T> over input where T isa Real =
    sqrt(input.Σvariance)
    defined where input.Σcount > 0;

// Ordered folds
fold T min<Type T> where ordered(T) =
    Σ{ first v ↦ v ; best v ↦ if v < best then v else best };

fold T max<Type T> where ordered(T) =
    Σ{ first v ↦ v ; best v ↦ if best < v then v else best };

// Ordered-input folds
fold String concat =
    Σ{ "" ; text v ↦ text + v };

The standard cardinality folds satisfy the following laws for finite inputs:

items.Σexists = (items.Σcount > 0)
items.Σempty  = (items.Σcount = 0)
items.Σexists = not items.Σempty

These equations are laws, not definitions. Σexists and Σempty are defined directly so an implementation can recognise their logical meaning and avoid counting every value when that is not needed.

For folds over unordered sets, the combining function must be associative and order-insensitive to ensure a well-defined result. Folds over an explicitly ordered list may use an order-sensitive combining function.