Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection

TL;DR

This paper introduces a reflection-based technique in dependently-typed host languages to combine the ease of shallow embeddings with the structural access of deep embeddings, enabling verified embedded languages to leverage existing tools.

Contribution

The paper presents a novel method to unify shallow and deep embeddings using reflection, demonstrated through embedding multiple languages into Agda and extracting verified programs.

Findings

Successfully embedded Kaleidoscope, SaC, and APL into Agda.

Enabled extraction of verified programs back into original languages.

Demonstrated a neural network implementation in the embedded APL.

Abstract

Dependently-typed host languages empower users to verify a wide range of properties of embedded languages and programs written in them. Designers of such embedded languages are faced with a difficult choice between using a shallow or a deep embedding. The former is easier to use because the entire infrastructure of the host langauge is immediately available. Meanwhile, the latter gives full access to the structure of embedded programs, but is difficult to use in practice, especially when the embedded language is itself dependently typed. The main insight presented in this paper is that the choice between shallow and deep embedding can be eliminated by working in a host language with reflection capabilities: we start from a shallow embedding that can use all libraries and tools of the host language, and later use reflection to expose the deep structure of the embedded programs. Concretely, we apply this technique to embed three programming languages -- Kaleidoscope, SaC, and (a subset of) APL -- into the dependently typed theorem prover Agda, using dependent types to statically enforce several properties of interest. We then use Agda's reflection capabilities to extract the embedded programs back into the original language, so that the existing toolchain can be leveraged. In this process, statically verified properties of the host language are mapped onto runtime checks in the target language, allowing extracted programs to interact safely with existing code. Finally, we demonstrate the feasibility of our approach with the implementation and extraction of a convolutional neural network in our embedding of APL.\@