Abstract
Elaboration-based type class resolution, as found in languages like Haskell, Mercury and PureScript, is generally nondeterministic: there can be multiple ways to satisfy a wanted constraint in terms of global instances and locally given constraints. Coherence is the key property that keeps this sane; it guarantees that, despite the nondeterminism, programs still behave predictably. Even though elaboration-based resolution is generally assumed coherent, as far as we know, there is no formal proof of this property in the presence of sources of nondeterminism, like superclasses and flexible contexts.
This paper provides a formal proof to remedy the situation. The proof is non-trivial because the semantics elaborates resolution into a target language where different elaborations can be distinguished by contexts that do not have a source language counterpart. Inspired by the notion of full abstraction, we present a two-step strategy that first elaborates nondeterministically into an intermediate language that preserves contextual equivalence, and then deterministically elaborates from there into the target language. We use an approach based on logical relations to establish contextual equivalence and thus coherence for the first step of elaboration, while the second step’s determinism straightforwardly preserves this coherence property.
Supplemental Material
Available for Download
Appendix containing the full formalization and proofs.
- Martín Abadi. 1999. Protection in Programming-Language Translations. Springer, 19–34. Google ScholarDigital Library
- Amal Ahmed. 2006. Step-indexed syntactic logical relations for recursive and quantified types. In European Symposium on Programming (ESOP). Google ScholarDigital Library
- Amal Ahmed. 2015. Logical Relations. https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html .Google Scholar
- Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for free: Parametricity for dependent types. Journal of Functional Programming 22, 2 (2012), 107–152. Google ScholarDigital Library
- Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. The essence of nested composition. In ECOOP.Google Scholar
- Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Distributive Disjoint Polymorphism for Compositional Programming. (2019).Google Scholar
- Dariusz Biernacki and Piotr Polesiuk. 2015. Logical relations for coherence of effect subtyping. In LIPIcs.Google Scholar
- Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Quantified Class Constraints. In Haskell 2017. ACM, 148–161. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.Google ScholarCross Ref
- Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005. Associated Type Synonyms. SIGPLAN Not. 40, 9 (2005), 241–253. Google ScholarDigital Library
- Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover. (2015).Google Scholar
- Dominique Devriese and Frank Piessens. 2011. On the Bright Side of Type Classes: Instance Arguments in Agda. In ICFP ’11. ACM, 143–155. Google ScholarDigital Library
- Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, and Gabriele Keller. 2007. Modular Type Classes. In POPL ’07. ACM, 63–70. Google ScholarDigital Library
- Phil Freeman. 2017. PureScript by Example. Leanpub. https://leanpub.com/purescript .Google Scholar
- Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional Proof-Irrelevance without K. Proceedings of the ACM on Programming Languages (Jan. 2019), 1–28. Google ScholarDigital Library
- Douglas Gregor, Jaakko Järvi, Jeremy Siek, Bjarne Stroustrup, Gabriel Dos Reis, and Andrew Lumsdaine. 2006. Concepts: Linguistic Support for Generic Programming in C++. SIGPLAN Not. 41, 10 (2006), 291–310. Google ScholarDigital Library
- Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. 1996. Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18, 2 (1996), 109–138. Google ScholarDigital Library
- Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press. Google ScholarDigital Library
- Fergus Henderson, Thomas Conway, Zoltan Somogyi, David Jeffery, Peter Schachte, Simon Taylor, and Chris Speirs. 1996. The Mercury Language Reference Manual. Technical Report.Google Scholar
- M.P. Jones. 1993. Coherence for qualified types. Research Report YALEU/DCS/RR-989. Yale University, Dept. of Computer Science.Google Scholar
- Mark P. Jones. 1994. Qualified Types: Theory and Practice. Cambridge University Press.Google ScholarCross Ref
- Mark P. Jones. 2000. Type Classes with Functional Dependencies. In Programming Languages and Systems. LNCS, Vol. 1782. Springer, 230–244. Google ScholarDigital Library
- Wolfram Kahl and Jan Scheffczyk. 2001. Named Instances for Haskell Type Classes. In Proc. Haskell Workshop 2001, Ralf Hinze (Ed.), Vol. 59.Google Scholar
- Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: Property-Based Testing in Coq (1st ed.). Software Foundations, Vol. 4.Google Scholar
- Lex Spoon Martin Odersky and Bill Venners. 2008. Implicit Conversions and Parameters. In Programming in Scala. Chapter 21.Google Scholar
- J. Garrett Morris. 2014. A simple semantics for Haskell overloading. In Haskell 2014, Wouter Swierstra (Ed.). ACM, 107–118. Google ScholarDigital Library
- James Hiram Morris Jr. 1969. Lambda-calculus models of programming languages. Ph.D. Dissertation. Massachusetts Institute of Technology.Google Scholar
- Team Mozilla Research. 2017. The Rust Programming Language. https://www.rust- lang.org/en- US/ .Google Scholar
- Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2017. Simplicitly: Foundations and Applications of Implicit Function Types. In POPL ’18. Google ScholarDigital Library
- Dominic Orchard and Tom Schrijvers. 2010. Haskell Type Constraints Unleashed. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 56–71. Google ScholarDigital Library
- Simon Peyton Jones. 2003. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press.Google Scholar
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple Unification-based Type Inference for GADTs. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, New York, NY, USA, 50–61. Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (2000), 1–44. Google ScholarDigital Library
- Gordon Plotkin. 1973. Lambda-definability and logical relations. Edinburgh University.Google Scholar
- John C. Reynolds. 1991. The Coherence of Languages with Intersection Types. In TACS ’91. Springer-Verlag, 675–700. Google ScholarDigital Library
- Tom Schrijvers, Bruno C.D.S. Oliveira, Philip Wadler, and Koar Marntirosian. 2019. COCHIS: Stable and coherent implicits. Journal of Functional Programming 29 (2019), e3.Google ScholarCross Ref
- Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In TPHOLs ’08. Springer-Verlag, 278–293. Google ScholarDigital Library
- Richard Statman. 1985. Logical relations and the typed λ-calculus. Information and Control 65, 2-3 (1985), 85–97.Google ScholarCross Ref
- William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 2 (1967), 198–212.Google Scholar
- P. Wadler and S. Blott. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc. In POPL ’89. ACM. Google ScholarDigital Library
- Leo White, Frédéric Bour, and Jeremy Yallop. 2014. Modular implicits. In ML/OCaml 2014.Google Scholar
- Thomas Winant and Dominique Devriese. 2018. Coherent Explicit Dictionary Application for Haskell. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (Haskell 2018). ACM, New York, NY, USA, 81–93. Google ScholarDigital Library
Index Terms
- Coherence of type class resolution
Recommendations
Fully-abstract compilation by approximate back-translation
POPL '16A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker ...
Aspect-oriented programming with type classes
FOAL '07: Proceedings of the 6th workshop on Foundations of aspect-oriented languagesWe consider the problem of adding aspects to a strongly typed language which supports type classes. We show that type classes as supported by the Glasgow Haskell Compiler can model an AOP style of programming via a simple syntax-directed transformation ...
Fully-abstract compilation by approximate back-translation
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesA compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker ...
Comments