{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:15Z","timestamp":1779836715250,"version":"3.53.1"},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5516,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1993,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This 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 \u03bb-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order \u03bb-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 the\n                    <jats:italic>type as specifications<\/jats:italic>\n                    paradigm 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.\n                  <\/jats:p>","DOI":"10.1017\/s0956796800000861","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:13:12Z","timestamp":1226056392000},"page":"485-525","source":"Crossref","is-referenced-by-count":13,"title":["Deciding type isomorphisms in a type-assignment framework"],"prefix":"10.1017","volume":"3","author":[{"given":"Roberto","family":"Di Cosmo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000861_ref040","doi-asserted-by":"publisher","DOI":"10.1007\/BF01084396"},{"key":"S0956796800000861_ref039","first-page":"173","volume-title":"Eighth International Conference on Logic Programming","author":"Rollins","year":"1991"},{"key":"S0956796800000861_ref038","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S0956796800020049","article-title":"Retrieving re-usable software components by polymorphic type","volume":"1","author":"Runciman","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"S0956796800000861_ref037","unstructured":"Rittri M. (1992) Retrieving library functions by unifying types modulo linear isomorphisms. Technical Report 66, Chalmers University of Technology and University of G\u00f6teborg 1992. Programming Methodology Group."},{"key":"S0956796800000861_ref035","unstructured":"Rittri M. (1990) Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of G\u00f6teborg, G\u00f6teborg, Sweden."},{"key":"S0956796800000861_ref033","volume-title":"Information Processing '83","author":"Reynolds","year":"1983"},{"key":"S0956796800000861_ref034","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_117"},{"key":"S0956796800000861_ref030","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796800000861_ref029","volume-title":"Commentary on Standard ML","author":"Milner","year":"1991"},{"key":"S0956796800000861_ref027","unstructured":"Morgan R. (1991) Component Library Retrieval using property models. PhD thesis, University of Durham - England, rick@easby.dur.ac.uk."},{"key":"S0956796800000861_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796800000861_ref022","first-page":"778","article-title":"Axiomatic bases for equational theories of natural numbers","volume":"19","author":"Martin","year":"1972","journal-title":"Notices of the Am. Math. Soc."},{"key":"S0956796800000861_ref021","unstructured":"Longo G. , Milsted K. and Soloviev S.V. (1992) The genericity theorem and the notion of parametericity in the polimorphic \u03bb-calculus. E-mail: longo@dmi.ens.fr and milsted@prl.dec.com., 08."},{"key":"S0956796800000861_ref018","unstructured":"Kirchner C. (1985) Methodes et utiles de conception systematique d'algoritmes d'unification dans les theories equationnelles. PhD thesis, Universit\u00e9 de Nancy."},{"key":"S0956796800000861_ref017","volume-title":"Strong normalisation for simply-typed lambda-calculus as in lambek-scott","author":"Jay","year":"1991"},{"key":"S0956796800000861_ref016","volume-title":"Introduction to Combinators and \u03bb-calculus","author":"Hindley","year":"1980"},{"key":"S0956796800000861_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90085-2"},{"key":"S0956796800000861_ref012","volume-title":"Workshop on Logic for Computer Science - MSRI","author":"Di Cosmo","year":"1989"},{"key":"S0956796800000861_ref041","unstructured":"Weis P. , Aponte M.V. , Laville A. , Mauny M. and Su\u00e1rez A. (1990) The CAML reference manual. Technical Report 121, INRIA, Roquencourt B.P.105 - 78153 Le Chesnay Cedex - France, 09."},{"key":"S0956796800000861_ref009","unstructured":"Damas L. (1985) Types Disciplines in Programming Languages. PhD thesis, Computer Science Dept., University of Edimburgh, 04."},{"key":"S0956796800000861_ref008","unstructured":"Cousineau G and Huet G. (1988) The caml primer. Technical report, LIENS - Ecole Normale Sup\u00e9rieure."},{"key":"S0956796800000861_ref002","volume-title":"The Lambda Calculus; Its syntax and Semantics (revised edition)","author":"Barendregt","year":"1984"},{"key":"S0956796800000861_ref001","volume-title":"Ann. ACM Symp. on Principles of Programming Languages (POPL)","author":"Abadi","year":"1993"},{"key":"S0956796800000861_ref026","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"S0956796800000861_ref011","first-page":"200","volume-title":"Ann. ACM Symp. on Principles of Programming Languages (POPL)","author":"Di Cosmo","year":"1992"},{"key":"S0956796800000861_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_142"},{"key":"S0956796800000861_ref015","article-title":"The principal type-scheme of a an object in combinatory logic","volume":"146","author":"Hindley","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0956796800000861_ref014","first-page":"207","volume-title":"Ann. ACM Symp. on Principles of Programming Languages (POPL)","author":"Damas","year":"1982"},{"key":"S0956796800000861_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_92"},{"key":"S0956796800000861_ref020","unstructured":"Leroy X. (1990) The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA."},{"key":"S0956796800000861_ref024","unstructured":"Mauny M. (1991) Functional programming using Caml Light. INRIA, 1991. Included in the Caml Light distribution."},{"key":"S0956796800000861_ref031","unstructured":"Nipkow T. (1990) A critical pair lemma for higher-order rewrite systems and its application to \u03bb*. First Annual Workshop on Logical Frameworks."},{"key":"S0956796800000861_ref006","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/22145.22175"},{"key":"S0956796800000861_ref005","article-title":"Provable isomorphisms of types","volume":"2","author":"Bruce","year":"1990","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0956796800000861_ref032","unstructured":"Narendran P. , Pfenning F. and Statman R. (1992) On the unification problem for cartesian closed categories. E-mail: dran@cs.albany.edu."},{"key":"S0956796800000861_ref023","volume-title":"Dept. Comput. Sci","author":"Matthews","year":"1992"},{"key":"S0956796800000861_ref019","volume-title":"Lambda calculus. Types et Mod\u00e9les","author":"Krivine","year":"1990"},{"key":"S0956796800000861_ref036","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000006X"},{"key":"S0956796800000861_ref010","unstructured":"Di Cosmo R. (1991) Invertibility of terms and valid isomorphisms. a proof theoretic study on second order \u03bb-calculus with surjective pairing and terminal object. Technical Report 91\u201310, LIENS - Ecole Normale Sup\u00e9rieure, 1991. Submitted to Information and Computation."},{"key":"S0956796800000861_ref028","unstructured":"Meertens L. and Siebes A. (1990) Universal type isomorphisms in cartesian closed categories. Centrum voor Wiskunde en Informatica, Amsterdam, the Netherlands. E-mail: lambert,arno@cwi.nl."},{"key":"S0956796800000861_ref004","unstructured":"Bruce K. , Di Cosmo R. and Longo G. (1990) Provable isomorphisms of types. Technical Report 90\u201314, LIENS - Ecole Normale Sup\u00e9rieure, 1990. To appear in Proc. of Symposium on Symbolic Computation, ETH, Zurich, March 1990, Mathematical Structures in Computer Science, 2(2)."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000861","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:12Z","timestamp":1779834912000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000861\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,10]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1993,10]]}},"alternative-id":["S0956796800000861"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000861","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,10]]}}}