Abstract
Parser combinators are a popular tool for designing parsers in functional programming languages. If such combinators generate an abstract representation of the grammar as an intermediate step, it becomes easier to perform analyses and transformations that can improve the behaviour of the resulting parser. Grammar transformations must satisfy a number of invariants. In particular, they have to preserve the semantics associated with the grammar. Using conventional type systems, these constraints cannot be expressed satisfactorily, but as we show in this article, dependent types are a natural fit. We present a framework for grammars and grammar transformations using Agda. We implement the left-corner transformation for left-recursion removal and prove a language-inclusion property as use cases.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Hutton, G.: Higher-order functions for parsing. Journal of Functional Programming 2, 323–343 (1992)
Swierstra, S.D., Duponcheel, L.: Deterministic, error-correcting combinator parsers. In: Launchbury, J., Sheard, T., Meijer, E. (eds.) AFP 1996. LNCS, vol. 1129, pp. 184–207. Springer, Heidelberg (1996)
Swierstra, S.D.: Combinator parsing: A short tutorial. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) ALFA. LNCS, vol. 5520, pp. 252–300. Springer, Heidelberg (2009)
Leijen, D., Meijer, E.: Parsec: Direct style monadic parser combinator for the real world. Technical Report UU-CS-2001-035, Utrecht University (2001)
Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)
Brink, K., Holdermans, S., Löh, A.: Dependently typed grammars, Agda code (2010), http://www.cs.uu.nl/~andres/DTG/
Fokker, J.: Functional parsers. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 1–23. Springer, Heidelberg (1995)
Rosenkrantz, D.J., Lewis, P.M.: Deterministic left corner parsing. In: Conference Record of 1970 Eleventh Annual Symposium on Switching and Automata Theory, pp. 139–152. IEEE, Los Alamitos (1970)
Johnson, M.: Finite-state approximation of constraint-based grammars using left-corner grammar transforms. In: COLING-ACL, pp. 619–623 (1998)
Baars, A.I., Swierstra, S.D., Viera, M.: Typed transformations of typed grammars: The left corner transform. To appear in the proceedings of the 9th Workshop on Language Descriptions, Tools and Applications (LDTA 2009), York, England (March 29, 2009)
Hughes, J.: Generalising monads to arrows. Science of Computer Programming 37, 67–111 (2000)
Pasǎlić, E., Linger, N.: Meta-programming with typed object-language representations. In: Karsai, G., Visser, E. (eds.) GPCE 2004. LNCS, vol. 3286, pp. 136–167. Springer, Heidelberg (2004)
Baars, A.I., Swierstra, S.D., Viera, M.: Typed transformations of typed abstract syntax. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, pp. 15–26. ACM Press, New York (2009)
Danielsson, N.A., Norell, U.: Structurally recursive descent parsing (2008), http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinators.html
Danielsson, N.A.: Total parser combinators (2009), http://www.cs.nott.ac.uk/~nad/publications/danielsson-parser-combinators.html
Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brink, K., Holdermans, S., Löh, A. (2010). Dependently Typed Grammars. In: Bolduc, C., Desharnais, J., Ktari, B. (eds) Mathematics of Program Construction. MPC 2010. Lecture Notes in Computer Science, vol 6120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13321-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-13321-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13320-6
Online ISBN: 978-3-642-13321-3
eBook Packages: Computer ScienceComputer Science (R0)