Reactive programming and dependent typing have opened my eyes to an interesting way to view syntax. Now if you’ll bear with me, I won’t get to syntax until the end of the post.
In programming languages we often build “data” out of sums (either this kind of thing or that kind of thing) and products (this kind of thing and that kind of thing together), and every serializable notion of data, like binary, Unicode text, JSON, etc. falls into that pattern pretty easily. But right down at the lowest level, when we encode a binary bit (or boolean value) as “either 0 or 1″… when the “kind of thing” is a 0, what does it take to store it? Nothing; if we know we’re trying to read something of kind 0, we already know the value without even looking at the data. The same goes for 1. It turns out a bit is just “either this or that” when we only care about the branch itself, not what this or that actually represent. Our algorithms could actually be operating on secretly richer data structures, and they just happen to ignore that substructure.
In most languages, we can hold state containers and external references in our data structures, even though they don’t have the same serializable nature as sums or products. Many utilities that operate on data structures (say, a utility that reverses a list) will simply leave these exotic values alone. The secretly rich substructure actually exists, and it’s crucial to the other parts of the program.
A more common word to use to discuss this secrecy is polymorphism. If a utility really doesn’t care about what type it’s dealing with, it’s polymorphic in that type. Often things are polymorphic only up to some condition on the types involved, and conditions on individual types tend to be represented as types of their own. Implications between conditions are subtyping relations: A is a subtype of B iff A’s condition is sufficient to ensure B’s condition.
Reactive programming
Reactive programming turns programming on its head in the following way: Suppose sums represent decisions that change over time, rather than eternally fixed, serializable bits. It turns out most of our programming patterns are actually polymorphic enough to continue making sense under this interpretation. Naively, we can just run our programs over and over every time a decision changes.
Dependent typing
Dependent typing turns programming on its head in a similar way: Suppose every value is associated with some other value (its type) that represents what we know about that value at compile time. Unlike in many kinds of static typing, dependent typing breaks down boundaries that typically distinguish types from values, and a polymorphic utility can potentially work on types as easily as it works on values, so that some of our existing programming patterns can essentially be used for extending the compiler.
That’s one ideal of dependent typing anyway; in dependent type systems, there’s a tradeoff between ease-of-use and the mathematical rigor of “what we know about that value.” Mathematical rigor isn’t really something we can have halfway (though there are multiple ways we can appraise it, e.g. multiple foundational theories our own theory can be relatively consistent to or expressive of), so lots of research effort goes into pushing the boundaries of usability while preserving desirable proof-theoretical properties. For instance, if we naively allow arbitrary (potentially nonterminating) computation or allow full polymorphism on some type of all types (including this one), we open the door to mathematical inconsistency, and our compile-time knowledge is no longer trustworthy.
In effect, dependent typing introduces some new exotic values to our data structures (the exotic values being types), and certain kinds of dependent typing classify nonterminating functions as being too exotic to fit.
Back to syntax
I opened with a mention of syntax, and then I’ve blitzed through data, polymorphism, and these alternate kinds of dataflow on my way to the point.
Lisp gets pretty good mileage out of its syntax. When it handles program fragments as hierarchical lists of symbols, they’re about as intuitive to manipulate as any other list-structured data.
The thing is, encoding a program as a hierarchical structure in the first place is finicky business, with variable scoping issues to worry about. Now that I’ve seen that there are meaningful ways to reinterpret whole programs, I wonder how much more mileage a lisp variant would get if its surface syntax took care of scoping issues itself and left us with just a dataflow graph to manipulate.
Unfortunately, I think this surface syntax would inevitably be more verbose. If we assume little about the programming model at hand, we don’t get to fine-tune the syntax to work in the best way for that model. Additional syntactic abstraction before this step, in the form of a hierarchical macro system or a context-free parser, may make it more palatable.
