research-article

The power of Pi

Authors:

Wouter SwierstraAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 9

Pages 39 - 50

https://doi.org/10.1145/1411203.1411213

Published: 20 September 2008 Publication History

Abstract

This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates particular design patterns inherent to dependently-typed programming. Documenting these techniques paves the way for further research in domain-specific embedded type systems.

References

[1]

Lennart Augustsson and Magnus Carlsson. An exercise in dependent types: a well-typed interpreter. Unpublished manuscript.

[2]

Godmar Back. Datascript - a specification and scripting language for binary data. In GPCE '02: Proceedings of the 1st ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, 2002.

Digital Library

[3]

Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. Lava: Hardware design in Haskell. In ICFP '98: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, 1998.

Digital Library

[4]

Björn Bringert, Anders Höckersten, Conny Andersson, Martin Andersson, Mary Bergman, Victor Blomqvist, and Torbjörn Martin. Student paper: HaskellDB improved. In Haskell '04: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, 2004.

Digital Library

[5]

Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of Haskell programs. In ICFP '00: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, 2000.

Digital Library

[6]

Conal Elliott and Paul Hudak. Functional reactive animation. In ICFP '97: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming, 1997.

Digital Library

[7]

Kathleen Fisher and Robert Gruber. PADS: a domain-specific language for processing ad hoc data. SIGPLAN Conference on Programming Language Design and Implementation, 2005.

Digital Library

[8]

Kathleen Fisher, Yitzhak Mandelbaum, and David Walker. The next 700 data description languages. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006.

Digital Library

[9]

Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the SIGPLAN '91 Symposium on Language Design and Implementation, 1991.

Digital Library

[10]

Galois, Inc. Cryptol Reference Manual, 2002.

[11]

Ralf Hinze and Johan Jeuring. Generic Haskell: Practice and theory. In Generic Programming, volume 2793 of Lecture Notes in Computer Science. Springer-Verlag, 2003.

[12]

Graham Hutton and Erik Meijer. Monadic parsing in Haskell. Journal of Functional Programming, 8 (4), 1998.

Digital Library

[13]

Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. Strongly typed heterogeneous collections. In Haskell '04: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, 2004.

Digital Library

[14]

