一句话：提出用模态标注函数类型，在依赖类型论中为关系参数性提供类型级保证，从而安全省略证明。
依赖类型论允许我们在同一语言中编写程序并证明其性质。然而，有些性质无需大量证明，因为它们从程序实现中即可看出：例如，多态程序若不是特设多态而是关系参数性的，便可免费获得 parametricity 定理。若要安全地依赖这种显然的良好行为来走捷径省略证明，就需要在类型层面保证程序确实表现良好。本文通过用模态标注函数类型，描述函数的行为，从而在类型系统中编码相关程度/关系行为，为依赖类型论中的参数性推理提供类型级保证。
Dependent type theory allows us to write programs and to prove properties about those programs in the same language. However, some properties do not require much proof, as they are evident from a program's implementation, e.g. if a polymorphic program is not ad hoc but relationally parametric, then we get parametricity theorems for free. If we want to safely shortcut proofs by relying on the evident good behaviour of a program, then we need a type-level guarantee that the program is indeed well-behaved. This can be achieved by annotating function types with a modality describing the behaviour of functions.