Dependently typed Haskell in industry (experience report)

Abstract

Recent versions of the Haskell compiler GHC have a number of advanced features that allow many idioms from dependently typed programming to be encoded. We describe our experiences using this "dependently typed Haskell" to construct a performance-critical library that is a key component in a number of verification tools. We have discovered that it can be done, and it brings significant value, but also at a high cost. In this experience report, we describe the ways in which programming at the edge of what is expressible in Haskell's type system has brought us value, the difficulties that it has imposed, and some of the ways we coped with the difficulties.

References

1. Lennart Augustsson and Kent Petersson. 1994. Silly Type Families. (September 1994). Unpublished draft.
2. Yves Bertot and Pierre Castéran. 2004. Proof by Reflection. Springer Berlin Heidelberg, Berlin, Heidelberg, 433–448.
3. François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wrocław, Poland, 53–64. https://hal.inria.fr/hal-00790310 .
4. Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Quantified class constraints. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017. 148–161.
5. Joachim Breitner, Richard Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2014. Safe, zero-cost coercions for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). ACM.
6. Manuel Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005. Associated Type Synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP ’05). ACM.
7. Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich. 2016. How to Avoid Proving the Absence of Integer Overflows. In Verified Software: Theories, Tools, and Experiments, Arie Gurfinkel and Sanjit A. Seshia (Eds.). Springer International Publishing, Cham, 94–109.
8. N. G. de Bruijn. 1991. Telescopic Mappings in Typed Lambda Calculus. Inf. Comput. 91, 2 (1991), 189–204.
9. Iavor S. Diatchki. 2015. Improving Haskell Types with SMT. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). ACM, New York, NY, USA, 1–10.
10. Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments -8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers. 56–72.
11. Richard Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In Proceedings of the 2012 Haskell Syposium (Haskell ’12). ACM, 117–130.
12. GHC Issue #15186 2018. ghc#15186 8.4.2 panic in profiling build. https://ghc.haskell.org/trac/ghc/ticket/15186
13. Jeremy Gibbons and Bruno C. d. S. Oliveira. 2009. The Essence of the Iterator Pattern. Journal of Functional Programming 19, 3–4 (July 2009), 377–402.
14. Oleg Kiselyov and Chung-chieh Shan. 2004. Functional pearl: implicit configurations-or, type classes reflect the values of types. In Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004, Henrik Nilsson (Ed.). ACM, 33–44.
15. John Launchbury and Simon Peyton Jones. 1994. Lazy functional state threads. In ACM Conference on Programming Languages Design and Implementation, Orlando (PLDI’94) (acm conference on programming languages design and implementation, orlando (pldi’94) ed.). ACM Press, 24–35. https://www.microsoft.com/en-us/research/publication/lazy-functional-statethreads/
16. J. R. Lewis and B. Martin. 2003. Cryptol: high assurance, retargetable crypto development and validation. In IEEE Military Communications Conference, 2003. MILCOM 2003., Vol. 2. 820–825.
17. Sam Lindley and Conor McBride. 2013. Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming. In Proceedings of the 2013 Haskell Symposium (Haskell ’13). ACM.
18. Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1–13.
19. Laura McKinney and Jef Bell. 2014. The collaborative web: Building a divergent organizational model for research and development, based on 21st century notions of employee engagement. In Proceedings of PICMET ’14 Conference: Portland International Center for Management of Engineering and Technology; Infrastructure and Service Integration. 7–17.
20. Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple Unification-Based Type Inference for GADTs. In Proceedings of the 2006 International Conference on Functional Programming (ICFP ’06). ACM.
21. Amr Sabry and Matthias Felleisen. 1993. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation 6, 3 (1993), 289–360.
22. Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. 2008. Type Checking with Open Type Functions. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). ACM, New York, NY, USA, 51–62.
23. Tim Sheard and Simon Peyton Jones. 2002. Template meta-programming for Haskell. 1–16.
24. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones. 2014. Refinement Types for Haskell (ICFP ’14). ACM, 269–282.
25. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). ACM.
26. Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. 2011. Generative type abstraction and type-level computation. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (proceedings of the 38th annual acm sigplan-sigact symposium on principles of programming languages ed.). ACM SIGPLAN. https://www.microsoft.com/en-us/research/publication/generative-type-abstraction-and-type-levelcomputation/
27. Edward Z. Yang. 2017. Backpack: Towards Practical Mix-In Linking In Haskell. Ph.D. Dissertation. Stanford University.
28. Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012. Giving Haskell a Promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI ’12). ACM, New York, NY, USA, 53–66.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software development techniques

  • Software notations and tools

    • General programming languages

      • Language features

        • Data types and structures

      • Language types

        • Functional languages