Structured recursion schemes such as folds and unfolds have been widely used for structuring both functional programs and program semantics. In this context, it has been customary to implement denotational semantics as folds over an inductive data type to ensure termination and compositionality. Separately, operational models can be given by unfolds, and naturally not all operational models coincide with a given denotational semantics in a meaningful way. To ensure these semantics are coherent it is important to consider the property of full abstraction which relates the denotational and the operational model. In this paper, we show how to engineer a compositional semantics such that full abstraction comes for free. We do this by using distributive laws from which we generate both the operational and the denotational model. The distributive laws ensure the semantics are fully abstract at the type level, thus relieving the programmer from the burden of the proofs.

翻译：诸如折叠与展开等结构化递归方案已被广泛用于构建函数式程序和程序语义。在此背景下，通常将指称语义实现为归纳数据类型上的折叠，以确保终止性和组合性。另一方面，操作模型可由展开给出，但并非所有操作模型都能以有意义的方式与给定的指称语义保持一致。为确保这些语义的连贯性，必须考虑将指称模型与操作模型相关联的完全抽象属性。本文展示如何设计一种组合语义，使得完全抽象能够自动实现。我们通过使用分配律来生成操作模型和指称模型，这些分配律能够在类型层级确保语义的完全抽象，从而减轻程序员进行证明的负担。