Conal Elliott
Skip Abstract Section
Abstract
It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages.
- Umut Acar. Self-adjusting computation . PhD thesis, School of Computer Science, Carnegie Mellon University, May 2005.Google Scholar
- Umut A. Acar, Guy E. Blelloch, Matthias Blume, and Robert Harper. Self-adjusting programming . In ML Workshop, 2005.Google Scholar
- Steve Awodey. Category theory, volume 49 of Oxford Logic Guides. Oxford University Press, 2006.Google Scholar
- Christiaan Baaij and Jan Kuper. Using rewriting to synthesize functional languages to digital circuits . In Trends in Functional Programming, Lecture Notes in Computer Science , pages 17–33, 2014.Google Scholar
- John Backus. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs . Communications of the ACM , 21(8):613–641, August 1978. Google ScholarDigital Library
- Michael Barr. Fixed points in cartesian closed categories . Theoretical Computer Science, 70(1):65–72, 1990. Google ScholarDigital Library
- Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. Lava: hardware design in Haskell . In ICFP, 1998.Google ScholarDigital Library
- Guy E. Blelloch. Prefix Sums and Their Applications . Technical Report CMU-CS-90-190, School of Computer Science, Carnegie Mellon University, November 1990.Google Scholar
- Max Bolingbroke. Constraint kinds for GHC. http://blog.omega-prime.co.uk/?p=127 , 2011.Google Scholar
- Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL . In Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience , volume A-10, pages 129–156, 1993.Google Scholar
- Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation . In PLDI ’14, pages 145–155, 2014.Google Scholar
- Magnus Carlsson. Monads for incremental computing . In ICFP, pages 26–35, 2002.Google ScholarDigital Library
- Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. Associated type synonyms . In ICFP, 2005a.Google ScholarDigital Library
- Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. Associated types with class . In Principles of Programming Languages , 2005b.Google Scholar
- Mark Chu-Carroll. Interpreting lambda calculus using closed cartesian categories. http://goodmath.scientopia.org/2012/03/ 11/interpreting-lambda-calculus-using-closed-cartesian-categories/ , March 2012.Google Scholar
- Koen Claessen and David Sands. In Asian Computing Science Conference, 1999.Google Scholar
- Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine . Science of Computer Programming, 8, 1987. Google ScholarDigital Library
- Pierre-Louis Curien. Categorical combinators. Information and Control, 69(1-3):188–254, 1986. Google ScholarDigital Library
- Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver . In Theory and Practice of Software, International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 337–340, 2008. Google ScholarCross Ref
- Conal Elliott. Programming graphics processors functionally . In Haskell Workshop, 2004. Google ScholarDigital Library
- Conal Elliott. Beautiful differentiation . In International Conference on Functional Programming, 2009. Google ScholarDigital Library
- Conal Elliott. Generic functional parallel algorithms: Scan and FFT . Proc. ACM Program. Lang., 1(ICFP), September 2017.Google ScholarDigital Library
- Conal Elliott, Sigbjørn Finne, and Oege de Moor. Compiling embedded languages . Journal of Functional Prog., 13(2), 2003. Google ScholarDigital Library
- Andrew Farmer, Andy Gill, Ed Komp, and Neil Sculthorpe. The HERMIT in the machine: A plugin for the interactive transformation of GHC core language programs . Haskell Symposium, pages 1–12, 2012. Google ScholarDigital Library
- GHC Team. The Glorious Glasgow Haskell compilation system user’s guide, version 8.0.1. https://downloads.haskell.org/ ~ghc/latest/docs/html/users_guide , 2016.Google Scholar
- Jeremy Gibbons. Calculating functional programs . In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction , volume 2297 of Lecture Notes in Computer Science. Springer-Verlag, 2002.Google ScholarCross Ref
- Jeremy Gibbons and Nicolas Wu. Folding domain-specific languages: Deep and shallow embeddings . In ICFP, 2014.Google Scholar
- Andy Gill. Type-safe observable sharing in Haskell . In Haskell Symposium, pages 117–128, September 2009. Google ScholarDigital Library
- Andy Gill. Domain-specific languages and code synthesis using Haskell . ACM Queue, 12(4), April 2014. Google ScholarDigital Library
- Andy Gill and Graham Hutton. The worker/wrapper transformation . Journal of Functional Prog., pages 227–251, 2009.Google ScholarDigital Library
- Ralf Hinze. Memo functions, polytypically! In Workshop on Generic Programming, pages 17–32, 2000.Google Scholar
- Ralf Hinze. Fun with phantom types . In The fun of programming. Palgrave, 2003. Google ScholarCross Ref
- Ralf Hinze. Polytypic values possess polykinded types . In Science of Computer Programming, pages 2–27, June 2004.Google Scholar
- John Hughes. The design of a pretty-printing library . In Advanced Functional Programming, pages 53–96, 1995.Google ScholarCross Ref
- John Hughes. Generalising monads to arrows . Science of Computer Programming, 37:67–111, 1998. Google ScholarDigital Library
- John Hughes and Simon Peyton Jones. The pretty package. https://hackage.haskell.org/package/pretty , November 2007. Haskell library.Google Scholar
- Geraint Jones and Mary Sheeran. Circuit design in Ruby . Formal methods for VLSI design, 1, 1990.Google Scholar
- Mark P. Jones. Dictionary-free overloading by partial evaluation . In In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation , pages 107–117, 1994.Google Scholar
- Jerzy Karczmarczuk. Functional differentiation of computer programs . In ICFP, pages 195–203, 1998.Google ScholarDigital Library
- Edward Kmett. What constraints entail: Part 1. http://comonad.com/reader/2011/what-constraints-entail-part-1/ , 2011.Google Scholar
- Joachim Lambek. From λ-calculus to cartesian closed categories. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism . Academic Press, 1980.Google Scholar
- Joachim Lambek. Cartesian closed categories and typed lambda-calculi. In Thirteenth Spring School of the LITP on Combinators and Functional Programming Languages , pages 136–175, 1986.Google ScholarCross Ref
- F. William Lawvere and Stephen H. Schanuel. Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press, 2nd edition, 2009. Google ScholarCross Ref
- Daan Leijen and Erik Meijer. Domain specific embedded compilers . In Conference on Domain-Specific Languages, pages 109–122, 1999. Google ScholarDigital Library
- José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh. A generic deriving mechanism for Haskell . In Haskell Symposium , pages 37–48, 2010. Google ScholarDigital Library
- José Pedro Magalhães et al. GHC.Generics, 2011. URL https://wiki.haskell.org/GHC.Generics . Haskell wiki page.Google Scholar
- M. Douglas McIlroy. Power series, power serious . Journal of Functional Programming, 9(3):325–337, 1999. Google ScholarDigital Library
- R.E. Moore. Interval analysis. Series in automatic computation. Prentice-Hall, 1966.Google Scholar
- Philip S. Mulry. Categorical fixed point semantics . Theoretical Computer Science, 70(1):85–97, January 1990. Google ScholarDigital Library
- Simon Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language . In Functional programming languages and computer architecture , pages 636–666, 1991.Google Scholar
- Simon Peyton Jones and Simon Marlow. Secrets of the Glasgow Haskell compiler inliner . Journal of Functional Programming, 12(5), July 2002.Google Scholar
- Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. Playing by the rules: Rewriting as a practical optimisation technique in GHC . In Haskell Workshop, pages 203–233, 2001.Google Scholar
- Simon L. Peyton Jones. Compiling Haskell by program transformation: A report from the trenches . In European Symposium on Programming , pages 18–44, 1996.Google Scholar
- Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. The constrained-monad problem . In International Conference on Functional Programming , pages 287–298, 2013a. Google ScholarDigital Library
- Neil Sculthorpe, Andrew Farmer, and Andy Gill. The HERMIT in the tree: Mechanizing program transformations in the GHC core language . In Symposium on Implementation and Application of Functional Languages, pages 86–103, 2013b. Google ScholarCross Ref
- Mary Sheeran. muFP, a language for VLSI design . In Symposium on LISP and Functional Programming, pages 104–112, 1984.Google ScholarDigital Library
- Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators . In Logic in Computer Science, pages 30–41, 2000.Google Scholar
- Jeffrey Mark Siskind and Barak A. Pearlmutter. Perturbation confusion and referential transparency: Correct functional implementation of forward-mode AD . In Implementation and Application of Functional Languages, pages 1–9, 2005.Google Scholar
- Jeffrey Mark Siskind and Barak A. Pearlmutter. Nesting forward-mode AD in a functional framework . Higher Order Symbolic Computation , 21(4):361–376, 2008. Google ScholarDigital Library
- Michael Spivak. Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. HarperCollins Publishers, 1971.Google Scholar
- Martin Sulzmann, Manuel M. T. Chakravarty, Simon L. Peyton Jones, and Kevin Donnelly. System F with type equality coercions . In Types In Languages Design And Implementation, pages 53–66, 2007.Google Scholar
- Pierre Weis et al. A history of Caml, 2005. URL https://caml.inria.fr/about/history.en.html . Last updated 2005-01-28.Google Scholar
- R. E. Wengert. A simple automatic derivative evaluation program. Communications of the ACM, 7(8):463–464, 1964. Google ScholarDigital Library
- Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon L. Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. Giving Haskell a promotion . In Types In Languages Design And Implementation, pages 53–66. ACM, 2012.Google Scholar
Index Terms
- Compiling to categories
Recommendations
Incremental concrete syntax for embedded languages with support for separate compilation
Embedded domain-specific languages (EDSLs) are known to improve the productivity of developers. However, for many domains no DSL implementation is available and two important reasons for this are: First, the effort to implement EDSLs that provide the ...
Incremental concrete syntax for embedded languages
SAC '11: Proceedings of the 2011 ACM Symposium on Applied ComputingEmbedded domain-specific languages (EDSLs) are known to improve the productivity of developers. However, for many domains no DSL implementation is available. Two important reasons are: First, the effort to implement embedded DSLs that provide the domain'...
Mixing source and bytecode: a case for compilation by normalization
Language extensions increase programmer productivity by providing concise, often domain-specific syntax, and support for static verification of correctness, security, and style constraints. Language extensions can often be realized through translation ...
Comments