Controlling Copatterns: There and Back Again

Deriving Semantics for Compositional Copatterns

The LaTeX source files for the article can be found in paper/.

Executable Racket versions of the examples (given in sections 1 and 2) can be found in ex/, along with the copattern-matching library composable.rkt. The same code can be run on another R6RS-compliant Scheme implementation (e.g., Chez Scheme) using [https://github.com/pdownen/CoScheme].

The step-by-step derivation of semantic artifacts in terms of Haskell program transformations can be found in the src/ directory. To follow along in the order of the paper, consider visiting the modules in this order:

1. (Section 3) Copattern.Block.Subst: Starting from a substitution-based reduction function and search algorithm for Copattern.Block.Syntax, derive a small-step operational semantics, abstract machine, and continuation-passing style (CPS) embedding.

   1. Copattern.Block.Subst.Reduce: The definitional reduction function for turning a (potential) Redex into a (potential) Reduct and Followup question. The reduction function is transformed as follows:

      1. Copattern.Block.Subst.Reduce.Direct: The direct-style reduction function.

      2. Copattern.Block.Subst.Reduce.CPS: CPS transformation of the direct reduction function.

      3. Copattern.Block.Subst.Reduce.Defunc: Defunctionalization of the CPS.

      4. Copattern.Block.Subst.Reduce.EnvCxt: Isomorphic change of representation, replacing the evaluation contexts generated by defunctionalization with an equivalent environment.

      5. Copattern.Block.Subst.Reduce.Reverse: Allowing a reversal of binding order for order-irrelevant environments (guaranteed for well-formed copatterns that bind distinct variable names).

      6. Copattern.Block.Subst.Reduce.Corridor: Compression of corridor transitions to short-cut known reduction paths.

   2. Copattern.Block.Subst.Search: The search function that identifies the next Redex and surrounding Question in a Term.

      1. Copattern.Block.Subst.Search.Direct: The direct style search function.

      2. Copattern.Block.Subst.Search.CPS: CPS transformation of the direct reduction function.

      3. Copattern.Block.Subst.Search.Defunc: Defunctionalization of the CPS.

      4. Copattern.Block.Subst.Search.EvalQuestion: Isomorphic change of representation, replacing the evaluation contexts generated by defunctionalization with an equivalent Question.

      5. Copattern.Block.Subst.Search.QuestionMonoid: Optimize the search function using the known monoid laws on Questions.

      6. Copattern.Block.Subst.Search.Corridor: Compression of corridor transitions to short-cut known reduction paths.

   3. Copattern.Block.Subst.Decomp: The decomposition, recomposition, and refocusing functions derived from search.

   4. Copattern.Block.Subst.SmallStep: The small-step reduction-based interpreter.

      1. Copattern.Block.Subst.Step.Small: The direct-style small-step interpreter loop.

      2. Copattern.Block.Subst.Step.Refocus: The refocusing optimization of the small-step interpreter.

      3. Copattern.Block.Subst.Step.Fuse: Loop fusion of the main interpreter loop with refocusing and reduction.

      4. Copattern.Block.Subst.Step.Corridor: Compression of corridor transitions to short-cut known reduction paths in the fused interpreter.

      5. Copattern.Block.Subst.Step.Deforest: Eliminate intermediate data structures that are no longer necessary in the compressed interpreter.

      6. Copattern.Block.Subst.Step.Subst: Immediately substitute when a binding becomes available in the deforested interpreter.

   5. Copattern.Block.Subst.Machine: The tail-recursive, abstract machine interpreter.

      1. Copattern.Block.Subst.Machine.Shallow: Break nested pattern-matching into flat patterns.

      2. Copattern.Block.Subst.Machine.Case: Desugar simultaneous pattern-matching on multiple values to sequential case analysis on a single value.

      3. Copattern.Block.Subst.Machine.Eta: Eta reduction.

      4. Copattern.Block.Subst.Machine.Denote: Convert to a "denotational" form, where transition functions are applied to sub-expressions as soon as they become available to the recursive interpreter.

   6. Copattern.Block.Subst.CPS: The CPS translation embedding the Copattern.Block.Sytnax into native Haskell functions.

2. (Section 5) Copattern.Nest.Subst: Copattern.Block.Subst: Starting from a continuation-passing style embedding for Copattern.Block.Syntax, derive an abstract machine and small-step operational semantics.

   1. Copattern.Nest.Subst.CPS: The CPS translation embedding the Copattern.Nest.Syntax into native Haskell functions.

      1. Copattern.Nest.Subst.CPS.Direct: The CPS embedding with some direct-style function composition of terms applied to responses.

      2. Copattern.Nest.Subst.CPS.Double: A second layer of CPS transformation of the above, generating a fully CPS embedding with another "meta-continuation" guiding application of terms to responses.

      3. Copattern.Nest.Subst.CPS.Defunc: Defunctionalization of the meta-continuations in the fully CPS embedding.

      4. Copattern.Nest.Subst.CPS.Syntactic: Delay application of the translation functions as late as possible, preserving the original syntax until right before the denotations would be applied.

      5. Copattern.Nest.Subst.CPS.Inline: Inline the relationship between variables as names versus variables as holding the substituted CPS denotations of expressions.

      6. Copattern.Nest.Subst.CPS.Fuse: Fuse the inlining of denotation substitution with the translation function.

      7. Copattern.Nest.Subst.CPS.Eta: Eta expansion.

      8. Copattern.Nest.Subst.CPS.Match: Compress multiple levels of case analysis into nested pattern matching.

   2. Copattern.Nest.Subst.Machine: The tail-recursive abstract machine interpreter derived from the CPS embedding.

      1. Copattern.Nest.Subst.Machine.CoCase: A reorganization of the machine, labeling each step as either "refocusing" (perfectly reversible, no information is lost), "reduction" (information loss due to reduction, loop continues), or "terminal" (loop ends, Answer is returned).

      2. Copattern.Nest.Subst.Machine.Reduced: An extraction of the non-recursive reduction function by defusing reduction steps from the main loop.

      3. Copattern.Nest.Subst.Machine.Refocused: An extraction of the independently self-recursive refocusing function by defusing refocusing steps from the main loop.

      4. Copattern.Nest.Subst.Machine.Recomp: A reversal of the refocusing optimization by recomposing after each step.

      5. Copattern.Nest.Subst.Machine.Small: The small-step interpreter loop.

   3. Copattern.Nest.Subst.Reduce: The non-recursive reduction function extracted from the abstract machine.

   4. Copattern.Nest.Subst.Decomp: The decomposition / refocusing functions extracted from the machine.

   5. Copattern.Nest.Subst.SmallStep: The small-step interpreter loop derived from the abstract machine.

3. (Appendix A.1) Copattern.Block.Env: Starting from an environment-based reduction function and search algorithm for Copattern.Nest.Syntax, derive a small-step operational semantics, abstract machine, and continuation-passing style (CPS) embedding.

   Follow a similar path as Copattern.Block.Subst.

   1. Copattern.Block.Subst.Reduce: The definitional reduction function for turning a (potential) Redex into a (potential) Reduct and Followup question. The reduction function is transformed as follows:

      1. Copattern.Block.Subst.Reduce.Direct: The direct-style reduction function.

      2. Copattern.Block.Subst.Reduce.CPS: CPS transformation of the direct reduction function.

      3. Copattern.Block.Subst.Reduce.Defunc: Defunctionalization of the CPS.

      4. Copattern.Block.Subst.Reduce.EnvCxt: Isomorphic change of representation, replacing the evaluation contexts generated by defunctionalization with an equivalent environment.

      5. Copattern.Block.Subst.Reduce.Reverse: Allowing a reversal of binding order for order-irrelevant environments (guaranteed for well-formed copatterns that bind distinct variable names).

      6. Copattern.Block.Subst.Reduce.Corridor: Compression of corridor transitions to short-cut known reduction paths.

   2. Copattern.Block.Subst.Decomp: The decomposition, recomposition, and refocusing functions. Note that since search is not impacted by environments, we skip the identical the derivation.

   3. Copattern.Block.Subst.SmallStep: The small-step reduction-based interpreter, already in refocusing form.

      1. Copattern.Block.Subst.Step.Small: The direct-style small-step interpreter loop.

      2. Copattern.Block.Subst.Step.Fuse: Loop fusion of the main interpreter loop with refocusing and reduction.

      3. Copattern.Block.Subst.Step.Corridor: Compression of corridor transitions to short-cut known reduction paths in the fused interpreter.

      4. Copattern.Block.Subst.Step.Deforest: Eliminate intermediate data structures that are no longer necessary in the compressed interpreter.

   4. Copattern.Block.Subst.Machine: The tail-recursive, abstract machine interpreter.

      1. Copattern.Block.Subst.Machine.Shallow: Break nested pattern-matching into flat patterns.

      2. Copattern.Block.Subst.Machine.Case: Desugar simultaneous pattern-matching on multiple values to sequential case analysis on a single value.

      3. Copattern.Block.Subst.Machine.Eta: Eta reduction.

      4. Copattern.Block.Subst.Machine.Denote: Convert to a "denotational" form, where transition functions are applied to sub-expressions as soon as they become available to the recursive interpreter.

      5. Copattern.Block.Subst.Machine.Bind: Merge separate environments (the "old" one inherited from surrounding scope and the "new" one created by copattern matching) by binding directly on top of the surrounding environment.

   5. Copattern.Block.Subst.CPS: The CPS translation embedding Copattern.Block.Syntax into native Haskell functions.

4. (Appendix A.2) Copattern.Nest.Env: Starting from a continuation-passing style embedding for Copattern.Nest.Syntax, derive an abstract machine.

   Follow a similar path as Copattern.Nest.Subst up to the tail-recursive, abstract machine interpreter.

   1. Copattern.Nest.Subst.CPS: The CPS translation embedding the Copattern.Nest.Syntax into native Haskell functions.

      1. Copattern.Nest.Subst.CPS.Direct: The CPS embedding with some direct-style function composition of terms applied to responses.

      2. Copattern.Nest.Subst.CPS.Double: A second layer of CPS transformation of the above, generating a fully CPS embedding with another "meta-continuation" guiding application of terms to responses.

      3. Copattern.Nest.Subst.CPS.Defunc: Defunctionalization of the meta-continuations in the fully CPS embedding.

      4. Copattern.Nest.Subst.CPS.Syntactic: Delay application of the translation functions as late as possible, preserving the original syntax until right before the denotations would be applied.

      5. Copattern.Nest.Subst.CPS.Eta: Eta expansion.

      6. Copattern.Nest.Subst.CPS.Match: Compress multiple levels of case analysis into nested pattern matching.

   2. Copattern.Nest.Subst.Machine: The tail-recursive abstract machine interpreter derived from the CPS embedding.