Monadification of Attribute Grammars
Mon 16 Nov 2020 05:20 - 05:40 at SPLASH-III - Chair(s): Friedrich Steimann
We describe a monadification process for attribute grammars for more concisely written attribute equations, closer to the style of inference rules used in traditional typing and evaluation specifications. Inference rules specifying, for example, a typing relation typically consider only typable expressions, whereas well-defined attribute grammars explicitly determine attribute values for any term, including untypable ones. The monadification approach lets one represent, for example, types as monadic optional/maybe values, but write non-monadic equations over the value inside the monad that only specify the rules for a correct typing, leading to more concise specifications. The missing failure cases are handled by a rewriting that inserts monadic return, bind, and failure operations to produce a well-defined attribute grammar that handles untypable trees. Thus, one can think in terms of a type T and not the actual monadic type M(T). To formalize this notion, typing and evaluation relations are given for the original and rewritten equations. The rewriting is total, preserves types, and a correctness property relating values of original and rewritten equations is given. A prototype implementation illustrates the benefits with examples such as typing of the simply-typed lambda calculus with Booleans, evaluation of the same, and type inference in Caml Light.
Sun 15 NovDisplayed time zone: Central Time (US & Canada) change
17:00 - 18:20 | |||
17:00 20mTalk | VarSem: Declarative Expression and Automated Inference of Variable Usage Semantics GPCE Link to publication DOI Media Attached | ||
17:20 20mTalk | Monadification of Attribute Grammars SLE Link to publication DOI Pre-print Media Attached | ||
17:40 20mTalk | Fluid Quotes: Metaprogramming across Abstraction Boundaries with Dependent Types GPCE Shadaj Laddad University of California at Berkeley, Koushik Sen University of California at Berkeley Link to publication DOI Pre-print Media Attached | ||
18:00 20mTalk | Strategic Tree Rewriting in Attribute Grammars SLE Link to publication DOI Pre-print Media Attached |
Mon 16 NovDisplayed time zone: Central Time (US & Canada) change
05:00 - 06:20 | |||
05:00 20mTalk | VarSem: Declarative Expression and Automated Inference of Variable Usage Semantics GPCE Link to publication DOI Media Attached | ||
05:20 20mTalk | Monadification of Attribute Grammars SLE Link to publication DOI Pre-print Media Attached | ||
05:40 20mTalk | Fluid Quotes: Metaprogramming across Abstraction Boundaries with Dependent Types GPCE Shadaj Laddad University of California at Berkeley, Koushik Sen University of California at Berkeley Link to publication DOI Pre-print Media Attached | ||
06:00 20mTalk | Strategic Tree Rewriting in Attribute Grammars SLE Link to publication DOI Pre-print Media Attached |