Orthologic Type Systems

TL;DR

This paper introduces a novel type system based on orthologic, enabling intersection, union, and negation types with subtyping, along with algorithms for subtyping decision and type normalization.

Contribution

It extends orthologic to support monotonic and antimonotonic functions, and provides algorithms for subtyping and type normalization in such systems.

Findings

Decidable subtyping relation with O(n^2(1+m)) complexity.

Polynomial-time normalization algorithm for minimal canonical types.

Proof system for orthologic with function symbols admits partial cut elimination.

Abstract

We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to extend orthologic to support monotonic and antimonotonic functions, supporting the use of type constructors in such type systems. We present a proof system for orthologic with function symbols, showing that it admits partial cut elimination. Using these insights, we present an $\mathcal O(n^2(1+m))$ algorithm for deciding the subtyping relation under $m$ assumptions. We also show $O(n^2)$ polynomial-time normalization algorithm, allowing simplification of types to their minimal canonical form.