The Inhabitation Problem for Low-Rank Type Systems

Types are an important abstraction in programming languages. They enable to program in a safer way and avoid bugs setting restriction on programs and distinguishing correct and incorrect ones. Type theory is the mathematical apparatus for this domain, one of whose basic questions is the inhabitation, usually defined as follows: «does there exist a term (some expression in the language) of a given type?». The question could be raised in different type systems (models of type-related programming languages parts), the goal of this project is to solve this question in some specific systems. Namely, simply typed lambda calculus with type intersection of rank two (type system restriction) and subtyping. Recently presented works show that the problem is undecidable in type systems without rank limitation and EXPSPACE-complete without subtyping, but the system with both of them is not studied yet. The approaches include an adaptation of an existing in similar type systems inhabitation algorithm, proof of its correctness and soundness, implementing and testing the algorithm in Haskell programming language. The preliminary results also cover several flaws in the previous works and suggest that the inhabitation algorithm scheme could be improved in terms of efficiency.