article

Quantified class constraints

Authors:

Gert-Jan Bottu,

Georgios Karachalias,

Tom Schrijvers,

Bruno C. d. S. Oliveira,

Philip WadlerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 10

Pages 148 - 161

https://doi.org/10.1145/3156695.3122967

Published: 07 September 2017 Publication History

Abstract

Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to the universal fragment of Hereditiary Harrop logic. Yet, while it has been much asked for over the years, the feature was never implemented or studied in depth. Instead, several workarounds have been proposed, all of which are ultimately stopgap measures.

This paper revisits the idea of quantified class constraints and elaborates it into a practical language design. We show the merit of quantified class constraints in terms of more expressive modeling and in terms of terminating type class resolution. In addition, we provide a declarative specification of the type system as well as a type inference algorithm that elaborates into System F. Moreover, we discuss termination conditions of our system and also provide a prototype implementation.

References

[1]

Jean-marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2 (1992), 297–347.

[2]

Richard S. Bird and Lambert G. L. T. Meertens. 1998. Nested Datatypes. In MPC ’98 . Springer, 52–67.

Digital Library

[3]

Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005. Associated Type Synonyms. SIGPLAN Not. 40, 9 (2005), 241–253.

Digital Library

[4]

Satvik Chauhan, Piyush P. Kurur, and Brent A. Yorgey. 2016. How to Twist Pointers Without Breaking Them. In Haskell 2016. ACM, 51–61.

Digital Library

[5]

Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In POPL ’82. ACM, 207–212.

Digital Library

[6]

Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, and Andrew Pond. 2016. Proof Relevant Corecursive Resolution. In FLOPS 2016. Springer, 126–143.

[7]

Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and Types. Cambridge University Press.

Digital Library

[8]

Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. 1996. Type Classes in Haskell. ACM TOPLAS 18, 2 (1996), 109–138.

Digital Library

[9]

Ronald Harrop. 1956. On disjunctions and existential statements in intuitionistic systems of logic. Math. Ann. 132, 4 (1956), 347–361.

[10]

Ralf Hinze. 2000. Perfect trees and bit-reversal permutations. JFP 10, 3 (2000), 305–317.

Digital Library

[11]

Ralf Hinze. 2010. Adjoint Folds and Unfolds: Or: Scything Through the Thicket of Morphisms. In MPC’10. Springer, 195–228.

Digital Library

[12]

Ralf Hinze and Simon Peyton Jones. 2000. Derivable Type Classes. In Proceedings of the Fourth Haskell Workshop . Elsevier Science, 227–236.

[13]

Mauro Jaskelioff. 2011. Monatron: an extensible monad transformer library. In IFL’08 . Springer, Berlin, Heidelberg, 233–248.

Digital Library

[14]

Mark P. Jones. 1992. A theory of qualified types. In ESOP ’92, Bernd KriegBrückner (Ed.). LNCS, Vol. 582. Springer Berlin Heidelberg, 287–306.

Digital Library

[15]

Mark P. Jones. 1995. Functional Programming with Overloading and HigherOrder Polymorphism. In Advanced Functional Programming. Springer, 97–136.

Digital Library

[16]

Mark P. Jones. 1995. Qualified Types: Theory and Practice. Cambridge University Press.

Digital Library

[17]

Mark P. Jones. 1995. Simplifying and Improving Qualified Types. In FPCA ’95. ACM, 160–169.

Digital Library

[18]

Mark P. Jones. 2000. Type Classes with Functional Dependencies. In Programming Languages and Systems . LNCS, Vol. 1782. Springer Berlin Heidelberg, 230–244.

Digital Library

[19]

Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: an exploration of the design space. In Proceedings of the 1997 Haskell Workshop. ACM.

[20]

Edward A. Kmett. 2017. The constraint package. (2017). https://hackage.haskell. org/package/constraints-0.9.1 .

[21]

Ralf Lämmel and Simon Peyton Jones. 2003. Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming. SIGPLAN Not. 38, 3 (2003), 26–37.

Digital Library

[22]

Ralf Lämmel and Simon Peyton Jones. 2005. Scrap Your Boilerplate with Class: Extensible Generic Functions. SIGPLAN Not. 40, 9 (2005), 204–215.

Digital Library

[23]

Chuck Liang and Dale Miller. 2009. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theor. Comput. Sci. 410, 46 (2009), 4747–4768.

Digital Library

[24]

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1989. Uniform Proofs As a Foundation for Logic Programming . Technical Report.

Digital Library

[25]

J. Garrett Morris. 2014. A Simple Semantics for Haskell Overloading. SIGPLAN Not. 49, 12 (2014), 107–118.

Digital Library

[26]

Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. 2010. Type Classes As Objects and Implicits. SIGPLAN Not. 45, 10 (2010), 341–360.

Digital Library

[27]

Bruno C.d.S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi. 2012. The Implicit Calculus: A New Foundation for Generic Programming. SIGPLAN Not. 47, 6 (2012), 35–44.

