Extending a refinement λ-calculus with polymorphism and data types

Abstract

Das Parsen von Stringeingaben ist eine häufige Programmieraufgabe, die oft ad hoc ohne Spezifikation einer formalen Grammatik implementiert wird. Die automatische Inferenz solcher Grammatiken bietet viele Vorteile, und das existierende Panini-System verwendet Refinement Typen, um Eingabegrammatiken für ad hoc Parser automatisch zu generieren. Dieser Ansatz ist jedoch durch den zugrunde liegenden λ-Kalkül eingeschränkt, dem Polymorphismus und algebraische Datentypen fehlen. Das Fehlen dieser häufig verwendeten Konzepte verhindert die Inferenzfähigkeit vieler Grammatiken.Um diese Einschränkungen zu beheben, erweitern wir den λ-Kalkül um die fehlenden Konzepte. Der resultierende λ-Kalkül führt außerdem eine neue Inferenzregel für die Zerlegung von Datentypen ein. Wir kategorisieren verschachtelte Grammatikstrukturen, die häufig in ad hoc Parsern auftreten, und konzentrieren uns auf Grammatiken, die durch split-Operationen und die dadurch erzeugten Listen und Tupel erzeugt werden. Für die Synthese solcher Grammatiken stellen wir einen Ansatz vor, der die verschachtelten Grammatiken innerhalb einer Datenstruktur zu einer Gesamtgrammatik zusammenführt.Diese Erweiterungen integrieren wir in das Panini-System und evaluieren sie anhand realer ad hoc Parser. Dabei zeigen wir, dass wir viele der betrachteten Parser lösen und komplexe geschachtelte Grammatiken durch Inferenz automatisch erkennen können. Die vorliegende Arbeit erweitert nicht nur die Möglichkeiten eines Refinement Typsystems, sondern verbessert auch das Panini-System erheblich, sodass es eine größere Anzahl von Grammatiken generieren kann.

Parsing strings is a common programming task often performed in an ad hoc manner without formally defining an input grammar. Inferring such grammars provides numerous benefits, and the existing Panini system leverages refinement types to automatically synthesize input grammars for ad hoc parsers. However, its current approach is limited by the underlying λΣ-calculus, which lacks polymorphism and algebraic data types, restricting its ability to infer many useful grammars.To address these limitations, we extend the λΣ calculus with these missing features, resulting in the λΣ+ calculus, and introduce a novel inference rule for data type destruction. We categorize the nested grammar structures common in ad hoc parsers, focusing on those arising from split operations and the resulting list and tuple algebraic data types. To synthesize such grammars, we introduce an approach to combine the nested grammars within a data structure to an overall grammar.We integrate these enhancements into the Panini system and evaluate them on real-world ad hoc parsers, demonstrating the ability to synthesize complex nested grammars in many cases. This work not only extends the capabilities of a refinement type system in the context of grammar synthesis, but also significantly improves the Panini system, enabling it to synthesize a broader range of grammars.