Computing free variables of a term generically. Different queries can be specialized to the appropriate short-circuiting behavior and to only pass around the necessary data. A query can be written as an instance to the ComputeFree class which bundles all parameters of the generic traversal. The traversal itself is defined in the instance of the Free class. See Agda.TypeChecking.Free for examples of queries.

Background notes:

The distinction between rigid and strongly rigid occurrences comes from: Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)

The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly in t. It might have a solution if the occurrence is not strongly rigid, e.g.

x = f -> suc (f (x ( y -> k))) has x = f -> suc (f (suc k))

Jason C. Reed, PhD thesis, page 106

Under coinductive constructors, occurrences are never strongly rigid. Also, function types and lambdas do not establish strong rigidity. Only inductive constructors do so. (See issue 1271).

For further reading on semirings and semimodules for variable occurrence, see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016). There, he treats the "quantity" dimension of variable occurrences.

The semiring has an additive operation for combining occurrences of subterms, and a multiplicative operation of representing function composition. E.g. if variable x appears o in term u, but u appears in context q in term t then occurrence of variable x coming from u is accounted for as q o in t.

Consider the example (λ{ x → (x,x)}) y:

• Variable x occurs once unguarded in x.
• It occurs twice unguarded in the aggregation x x
• Inductive constructor , turns this into two strictly rigid occurrences.

If , is a record constructor, then we stay unguarded.

• The function ({λ x → (x,x)}) provides a context for variable y. This context can be described as weakly rigid with quantity two.
• The final occurrence of y is obtained as composing the context with the occurrence of y in itself (which is the unit for composition). Thus, y occurs weakly rigid with quantity two.

It is not a given that the context can be described in the same way as the variable occurrence. However, for the purpose of quantity it is the case and we obtain a semiring of occurrences with 0, 1, and even ω, which is an absorptive element for addition.