Digital Library

[28]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical Type Inference for Arbitrary-rank Types. JFP 17, 1 (2007).

Digital Library

[29]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple Unification-based Type Inference for GADTs. SIGPLAN Not. 41, 9 (2006), 50–61.

Digital Library

[30]

Frank Pfenning. 2010. Lecture Notes on Focusing. (2010). https://www.cs.cmu. edu/~fp/courses/oregon-m10/04-focusing.pdf .

[31]

Tom Schrijvers and Bruno C.d.S. Oliveira. 2011. Monads, Zippers and Views: Virtualizing the Monad Stack. SIGPLAN Not. 46, 9 (2011), 32–44.

Digital Library

[32]

Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Cochis: Deterministic and Coherent Implicits . Report CW 705. KU Leuven.

[33]

Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In TPHOLs 2008 (LNCS), Vol. 5170. Springer, 278–293.

Digital Library

[34]

Mike Spivey. 2017. Faster Coroutine Pipelines. In ICFP 2017. accepted.

Digital Library

[35]

Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey. 2007. Understanding Functional Dependencies via Constraint Handling Rules. JFP 17, 1 (2007), 83–129.

Digital Library

[36]

Valery Trifonov. 2003. Simulating Quantified Class Constraints. In Haskell ’03. ACM, 98–102.

Digital Library

[37]

Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. 2010. Let Should Not Be Generalized. In TLDI ’10. ACM, 39–50.

Digital Library

[38]

P. Wadler and S. Blott. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc. In POPL ’89. ACM, 60–76.

Digital Library

Cited By

Marntirosian KSchrijvers TOliveira BKarachalias G(2020)Resolution as intersection subtyping via Modus PonensProceedings of the ACM on Programming Languages10.1145/34282744:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428274
Xia LOrchard DWang M(2019)Composing Bidirectional Programs MonadicallyProgramming Languages and Systems10.1007/978-3-030-17184-1_6(147-175)Online publication date: 6-Apr-2019
https://doi.org/10.1007/978-3-030-17184-1_6
Prott KTeegen FChristiansen J(2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_3
Show More Cited By

Index Terms

Quantified class constraints
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Quantified class constraints
Haskell 2017: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell

Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to the universal fragment of Hereditiary Harrop logic. Yet, while it has been much asked for over the years, the feature was ...
Type classes with more higher-order polymorphism

We propose an extension of Haskell's type class system with lambda abstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure ...
Type classes with more higher-order polymorphism
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

We propose an extension of Haskell's type class system with lambda abstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 10

Haskell '17

October 2017

211 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3156695

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

Haskell 2017: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell
September 2017
211 pages
ISBN:9781450351829
DOI:10.1145/3122955
General Chair:
Iavor Diatchki

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 September 2017

Published in SIGPLAN Volume 52, Issue 10

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
207
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)2

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Marntirosian KSchrijvers TOliveira BKarachalias G(2020)Resolution as intersection subtyping via Modus PonensProceedings of the ACM on Programming Languages10.1145/34282744:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428274
Xia LOrchard DWang M(2019)Composing Bidirectional Programs MonadicallyProgramming Languages and Systems10.1007/978-3-030-17184-1_6(147-175)Online publication date: 6-Apr-2019
https://doi.org/10.1007/978-3-030-17184-1_6
Prott KTeegen FChristiansen J(2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
https://doi.org/10.1007/978-3-031-24841-2_3
Spiwack AKiss CBernardy JWu NEisenberg R(2022)Linearly qualified types: generic inference for capabilities and uniquenessProceedings of the ACM on Programming Languages10.1145/35476266:ICFP(137-164)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547626
Ingle AHubers AMorris JPolikarpova N(2022)Partial type constructors in practiceProceedings of the 15th ACM SIGPLAN International Haskell Symposium10.1145/3546189.3549923(95-107)Online publication date: 6-Sep-2022
https://dl.acm.org/doi/10.1145/3546189.3549923
Karimov TLefaucheux EOuaknine JPurser DVaronka AWhiteland MWorrell J(2022)What’s decidable about linear loops?Proceedings of the ACM on Programming Languages10.1145/34987276:POPL(1-25)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498727
Hou (Favonia) KWang Z(2022)Logarithm and program testingProceedings of the ACM on Programming Languages10.1145/34987266:POPL(1-26)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498726
Xie NPickering MLöh AWu NYallop JWang M(2022)Staging with class: a specification for typed template HaskellProceedings of the ACM on Programming Languages10.1145/34987236:POPL(1-30)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498723
K HShoham SGurfinkel A(2022)Solving constrained Horn clauses modulo algebraic data types and recursive functionsProceedings of the ACM on Programming Languages10.1145/34987226:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498722
Gäher LSammler MSpies SJung RDang HKrebbers RKang JDreyer D(2022)Simuliris: a separation logic framework for verifying concurrent program optimizationsProceedings of the ACM on Programming Languages10.1145/34986896:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498689
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents