Embedding by Unembedding - Extending HOAS for Complex Semantic Domains

Explore a 27-minute video presentation from ICFP 2023 that introduces the concept of "Embedding by Unembedding" in language development. Delve into the limitations of Higher-Order Abstract Syntax (HOAS) and discover a novel solution for extending its applicability while maintaining its elegance. Learn how this technique addresses challenges in semantic domains that are difficult to express as functions, particularly in open expressions. Examine case studies in incremental computation and bidirectional transformations to understand the practical implications of this approach. Gain insights into the conversion process from finally-tagless representation to de Bruijn-indexed terms, and understand the strong correctness guarantees it provides. Compare the resulting embedded implementations with state-of-the-art language implementations in their respective domains.

[ICFP'23] Embedding by Unembedding