Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types

This paper shows that type-checking and type-inference problems are equivalent in domain-free lambda calculi with existential types, that is, type-checking problem is Turing reducible to typeinference problem and vice versa. In this paper, the equivalence is proved for two variants of domain-free lambda calculi with existential types: one is an implication and existence fragment, and the other is a negation, conjunction and existence fragment. This result gives another proof of undecidability of type inference in the domain-free calculi with existence. Keywords. undecidability, existential type, type checking, type inference, domain-free type system.

• Type: Conference
• Year: 2009
• Where: WFLP
• Authors: Yuki Kato, Koji Nakazawa
• Keywords: Algorithms, Domain-free Lambda Calculi, Existence Fragment, Existential Type, WFLP 2009