Higher-Order Dynamic Pattern Unification for Dependent Types and Records
While higher-order pattern unification for the λ Π-calculus is decidable and unique unifiers exists, we face several challenges in practice: 1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification algorithm. 2) Many systems implement λ ΠΣ calculus and hence the known pattern unification algorithms for λ Π are too restrictive.
In this paper, we present a constraint-based unification algorithm for λ ΠΣ-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing Σ-types into problems only involving Π-types. We prove correctness of our algorithm and discuss its application.
KeywordsFree Variable Deductive System Logical Framework Typing Rule Pattern Fragment
Unable to display preview. Download preview PDF.
- 2.Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Joint International Conference Logic Programming, pp. 259–273. MIT Press, Cambridge (1996)Google Scholar
- 4.Elliott, C.: Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University (1990)Google Scholar
- 8.McBride, C.: Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In: ACM SIGPLAN Workshop on Genetic Programming (WGP 2010), pp. 1–12. ACM, New York (2010)Google Scholar
- 9.Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, pp. 255–269. MIT Press, Cambridge (1991)Google Scholar
- 11.Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Technical Report 33D (2007)Google Scholar
- 13.Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, CMU-CS-03-185 (2003)Google Scholar
- 15.Poswolsky, A., Schürmann, C.: System description: Delphin—a functional programming language for deductive systems. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008). ENTCS, vol. 228, pp. 135–141. Elsevier, Amsterdam (2009)Google Scholar
- 16.Reed, J.: Higher-order constraint simplification in dependent type theory. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 (2009)Google Scholar
- 17.Reed, J.: A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University (2009)Google Scholar
- 18.Schack-Nielson, A., Schürmann, C.: Pattern unification for the lambda calculus with linear and affine types. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010). EPTCS, vol. 34, pp. 101–116 (2010)Google Scholar
- 19.Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh (2003)Google Scholar