[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/1596550.1596577acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

Free theorems involving type constructor classes: functional pearl

Published: 31 August 2009 Publication History

Abstract

Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type constructors restricted by class constraints. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof.

Supplementary Material

JPG File (freetheoremsinvolvingtypeconstructorclassesonvimeo.jpg)
MP4 File (freetheoremsinvolvingtypeconstructorclassesonvimeo.mp4)

References

[1]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Domain-theoretical models of parametric polymorphism. Theoretical Computer Science, 388(1--3):152--172, 2007.
[2]
S. Böhme. Free theorems for sublanguages of Haskell. Master's thesis, Technische Universität Dresden, 2007.
[3]
N.A. Danielsson, R.J.M. Hughes, P. Jansson, and J. Gibbons. Fast and loose reasoning is morally correct. In Principles of Programming Languages, Proceedings, pages 206--217. ACM Press, 2006.
[4]
L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, Programs from outer space). In Principles of Programming Languages, Proceedings, pages 284--294. ACM Press, 1996.
[5]
A. Filinski. On the relations between monadic semantics. Theoretical Computer Science, 375(1-3):41--75, 2007.
[6]
A. Filinski and K. Støvring. Inductive reasoning about effectful data types. In International Conference on Functional Programming, Proceedings, pages 97--110. ACM Press, 2007.
[7]
A. Gill, J. Launchbury, and S.L. Peyton Jones. A short cut to deforestation. In Functional Programming Languages and Computer Architecture, Proceedings, pages 223--232. ACM Press, 1993.
[8]
R.J.M. Hughes. A novel representation of lists and its application to the function "reverse". Information Processing Letters, 22(3):141--144, 1986.
[9]
G. Hutton and D. Fulger. Reasoning about effects: Seeing the wood through the trees. In Trends in Functional Programming, Draft Proceedings, 2008.
[10]
P. Johann and J. Voigtländer. Free theorems in the presence of seq. In Principles of Programming Languages, Proceedings, pages 99--110. ACM Press, 2004.
[11]
J. Kuan. Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS Transform and "Free Theorems". PhD thesis, Massachusetts Institute of Technology, 1997.
[12]
J. Launchbury and S.L. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293--341, 1995.
[13]
S. Liang, P. Hudak, and M.P. Jones. Monad transformers and modular interpreters. In Principles of Programming Languages, Proceedings, pages 333--343. ACM Press, 1995.
[14]
J.C. Mitchell and A.R. Meyer. Second--order logical relations (Extended abstract). In Logic of Programs, Proceedings, volume 193 of LNCS, pages 225--236. Springer--Verlag, 1985.
[15]
E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55--92, 1991.
[16]
A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In International Conference on Functional Programming, Proceedings, pages 229--240. ACM Press, 2008.
[17]
S.L. Peyton Jones and P. Wadler. Imperative functional programming. In Principles of Programming Languages, Proceedings, pages 71--84. ACM Press, 1993.
[18]
J.C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, Proceedings, pages 513--523. Elsevier, 1983.
[19]
F. Stenger and J. Voigtländer. Parametricity for Haskell with imprecise error semantics. In Typed Lambda Calculi and Applications, Proceedings, volume 5608 of LNCS, pages 294--308. Springer-Verlag, 2009.
[20]
W. Swierstra. Data types à la carte. Journal of Functional Programming, 18(4):423--436, 2008.
[21]
W. Swierstra and T. Altenkirch. Beauty in the beast -- A functional semantics for the awkward squad. In Haskell Workshop, Proceedings, pages 25--36. ACM Press, 2007.
[22]
I. Takeuti. The theory of parametricity in lambda cube. Manuscript, 2001.
[23]
J. Voigtländer. Concatenate, reverse and map vanish for free. In International Conference on Functional Programming, Proceedings, pages 14--25. ACM Press, 2002.
[24]
J. Voigtländer. Asymptotic improvement of computations over free monads. In Mathematics of Program Construction, Proceedings, volume 5133 of LNCS, pages 388--403. Springer-Verlag, 2008a.
[25]
J. Voigtländer. Much ado about two: A pearl on parallel prefix computation. In Principles of Programming Languages, Proceedings, pages 29--35. ACM Press, 2008b.
[26]
J. Voigtländer. Bidirectionalization for free! In Principles of Programming Languages, Proceedings, pages 165--176. ACM Press, 2009.
[27]
D. Vytiniotis and S. Weirich. Type-safe cast does no harm: Syntactic parametricity for F-omega and beyond. Manuscript, 2009.
[28]
P. Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, Proceedings, pages 347--359. ACM Press, 1989.
[29]
P. Wadler. The essence of functional programming (Invited talk). In Principles of Programming Languages, Proceedings, pages 1--14. ACM Press, 1992.
[30]
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Principles of Programming Languages, Proceedings, pages 60--76. ACM Press, 1989.

Cited By

View all
  • (2025)From high to low: Simulating nondeterminism and state with stateJournal of Functional Programming10.1017/S095679682400013334Online publication date: 3-Jan-2025
  • (2020)State Will doTrends in Functional Programming10.1007/978-3-030-57761-2_10(204-225)Online publication date: 18-Aug-2020
  • (2019)Modular effects in Haskell through effect polymorphism and explicit dictionary applications: a new approach and the μVeriFast verifier as a case studyProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342589(1-14)Online publication date: 8-Aug-2019
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming
August 2009
364 pages
ISBN:9781605583327
DOI:10.1145/1596550
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 44, Issue 9
    ICFP '09
    September 2009
    343 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1631687
    Issue’s Table of Contents
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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Permissions

Request permissions for this article.

Check for updates

Author Tag

  1. relational parametricity

Qualifiers

  • Research-article

Conference

ICFP '09
Sponsor:
ICFP '09: ACM SIGPLAN International Conference on Functional Programming
August 31 - September 2, 2009
Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 25 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)From high to low: Simulating nondeterminism and state with stateJournal of Functional Programming10.1017/S095679682400013334Online publication date: 3-Jan-2025
  • (2020)State Will doTrends in Functional Programming10.1007/978-3-030-57761-2_10(204-225)Online publication date: 18-Aug-2020
  • (2019)Modular effects in Haskell through effect polymorphism and explicit dictionary applications: a new approach and the μVeriFast verifier as a case studyProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342589(1-14)Online publication date: 8-Aug-2019
  • (2015)Applicative bidirectional programming with lensesACM SIGPLAN Notices10.1145/2858949.278475050:9(62-74)Online publication date: 29-Aug-2015
  • (2015)Applicative bidirectional programming with lensesProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784750(62-74)Online publication date: 29-Aug-2015
  • (2015)Fusion for FreeMathematics of Program Construction10.1007/978-3-319-19797-5_15(302-322)Online publication date: 9-Jun-2015
  • (2013)Understanding idiomatic traversals backwards and forwardsACM SIGPLAN Notices10.1145/2578854.250378148:12(25-36)Online publication date: 23-Sep-2013
  • (2013)Modular monadic meta-theoryACM SIGPLAN Notices10.1145/2544174.250058748:9(319-330)Online publication date: 25-Sep-2013
  • (2013)Bidirectionalization for free with runtime recordingProceedings of the 15th Symposium on Principles and Practice of Declarative Programming10.1145/2505879.2505888(297-308)Online publication date: 16-Sep-2013
  • (2013)Understanding idiomatic traversals backwards and forwardsProceedings of the 2013 ACM SIGPLAN symposium on Haskell10.1145/2503778.2503781(25-36)Online publication date: 23-Sep-2013
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media