Extensional equivalence and singleton types

ABSTRACT

We study the &lamda;^ΠΣS_≤ calculus, which contains singleton types S(M) classifying terms of base type provably equivalent to the term M. The system includes dependent types for pairs and functions (Σ and Π) and a subtyping relation induced by regarding singletons as subtypes of the base type. The decidability of type checking for this language is non-obvious, since to type check we must be able to determine equivalence of well-formed terms. But in the presence of singleton types, the provability of an equivalence judgment Γ ⊢ M₁ &eqiv;M₂ : A can depend both on the typing context Γ and on the particular type A at which M₁ and M₂ are compared.We show how to prove decidability of term equivalence, hence of type checking, in &lamda;^ΠΣS_≤ by exhibiting a type-directed algorithm for directly computing normal forms. The correctness of normalization is shown using an unusual variant of Kripke logical relations organized around sets; rather than defining a logical equivalence relation, we work directly with (subsets of) the corresponding equivalence classes.We then provide a more efficient algorithm for checking type equivalence without constructing normal forms. We also show that type checking, subtyping, and all other judgments of the system are decidable.The &lamda;^ΠΣS_≤ calculus models type constructors and kinds in the intermediate language used by the TILT compiler for Standard ML to implement the SML module system. The decidability of &lamda;^ΠΣS_≤ term equivalence allows us to show decidability of type checking for TILT's intermediate language. We also obtain a consistency result that allows us to prove type safety for the intermediate language. The algorithms derived here form the core of the type checker used for internal type checking in TILT.

REFERENCES

• 1: David Aspinall, Subtyping with Singleton Types, Selected Papers from the 8th International Workshop on Computer Science Logic, p.1-15, September 25-30, 1994
• 2: Aspinall, D. 1997. Type systems for modular programs and specifications. Ph.D. dissertation, Department of Computer Science, University of Edinburgh.
• 3: David Aspinall, Subtyping with Power Types, Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, p.156-171, August 21-26, 2000
• 4: Matthias Blume, Hierarchical modulatory and intermodule optimization, Princeton University, Princeton, NJ, 1998
• 5: Matthias Blume , Andrew W. Appel, Lambda-splitting: a higher-order approach to cross-module optimizations, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.112-124, June 09-11, 1997, Amsterdam, The Netherlands
• 6: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 7: Adriana Compagnoni , Healfdene Goguen, Typed operational semantics for higher-order subtyping, Information and Computation, v.184 n.2, p.242-297, August 01, 2003 [doi>10.1016/S0890-5401(03)00062-2]
• 8: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 9: Coquand, T., Pollack, R., and Takeyama, M. 2003. A logical framework with dependently typed records. In Proceedings of the Typed Lambda Calculi and Applications (TLCA 2003). 105--119. (Available as LNCS 2701). Lecture Notes in Computer Science, vol. 2701, Springer-Verlag, New York.
• 10: Courant, J. 2002. Strong normalization with singleton types. In Proceedings of the Second Workshop on Intersection Types and Related Systems (ITRS '02). ENTCS, vol. 70.
• 11: Karl Crary, A simple proof technique for certain parametricity results, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.82-89, September 27-29, 1999, Paris, France
• 12: Crary, K. 2000. Sound and complete elimination of singleton kinds. Tech. Rep. CMU-CS-00-104, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.
• 13: Crary, K. 2005. Logical relations and a case study in equivalence checking. In Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Cambridge, MA.
• 14: Karl Fredrick Crary , Robert L. Constable, Type-theoretic methodology for practical programming languages, 1998
• 15: Pierre-Louis Curien , Giorgio Ghelli, Decidability and confluence of bhtop⩽ reduction in F⩽ , Information and Computation, v.109 n.1-2, p.57-114, Feb. 15/March 1994 [doi>10.1006/inco.1994.1014]
• 16: Girard, J. 1972. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Ph.D. dissertation, Université Paris 7.
• 17: Goguen, H. 1994. A typed operational semantics for type theory. Ph.D. dissertation, Department of Computer Science, University of Edinburgh. (Available as Technical Report ECS-LFCS-94-304).
• 18: Healfdene Goguen, A syntactic approach to eta equality in type theory, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.75-84, January 12-14, 2005, Long Beach, California, USA
• 19: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 20: Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
• 21: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 22: Harper, R. and Pfenning, F. 1999. On equivalence and canonical forms in the LF type theory. In Proceedings of the Workshop on Logical Frameworks and Meta-Languages. Extended version available as Tech. Rep. CMU-CS-99-159.
• 23: Hofmann, M. 1995. Extensional concepts in intensional type theory. Ph.D. dissertation, Edinburgh LFCS. (Available as Edinburgh LFCS Technical Report ECS-LFCS-95-327).
• 24: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 25: Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199476]
• 26: Lillibridge, M. 1997. Translucent Sums: A Foundation for Higher-Order Module Systems. Ph.D. dissertation, School of Computer Science, Carnegie Mellon University. (Available as Technical Report) CMU-CS-97-122.
• 27: Martin-Löf, P. 1984. Intuitionistic Type Theory. Bibliopolis-Napoli.
• 28: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 29: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From System F to Typed Assembly Language (Extended Version), Cornell University, Ithaca, NY, 1997
• 30: Petersen, L., Cheng, P., Harper, R., and Stone, C. 2000. Implementing the TILT internal language. Tech. Rep. CMU-CS-00-180, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.
• 31: Paula Severi , Erik Poll, Pure Type Systems with Definitions, Proceedings of the Third International Symposium on Logical Foundations of Computer Science, p.316-328, July 11-14, 1994
• 32: Andrew Shalit, The Dylan reference manual: the definitive guide to the new object-oriented dynamic language, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1996
• 33: Zhong Shao, Typed cross-module compilation, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.141-152, September 26-29, 1998, Baltimore, Maryland, United States
• 34: Christopher Allan Stone , Robert Harper, Singleton kinds and singleton types, 2000
• 35: Stone, C. A. 2005. Type definitions. In Proceedings of the Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Cambridge, MA.
• 36: Christopher A. Stone , Robert Harper, Deciding type equivalence in a language with singleton kinds, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325724]
• 37: Stone, C. A. and Harper, R. 2004. Extensional equivalence and singleton types. Tech. Rep. HMC-CS-04-100, Computer Science Department, Harvey Mudd College.
• 38: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

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
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
Singleton types, equivalence algorithms, logical relations