42
views
0
recommends
+1 Recommend
0 collections
    4
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Elaborating Intersection and Union Types

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections, which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast, unrestricted intersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and implementation. We describe a foundation for compiling unrestricted intersection and union types: an elaboration type system that generates ordinary lambda-calculus terms. The key feature is a Forsythe-like merge construct. With this construct, not all reductions of the source program preserve types; however, we prove that ordinary call-by-value evaluation of the elaborated program corresponds to a type-preserving evaluation of the source program. We also describe a prototype implementation and applications of unrestricted intersections and unions: records, operator overloading, and simulating dynamic typing.

          Related collections

          Most cited references 18

          • Record: found
          • Abstract: not found
          • Article: not found

          Local type inference

            Bookmark
            • Record: found
            • Abstract: not found
            • Conference Proceedings: not found

            How to make ad-hoc polymorphism less ad hoc

             S Blott,  P. Wadler (1989)
              Bookmark
              • Record: found
              • Abstract: not found
              • Conference Proceedings: not found

              Refinement types for ML

                Bookmark

                Author and article information

                Journal
                23 June 2012
                Article
                10.1017/S0956796813000270
                1206.5386

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                Custom metadata
                13 pages, 12 figures, to appear in International Conference on Functional Programming (ICFP) 2012
                cs.PL

                Comments

                Comment on this article