Although systems with intersection types have many unique capabilities, there has never been a fully satisfactory explicitly typed system with intersection types. We introduce ?B with branching types and types which are quantified over type selectors to provide an explicitly typed system with the same expressiveness as a system with intersection types. Typing derivations in ?B effectively squash together what would be separate parallel derivations in earlier systems with intersection types.
['J. B. Wells', 'C. Haack']
Branching Types