Deciding type isomorphisms in a type-assignment framework

Journal of Functional Programming - Tập 3 Số 4 - Trang 485-525 - 1993
Roberto Di Cosmo1
1LIENS (CNRS) - DMI, Ecole Normale Supérieure, 45 Rue d'Ulm, 75005 Paris, France and Dipartimento di Informatica, Corso Italia 40, 56100 Pisa, Italy (

Tóm tắt

AbstractThis paper provides a formal treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. The results obtained make less justified the commonplace feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism allows to provide a complete (and decidable) axiomatization of all the types isomorphic in ML style languages, a relevant issue for thetype as specificationsparadigm in library searches. This work is a very extended version of Di Cosmo (1992): we provide both a thorough theoretical treatment of the topic and describe a practical implementation of a library search system so that the paper can be used as a reference both by those interested in the formal theory of ML style languages, and by those simply concerned with implementation issues. The new isomorphism can also be used to extend the usual ML type-inference algorithm, as suggested by Di Cosmo (1992). Building on that proposal, we introduce a better type-inference algorithm that behaves well in the presence of non-functional primitives like references and exceptions. The algorithm described here has been implemented easily as a variation to the Caml-Light 0.4 system.

Từ khóa


Tài liệu tham khảo

10.1007/BF01084396

Rollins, 1991, Eighth International Conference on Logic Programming, 173

Runciman, 1991, Retrieving re-usable software components by polymorphic type, Journal of Functional Programming, 1, 191, 10.1017/S0956796800020049

Rittri M. (1992) Retrieving library functions by unifying types modulo linear isomorphisms. Technical Report 66, Chalmers University of Technology and University of Göteborg 1992. Programming Methodology Group.

Rittri M. (1990) Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of Göteborg, Göteborg, Sweden.

Reynolds, 1983, Information Processing '83

10.1007/3-540-52885-7_117

Milner, 1990, The Definition of Standard ML

Milner, 1991, Commentary on Standard ML

Morgan R. (1991) Component Library Retrieval using property models. PhD thesis, University of Durham - England, [email protected].

10.1016/0022-0000(78)90014-4

Martin, 1972, Axiomatic bases for equational theories of natural numbers, Notices of the Am. Math. Soc., 19, 778

Longo G. , Milsted K. and Soloviev S.V. (1992) The genericity theorem and the notion of parametericity in the polimorphic λ-calculus. E-mail: [email protected] and [email protected]., 08.

Kirchner C. (1985) Methodes et utiles de conception systematique d'algoritmes d'unification dans les theories equationnelles. PhD thesis, Université de Nancy.

Jay, 1991, Strong normalisation for simply-typed lambda-calculus as in lambek-scott

Hindley, 1980, Introduction to Combinators and λ-calculus

10.1016/0304-3975(76)90085-2

Di Cosmo, 1989, Workshop on Logic for Computer Science - MSRI

Weis P. , Aponte M.V. , Laville A. , Mauny M. and Suárez A. (1990) The CAML reference manual. Technical Report 121, INRIA, Roquencourt B.P.105 - 78153 Le Chesnay Cedex - France, 09.

Damas L. (1985) Types Disciplines in Programming Languages. PhD thesis, Computer Science Dept., University of Edimburgh, 04.

Cousineau G and Huet G. (1988) The caml primer. Technical report, LIENS - Ecole Normale Supérieure.

Barendregt, 1984, The Lambda Calculus; Its syntax and Semantics (revised edition)

Abadi, 1993, Ann. ACM Symp. on Principles of Programming Languages (POPL)

10.1016/0890-5401(88)90009-0

Di Cosmo, 1992, Ann. ACM Symp. on Principles of Programming Languages (POPL), 200

10.1007/3-540-54233-7_142

Hindley, 1969, The principal type-scheme of a an object in combinatory logic, Transactions of the American Mathematical Society, 146

Damas, 1982, Ann. ACM Symp. on Principles of Programming Languages (POPL), 207

10.1007/3-540-52885-7_92

Leroy X. (1990) The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA.

Mauny M. (1991) Functional programming using Caml Light. INRIA, 1991. Included in the Caml Light distribution.

Nipkow T. (1990) A critical pair lemma for higher-order rewrite systems and its application to λ*. First Annual Workshop on Logical Frameworks.

Bruce K. and Longo G. (1985) Provable isomorphisms and domain equations in models of typed languages. ACM Symposium on Theory of Computing (STOC 85), 05.

Bruce, 1990, Provable isomorphisms of types, Mathematical Structures in Computer Science, 2

Narendran P. , Pfenning F. and Statman R. (1992) On the unification problem for cartesian closed categories. E-mail: [email protected].

Matthews, 1992, Dept. Comput. Sci

Krivine, 1990, Lambda calculus. Types et Modéles

10.1017/S095679680000006X

Di Cosmo R. (1991) Invertibility of terms and valid isomorphisms. a proof theoretic study on second order λ-calculus with surjective pairing and terminal object. Technical Report 91–10, LIENS - Ecole Normale Supérieure, 1991. Submitted to Information and Computation.

Meertens L. and Siebes A. (1990) Universal type isomorphisms in cartesian closed categories. Centrum voor Wiskunde en Informatica, Amsterdam, the Netherlands. E-mail: lambert,[email protected].

Bruce K. , Di Cosmo R. and Longo G. (1990) 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, Mathematical Structures in Computer Science, 2(2).

Thông tin
Thông tin xuất bản

Journal of Functional Programming

Tập 3 Số 4

485-525

Thông tin tác giả