Pure Subtype Systems Are Type-Safe
<|reference_start|>Pure Subtype Systems Are Type-Safe: We address the open problem of type safety in Hutchins' pure subtype systems (PSS). PSS (hereafter in the singular) harmoniously mixes terms and types, thus enabling a number of advanced language features that combine dependent types with higher-order subtyping. In PSS terms and types belong to the same kind (everything is a subtype) and the resulting theory is based on subtyping. Since PSS lacks strong normalisation, a type soundness result can only be stated in terms of type safety defined as progress and preservation. Proving type safety rests on the well-known problem of transitivity elimination in higher-order subtyping, where a key inversion lemma fails under the presence of intermediary steps in transitive subtype derivations. Despite his attempts, Hutchins failed to prove PSS type safety. We propose a reformulation of pure subtype systems with a more fine-grained notion of subtyping derivation that enables a direct proof of transitivity elimination, and thus of type safety. We also reformulate Hutchins' practical type-checking algorithm to our system and prove it correct.<|reference_end|>
@article{pasquale2024pure,
    title={Pure Subtype Systems Are Type-Safe},
    author={Valentin Pasquale, 'Alvaro Garc'ia-P'erez},
    journal={arXiv preprint arXiv:2407.13882},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.13882},
    primaryClass={cs.LO}
}