Higher-order intensional type analysis

Abstract. Languages for intensional type analysis permit ad-hoc polymorphism, or run-time analysis of types. However, such languages require complex, specialized constructs to support this operation, which hinder optimization and complicate the meta-theory of these languages. In this paper, we observe that such specialized operators need not be intrinsic to the language, and in fact, their operation may be simulated through standard encodings of iteration in the polymorphic lambda calculus. Therefore, we may more easily add intensional analysis operators to complicated languages via translation, instead of language extension.