一句话：为带维度界的交类型演算建立主类型性的代数与算法理论，并实现无需 β-归约的近似范式计算。
本文针对近期提出的带维度界交类型演算，建立主类型性（principality）的代数与算法理论。该理论支持在维度界下推断主类型信息，并借助抽象向量空间（更准确地说是半模）的可计算基，给出经典主类型的近似理论，同时揭示维度演算与 approximants 理论的系统联系。作者证明：有限可计算基在维数足够高时张成给定项的经典主类型，从而用类型推断近似标准主类型，并在维数参数足够大时精确刻画之。副产品包括交类型的主居留性可判定（给定类型，是否存在以其为主类型的范式）。结合有界类型推断与主居留性，可在不使用 β-归约的情况下计算任意项的近似范式。
We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides an algebraic and algorithmic theory of approximation of classical principal types in terms of computable bases of abstract vector spaces (more precisely, semimodules), and it shows a systematic connection of dimensional calculi to the theory of approximants. Finite, computable bases are shown to span standard principal typings of a given term for sufficiently high dimension, thereby providing an approximation to standard principality by type inference, and capturing it precisely for sufficiently large dimensional parameter. Subsidiary results include decidability of principal inhabitation for intersection types (given a type does there exist a normal form for which the type is principal?). Remarkably, combining bounded type inference with principal inhabitation allows us to compute approximate normal forms of arbitrary terms without using beta-reduction.
@article{paperbot689,
title = {Principality and approximation under dimensional bound},
author = {Andrej Dudenhefner and Jakob Rehof},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290321}
}