arXiv:2611.17127 · v1

Graded Intersection Types

分级交集类型

首次提交 2026-11-13 01:20

版本更新 2026-11-13 01:20

雷达观测 2026-11-13 14:15

摘要

We introduce graded intersection types, in which arrow domains are multisets of types with coefficients in a semiring. Boolean and natural number grades recover idempotent and non-idempotent intersection types. We give algebraic conditions on the semiring for subject reduction and expansion in finite systems and in locally finite systems with guarded infinite types. We construct a lifting to multisets of grades corresponding, in this general setting, to lifting the idempotent system to the non-idempotent one. We recall the main existing operational characterisations from the literature, and show some general extensions.