Software development is a complex and error prone task. Programming languages with strong static type systems assist programmers by capturing and checking the fundamental structure of programs in a very intuitive way. Given this success, it is natural to ask: can we capture and check more of the structure of programs__ __
In this dissertation I describe an approach called refinement-type checking that allows many common program properties to be captured and checked. This approach builds on the strength of the type system of a language by adding the ability to specify refinements of each type. Following previous work, I focus on refinements that include subtyping and a form of intersection types.
Central to my approach is the use of a bidirectional checking algorithm. This does not attempt to infer refinements for some expressions, such as functions, but only checks them against refinements. This avoids some difficulties encountered in previous work, and requires that the programmer annotate their program with some of the intended refinements. The required annotations appear to be very reasonable. Further, they document properties in a way that is natural, precise, easy to read, and reliable.
I demonstrate the practicality of my approach by showing that it can be used to design a refinement-type checker for a widely-used language with a strong type system: Standard ML. This requires two main technical developments. Firstly, I present a new valiant of intersection types that obtain soundness in the presence of call-by-value effects by incorporating a value restriction. Secondly, I present a practical approach to incorporating recursive refinements of ML datatypes, including a pragmatic method for checking the sequential pattern matching construct of ML.
I conclude by reporting the results of experiments with my implementation of refinement-type checking for SML. These indicate that refinement-type checking is a practical method for capturing and checking properties of real code.
Cited By
- Dunfield J and Krishnaswami N (2021). Bidirectional Typing, ACM Computing Surveys, 54:5, (1-38), Online publication date: 30-Jun-2022.
- Savvides S, Stephen J, Ardekani M, Sundaram V and Eugster P Secure data types Proceedings of the 2017 Symposium on Cloud Computing, (479-492)
- Jafery K and Dunfield J (2017). Sums of uncertainty: refinements go gradual, ACM SIGPLAN Notices, 52:1, (804-817), Online publication date: 11-May-2017.
- Davies R (2017). A Temporal Logic Approach to Binding-Time Analysis, Journal of the ACM, 64:1, (1-45), Online publication date: 29-Mar-2017.
- Jafery K and Dunfield J Sums of uncertainty: refinements go gradual Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (804-817)
- Oliveira B, Shi Z and Alpuim J (2016). Disjoint intersection types, ACM SIGPLAN Notices, 51:9, (364-377), Online publication date: 5-Dec-2016.
- Oliveira B, Shi Z and Alpuim J Disjoint intersection types Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, (364-377)
- Dunfield J (2015). Elaborating evaluation-order polymorphism, ACM SIGPLAN Notices, 50:9, (256-268), Online publication date: 18-Dec-2015.
- Dunfield J Elaborating evaluation-order polymorphism Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (256-268)
- Castagna G, Nguyen K, Xu Z and Abate P (2015). Polymorphic Functions with Set-Theoretic Types, ACM SIGPLAN Notices, 50:1, (289-302), Online publication date: 11-May-2015.
- Castagna G, Nguyen K, Xu Z and Abate P Polymorphic Functions with Set-Theoretic Types Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (289-302)
- Dunfield J (2012). Elaborating intersection and union types, ACM SIGPLAN Notices, 47:9, (17-28), Online publication date: 15-Oct-2012.
- Dunfield J Elaborating intersection and union types Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, (17-28)
- Chugh R, Rondon P and Jhala R Nested refinements Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (231-244)
- Chugh R, Rondon P and Jhala R (2012). Nested refinements, ACM SIGPLAN Notices, 47:1, (231-244), Online publication date: 18-Jan-2012.
- Atkey R, Johann P and Ghani N When is a type refinement an inductive type? Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software, (72-87)
- Unno H, Tabuchi N and Kobayashi N Verification of tree-processing programs via higher-order model checking Proceedings of the 8th Asian conference on Programming languages and systems, (312-327)
- Kobayashi N, Tabuchi N and Unno H Higher-order multi-parameter tree transducers and recursion schemes for program verification Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (495-508)
- Kobayashi N, Tabuchi N and Unno H (2010). Higher-order multi-parameter tree transducers and recursion schemes for program verification, ACM SIGPLAN Notices, 45:1, (495-508), Online publication date: 2-Jan-2010.
- Dunfield J Greedy bidirectional polymorphism Proceedings of the 2009 ACM SIGPLAN workshop on ML, (15-26)
- Lovas W and Pfenning F (2019). A Bidirectional Refinement Type System for LF, Electronic Notes in Theoretical Computer Science (ENTCS), 196, (113-128), Online publication date: 1-Jan-2008.
- Dunfield J Refined typechecking with Stardust Proceedings of the 2007 workshop on Programming languages meets program verification, (21-32)
- Fluet M and Pucella R (2006). Practical Datatype Specializations with Phantom Types and Recursion Schemes, Electronic Notes in Theoretical Computer Science (ENTCS), 148:2, (211-237), Online publication date: 1-Mar-2006.
- Dunfield J and Pfenning F Tridirectional typechecking Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (281-292)
- Dunfield J and Pfenning F (2004). Tridirectional typechecking, ACM SIGPLAN Notices, 39:1, (281-292), Online publication date: 1-Jan-2004.
- Dunfield J and Pfenning F Type assignment for intersections and unions in call-by-value languages Proceedings of the 6th International conference on Foundations of Software Science and Computation Structures and joint European conference on Theory and practice of software, (250-266)
- Xi H and Pfenning F (1998). Eliminating array bound checking through dependent types, ACM SIGPLAN Notices, 33:5, (249-257), Online publication date: 1-May-1998.
- Xi H and Pfenning F Eliminating array bound checking through dependent types Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, (249-257)
Recommendations
Practical dependent type checking using twin types
TyDe 2020: Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven DevelopmentPeople writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a type-...
Refinement kinds: type-safe programming with practical type-level computation
This work introduces the novel concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles ...