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...

Algebra.NET is a simple library designed to facilitate easy expression and manipulation of algebraic functions. For instance, here's a simple function: Function<Func<double, double>> a = Algebra.Function(x => 2 * x + 1); We can compile such a function to efficient IL: Func<double, double> func = a.Compile("times2plus1"); Or we can apply some algebraic identities to rewrite it: Identity associative = Algebra.Identity(x => x + 1 == 1 + x); Identity mulEqAdd = Algebra.Identity(x => 2 * x == x + x); Console.WriteLine(a); Console.WriteLine(a.Rewrite(1, associative, mulEqAdd)); // Prints: // ((2 * x) + 1) // (1 + (x + x)) Rewrites can sometimes loop forever (consider "x + y == y + x"), so the Rewrite method takes a number indicating the maximum number of iterations to perform all the rewrites. All the usual arithmetic operations are available, including an extension method for exponentiation: var f = Algebra.Function(x => x.Po...

The µKanren paper is a nice introduction to a lightweight logic programming language which is a simplification of the miniKanren family of languages. The existing µKanren implementation in C# was a translation from Scheme, and thus is verbose, untyped with lots of casts, and non-idiomatic. I also found most of the other Kanren implementations unnecessarily obscure, heavily relying on native idioms that aren't clear to newcomers. uKanren.NET provides a clear presentation of the core principles of µKanren using only IEnumerable<T> and lambdas, showing that µKanren's search is fundamentally just a set of combinators for transforming sequences of states. The values of the sequence are sets of bound variables that satisfy a set of equations. For instance, given the following expression: Kanren.Exists(x => x == 5 | x == 6) You can read it off as saying there exists an integer value to which we can bind variable x, such that x equals either 5 or 6 [1]. Solving this eq...

A bit of departure from my usual practical posts in C#, I decided to try my hand at an abstract computer science topic. I've become interested in concatenative programming, and combinator calculi are right up this alley. The quintessential combinator calculus is the well-known SKI calculus , which features two core combinators, S and K, and one optional combinator I. SKI is quite simple, and it's pretty straightforward to implement as an EDSL. I suspect the key stumbling block for most programmers unfamiliar with functional programming will be the pervasive partial application inherent to combinators. Partial Application Partial application is a pretty simple concept for anyone whose done even a little programming with LINQ. C#/.NET features first-class functions called "delegates" with types like: public delegate T2 Func<T0, T1, T2>(T0 arg0, T1 arg1); That's the type declaration for a delegate that accepts two arguments of types T0 and T1, and retu...

I posted awhile ago about a pattern for ad-hoc extensions in .NET using generics. Unfortunately, like every "design pattern", you had to manually ensure that your abstraction properly implements the pattern. There was no way to have the compiler enforce it, like conforming to an interface. It's common wisdom that "design patterns" are simply a crutch for languages with insufficient abstractive power. Fortunately, .NET's multicast delegates provides the abstractive power we need to eliminate the design pattern for ad-hoc extensions: /// <summary> /// Dispatch cases to handlers. /// </summary> /// <typeparam name="T">The type of the handler.</typeparam> public static class Pattern<T> { static Dispatcher<T> dispatch; static Action<T, object> any; delegate void Dispatcher<T>(T func, object value, Type type, ref bool found); /// <summary> //...

A recent discussion on LtU brought up a common limitation of modern languages and runtimes. Consider some set of abstractions A, B, ..., Z that we wish supported some custom operation Foo(). Languages like C# give only two straightforward possibilities: inheritance and runtime type tests and casts. Inheritance is straightforward: we simply inherit from each A, B, ..., Z to make A_Foo, B_Foo, ..., Z_Foo, with a custom Foo() method. Unfortunately, inheritance is sometimes forbidden in C#, and furthermore, it sometimes prevents us from integrating with existing code. For instance, say we want to integrate with callback-style code, where the existing code hands our program an object of type A. We can't call Foo() on this A, because it's not an A_Foo, which is what we really wanted. This leaves us with the undesirable option of using a large set of runtime type tests. Now type tests and casts are actually pretty fast , faster than virtual dispatch in fact, but the danger is i...

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...

Awhile ago, I had posted about an embedding of a stack language in C#. The type signatures of the functions and the stack object encoded the consumption and production of stack values, so if your program compiled, it ran correctly. Unfortunately, the prior structure had a safety problem when generating code which I noted, but didn't have time to address. The new structure provided below does not have the safety problem, and any functions that compile are guaranteed to execute correctly. I have also altered the style to emphasize the row variable representing the "rest of the record" which the operation knows nothing about. The row variable is denoted by "_". This is still a fairly limited embedding, but I have added a few convenience functions, and may yet add more. Here is a sample program: var d = new DynamicMethod("test", typeof(void), null); var s = 1.Load() // load constant: { int } .Int(2) // load constan...

Parametric polymorphism is a powerful tool for constructing and composing safe programs. To demonstrate this, I've constructed a tiny embedded stack language in C#, and I exploited C# generics, aka parametric polymorphism, to ensure that any embedded programs are type-safe, and thus, "can't go wrong". Moreover, this language is jitted, since I use ILGenerator of System.Reflection.Emit, and the complexity of doing this was no higher than creating an interpreter. This is mainly because the CLR is itself a stack-based VM, and so jitting a stack-based program to a stack-based IL is fairly natural. Here is the type-safe representation of the stack: public struct Stack<R, T> : IDisposable { internal ILGenerator gen; public Stack(ILGenerator gen) { this.gen = gen; } public void Dispose() { this.Return(); } } This type encapsulates the IL output stream and uses two phantom type variables to encode the values at the top of the ...

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...