This paper proves undecidability of type checking
and type inference problems in some variants of
typed lambda calculi with polymorphic and existential
types. First, type inference in the domain-free
polymorphic lambda calculus is proved to be undecidable,
and then it is proved that type inference is
undecidable in the negation, conjunction, and existence
fragment of the domain-free typed lambda calculus.
Secondly, their variants with multiple quantifier
rules are introduced, and their type checking and
type inference are proved to be undecidable. Finally,
it is proved that we can reduce undecidability of type
checking and type inference problems in the Currystyle
lambda calculus in negation, conjunction, and
existential fragment to undecidability of those problems
in another variant of the domain-free polymorphic
lambda calculus.
Cite as: Nakazawa, K. and Tatsuta, M. (2009). Type Checking and Inference for Polymorphic and Existential Types. In Proc. Fifteenth Computing: The Australasian Theory Symposium (CATS 2009), Wellington, New Zealand. CRPIT, 94. Downey, R. and Manyem, P., Eds. ACS. 61-69.
(from crpit.com)
(local if available)