SINGLETON, UNION AND INTERSECTION TYPES FOR PROGRAM EXTRACTION

Two type theories, ATT and ATTT, are introduced. ATT is an impredicative type theory closely related to the polymorphic type theory of implicit typing of MacQueen et al. [MPS86]. ATTT is another version of ATT that extends the Girard-Reynolds second order lambda calculus. ATT has notions of intersection, union and singleton types. ATTT has a notion of refinement types as in the type system for ML by Freeman and Pfenning [FP91], plus intersection and union of refinement types and singleton refinement types. We will show how singleton, union and intersection types serve for development of programs without unnecessary codes via a variant of the Curry-Howard isomorphism. More exactly, they give a way to write types as specifications of programs without unnecessary codes which is inevitable in the usual Curry-Howard isomorphism.