Subtyping and intersection types revisited

ABSTRACT

Church's system of simple types has proven to be remarkably robust: call-by-name, call-by-need, and call-by-value languages, with or without effects, and even logical frameworks can be based on the same typing rules. When type systems become more expressive, this unity fractures. An early example is the value restriction for parametric polymorphism which is necessary for ML but not Haskell; a later manifestation is the lack of distributivity of function types over intersections in call-by-value languages with effects.

In this talk we reexamine the logical justification for systems of subtyping and intersection types and then explore the consequences in two different settings: logical frameworks and functional programming.

In logical frameworks functions are pure and their definitions observable, but complications could arise from the presence of dependent types. We show that this is not the case, and that we can obtain soundness and completeness theorems for a certain axiomatization of subtyping. We also sketch a connection to the type-theoretic notion of proof irrelevance.

In functional programming we investigate how the encapsulation of effects in monads interacts with subtyping and intersection types, providing an updated analysis of the value restriction and related phenomena. While at present this study is far from complete, we believe that its origin in purely logical notions will give rise to a uniform theory that can easily be adapted to specific languages and their operational interpretations.

REFERENCES

• 1: Rowan Davies , Frank Pfenning, Intersection types and computational effects, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.198-208, September 2000
• 2: William Lovas and Frank Pfenning. A bidirectional refinement type system for LF. In B. Pientka and C. Schürmann, editors, Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 11--25, Bremen, Germany, July 2007.
• 3: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 4: Noam Zeilberger. On the unity of duality. Annals of Pure and Applied Logic, 2007. To appear in a special issue on "Classical Logic and Computation".

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

General Terms:
Languages, Theory, Verification