Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/2003476.2003487acmotherconferencesArticle/Chapter ViewAbstractPublication PagesppdpConference Proceedingsconference-collections
research-article

Minimally strict polymorphic functions

Published: 20 July 2011 Publication History

Abstract

In this paper we show how to efficiently check whether a polymorphic function is minimally strict. A function is minimally strict if it is the minimal element of a specific less-strict ordering. We prove that we can check whether two polymorphic functions are related by the less-strict ordering by either checking it a) for an arbitrary monomorphic instance of the functions or b) for all shapes of the functions' argument type. A shape is a value of a monomorphic instance of a polymorphic data type where each polymorphic component is replaced by an element that identifies its position in the data structure. In contrast to recent publications that characterize polymorphic functions by monomorphic instances we consider non-termination and selective strictness, ie a language closer to Haskell.

References

[1]
J.-P. Bernardy, P. Jansson, and K. Claessen. Testing Polymorphic Properties. In ESOP'10 Proceedings, volume 6012, pages 125--144. Springer, 2010.
[2]
S. Böhme. Free Theorems for sublanguages of Haskell, 2007. Master's thesis, Technische Universität Dresden.
[3]
A. Bundy and J. Richardson. Proofs About Lists Using Ellipsis. In Logic for Programming and Automated Reasoning, volume 1705, pages 1--12. Springer, 1999.
[4]
J. Christiansen. Sloth - A Tool for Checking Minimal Strictness. In PADL'11 Proceedings, volume 6539, pages 160--174. Springer, 2011.
[5]
N. A. Danielsson and P. Jansson. Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values. In MPC'04 Proceedings, volume 3125, pages 85--109. Springer, 2004.
[6]
P. Johann and J. Voigtländer. Free Theorems in the Presence of seq. In POPL'04 Proceedings, pages 99--110. ACM, 2004.
[7]
J. P. Magalhães, A. Dijkstra, J. Jeuring, and A. Löh. A generic deriving mechanism for Haskell. In Haskell Symposium Proceedings, pages 37--48. ACM, 2010.
[8]
S. Peyton Jones, editor. Haskell 98 Language and Libraries--The Revised Report. Cambridge University Press, 2003.
[9]
R. Prince, N. Ghani, and C. McBride. Proving Properties about Lists Using Containers. In FLOPS'08 Proceedings, volume 4989, pages 97--112. Springer, 2008.
[10]
D. Seidel and J. Voigtländer. Taming Selective Strictness. In ATPS'09 Proceedings. GI, 2009.
[11]
J. Voigtländer. Bidirectionalization for Free! In POPL'09 Proceedings, pages 165--176. ACM, 2009.
[12]
P. Wadler. Theorems for free! In FPCA'89 Proceedings. ACM, 1989.\endthebibliography

Cited By

View all
  • (2021)Reasoning about the garden of forking pathsProceedings of the ACM on Programming Languages10.1145/34735855:ICFP(1-28)Online publication date: 19-Aug-2021

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences
PPDP '11: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming
July 2011
202 pages
ISBN:9781450307765
DOI:10.1145/2003476
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]

Sponsors

  • University of Southern Denmark
  • Danish Agency for Science Technology and Innovation: DASTI

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 July 2011

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. free theorems
  2. generic programming
  3. less strictness
  4. parametricity
  5. polymorphism
  6. selective strictness
  7. testing

Qualifiers

  • Research-article

Conference

PPDP '11
Sponsor:
  • Danish Agency for Science Technology and Innovation

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2021)Reasoning about the garden of forking pathsProceedings of the ACM on Programming Languages10.1145/34735855:ICFP(1-28)Online publication date: 19-Aug-2021

View Options

Get Access

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media