ch:modal-effect-types: ch:modal-effect-types

Problem, result, and invariant. Build a finite observation model for the distinction between absolute effect replacement and relative extension, then represent one row arrow and one capability block as source data. The result is the eight-line report in subsubappendix E.3.8. Maintain two invariants: row translation keeps every label occurrence, and the capability call substitutes the actual effect for the block’s explicit formal effect variable.

Representation. Use a nominal Label datatype and lists for finite contexts. Define Modality with Absolute and Extend constructors. The action of the first returns its stored list; the action of the second prepends its stored list to the ambient list. Keep RowArrow, CapabilityBlock, ModalArrow, and ModalBlock distinct, so a source card cannot be accepted by the wrong translation.

Modal actions first. Use ambient context [Write] and modality payload [Ask]. Absolute action must return [Ask]; extension must return [Ask, Write]. Composition is left to right. Test an absolute [Write] followed by extension [Ask]; the result is the absolute context [Ask, Write], independent of the original ambient list.

The two source translations. Translate the row [Ask, Ask] without normalization. The target arrow stores an absolute modality carrying both occurrences. Translate a capability block by retaining its formal effect variable in the target block and using an extension modality around the block body. Instantiate that formal with [Write] at a call, and require the result to be exactly [Write].

Modal elimination. The finite check compares the context produced by a box’s modality with the context at its elimination site. An absolute [Ask] box introduced over [Write] eliminates at [Ask] and is rejected at [Ask, Write]. This is only a finite analogue of lock compatibility; it is not a type checker for Met.

Three failing versions. Replay each mutation independently:

1. make Absolute prepend its payload to the ambient list;

2. replace the translated duplicate row by the singleton [Ask]; and

3. make capability instantiation return the empty list.

Each mutant remains well typed in Kappa. Require its frozen inline test and run-time acceptance guard to fail, then restore the accepted source before testing the next mutant.

Acceptance test. Run the four commands in subsubappendix E.3.8. Require eight named PASS lines, the final line

All 8 Chapter 33 corpus cases passed.

and audit output []. Then replay the three mutations and restore the accepted corpus digest.

Mathematical boundary. The model checks finite list calculations and constructor-sensitive translations. It proves none of target safety, row-to-Met preservation, capability-to-Met preservation, operational simulation, full abstraction, or source equivalence.