{'fraction_non_alphanumeric': 0.0410958904109589, 'fraction_numerical': 0.020021074815595362, 'mean_word_length': 4.864197530864198, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Linear Rank Intersection Types

Intersection type systems [2] characterize termination, in the sense that a λ-term is stronglynormalizable if and only if it is typable in an intersection type system. Thus, typability is undecidable for these systems. To get around this, some current intersection type systems are restricted to types of finite rank [4, 8, 9, 12], using a notion of rank first defined by Daniel Leivant in [11]. This restriction makes type inference decidable [9]. Despite using finite-rank intersection types, these systems are still very powerful and useful. For instance, rank 2 intersection type systems [4, 8, 12] are more powerful, in the sense that they can type strictly more terms, than popular systems like the ML type system. Intersections arise in different systems in different scopes. Here we follow several previous presentations where intersections are only allowed in the left-hand side of arrow types [2, 3, 8, 13].