This program is tentative and subject to change.
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
This program is tentative and subject to change.
Sun 12 OctDisplayed time zone: Perth change
14:00 - 15:30 | |||
14:00 30mTalk | Gradual Metaprogramming TyDe Tianyu Chen Indiana University, Darshal Shetty Indiana University, Jeremy G. Siek Indiana University, USA, Chao-Hong Chen Meta, Weixi Ma Meta, Arnaud Venet Meta, Rocky Liu Meta Link to publication DOI Pre-print | ||
14:30 30mTalk | Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search TyDe Satoshi Takimoto Institute of Science Tokyo, Sosuke Moriguchi Institute of Science Tokyo, Takuo Watanabe Institute of Science Tokyo DOI | ||
15:00 30mTalk | Generating a corpus of Hazel programs from ill-typed OCaml programs (Extended Abstract) TyDe |