Andres Löh, Dependently Typed Grammars
TCS Oberseminar, 04.11.2011, 14:15
Dependently typed grammars (Andres Löh, Well-Typed LLP) Parser combinators are a success story for functional programming. Higher-order functions make it incredibly easy to combine powerful parsers out of a few small building blocks. In practice, however, parser combinators often suffer a number of disadvantages, from the inability to handle left-recursion to (comparatively) bad performance. If we do not aim to describe a parser directly, but instead describe a grammar with attached semantic functions, then we have new possibilities: We can analyze and transform the grammar, and generate not only combinator parsers, but also visualizations, or even perform the computations typically done by parser generators. The challenge is to do all of this without sacrificing type safety, and maintaining the benefits and flexibility of parser combinators. In this talk, I will demonstrate that in a dependently typed programming language such as Agda, we can get quite close to that goal.
abgelegt unter: Oberseminar