Type isomorphisms in a type-assignment framework

ABSTRACT

This paper contains a full treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. Surprisingly enough the results obtained contradict the common-place feeling that (the core of) ML is a subset of second order &lgr;-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order &lgr;-calculus. This new isomorphism not only allows to provide a complete (and decidable) axiomatisation of all the type isomorphic in ML style languages, a relevant issue for the type as specifications paradigm in library searches, but also suggest a natural extension that in a sense completes the type-inference mechanism in ML. This extension is easy to implement and allows to get a further insight in the nature of the let polymorphic construct.

REFERENCES

• Bar84: Henk Barendlregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984.
• Bas90: David A. Basin, Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete, Proceedings of the tenth international conference on Automated deduction, p.251-260, July 1990, Kaiserslautern, Germany
• BDCL90: Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report 90-14, LIENS - Ecole Normale Sup~rieure, 1990. To appear in Proc. of Symposium on Symbolic Computation, ETH, Zurich, March 1990: MSCS.
• BL85: K B Bruce , G Longo, Provable isomorphisms and domain equations in models of typed languages, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.263-272, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22175]
• CDC91: Pierre-Louis Curien , Roberto Di Cosmo, A confluent reduction for the &lgr;-calculus with surjective pairing and terminal object, Proceedings of the 18th international colloquium on Automata, languages and programming, p.291-302, June 1991, Madrid, Spain
• CH88: Guy Cousineau and Gerard Huet. The CAML primer. Technical Report, LIENS - Ecole Normale Sup~rieure, 1988.
• DC91: Roberto Di Cosmo. Invertibility of terms and valid isomorphi~ms. A proof theoretic study on second order )~-calculus with surjective pairing and terminal object. Technical Report 91-10, LIENS - Ecole Normale Sup~rieure, 1991.
• DC92: Roberto Di Cosmo. Deciding Type isomorphisms in a type assignment framework. Technical Report, LIENS - Ecole Normale Sup~rieure, 1992. To appear.
• DCL89: Roberto Di Cosmo and Giuseppe Longo. Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). Workshop on Logic for Computer Science- MSRI, Berkeley, November 1989.
• Dez76: Mariangiola Dezani-Ciancaglini. Characterization of normal forms possessing an inverse in he Aflr/ calculus. Theoretical Computer Science, 2:323-337, 1976.
• Hin69: R. Hindley. The principal type-scheme of a an object in combinatory logic. Transactions of the American Mathematical Society, 146, 1969.
• HS80: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• Jay91: C. Barry Jay. Strong normalisation for simply-typed lambda-calculus as in lambekscott. February 1991. LFCS, University of Edimburgh.
• Kir85: Claude Kirchner. Methodes et utiles de conception systematique d 'algoritmes d 'unification dans le~ theories equationnelles. PhD thesis, Universit~ de Nancy, 1985.
• Mar72: C.F. Martin. Axiomatic bases for equational theories of natural numbers. Notices of the Am. Math. Soc., 19(7):778, 1972.
• Mil78: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Science, 17(3):348-375, 1978.
• NPS89: Paliath Narendran, Frank Pfenning, and Rick Statman. On the unification problem for cartesian closed categories. Hardware Verification Workshop, September 1989.
• Rit89: Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1), 1989.
• Rit90a: Mikael Rittri, Retrieving library identifiers via equational matching of types, Proceedings of the tenth international conference on Automated deduction, p.603-617, July 1990, Kaiserslautern, Germany
• Rit90b: Mikael Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, Chalmers University of Technology, GSteborg, Sweden, 1990.
• RT89: Colin Runciman , Ian Toyn, Retrieving re-usable software components by polymorphic type, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.166-173, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99383]
• Sol83: Serjey V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387-1400, 1983.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory