In this talk, we present the insight that the practical concept of embedded domain-specific compilers (EDSC), describing embedded domain-specific languages (EDSL) used for generating code often for external targets, is deeply related to the theoretical concept of Normalisation-By-Evaluation (NBE), describing the process of deriving the canonical form of terms with respect to an equational theory. Since an embedded term is encoded as a collection of host language terms, evaluation of the non-value host terms results in normalisation of the embedded term, and since EDSCs rely on an intermediate interface to generate their target code from, all embedded terms are designed to eventually adhere to the normal forms described by the interface. In other words, the structure of an EDSC allows it to perform normalisation on embedded terms by encoding them as a collection of value and non-value host terms, employing evaluation in the host language, and then deriving the resulting terms adhering to the intermediate interface. This structure, together with a collection of correctness laws, forms an NBE process. This connection, referred to as embedding by normalisation (EBN), is theoretically useful in that it helps us to understand and reason about embedded terms and their semantics, and practically beneficial in that it enables us to directly apply techniques from NBE. For instance, through EBN, we adapt the treatment of sums, or constants, from NBE to embedding, resolving some not fully resolved problems.
(dsldi17-final15.pdf) | 162KiB |
(Embedding By Normalisation -- DSLDI.pdf) | 1.44MiB |
Sun 22 OctDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00 | |||
15:30 22mTalk | Property Law as a Programming Language DSLDI Shrutarshi Basu Cornell University, James Grimmelmann Cornell Law School, Nate Foster Cornell University File Attached | ||
15:52 22mTalk | Embedding By Normalisation DSLDI Shayan Najd University of Edinburgh File Attached | ||
16:15 22mTalk | Reliable composition of domain-specific language features DSLDI File Attached | ||
16:37 22mDay closing | Discussion and closing remarks DSLDI |