一句话：提出 PITS 演算族：以统一语法兼顾项与类型、支持无限制一般递归，并通过 iso-types 与显式 cast 保持类型检查可判定。
传统函数式语言（如 Haskell、ML）为项和类型设置分离语法，而依赖类型语言多采用统一语法，但统一语法下引入无限制一般递归时，只要存在类型层计算，就很容易丧失类型检查可判定性等性质。本文提出纯同构类型系统（PITS）演算族，其简洁程度与纯类型系统（PTS）相当，可作为介于 ML 风格语言与完整依赖类型语言之间的语言基础。PITS 完全允许递归与递归类型，类型相等仅基于 alpha 等价，同时借助统一语法自然支持诸多高级类型特性。它用 iso-types（iso-递归类型的推广）取代依赖类型演算中的转换规则，通过 cast 算子使类型层计算显式化，从而避免其他 cast 方案中显式相等证明的复杂性。作者研究了对应三种 cast 归约策略的变体：call-by-name、call-by-value 与并行归约。关键发现是：前两者虽损失部分表达力，却拥有简单直接的操作语义与证明；并行归约变体保留了 PTS 转换的表达力，代价是元理论更复杂。
Abstract Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, and added expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level of type-level computation is present, since properties such as decidable type-checking are easily lost. This paper presents a family of calculi called pure iso-type systems (PITSs), which employs unified syntax, supports general recursion and preserves decidable type-checking. PITS is comparable in simplicity to pure type systems (PTSs), and is useful to serve as a foundation for functional languages that stand in-between traditional ML-like languages and fully blown dependently typed languages. In PITS, recursion and recursive types are completely unrestricted and type equality is simply based on alpha-equality, just like traditional ML-style languages. However, like most dependently typed languages, PITS uses unified syntax, naturally supporting many advanced type system features. Instead of implicit type conversion, PITS provides a generalization of iso-recursive types called iso-types . Iso-types replace the conversion rule typically used in dependently typed calculus and make every type-level computation explicit via cast operators. Iso-types avoid the complexity of explicit equality proofs employed in other approaches with casts. We study three variants of PITS that differ on the reduction strategy employed by the cast operators: call-by-name , call-by-value and parallel reduction . One key finding is that while using call-by-value or call-by-name reduction in casts loses some expressive power, it allows those variants of PITS to have simple and direct operational semantics and proofs. In contrast, the variant of PITS with parallel reduction retains the expressive power of PTS conversion, at the cost of a more complex metatheory.