Daan Leijen and Erik Meijer. Domain specific embedded compilers. In 2nd USENIX Conference on Domain Specific Languages (DSL'99), October 1999.

Digital Library

[15]

Daan Leijen and Erik Meijer. Parsec: Direct style monadic parser combinators for the real world. Technical Report UU-CS-2001-27, Universiteit Utrecht, 2001.

[16]

Conor McBride. Epigram: Practical programming with dependent types. In Advanced Functional Programming, volume 3622 of LNCS-Tutorial, pages 130--170. Springer-Verlag, 2004.

Digital Library

[17]

Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14 (1), 2004.

Digital Library

[18]

Peter J. McCann and Satish Chandra. Packet types: abstract specification of network protocol messages. In SIGCOMM '00: Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, 2000.

Digital Library

[19]

James McKinna and Joel Wright. A type-correct, stack-safe, provably correct expression compiler in Epigram. Accepted for publication in the Journal of Functional Programming.

[20]

Peter Morris, Thorsten Altenkirch, and Conor McBride. Exploring the regular tree types. In Types for Proofs and Programs, volume 3839 of LNCS. Springer-Verlag, 2004.

Digital Library

[21]

Henrik Nilsson, Antony Courtney, and John Peterson. Functional reactive programming, continued. In Haskell '02: Proceedings of the 2002 ACM SIGPLAN Haskell Workshop, 2002.

Digital Library

[22]

Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990.

[23]

Ulf Norell. Towards a practical programming language based on dependent type theory. D thesis, Chalmers University of Technology, 2007.

[24]

Simon Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.

[25]

Simon Peyton Jones, Jean-Marc Eber, and Julian Seward. Composing contracts: an adventure in financial engineering. In ICFP '00: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, 2000.

Digital Library

[26]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In ICFP '06: Proceedings of the eleventh ACM SIGPLAN International Conference on Functional Programming, 2006.

Digital Library

[27]

Tim Sheard. Putting Curry-Howard to work. In Haskell '05: Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, 2005.

Digital Library

[28]

Matthieu Sozeau. Subset coercions in Coq. In Types for Proofs and Programs, volume 4502 of LNCS. Springer-Verlag, 2007.

Digital Library

[29]

S. Doaitse Swierstra and Luc Duponcheel. Deterministic, error-correcting combinator parsers. In Advanced Functional Programming, volume 1129 of LNCS-Tutorial, 1996.

Digital Library

[30]

Wouter Swierstra and Thorsten Altenkirch. Dependent types for distributed arrays. In Proceedings of the Ninth Symposium on Trends in Functional Programming, 2008.

[31]

The Agda Team. Agda homepage. http://www.cs.chalmers.se/~ulfn/Agda, 2008.

[32]

Peter Thiemann. Server-side web programming in WASH. In Advanced Functional Programming, volume 3622 of LNCS-Tutorial. Springer-Verlag, 2004.

Digital Library

[33]

Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In 14th Symposium on Principles of Programming Languages, 1987.

Digital Library

Cited By

van Geest MSwierstra WLindley SYorgey B(2017)Generic packet descriptions: verified parsing and pretty printing of low-level dataProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122979(30-40)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122979
Cai YGiarrusso POstermann K(2016)System f-omega with equirecursive types for datatype-generic programmingACM SIGPLAN Notices10.1145/2914770.283766051:1(30-43)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837660
Cai YGiarrusso POstermann KBodik RMajumdar R(2016)System f-omega with equirecursive types for datatype-generic programmingProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837660(30-43)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837660
Show More Cited By

Index Terms

The power of Pi
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types
        Functional languages

Recommendations

The power of Pi
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates ...
General purpose languages should be metalanguages
PEPM '10: Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation

In his paper, The Next 700 Programming Languages, the late Landin writes that "most programming languages are partly a way of expressing things in terms of other things and partly a basic set of given things." Landin tries to separate the general ...
Intrinsically-typed definitional interpreters for imperative languages

A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 9

ICFP '08

September 2008

399 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1411203

Issue’s Table of Contents

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
September 2008
422 pages
ISBN:9781595939197
DOI:10.1145/1411204
General Chair:
James Hook
Portland State University, USA
,
Program Chair:
Peter Thiemann
Universität Freiburg, Germany

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2008

Published in SIGPLAN Volume 43, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
630
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)2

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

van Geest MSwierstra WLindley SYorgey B(2017)Generic packet descriptions: verified parsing and pretty printing of low-level dataProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122979(30-40)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122979
Cai YGiarrusso POstermann K(2016)System f-omega with equirecursive types for datatype-generic programmingACM SIGPLAN Notices10.1145/2914770.283766051:1(30-43)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837660
Cai YGiarrusso POstermann KBodik RMajumdar R(2016)System f-omega with equirecursive types for datatype-generic programmingProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837660(30-43)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837660
Christiansen DCarette JWillcock J(2013)Dependent type providersProceedings of the 9th ACM SIGPLAN workshop on Generic programming10.1145/2502488.2502495(25-34)Online publication date: 28-Sep-2013
https://dl.acm.org/doi/10.1145/2502488.2502495
Barlatier PDapoigny R(2012)A type-theoretical approach for ontologiesApplied Ontology10.5555/2594742.25947457:3(311-356)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.5555/2594742.2594745
Ciccone LPadovani LGabbrielli MAbel ACheney J(2020)A Dependently Typed Linear π-Calculus in AgdaProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414109(1-14)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414109
Weirich SChoudhury PVoizard AEisenberg R(2019)A role for dependent types in HaskellProceedings of the ACM on Programming Languages10.1145/33417053:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341705
Tomé Cortiñas CSwierstra WEisenberg RVazou N(2018)From algebra to abstract machine: a verified generic constructionProceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3240719.3241787(78-90)Online publication date: 27-Sep-2018
https://dl.acm.org/doi/10.1145/3240719.3241787
Ionescu CJansson PBotta N(2018)Type Theory as a Framework for Modelling and ProgrammingLeveraging Applications of Formal Methods, Verification and Validation. Modeling10.1007/978-3-030-03418-4_8(119-133)Online publication date: 29-Oct-2018
https://doi.org/10.1007/978-3-030-03418-4_8
van Geest MSwierstra WLindley SYorgey B(2017)Generic packet descriptions: verified parsing and pretty printing of low-level dataProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122979(30-40)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122979
Show More Cited By

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.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents