Cited By
View all- Gordon C(2021)Polymorphic Iterable Sequential Effect SystemsACM Transactions on Programming Languages and Systems10.1145/345027243:1(1-79)Online publication date: Apr-2021
Partial type constructors: or, making ad hoc datatypes less ad hoc
Article No.: 40, Pages 1 - 28
Abstract
Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.
Supplementary Material
WEBM File (a40-jones.webm)
- Download
- 87.20 MB
References
[1]
Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Quantified Class Constraints. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017). ACM, New York, NY, USA, 148–161.
[2]
Ana Bove, Alexander Krauss, and Matthieu Sozeau. 2016. Partiality and recursion in interactive theorem provers - an overview. Mathematical Structures in Computer Science 26, 1 (2016), 38–88.
[3]
Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. 1998. Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA ’98), Vancouver, British Columbia, Canada, October 18-22, 1998. ACM, Vancouver, British Columbia, Canada, 183–200.
[4]
Luca Cardelli and Peter Wegner. 1985. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17, 4 (Dec 1985), 471–523.
[5]
Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. 2005. Associated types with class. In Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’05). ACM, Long Beach, California, USA, 1–13.
[6]
James Cheney and Ralf Hinze. 2003. First-class Phantom Types. Technical Report TR1901. Cornell University.
[7]
Alonzo Church. 1940. A Formulation of the Simple Theory of Types. J. Symb. Log. 5, 2 (1940), 56–68.
[8]
Gabriel Dos Reis and Bjarne Stroustrup. 2006. Specifying C++ Concepts. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). ACM, New York, NY, USA, 295–308.
[9]
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Making a Faster Curry with Extensional Types. In Proceedings of the 12th ACM SIGPLAN Haskell Symposium (Haskell ’19). ACM, Berlin, Germany.
[10]
Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, and Gabriele Keller. 2007. Modular type classes. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, Martin Hofmann and Matthias Felleisen (Eds.). ACM, 63–70.
[11]
Benedict R. Gaster and Mark P. Jones. 1996. A Polymorphic Type System for Extensible Records and Variants. Technical Report NOT TCS-TR-96-3. University of Nottingham.
[12]
GHC Team. 2017. GHC User’s Guide Documentation. http://www.haskell.org/ghc/docs/latest/users_guide.pdf .
[13]
Paul Hudak, Simon Peyton Jones, and Philip Wadler (Eds.). 1991. Report on the Programming Language Haskell, Version 1.1. Available from http://haskell.org/definition/haskell- report- 1.1.tar.gz .
[14]
Paul Hudak and Philip Wadler (Eds.). 1990. Report on the Programming Language Haskell, Version 1.0. Available from http://haskell.org/definition/haskell- report- 1.0.ps.gz .
[15]
Brian Charles Huffman. 2012. HOLCF’11: A Definitional Domain Theory for Verifying Functional Programs. Ph.D. Dissertation. Portland State University, Portland, OR, USA. Advisor(s) Hook, James G. and Matthews, John.
[16]
John Hughes. 1999. Restricted Data Types in Haskell. In Proceedings of the 1999 Haskell Workshop. University of Utrecht, Technical Report UU-CS-1999-28, Paris, France, 83–100.
[17]
Mark P. Jones. 1993a. Coherence for qualified types. Technical Report YALEU/DCS/RR-989. Yale University.
[18]
Mark P. Jones. 1993b. A system of constructor classes: overloading and implicit higher-order polymorphism. In Conference on Functional Programming and Computer Architecture (FPCA ’93). ACM, Copenhagen, Denmark, 52–61.
[19]
Mark P. Jones. 1994. Qualified Types: Theory and Practice. Cambridge University Press, Cambridge, UK.
[20]
Mark P. Jones. 1995a. Functional Programming with Overloading and Higher-Order Polymorphism. In First International Spring School on Advanced Functional Programming Techniques (Lecture Notes in Computer Science), Vol. 925. Springer, Berlin Heidelberg, 97–136.
[21]
Mark P. Jones. 1995b. Simplifying and improving qualified types. In Proceedings of the seventh international conference on Functional programming languages and computer architecture (FPCA ’95). ACM, La Jolla, California, USA, 160–169.
[22]
Mark P. Jones. 2000. Type Classes with Functional Dependencies. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP ’00). Springer-Verlag, Berlin, Germany, 230–244.
[23]
Oleg Kiselyov. 2007. Haskell with only one type class. http://okmij.org/ftp/Haskell/Haskell1/Haskell1.txt .
[24]
Csongor Kiss, Tony Field, Susan Eisenbach, and Simon Peyton Jones. 2019. Higher-order Type-level Programming in Haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP ’19). ACM, Berlin, Germany.
[25]
John Launchbury and Ross Paterson. 1996. Parametricity and Unboxing with Unpointed Types. In Proceedings of the 6th European Symposium on Programming Languages and Systems (ESOP ’96). Springer-Verlag, London, UK, UK, 204–218. http://dl.acm.org/citation.cfm?id=645391.651452
[26]
Simon Marlow (Ed.). 2010. Haskell 2010 Language Report. Available online in HTML and pdf formats from https: //www.haskell.org/documentation .
[27]
Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Generics of a Higher Kind. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications (OOPSLA ’08). ACM, New York, NY, USA, 423–438.
[28]
J. Garrett Morris and Richard A. Eisenberg. 2017. Constrained Type Families. Proc. ACM Program. Lang. 1, ICFP, Article 42 (Aug. 2017), 28 pages.
[29]
J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name. PACMPL 3, POPL (2019), 12:1–12:28. https://dl.acm.org/citation.cfm?id=3290325
[30]
Dominic Orchard and Tom Schrijvers. 2010. Haskell Type Constraints Unleashed. In Proceedings of the 10th International Conference on Functional and Logic Programming (FLOPS’10). Springer-Verlag, Berlin, Heidelberg, 56–71.
[31]
Anders Persson, Emil Axelsson, and Josef Svenningsson. 2011. Generic Monadic Constructs for Embedded Languages. In Implementation and Application of Functional Languages - 23rd International Symposium, IFL 2011, Lawrence, KS, USA, October 3-5, 2011, Revised Selected Papers (Lecture Notes in Computer Science), Andy Gill and Jurriaan Hage (Eds.), Vol. 7257. Springer, 85–99.
[32]
Simon Peyton Jones. 1991. Contexts in data and type. http://code.haskell.org/~dons/haskell- 1990- 2000/msg00072.html .
[33]
Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. 2008. Type checking with open type functions. In Proceeding of the 13th ACM SIGPLAN international conference on Functional programming (IFCP ’08). ACM, Victoria, BC, Canada, 51–62.
[34]
Tom Schrijvers, Simon L. Peyton Jones, Martin Sulzmann, and Dimitrios Vytiniotis. 2009. Complete and decidable type inference for GADTs. In Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, Graham Hutton and Andrew P. Tolmach (Eds.). ACM, 341–352.
[35]
Dana Scott. 1979. Identity and existence in intuitionistic logic. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, Michael Fourman, Christopher Mulvey, and Dana Scott (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 660–696.
[36]
Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. 2013. The Constrained-monad Problem. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). ACM, New York, NY, USA, 287–298.
[37]
Jan Stolarek, Simon L. Peyton Jones, and Richard A. Eisenberg. 2015. Injective type families for Haskell. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, Ben Lippmeier (Ed.). ACM, Vancouver, BC, Canada, 118–128.
[38]
Bjarne Stroustrup. 1994. The Design and Evolution of C++. Addison-Wesley, Boston, MA.
[39]
Sandro Stucki. 2017. Higher-Order Subtyping with Type Intervals. Ph.D. Dissertation. School of Computer and Communication Sciences, École polytechnique fédérale de Lausanne, Lausanne, Switzerland.
[40]
Martin Sulzmann, Manuel M. T. Chakravarty, Simon L. Peyton Jones, and Kevin Donnelly. 2007. System F with type equality coercions. In Proceedings of TLDI’07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007, François Pottier and George C. Necula (Eds.). ACM, 53–66.
[41]
Josef Svenningsson and Bo Joel Svensson. 2013. Simple and compositional reification of monadic embedded languages. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 299–304.
[42]
Thomas Winant, Dominique Devriese, Frank Piessens, and Tom Schrijvers. 2014. Partial Type Signatures for Haskell. In Practical Aspects of Declarative Languages, Vol. 8324. Springer International Publishing, 17–32.
[43]
Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94.
[44]
Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded Recursive Datatype Constructors. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’03). ACM, New York, NY, USA, 224–235.
Index Terms
- Partial type constructors: or, making ad hoc datatypes less ad hoc
Recommendations
Partial type constructors in practice
Haskell 2022: Proceedings of the 15th ACM SIGPLAN International Haskell SymposiumType constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only ...
Parametric Subtyping for Structural Parametric Polymorphism
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then ...
Polymorphic algebraic data type reconstruction
PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programmingOne of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2019 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 December 2019
Published in PACMPL Volume 4, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 1,267Total Downloads
- Downloads (Last 12 months)132
- Downloads (Last 6 weeks)10
Reflects downloads up to 01 Oct 2024
Other Metrics
Citations
Cited By
View all- Gordon C(2021)Polymorphic Iterable Sequential Effect SystemsACM Transactions on Programming Languages and Systems10.1145/345027243:1(1-79)Online publication date: Apr-2021
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.
Sign in