Computing the free variables of a term lazily.
We implement a reduce (traversal into monoid) over internal syntax
for a generic collection (monoid with singletons). This should allow
a more efficient test for the presence of a particular variable.
Worst-case complexity does not change (i.e. the case when a variable
does not occur), but best case-complexity does matter. For instance,
see Agda.TypeChecking.Substitute.mkAbs: each time we construct
a dependent function type, we check whether it is actually dependent.
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 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 quantity it is the case
and we obtain a semiring of occurrences with 0, 1, and even ω, which
is an absorptive element for addition.