7.4. Well-formedness

{A mode is well formed if

the elaboration of an actual-declarer specifying that mode is a finite action (i.e., any value of that mode can be stored in a finite memory) and
it is not strongly coercible from itself (since this would lead to ambiguities in coercion).

}

7.4.1. Syntax

a) WHETHER (NOTION) shields SAFE to SAFE{73c } : where (NOTION) is (PLAIN) or (NOTION) is (FLEXETY ROWS of) or (NOTION) is (union of) or (NOTION) is (void), WHETHER true.

b) WHETHER (PREF) shields SAFE to yin SAFE{73c } : WHETHER true.

c) WHETHER (structured with) shields SAFE to yang SAFE{73c } : WHETHER true.

d) WHETHER (procedure with) shields SAFE to yin yang SAFE{73c } : WHETHER true. {As a by-product of mode equivalencing, modes are tested for well-formedness {7.3.1.c }. All nonrecursive modes are well formed. For recursive modes, it is necessary that each cycle in each spelling of that mode (from 'MU definition of MODE' to 'MU application') passes through at least one 'HEAD' which is yin, ensuring condition (i) and one (possibly the same) 'HEAD' which is yang, ensuring condition (ii). Yin 'HEAD's are 'PREF' and 'procedure with'. Yang 'HEAD's are 'structured with' and 'procedure with'. The other 'HEAD's, including 'FLEXETY ROWS of' and 'union of', are neither yin nor yang. This means that the modes specified by A, B and C in

MODE A = STRUCT(INT n, REF A next), B = STRUCT(PROC B next), C = PROC(C)C

are all well formed. However, MODE D = [1 : 10] D, E = UNION(INT, E) is not a mode-declaration.}

{Tao produced the one. The one produced the two. The two produced the three. And the three produced the ten thousand things. The ten thousand things carry the yin and embrace the yang, and through the blending of the material force they achieve harmony. Tao-te Ching, 42, Lao Tzu.}