Higher Logics

I recently built a REST API prototype where one of the endpoints accepted a string representing a filter to apply to a set of results. For instance, for entities with named properties "Foo" and "Bar", a string like "(Foo = 'some string') or (Bar > 99)" would filter out the results where either Bar is less than or equal to 99, or Foo is not "some string". This would translate pretty straightforwardly into a SQL query, but as a masochist I was set on using Google Datastore as the backend, which unfortunately has a limited filtering API : It does not support disjunctions, ie. "OR" clauses. It does not support filtering using inequalities on more than one property. It does not support a not-equal operation. So in this post, I will describe the design which achieves the following goals: A backend-agnostic querying API supporting arbitrary clauses, conjunctions ("AND"), and disjunctions ("OR"). Implemen...

I've written quite a few times about my experiments with the CLR type system [ 1 , 2 , 3 ]. After much exploration and reflection, I had devised a pretty good approach to encoding ML-style modules and abstracting over type constructors in C#. A recent question on Stack Overflow made me realize that I never actually explained this technique in plain English. The best encoding of ML modules and type constructor polymorphism requires the use of partly safe casting. An ML signature maps to a C# interface with a generic type parameter called a "brand". The brand names the class that implements the interface, ie. the module implementation. An ML module maps to a C# class. If the module implements a signature, then it implements the corresponding interface and specifies itself as the signature's brand. Since classes and interfaces are first-class values, an ML functor also maps to a class. An ML type component maps to an abstract class that shares the same brand as the modu...

Awhile back I described an idea to transparently execute code server-side or client-side given the same program. I've finally gotten around to implementing this using my encoding for type constructor polymorphism in C#. Here is an example you can run from the original paper showcasing exponentiation which can execute transparently either server-side or client-side. The server-side code is intentionally limited to bases less than 100 and exponents less than 20. Here is some simplified code that defines an exponentiation function: void Build<B, R>(B _) where B : ISymantics<B>, new() { var e = _.Lambda<int, Func<int, int>>( x => _.Fix<int, int>(self => _.Lambda<int, int>(n => _.If(_.Lte(n, _.Int(0)), () => _.Int(1), () => _.Mul(x, _.Apply(self, _.Add(n, _.Int(-1)))))))); } The parameter "_" is the tagless interpeter and it's type is ISymant...

Creating DSLs is all the rage these days, and for good reason. Most abstractions are actually a little language struggling to get out. Design consists of creating abstractions with maximum power, and minimum restrictions, and reusing this abstraction as much as possible. Small domain-specific languages are the ticket. However, language implementations are often written in fairly ad-hoc ways, and most interpreters are difficult to extend to compilers and partial evaluators. Languages are usually described by an "initial algebra", which basically just means that language terms are described by data types. Here's a simple definition of a language with integers, variables and addition: (* * Expressions := [0-9]* | e1 + e2 | e1 - e2 *) type expression = Int of int | Add of expression * expression | Sub of expression * expression So a program in this language can consist of integers, subtraction or addition expressions. The interpreter for this language unpacks the expression...

As Chung-chieh Shan pointed out , my encoding of modules in C# is somewhat limited. In particular, I cannot abstract over type constructors, which is to say, C# is missing generics over generics. Consider the Orc.NET interpreter: class Orc { class Exp<T> { ... } public Exp<U> Seq<T,U>(Exp<T> e1, <U>) { ... } public Exp<T> Par<T>(Exp<T> e1, Exp<T>) { ... } public Exp<T> Where<T>(Exp<T> e1, Exp<Promise<T>>) { ... } } This is the result of my translation, which was necessitated by the "Where" method. Where introduces a dependency which currently cannot be expressed with ordinary C# constraints, so the module encoding is necessary. The above interface is a direct, faithful implementation of the Orc semantics. The implementation I currently have is an interpreter for those semantics. What if I want to provide a compiler instead? The interface should remain the same , but the implementation ...