{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:46Z","timestamp":1779836746442,"version":"3.53.1"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2011,5,16]],"date-time":"2011-05-16T00:00:00Z","timestamp":1305504000000},"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":[[2011,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as\n                    <jats:italic>local<\/jats:italic>\n                    type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and \u2013 perhaps controversially \u2013 argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called\n                    <jats:sc>OutsideIn(X)<\/jats:sc>\n                    , is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm.\n                    <jats:sc>OutsideIn(X)<\/jats:sc>\n                    extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.\n                  <\/jats:p>","DOI":"10.1017\/s0956796811000098","type":"journal-article","created":{"date-parts":[[2011,5,16]],"date-time":"2011-05-16T03:51:51Z","timestamp":1305517911000},"page":"333-412","source":"Crossref","is-referenced-by-count":101,"title":["<scp>OutsideIn(X)<\/scp>\n                    Modular type inference with local assumptions"],"prefix":"10.1017","volume":"21","author":[{"given":"DIMITRIOS","family":"VYTINIOTIS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"SIMON","family":"PEYTON JONES","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"TOM","family":"SCHRIJVERS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MARTIN","family":"SULZMANN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2011,5,16]]},"reference":[{"key":"S0956796811000098_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1108970.1108974"},{"key":"S0956796811000098_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086391"},{"key":"S0956796811000098_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62950-5_59"},{"key":"S0956796811000098_ref13","volume-title":"Coherence for Qualified Types","author":"Jones","year":"1993"},{"key":"S0956796811000098_ref3","first-page":"241","volume-title":"Proceedings of International Conference on Functional Programming (ICFP '05)","author":"Chakravarty","year":"2005"},{"key":"S0956796811000098_ref2","first-page":"678","volume-title":"Proceedings of International Conference on Automated Deduction (CADE '94)","author":"Beckert","year":"1994"},{"key":"S0956796811000098_ref45","volume-title":"Type Inference for GADTs via Herbrand Constraint Abduction","author":"Sulzmann","year":"2008"},{"key":"S0956796811000098_ref16","volume-title":"Type Inference and Equational Theories","author":"Kennedy","year":"1996"},{"key":"S0956796811000098_ref50","volume-title":"Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10)","author":"Weirich","year":"2010"},{"key":"S0956796811000098_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006137"},{"key":"S0956796811000098_ref32","first-page":"389","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pottier","year":"2005"},{"key":"S0956796811000098_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481855"},{"key":"S0956796811000098_ref31","first-page":"232","volume-title":"Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06)","author":"Pottier","year":"2006"},{"key":"S0956796811000098_ref17","first-page":"303","volume-title":"Reflections on the work of C. A. R. Hoare","author":"Kiselyov","year":"2010"},{"key":"S0956796811000098_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_5"},{"key":"S0956796811000098_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"S0956796811000098_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186031"},{"key":"S0956796811000098_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/128749.128754"},{"key":"S0956796811000098_ref12","unstructured":"Jones M. P. (September 1992) Qualified Types: Theory and Practice. DPhil thesis, Oxford University."},{"key":"S0956796811000098_ref27","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"S0956796811000098_ref18","first-page":"26","volume-title":"Proceedings of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI '03)","author":"L\u00e4mmel","year":"2003"},{"key":"S0956796811000098_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796811000098_ref35","volume-title":"Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP '09)","author":"Schrijvers","year":"2009"},{"key":"S0956796811000098_ref49","volume-title":"Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '89)","author":"Wadler","year":"1989"},{"key":"S0956796811000098_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80779-5"},{"key":"S0956796811000098_ref41","volume-title":"Proceedings of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI '07)","author":"Sulzmann","year":"2007"},{"key":"S0956796811000098_ref23","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.21"},{"key":"S0956796811000098_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_2"},{"key":"S0956796811000098_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180476"},{"key":"S0956796811000098_ref25","first-page":"453","volume-title":"Proceedings of International Conference on Rewriting Techniques and Applications (RTA '05)","author":"Nieuwenhuis","year":"2005"},{"key":"S0956796811000098_ref36","first-page":"233","volume-title":"Proceedings of International Symposium on Implementation and Application of Functional Languages (IFL '09)","author":"Schrijvers","year":"2007"},{"key":"S0956796811000098_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708024"},{"key":"S0956796811000098_ref5","unstructured":"Cheney J. & Hinze R. (2003) First-Class Phantom Types. TR 1901. Cornell University. Available at: http:\/\/techreports.library.cornell.edu:8081\/Dienst\/UI\/1.0\/Display\/cul.cis\/TR2003-1901"},{"key":"S0956796811000098_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"S0956796811000098_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"S0956796811000098_ref7","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/871895.871905","volume-title":"Proceedings of the 2003 ACM SIGPLAN Workshop on Haskell (Haskell '03)","author":"Fax\u00e9n","year":"2003"},{"key":"S0956796811000098_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"S0956796811000098_ref1","first-page":"64","volume-title":"Proceedings of International Conference on Automated Deduction (CADE '00)","author":"Bachmair","year":"2000"},{"key":"S0956796811000098_ref14","volume-title":"Proceedings of European Symposium on Programming Languages and Systems (ESOP '00)","author":"Jones","year":"2000"},{"key":"S0956796811000098_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"S0956796811000098_ref11","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/871895.871902","volume-title":"Proceedings of ACM SIGPLAN 2003 Haskell Workshop","author":"Heeren","year":"2003"},{"key":"S0956796811000098_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"S0956796811000098_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"S0956796811000098_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"S0956796811000098_ref30","volume-title":"Wobbly Types: Type Inference for Generalised Algebraic Data Types","author":"Peyton Jones","year":"2004"},{"key":"S0956796811000098_ref4","first-page":"1","volume-title":"Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05)","author":"Chakravarty","year":"2005"},{"key":"S0956796811000098_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708023"},{"key":"S0956796811000098_ref43","unstructured":"Sulzmann M. , M\u00fcller M. & Zenger C. (1999) Hindley\/Milner Style Type Systems in Constraint Form. Research Report ACRC-99-009. School of Computer and Information Science, University of South Australia."},{"key":"S0956796811000098_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"S0956796811000098_ref40","doi-asserted-by":"crossref","unstructured":"Sulzmann M. (May 2000) A General Framework for Hindley\/Milner Type Systems with Constraints. Ph.D. thesis, Department of Computer Science, Yale University.","DOI":"10.1007\/3-540-44716-4_16"},{"key":"S0956796811000098_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001325"},{"key":"S0956796811000098_ref22","volume-title":"Three Techniques for GADT Type Inference","author":"Lin","year":"2010"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796811000098","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:23Z","timestamp":1779834983000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796811000098\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,16]]},"references-count":52,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["S0956796811000098"],"URL":"https:\/\/doi.org\/10.1017\/s0956796811000098","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,16]]}}}