Meta-interpreters in Prolog are a powerful and elegant way to implement language extensions and non-standard semantics. But how can we bring the benefits of Prolog-style meta-interpreters to systems that combine functional and logic programming? In Prolog, a program can access its own structure via reflection, and meta-interpreters are simple to implement because the “pure” core language is small—not so, in larger systems that combine different paradigms.
In this paper, we present a particular kind of functional logic meta- programming, based on embedding a small first-order logic system in an expressive host language. Embedded logic engines are not new, as exemplified by various systems including miniKanren in Scheme and LogicT in Haskell. However, previous embedded systems generally lack meta- programming capabilities in the sense of meta-interpretation.
Instead of relying on reflection for meta-programming, we show how to adapt popular multi-stage programming techniques to a logic program- ming setting and use the embedded logic to generate reified first-order structures, which are again simple to interpret. Our system has an appealing power-to-weight ratio, based on the simple and general notion of dynamically scoped mutable variables. We also show how, in many cases, non-standard semantics can be realized without explicit reification and interpretation, but instead by customizing program execution through the host language. As a key example, we extend our system with a tabling/memoization facility. The need to interact with mutable variables renders this is a highly nontrivial challenge, and the crucial insight is to extract symbolic representations of their side effects from memoized rules. We demonstrate that multiple independent semantic modifications can be combined successfully in our system, for example tabling and tracing.
Tue 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00
|Lightweight Functional Logic Meta-Programming
|Mimalloc: Free List Sharding in Action
|LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Yutaka Nagashima Data61, Australia