Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-24T21:43:56.977Z Has data issue: false hasContentIssue false
  • English
  • Français

COCHIS: Stable and coherent implicits

Part of: JFP Research Articles

Published online by Cambridge University Press:  08 February 2019

TOM SCHRIJVERS ,
BRUNO C.D.S. OLIVEIRA ,
PHILIP WADLER  and
KOAR MARNTIROSIAN
TOM SCHRIJVERS
Affiliation:
Department of Computer Science, KU Leuven, Leuven, Belgium (e-mail: [email protected])
BRUNO C.D.S. OLIVEIRA
Affiliation:
Department of Computer Science, The University of Hong Kong, Hong Kong (e-mail: [email protected])
PHILIP WADLER
Affiliation:
School of Informatics, University of Edinburgh, Edinburgh, UK (e-mail: [email protected])
KOAR MARNTIROSIAN
Affiliation:
Department of Computer Science, KU Leuven, Leuven, Belgium (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Implicit programming (IP) mechanisms infer values by type-directed resolution, making programs more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s implicits, Agda’s instance arguments, Coq’s type classes and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning properties, while proponents of another school argue for the power and flexibility of local scoping or overlapping instances. The current state of affairs seems to indicate that the two goals are at odds with one another and cannot easily be reconciled. This paper presents COCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of the implicit calculus that offers flexibility while preserving two key properties: coherence and stability of type substitutions. COCHIS supports polymorphism, local scoping, overlapping instances, first-class instances and higher-order rules, while remaining type-safe, coherent and stable under type substitution. We introduce a logical formulation of how to resolve implicits, which is simple but ambiguous and incoherent, and a second formulation, which is less simple but unambiguous, coherent and stable. Every resolution of the second formulation is also a resolution of the first, but not conversely. Parts of the second formulation bear a close resemblance to a standard technique for proof search called focusing. Moreover, key for its coherence is a rigorous enforcement of determinism.

Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e3
Copyright
© Cambridge University Press 2019 

References

Andreoli, J.-M. (1992) Logic programming with focusing proofs in linear logic. J. Logic Comput. 2, 297–347.CrossRefGoogle Scholar
Barendregt, H. (1981) The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland.Google Scholar
Barendregt, H., Dekkers, W. & Statman, R. (2013) Lambda Calculus with Types. Cambridge University Press.CrossRefGoogle Scholar
Biernacki, D. & Polesiuk, P. (2018) Logical relations for coherence of effect subtyping. Log. Methods Comput. Sci. 14(1), pp. 1–28.Google Scholar
Boehm, H.-J. (1985) Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of Computer Science. IEEE, pp. 339–345.CrossRefGoogle Scholar
Bottu, G.-J., Karachalias, G., Schrijvers, T., Oliveira, B. & Wadler, P. (2017) Quantified class constraints. In Proceedings of the 10th ACMSIGPLAN International Symposium on Haskell, Haskell. New York, NY, USA: ACM, pp. 148–161.CrossRefGoogle Scholar
Bottu, G.-J. & Simon, P. J. (2018) Quantified constraints – proposals [online]. Available at: https://github.com/Gertjan423/ghc-proposals/blob/quantified-constraints/proposals/0000-quantified-constraints.rst#overlapGoogle Scholar
Brady, E. (2015) Type classes in Idris [online]. Available at: https://groups.google.com/forum/#!topic/idris-lang/OQQ3oc6zBaMGoogle Scholar
Breazu-Tannen, V., Coquand, T., Gunter, C. & Scedrov, A. (1991) Inheritance as implicit coercion. Inform. Comput. 93, 172–221.CrossRefGoogle Scholar
Camarão, C. & Figueiredo, L. (1999) Type inference for overloading without restrictions, declarations or annotations. In FLOPS. London, UK: Springer-Verlag, pp. 37–52.Google Scholar
Chakravarty, M., Keller, G. & Peyton Jones, S. L. (2005a). Associated type synonyms. In ICFP. New York: ACM, pp. 241–253.Google Scholar
Chakravarty, M., Keller, G., Peyton Jones, S. L. & Marlow, S. (2005b) Associated types with class. In POPL. New York: ACM, pp. 1–13.Google Scholar
Chong, S. (2017) Lecture 2: Logical relations Part 2 [online]. Available at: https://www.seas.harvard.edu/courses/cs252/2017fa/lectures/lec02-contextual-equiv.pdfGoogle Scholar
Damas, L. & Milner, R. (1982) Principal type-schemes for functional programs. In POPL. New York: ACM, pp. 207–212.Google Scholar
Devriese, D. & Piessens, F. (2011) On the bright side of type classes: Instance arguments in Agda. In ICFP. New York: ACM, pp. 143–155.Google Scholar
Dijkstra, A. & Swierstra, S. D. (2005) Making Implicit Parameters Explicit. Tech. rept. Utrecht University.Google Scholar
Dreyer, D., Harper, R., Chakravarty, M. & Keller, G. (2007) Modular type classes. In POPL. New York: ACM, pp. 63–70.Google Scholar
Dunfield, J. & Krishnaswami, N. R. (2013) Complete and easy bidirectional typechecking for higherrank polymorphism. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Morrisett, G. & Uustalu, T. (eds), Boston, MA: ACM, pp. 429–442.Google Scholar
Eisenberg, R. A., Vytiniotis, D., Peyton, J. S. & Weirich, S. (2014) Closed type families with overlapping equations. In POPL. New York: ACM, pp. 671–683.Google Scholar
Garcia, R., Jarvi, J., Lumsdaine, A., Siek, J. & Willcock, J. (2007) An extended comparative study of language support for generic programming. J. funct. program. 17(2), 145–205.CrossRefGoogle Scholar
GHC. (2017a) Ghc users guide: Overlapping instances [online]. Available at: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instancesGoogle Scholar
GHC. (2017b) Quantified constraints – GHC [online]. Available at https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraintsGoogle Scholar
Gonthier, G., Ziliani, B., Nanevski, A. & Dreyer, D. (2011) How to make ad hoc proof automation less ad hoc. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP’11. New York: ACM, pp. 163–175.CrossRefGoogle Scholar
Gregor, D., Järvi, J., Siek, J. G., Stroustrup, B., Dos Reis, G. & Lumsdaine, A. (2006) Concepts: Linguistic support for generic programming in c++. In OOPSLA. New York: ACM, pp. 291–310.Google Scholar
Hindley, J. R. (1969) The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29–60.Google Scholar
Hulley, B. (2009) A show-stopping problem for modular type classes? [online]. Available at: http://lists.seas.upenn.edu/pipermail/types-list/2009/001405.htmlGoogle Scholar
Jones, M. P. (1992). A theory of qualified types. In Proceedings of the 4th European Symposium on Programming (ESOP ’92), Krieg-Brückner, B. (ed), London, UK: Springer-Verlag, pp. 287–306.Google Scholar
Jones, M. P. (1995a) Qualified Types: Theory and Practice. Cambridge University Press.Google Scholar
Jones, M. P. (1995b) Simplifying and improving qualified types. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA ’95). New York, NY, USA: ACM, pp. 160–169.Google Scholar
Jones, S. P., Vytiniotis, D., Weirich, S. & Shields, M. (2007) Practical type inference for arbitraryrank types. Journal of Functional Programming 17(1), 1–82.CrossRefGoogle Scholar
Kahl, W. & Scheffczyk, J. (2001). Named instances for Haskell type classes. In Preliminary Proceedings of the 2001 ACM SIGPLAN Haskell Workshop (HW’2001), Hinze, R. (ed), Technical Report UU-CS-2001-23. Firenze, Italy: Institute of Information and Computing Sciences, Utrecht University.Google Scholar
Kiselyov, O. & Shan, C.-C. (2004) Functional pearl: Implicit configurations–or, type classes reflect the values of types. In Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell. Haskell ’04, ACM, pp. 33–44.CrossRefGoogle Scholar
Kmett, E. (2015) Type classes vs. the world [online]. Available at: https://www.youtube.com/watch?v=hIZxTQP1ifoGoogle Scholar
Le Botlan, D. & Rémy, D. (2003) MLF: Raising ML to the power of system F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming. ICFP ’03. SIGPLAN Not. 49, 4. pp. 52–63.CrossRefGoogle Scholar
Leijen, D. (2008) HMF: Simple type inference for first-class polymorphism. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). New York, NY, USA: ACM, pp. 283–294.CrossRefGoogle Scholar
Lewis, J., Launchbury, J., Meijer, E. & Shields, M. (2000) Implicit parameters: Dynamic scoping with static types. In POPL. New York: ACM, pp. 108–118.CrossRefGoogle Scholar
Liang, C. & Miller, D. (2009) Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747–4768.CrossRefGoogle Scholar
Manna, Z. & Waldinger, R. (1980) A deductive approach to program synthesis. Acm Trans. Program. Lang. Syst. 2(1), 90–121.CrossRefGoogle Scholar
Marlow, S. (2012) Safe Haskell and instance coherence [online]. Available at: https://mail.haskell.org/pipermail/haskell-cafe/2012-October/103887.htmlGoogle Scholar
Martelli, A. & Montanari, U. (1982). An efficient unification algorithm. Acm Trans. Program. Lang. Syst. 4(2), 258–282.CrossRefGoogle Scholar
Miller, D. (1992) Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358.CrossRefGoogle Scholar
Miller, D., Nadathur, G., Pfenning, F. & Scedrov, A. (1991) Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51(1–2), 125–157.CrossRefGoogle Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375.CrossRefGoogle Scholar
Morris, J. G. & Jones, M. P. (2010) Instance chains: Type class programming without overlapping instances. In ICFP. New York: ACM, pp. 375–386.Google Scholar
Morris, J. H., Jr. (1969) Lambda-calculus Models of Programming Languages. Ph.D. thesis, Sloan School of Management.Google Scholar
Research, Mozilla, Team. (2017) The rust programming language [online]. Available at: https://www.rust-lang.org/en-US/Google Scholar
Norell, U. (2008) Dependently typed programming in Agda. In Proceedings of the 6th International Conference on Advanced Functional Programming (AFP’08), Koopman, P., Plasmeijer, R. & Swierstra, D. (eds), Berlin, Heidelberg: Springer-Verlag, pp. 230–266.Google Scholar
nponeccop. (2012) Breaking data.set integrity without generalizednewtypederiving [online]. Available at: https://stackoverflow.com/questions/12735274/breaking-data-set-integrity-withoutgeneralizednewtypederivingGoogle Scholar
Odersky, M. (2010) The Scala Language Specification, version 2.8.Google Scholar
Odersky, M., Blanvillain, O., Liu, F., Biboudis, A., Miller, H. & Stucki, S. (2017) Simplicitly: Foundations and applications of implicit function types. Proc. ACM Program. Lang. 2(POPL), 42:1–42:29.CrossRefGoogle Scholar
Odersky, M. & Läufer, K. (1996) Putting type annotations to work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’96). New York, NY, USA: ACM, pp. 54–67.Google Scholar
oleg. (2006) Typeclass vs. prolog programming [online]. Available at: https://mail.haskell.org/pipermail/haskell-cafe/2006-September/018500.htmlGoogle Scholar
Oliveira, B. C. d. S., Moors, A. & Odersky, M. (2010) Type classes as objects and implicits. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA ’10). New York, NY, USA: ACM, pp. 341–360.CrossRefGoogle Scholar
Oliveira, B. C. d. S., Schrijvers, T., Choi, W., Lee, W. & Yi, K. (2012) The implicit calculus: A new foundation for generic programming. In PLDI ’12. New York: ACM.Google Scholar
Peyton Jones, S. L., Jones, M. P. & Meijer, E. (1997) Type classes: An exploration of the design space. In Haskell Workshop, Launchbury, J. (ed), Amsterdam, pp. 1–16.Google Scholar
Pfenning, Frank. (1993) On the undecidability of partial polymorphic type reconstruction. Fundam. Inform. 19(1/2), 185–199.Google Scholar
Pierce, B. C. (2002) Types and Programming Languages. Cambridge, MA: MIT Press.Google Scholar
Reynolds, J. C. (1991) The coherence of languages with intersection types. In Proceedings of the International Conference on Theoretical Aspects of Computer Software. TACS ’91. London, UK: Springer-Verlag, pp. 675–700.CrossRefGoogle Scholar
rHaskell. (2006) The constraint trick for instances [online]. Available at: https://www.reddit.com/r/haskell/comments/3afi3t/the_constraint_trick_for_instances/cscb33j/?st=jjcz7zeh&sh=1e5f3c8bGoogle Scholar
Rouvoet, A. (2016) Programs for Free: Towards the Formalization of Implicit Resolution in Scala. M.Phil. Thesis. TU Delft, the Netherlands.Google Scholar
Scharli, N., Ducasse, S., Nierstrasz, O. & Black, A. P. (2003) Traits: Composable units of behaviour. In European Conference on Object-Oriented Programming (ECOOP 2003). Springer, pp. 248–274.CrossRefGoogle Scholar
Schrijvers, T., Peyton Jones, S. L., Chakravarty, M. & Sulzmann, M. (2008) Type checking with open type functions. In ICFP. New York: ACM.Google Scholar
Siek, J. G. (2011) The C++0x “Concepts”˙I Effort [online]. Available at: http://ecee.colorado.edu/~siek/concepts_effort.pdfGoogle Scholar
Siek, J. G. & Lumsdaine, A. (2005) Essential language support for generic programming. In PLDI. New York: ACM, pp. 73–84.Google Scholar
Sozeau, M. & Oury, N. (2008) First-class type classes. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs ’08), Ait Mohamed, O., Muñoz, C. & Tahar, S. (eds), Berlin, Heidelberg: Springer-Verlag, pp. 278–293.CrossRefGoogle Scholar
Sulzmann, M., Duck, G., Peyton Jones, S. L. & Stuckey, P. J. (2007) Understanding functional dependencies via Constraint Handling Rules. J. Funct. Program. 17, 83–129.CrossRefGoogle Scholar
Vytiniotis, D., Peyton Jones, S., Schrijvers, T. & Suzmann, M. (2011) OutsideIn(X): Modular type inference with local assumptions. J. Funct. Program. 21(4–5), 333–412.CrossRefGoogle Scholar
Vytiniotis, D., Weirich, S. & Peyton Jones, S. (2008) FPH: First-class polymorphism for Haskell. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. ICFP ’08, ACM, pp. 295–306.CrossRefGoogle Scholar
Wadler, P. (2015) Propositions as types. Commun. ACM 58(12), 75–84.CrossRefGoogle Scholar
Wadler, P. L. & Blott, S. (1989) How to make ad-hoc polymorphism less ad hoc. In POPL. New York: ACM, pp. 60–76.Google Scholar
Wehr, S., Lämmel, R. & Thiemann, P. (2007) JavaGI: Generalized interfaces for java. In ECOOP, Springer Verlag, pp. 347–372.Google Scholar
White, L., Bour, F. & Yallop, J. (2014) Modular implicits. In Proceedings ML Family/OCaml Users and Developers Workshops, ML/OCaml 2014, Kiselyov, O. & Garrigue, J. (eds), Gothenburg, Sweden, September 4–5, 2014. EPTCS, pp. 22–63, vol. 198.Google Scholar
Zhang, E. (2014) Type classes: Confluence, coherence and global uniqueness [online]. Available at: http://blog.ezyang.com/2014/07/type-classes-confluence-coherence-global-/uniqueness/Google Scholar
Zhang, Y., Loring, M. C., Salvaneschi, G., Liskov, B. & Myers, A. C. (2015). Lightweight, flexible object-oriented generics. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, ACM, pp. 436–445.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.