Linear Rank Intersection Types
F\'abio Reis, Sandra Alves, M\'ario Florido

TL;DR
This paper introduces a new rank concept for non-idempotent intersection types, developing a type system and inference algorithm that provide quantitative resource usage information for lambda calculus programs.
Contribution
It proposes a novel rank notion and extends the type system and inference algorithm to infer resource-related quantitative properties.
Findings
Defined a new rank 2 for non-idempotent intersection types
Developed a type inference algorithm based on the new rank
Extended the system to infer resource usage information
Abstract
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the lambda-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
