Galois Embedding from Polymorphic Types into Existential Types

摘要

We show that there exist bijective translations between polymorphic λ-calculus and a subsystem of minimal logic with existential types, which form a Galois connection and moreover a Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.