{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:31:17Z","timestamp":1787063477601,"version":"3.56.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>\n                    Implicit functions are dependently typed functions, such that arguments are provided (by default) by inference machinery instead of programmers of the surface language. Implicit functions in Agda are an archetypal example. In the Haskell language as implemented by the Glasgow Haskell Compiler (GHC), polymorphic types are another example. Implicit function types are\n                    <jats:italic>first-class<\/jats:italic>\n                    if they are treated as any other type in the surface language. This holds in Agda and partially holds in GHC. Inference and elaboration in the presence of first-class implicit functions poses a challenge; in the context of Haskell and ML-like languages, this has been dubbed \u201cimpredicative instantiation\u201d or \u201cimpredicative inference\u201d. We propose a new solution for elaborating first-class implicit functions, which is applicable to full dependent type theories and compares favorably to prior solutions in terms of power, generality and simplicity. We build atop Norell\u2019s bidirectional elaboration algorithm for Agda, and we note that the key issue is incomplete information about insertions of implicit abstractions and applications. We make it possible to track and refine information related to such insertions, by adding a function type to a core Martin-L'of type theory, which supports strict (definitional) currying. This allows us to represent undetermined domain arities of implicit function types, and we can decide at any point during elaboration whether implicit abstractions should be inserted.\n                  <\/jats:p>","DOI":"10.1145\/3408983","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T09:48:02Z","timestamp":1596448082000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Elaboration with first-class implicit function types"],"prefix":"10.1145","volume":"4","author":[{"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_5"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944709"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_2_2_11_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 ( 2016 ). arXiv: 1610.07978 http:\/\/arxiv.org\/abs\/1610.07978  Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 ( 2016 ). arXiv: 1610.07978 http:\/\/arxiv.org\/abs\/1610.07978"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_2_2_14_1","volume-title":"Practical foundations for programming languages","author":"Harper Robert"},{"key":"e_1_2_2_15_1","unstructured":"Marcus Johansson and Jesper Lloyd. 2015. Eliminating the problems of hidden-lambda insertion-Restricting implicit arguments for increased predictability of type checking in a functional programming language with depending types. Master's thesis. Chalmers University of Technology.  Marcus Johansson and Jesper Lloyd. 2015. Eliminating the problems of hidden-lambda insertion-Restricting implicit arguments for increased predictability of type checking in a functional programming language with depending types. Master's thesis. Chalmers University of Technology."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480891"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.22"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_2_2_24_1","volume-title":"Simon Peyton Jones, and Dimitrios Vytiniotis","author":"Serrano Alejandro","year":"2020"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_2_2_26_1","volume-title":"Algebraic Type Theory and Universe Hierarchies. CoRR abs\/","author":"Sterling Jonathan","year":"1902"},{"key":"e_1_2_2_27_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159838"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167091"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408983","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408983","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:58Z","timestamp":1750178878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408983"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":28,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408983"],"URL":"https:\/\/doi.org\/10.1145\/3408983","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}