ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Wed 6 Sep 2023 13:30 - 14:00 at B - Fifth Avenue - Meta programming Chair(s): Gabriel Radanne

Embedding is a language development technique that implements the object language as a library in a host language.
There are many advantages of the approach, including being lightweight and the ability to inherit features of the host language. A notable example is the technique of HOAS, which makes crucial use of higher-order functions to represent abstract syntax trees with binders.
Despite its popularity, HOAS has its limitations.
We observe that HOAS struggles with semantic domains that cannot be naturally expressed as functions, particularly when open expressions are involved.
Prominent examples of this include incremental computation and reversible/bidirectional languages.

In this paper, we pin-point the challenge faced by HOAS as a mismatch between the semantic domain of host and object language functions, and propose a solution.
The solution is based on the technique of <em>unembedding</em>, which converts
from the finally-tagless representation to de Bruijn-indexed terms with
strong correctness guarantees. We show that this approach is able to extend the
applicability of HOAS while preserving its elegance. We provide a generic
strategy for Embedding by Unembedding, and then demonstrate its effectiveness
with two substantial case studies in the domains of incremental computation
and bidirectional transformations. The resulting embedded implementations are
comparable in features to the state-of-the-art language implementations in
the respective areas.

Wed 6 Sep

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:30
Meta programmingICFP Papers and Events at B - Fifth Avenue
Chair(s): Gabriel Radanne Inria
Embedding by Unembedding
ICFP Papers and Events
Kazutaka Matsuda Tohoku University, Samantha Frohlich University of Bristol, Meng Wang University of Bristol, Nicolas Wu Imperial College London
MacoCaml: Staging Composable and Compilable Macros
ICFP Papers and Events
Ningning Xie University of Toronto / Google DeepMind, Leo White Jane Street, Olivier Nicole Tarides, Jeremy Yallop University of Cambridge
DOI Pre-print