zz note: type checked embedded DSLs with quotations

There is an interesting technique used in C# and F# for type-checking embedded DSLs, by using quotations.

In a nutshell, the technique is to express a DSL program fragment in a form the compiler can type-check... but never actually turn it into executable code. Then, instead generate code to construct an expression tree, which a library can use to execute the DSL at runtime.

Imagine we want a type-checked SQL DSL embedded in Irken that looks something like this:

(define query 
  (from c in db.Customers
      where (= c.City "Nantes")
      select (:record c.City c.CompanyName)))

First we model the SQL db schema into an Irken data-structure...

(define db { 
   Customers = {          ; db table
     City = string        ; db column
     CompanyName = string ; db column
   }})

Then we define Irken macros and functions that establish the type relationships for type checking our SQL DSL... note these do not do anything, they are just for type-checking the DSL

(defmacro from
    (from value <in> table
         <where> expr
         <select> result) -> 
    (:sqldsl @( let ((value table))
                (where expr)
                (select-into result)))
(define (where x) : (bool -> #u) #u)
(define (select-info x) : ('a -> #u) 

When we compile the code, our SQL DSL translates into:

(define query
   (:sqldsl @(let ((c db.Customers))
      (where (= c.City "Nantes"))
      (select-into (:result c.City c.CompanyName))))

Irken Inference will type-check that the column names on c are valid in our db schema, and that c.City is a string. However, @( expr ) causes the code-generator to output code that returns an expression-tree, instead of trying to run that code.

Next, we call a sql-execute function with query, and at runtime it reads the expression tree and constructs the SQL query.

The real macro would be more flexible, typecheck more, and also create an "unpack" lambda to unpack the sql result into the user-supplied result type (:result ...).

Unquoting expresions

In order for this to be useful, there needs to be a way to unquote expressions within the quotation. This can be done either by:

• explicitly marking all unquoted expressions (for example, with ~) (F# does this)
• using a ruleset to decide the boundary between quoted and evaluated expressions (C# LINQ does this)

This is to handle situations like the following, where we want the created quoted expressions to capture the runtime value of some_variable, not merely the name of the variable.

(define query 
  (from c in db.Customers
      where (= c.City some_variable)
      select (:record c.City c.CompanyName)))

I believe the rules for C# LINQ might be common to this technique of using quoting to convert type-checked code into expression trees. As far as I can reason so far, those rules are:

• a list of valid "outermost" quoted applications (i.e. in the case of sql, outermost occurrences of operations which can be translated into SQL, including: ==, !=, <, >, &&, ||, substring)
• a list of operations to quote only on let variables created inside the quotation (the '.' dot operator, for example)

The above rules could be hard-coded into the compiler, as they are in C#, they could be implemented as syntax-rules macro code running in the compiler, or they could be avoided - by using the F# explicit quoting method.

---

Research

• FSharp Quotation Samples
• How does LINQ decide which expressions to evaluate and which to capture?
• Expressions in LINQ to Entities Queries
• Howto: LINQ to SQL Transaction (part 1, part 2, part 3)

Related

• Type Systems as Macros