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

research-article

Free theorems involving type constructor classes: functional pearl

Author:

Janis VoigtländerAuthors Info & Claims

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

Pages 173 - 184

https://doi.org/10.1145/1596550.1596577

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)

Download
10.00 KB

MP4 File (freetheoremsinvolvingtypeconstructorclassesonvimeo.mp4)

Download
80.49 MB

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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[5]

A. Filinski. On the relations between monadic semantics. Theoretical Computer Science, 375(1-3):41--75, 2007.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[15]

E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55--92, 1991.

Digital Library

[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.

Digital Library

[17]

S.L. Peyton Jones and P. Wadler. Imperative functional programming. In Principles of Programming Languages, Proceedings, pages 71--84. ACM Press, 1993.

Digital Library

[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.

Digital Library

[20]

W. Swierstra. Data types à la carte. Journal of Functional Programming, 18(4):423--436, 2008.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[26]

J. Voigtländer. Bidirectionalization for free! In Principles of Programming Languages, Proceedings, pages 165--176. ACM Press, 2009.

Digital Library

[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.

Digital Library

[29]

P. Wadler. The essence of functional programming (Invited talk). In Principles of Programming Languages, Proceedings, pages 1--14. ACM Press, 1992.

Digital Library

[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.

Digital Library

Cited By

TANG WSCHRIJVERS T(2025)From high to low: Simulating nondeterminism and state with stateJournal of Functional Programming10.1017/S095679682400013334Online publication date: 3-Jan-2025
https://doi.org/10.1017/S0956796824000133
Seynaeve WPauwels KSchrijvers T(2020)State Will doTrends in Functional Programming10.1007/978-3-030-57761-2_10(204-225)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_10
Devriese DEisenberg R(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
https://dl.acm.org/doi/10.1145/3331545.3342589
Show More Cited By

Index Terms

Free theorems involving type constructor classes: functional pearl
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
      2. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

Free theorems involving type constructor classes: functional pearl
ICFP '09

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 ...
A relationally parametric model of dependent type theory
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, ...
A relationally parametric model of dependent type theory
POPL '14

Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, ...

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

General Chair:
Graham Hutton
University of Nottingham
,
Program Chair:
Andrew Tolmach
Portland State University

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

Copyright © 2009 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

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

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
489
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

TANG WSCHRIJVERS T(2025)From high to low: Simulating nondeterminism and state with stateJournal of Functional Programming10.1017/S095679682400013334Online publication date: 3-Jan-2025
https://doi.org/10.1017/S0956796824000133
Seynaeve WPauwels KSchrijvers T(2020)State Will doTrends in Functional Programming10.1007/978-3-030-57761-2_10(204-225)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_10
Devriese DEisenberg R(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
https://dl.acm.org/doi/10.1145/3331545.3342589
Matsuda KWang M(2015)Applicative bidirectional programming with lensesACM SIGPLAN Notices10.1145/2858949.278475050:9(62-74)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784750
Matsuda KWang MFisher KReppy J(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
https://dl.acm.org/doi/10.1145/2784731.2784750
Wu NSchrijvers T(2015)Fusion for FreeMathematics of Program Construction10.1007/978-3-319-19797-5_15(302-322)Online publication date: 9-Jun-2015
https://doi.org/10.1007/978-3-319-19797-5_15
Bird RGibbons JMehner SVoigtländer JSchrijvers T(2013)Understanding idiomatic traversals backwards and forwardsACM SIGPLAN Notices10.1145/2578854.250378148:12(25-36)Online publication date: 23-Sep-2013
https://dl.acm.org/doi/10.1145/2578854.2503781
Delaware BKeuchel SSchrijvers TOliveira B(2013)Modular monadic meta-theoryACM SIGPLAN Notices10.1145/2544174.250058748:9(319-330)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500587
Matsuda KWang MPeña RSchrijvers T(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
https://dl.acm.org/doi/10.1145/2505879.2505888
Bird RGibbons JMehner SVoigtländer JSchrijvers TShan C(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
https://dl.acm.org/doi/10.1145/2503778.2503781
Show More Cited By

View Options

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.

Figures

Tables

Media

View Table of Conten