{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:01Z","timestamp":1763467981897},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2010,4,15]],"date-time":"2010-04-15T00:00:00Z","timestamp":1271289600000},"content-version":"unspecified","delay-in-days":45,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Propositions that express type equality are a frequent ingredient of modern functional programming \u2013 they can encode generic functions, dynamic types, and GADTs. Via the Curry\u2013Howard correspondence, these propositions are ordinary<jats:italic>types<\/jats:italic>inhabited by proof<jats:italic>terms<\/jats:italic>, computed using runtime type representations. In this paper we show that two examples of type equality propositions actually do reflect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to equivalence.) We show this result in the context of a strongly normalizing language with higher-order polymorphism and primitive recursion over runtime-type representations by proving Reynolds's abstraction theorem. We then use this theorem to derive \u201cfree\u201d theorems about equality types.<\/jats:p>","DOI":"10.1017\/s0956796810000079","type":"journal-article","created":{"date-parts":[[2010,4,15]],"date-time":"2010-04-15T09:16:11Z","timestamp":1271322971000},"page":"175-210","source":"Crossref","is-referenced-by-count":20,"title":["Parametricity, type equality, and higher-order polymorphism"],"prefix":"10.1017","volume":"20","author":[{"given":"DIMITRIOS","family":"VYTINIOTIS","sequence":"first","affiliation":[]},{"given":"STEPHANIE","family":"WEIRICH","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2010,4,15]]},"reference":[{"key":"S0956796810000079_ref41","doi-asserted-by":"crossref","unstructured":"Yang Z. (1998) Encoding types in ML-like languages. In 1998 ACM SIGPLAN International Conference on Functional Programming. ACM SIGPLAN Notices 34, pp. 289\u2013300.","DOI":"10.1145\/289423.289458"},{"key":"S0956796810000079_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005179"},{"key":"S0956796810000079_ref37","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.20"},{"key":"S0956796810000079_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317789"},{"key":"S0956796810000079_ref36","first-page":"347","volume-title":"FPCA89: Conference on Functional Programming Languages and Computer Architecture","author":"Wadler","year":"1989"},{"key":"S0956796810000079_ref31","unstructured":"Sheard T. & Pasalic E. (2004) Meta-programming with built-in type equality. In Proc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. pp. 106\u2013124."},{"key":"S0956796810000079_ref23","first-page":"324","volume-title":"FPCA95: Conference on Functional Programming Languages and Computer Architecture","author":"Meijer","year":"1995"},{"key":"S0956796810000079_ref22","unstructured":"Ku\u010dan J. (1997) Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS Transform and Free Theorems. PhD thesis, Massachusetts Institute of Technology."},{"key":"S0956796810000079_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"S0956796810000079_ref17","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1145\/1328438.1328475","volume-title":"POPL","author":"Johann","year":"2008"},{"key":"S0956796810000079_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00025-4"},{"key":"S0956796810000079_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596577"},{"key":"S0956796810000079_ref14","first-page":"130","volume-title":"Twenty-Second ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Harper","year":"1995"},{"key":"S0956796810000079_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(99)00036-8"},{"key":"S0956796810000079_ref12","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9 limination des coupures de l'arithm\u00e9tique d'ordre Sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII."},{"key":"S0956796810000079_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.043"},{"key":"S0956796810000079_ref11","first-page":"123","volume-title":"Logic and Computer Science","author":"Gallier","year":"1990"},{"key":"S0956796810000079_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"S0956796810000079_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111056"},{"key":"S0956796810000079_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"S0956796810000079_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172707"},{"key":"S0956796810000079_ref40","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/604131.604150","volume-title":"POPL","author":"Xi","year":"2003"},{"key":"S0956796810000079_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"S0956796810000079_ref6","volume-title":"First-Class Phantom Types","author":"Cheney","year":"2003"},{"key":"S0956796810000079_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_7"},{"key":"S0956796810000079_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_17"},{"key":"S0956796810000079_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964010"},{"key":"S0956796810000079_ref30","first-page":"513","volume-title":"Information Processing '83","author":"Reynolds","year":"1983"},{"key":"S0956796810000079_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581698"},{"key":"S0956796810000079_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581494"},{"key":"S0956796810000079_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.42"},{"key":"S0956796810000079_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"S0956796810000079_ref28","first-page":"245","volume-title":"Chap. 7 of: Advanced Topics in Types and Programming Languages","author":"Pitts","year":"2005"},{"key":"S0956796810000079_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"S0956796810000079_ref21","volume-title":"Mathematical Logic","author":"Kleene","year":"1967"},{"key":"S0956796810000079_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"S0956796810000079_ref33","unstructured":"Takeuti I. (2001) The Theory of Parametricity in Lambda Cube (Towards new interaction between category theory and proof theory). Technical Report. Kyoto University Research Information Repository."},{"key":"S0956796810000079_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004282"},{"key":"S0956796810000079_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"S0956796810000079_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"},{"key":"S0956796810000079_ref1","first-page":"69","volume-title":"Proceedings of ESOP","author":"Ahmed","year":"2006"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796810000079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T20:32:37Z","timestamp":1685565157000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796810000079\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["S0956796810000079"],"URL":"https:\/\/doi.org\/10.1017\/s0956796810000079","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}