Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language concepts, to understand how programs behave and to reason about programs. At the same time it serves as a great theory to model various algebraic effects such as non-determinism, partial functions, side effects and numerous other forms of computation. In the present paper, we present a general framework to construct algebraic effects in domain theory, where our domains are DCPOs: directed complete partial orders. We first describe so called DCPO algebras for a signature, where the signature specifies the operations on the DCPO and the inequational theory they obey. This provides a method to represent various algebraic effects, like partiality. We then show that initial DCPO algebras exist by defining them as so called Quotient Inductive-Inductive Types (QIITs), known from homotopy type theory. A quotient inductive-inductive type allows one to simultaneously define an inductive type and an inductive relation on that type, together with equations on the type. We illustrate our approach by showing that several well-known constructions of DCPOs fit our framework: coalesced sums, smash products and free DCPOs (partiality and power domains). Our work makes use of various features of homotopy type theory and is formalized in Cubical Agda.

翻译：域理论已发展为一种计算数学理论，并为编程语言提供指称语义。它帮助我们确定语言概念的含义、理解程序行为并推理程序性质。同时，该理论也为建模各类代数效应提供了强大框架，例如非确定性、部分函数、副作用及多种其他计算形式。本文提出在域理论中构造代数效应的通用框架，其中域采用DCPO（有向完全偏序）结构。我们首先描述针对特定签名的DCPO代数，该签名规定了DCPO上的运算及其遵循的不等式理论。这为表示部分性等多种代数效应提供了方法。随后，我们通过将初始DCPO代数定义为商归纳-归纳类型（QIIT）——该概念源于同伦类型论——证明其存在性。商归纳-归纳类型允许同时定义归纳类型及其上的归纳关系，并附带类型上的等式约束。我们通过证明若干经典DCPO构造符合本框架来例证该方法：融合和、张量积与自由DCPO（部分性与幂域）。本研究运用了同伦类型论的多种特性，并在Cubical Agda中完成形式化验证。