{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:29:11Z","timestamp":1767929351236,"version":"3.49.0"},"reference-count":44,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2007,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Haskell's popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types \u2013 that is, functions that take polymorphic functions as their arguments. Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code. However, the choice of just what annotations are required, and what changes are required in the type system and its inference algorithm, has been an ongoing topic of research. We take as our starting point a \u03bb-calculus proposed by Odersky and L\u00e4ufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on \u03bb-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than some other proposals, Odersky and L\u00e4ufer's system requires many annotations. We show how to use local type inference (invented by Pierce and Turner) to greatly reduce the annotation burden, to the point where higher-rank types become eminently usable. Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference engine using a monadic framework: it turns out to be a particularly compelling example of monads in action. The paper is long, but is strongly tutorial in style. Although we use Haskell as our example source language, and our implementation language, much of our work is directly applicable to any ML-like functional language.<\/jats:p>","DOI":"10.1017\/s0956796806006034","type":"journal-article","created":{"date-parts":[[2006,6,9]],"date-time":"2006-06-09T09:30:27Z","timestamp":1149845427000},"page":"1-82","source":"Crossref","is-referenced-by-count":127,"title":["Practical type inference for arbitrary-rank types"],"prefix":"10.1017","volume":"17","author":[{"given":"SIMON PEYTON","family":"JONES","sequence":"first","affiliation":[]},{"given":"DIMITRIOS","family":"VYTINIOTIS","sequence":"additional","affiliation":[]},{"given":"STEPHANIE","family":"WEIRICH","sequence":"additional","affiliation":[]},{"given":"MARK","family":"SHIELDS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,1,1]]},"reference":[{"key":"S0956796806006034_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"S0956796806006034_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360207"},{"key":"S0956796806006034_ref28","unstructured":"Morrisett G. 1995 (Dec.). Compiling with types. Ph.D. thesis, Carnegie Mellon University."},{"key":"S0956796806006034_ref41","doi-asserted-by":"crossref","unstructured":"Tiuryn J , & Urzyczyn P. (1996). The subtyping problem for second order types is undecidable. Proc. IEEE Symposium on Logic in Computer Science (LICS'96).","DOI":"10.1109\/LICS.1996.561306"},{"key":"S0956796806006034_ref14","volume-title":"ACM SIGPLAN International Conference on Functional Programming (ICFP'03)","year":"2003"},{"key":"S0956796806006034_ref21","unstructured":"Le Botlan D , & \u00e9my D. (2003). MLF: raising ML to the power of System F. In: ICFP03, 2003."},{"key":"S0956796806006034_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_2"},{"key":"S0956796806006034_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325709"},{"key":"S0956796806006034_ref32","first-page":"47","volume-title":"Engineering theories of software construction, Marktoberdorf Summer School 2000","author":"Peyton Jones","year":"2001"},{"key":"S0956796806006034_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90020-G"},{"key":"S0956796806006034_ref10","doi-asserted-by":"crossref","unstructured":"Heeren B , Hage J , & Swierstra SD. (2003). Scripting the type inference process. In: CFP03, 2003.","DOI":"10.1145\/944705.944707"},{"key":"S0956796806006034_ref7","first-page":"223","volume-title":"ACM Conference on Functional Programming and Computer Architecture (FPCA'93)","author":"Gill","year":"1993"},{"key":"S0956796806006034_ref16","unstructured":"Jones Mark . (1999). Typing Haskell in Haskell. Meijer, Erik (ed), Proceedings of the 1999 haskell workshop. Technical Reports, nos. UU\u2013CS\u20131999\u201328. Available at ftp:\/\/ftp.cs.uu.nl\/pub\/RUU\/CS\/techreps\/CS-1999\/1999-28.pdf."},{"key":"S0956796806006034_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"S0956796806006034_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581494"},{"key":"S0956796806006034_ref40","first-page":"181","volume-title":"ACM Conference on Programming Languages Design and Implementation (PLDI'96)","author":"Tarditi","year":"1996"},{"key":"S0956796806006034_ref19","first-page":"26","volume-title":"ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'03)","author":"L\u00e4mmel","year":"2003"},{"key":"S0956796806006034_ref18","first-page":"196","volume-title":"ACM Symposium on Lisp and Functional Programming","author":"Kfoury","year":"1994"},{"key":"S0956796806006034_ref4","first-page":"13","volume-title":"ACM Symposium on Lisp and Functional Programming","author":"Clement","year":"1986"},{"key":"S0956796806006034_ref6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2830"},{"key":"S0956796806006034_ref42","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2941"},{"key":"S0956796806006034_ref8","volume-title":"Logical foundations of functional programming","author":"Girard","year":"1990"},{"key":"S0956796806006034_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"S0956796806006034_ref38","unstructured":"Shao Zhong . 1997 (June). An overview of the FLINT\/ML compiler. Proc. 1997 ACM SIGPLAN workshop on types in compilation (TIC'97)."},{"key":"S0956796806006034_ref39","volume-title":"Lexically scoped type variables","author":"Shields","year":"2002"},{"key":"S0956796806006034_ref9","first-page":"163","volume-title":"The implementation of functional programming languages","author":"Hancock","year":"1987"},{"key":"S0956796806006034_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"S0956796806006034_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00029-4"},{"key":"S0956796806006034_ref12","article-title":"Manufacturing datatypes","volume":"1","author":"Hinze","year":"2001","journal-title":"Journal of Functional Programming"},{"key":"S0956796806006034_ref24","unstructured":"Longo Giuseppe , Milsted Kathleen , & Soloviev Sergei . (1995). A logic of subtyping (extended abstract). Pages 292\u2013299 of: |lics95|."},{"key":"S0956796806006034_ref26","article-title":"A theory of type polymorphism in programming","volume":"13","author":"Milner","year":"1978","journal-title":"Jcss"},{"key":"S0956796806006034_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"S0956796806006034_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317781"},{"key":"S0956796806006034_ref34","volume-title":"Types and programming languages","author":"Pierce","year":"2002"},{"key":"S0956796806006034_ref43","unstructured":"Vytiniotis Dimitrios , Weirich Stephanie , & Peyton Jones Simon . 2005 (July). Practical type inference for arbitrary-rank types, Technical Appendix. Tech. rept. MS-CIS-05-14. University of Pennsylvania."},{"key":"S0956796806006034_ref5","first-page":"207","volume-title":"Conference record of the 9th annual acm symposium on principles of programming languages","author":"Damas","year":"1982"},{"key":"S0956796806006034_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"S0956796806006034_ref23","unstructured":"Leijen Daan , & L\u00f6h Andres . (2005). Qualified types for MLF. In: ICFP05, 2005."},{"key":"S0956796806006034_ref36","volume-title":"Advanced topics in types and programming languages","author":"Pottier","year":"2004"},{"key":"S0956796806006034_ref15","volume-title":"ACM SIGPLAN International Conference on Functional Programming (ICFP'05)","year":"2005"},{"key":"S0956796806006034_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90019-0"},{"key":"S0956796806006034_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"S0956796806006034_ref37","unstructured":"R\u00e9my Didier . (2005). Simple, partial type inference for System F, based on type containment. In: ICFP05, 2005."},{"key":"S0956796806006034_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796806006034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T19:11:13Z","timestamp":1554145873000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796806006034\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,1]]}},"alternative-id":["S0956796806006034"],"URL":"https:\/\/doi.org\/10.1017\/s0956796806006034","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1]]}}}