More Web Proxy on the site http://driver.im/

research-article

Open access

Constrained type families

Authors:

J. Garrett Morris,

Richard A. EisenbergAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 1, Issue ICFP

Article No.: 42, Pages 1 - 28

https://doi.org/10.1145/3110286

Published: 29 August 2017 Publication History

Abstract

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

Supplementary Material

Auxiliary Archive (icfp17-main89-s.zip)

Our artifact for submission is the paper proof of the soundness of the System CFC presented in our paper. There is no implementation to evaluate, and we believe that our proof is straightforward enough to meet the criteria for the artifact evaluation process. The proof appears, in full, in this document. Although all the details necessary for the proof are herein, it may be helpful to read this alongside §6 of our submission, as that section introduces the reader to the type system described here.

Download
54.29 KB

References

[1]

Patrick Bahr. 2014. Composing and decomposing data types: a closed type families implementation of data types à la carte. In Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, WGP 2014, Gothenburg, Sweden, August 31, 2014, José Pedro Magalhães and Tiark Rompf (Eds.). ACM, 71–82.

Digital Library

[2]

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In Foundations of Software Science and Computational Structures (FOSSACS 2008), Roberto Amadio (Ed.). Springer Berlin Heidelberg, Budapest, Hungary, 365–379.

[3]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe Zero-cost Coercions for Haskell. J. Funct. Program. 26 (2016), 1–79.

[4]

Manuel M. T. Chakravarty, Gabriele Keller, and Simon L. Peyton Jones. 2005. Associated type synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, Olivier Danvy and Benjamin C. Pierce (Eds.). ACM, 241–253.

Digital Library

[5]

Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, and Gabriele Keller. 2007. Modular type classes. In Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’07). ACM, Nice, France, 63–70.

Digital Library

[6]

Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph.D. Dissertation. University of Pennsylvania.

[7]

Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. 2014. Closed Type Families with Overlapping Equations. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM, San Diego, California, USA, 671–683.

Digital Library

[8]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. 2016. Visible Type Application. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016 (Lecture Notes in Computer Science), Peter Thiemann (Ed.), Vol. 9632. Springer, 229–254.

Digital Library

[9]

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

[10]

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 (March 1996).

Digital Library

[11]

Thomas Hallgren. 2000. Fun with functional dependencies, or (draft) types as values in static computations in Haskell. http://www.cse.chalmers.se/~hallgren/Papers/wm01.html . (2000).

[12]

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

[13]

Mark P. Jones. 1995. 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.

Digital Library

[14]

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.

[15]

Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. 2004. Strongly typed heterogeneous collections. In Proceedings of the 2004 ACM SIGPLAN workshop on Haskell (Haskell ’04). ACM Press, Snowbird, Utah, USA, 96–107.

Digital Library

[16]

Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, Chris Hankin and Dave Schmidt (Eds.). ACM, 81–92.

Digital Library

[17]

Sam Lindley and J. Garrett Morris. 2016. Embedding session types in Haskell. In Proceedings of the 9th International Symposium on Haskell, Haskell 2016, Nara, Japan, September 22-23, 2016, Geoffrey Mainland (Ed.). ACM, 133–145.

Digital Library

[18]

Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures (FoSSaCS). Springer.

[19]

J. Garrett Morris. 2015. Variations on variants. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell (Haskell ’15), Ben Lippmeier (Ed.). ACM, Vancouver, BC, 71–81.

Digital Library

[20]

J. Garrett Morris and Mark P. Jones. 2010. Instance chains: Type-class programming without overlapping instances. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP ’10). ACM, Baltimore, MD.

Digital Library

[21]

Takayuki Muranushi and Richard A. Eisenberg. 2014. Experience report: Type-checking polymorphic units for astrophysics research in Haskell. In Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, Wouter Swierstra (Ed.). ACM, 31–38.

Digital Library

[22]

Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky. 2010. Type classes as objects and implicits. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA, William R. Cook, Siobhán Clarke, and Martin C. Rinard (Eds.). ACM, 341–360.

Digital Library

[23]

Simon Peyton Jones, Mark P. Jones, and Erik Meijer. 1997. Type classes: An exploration of the design space. In Proceedings of the 1997 workshop on Haskell (Haskell ’97). Amsterdam, The Netherlands.

[24]

Riccardo Pucella and Jesse A. Tov. 2008. Haskell session types with (almost) no class. In Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008. ACM, 25–36.

[25]

John C. Reynolds. 1974. Towards a theory of type structure. In Paris Colloquium on Programming. Springer-Verlag, 408–423.

[26]

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.

Digital Library

[27]

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.

[28]

Damien Sereni and Neil D. Jones. 2005. Termination Analysis of Higher-Order Functional Programs. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings (Lecture Notes in Computer Science), Kwangkeun Yi (Ed.), Vol. 3780. Springer, 281–297.

Digital Library

[29]

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, 118–128.

Digital Library

[30]

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.

Digital Library

[31]

Wouter Swierstra. 2008. Data types à la carte. JFP 18, 04 (2008), 423–436.

Digital Library

[32]

Matúš Tejiščák and Edwin Brady. 2015. Practical Erasure in Dependently Typed Languages. (2015). http://eb.host.cs. st- andrews.ac.uk/drafts/dtp- erasure- draft.pdf Draft.

[33]

Philip Wadler and Stephen Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’89). ACM, Austin, Texas, USA, 60–76.

Digital Library

[34]

Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon L. Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012. Giving Haskell a promotion. In Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012, Benjamin C. Pierce (Ed.). ACM, 53–66.

Digital Library

Cited By

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
Jones MMorris JEisenberg R(2019)Partial type constructors: or, making ad hoc datatypes less ad hocProceedings of the ACM on Programming Languages10.1145/33711084:POPL(1-28)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371108
Pauwels KKarachalias GDerhaeg MSchrijvers TEisenberg R(2019)Bidirectional type class instancesProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342596(30-43)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342596

Index Terms

Constrained type families
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

Type families with class, type classes with family
Haskell '15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell

Type classes and type families are key ingredients in Haskell programming. Type classes were introduced to deal with ad-hoc polymorphism, although with the introduction of functional dependencies, their use expanded to type-level programming. Type ...
Type families with class, type classes with family
Haskell '15

Type classes and type families are key ingredients in Haskell programming. Type classes were introduced to deal with ad-hoc polymorphism, although with the introduction of functional dependencies, their use expanded to type-level programming. Type ...
Closed type families with overlapping equations
POPL '14

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 1, Issue ICFP

September 2017

1173 pages

EISSN:2475-1421

DOI:10.1145/3136534

Issue’s Table of Contents

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 the author(s) 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: 29 August 2017

Published in PACMPL Volume 1, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
591
Total Downloads

Downloads (Last 12 months)64
Downloads (Last 6 weeks)8

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Jones MMorris JEisenberg R(2019)Partial type constructors: or, making ad hoc datatypes less ad hocProceedings of the ACM on Programming Languages10.1145/33711084:POPL(1-28)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371108
Pauwels KKarachalias GDerhaeg MSchrijvers TEisenberg R(2019)Bidirectional type class instancesProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342596(30-43)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342596

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents