Implicit homomorphism

One of the really nice features of macros and their mathematical first cousin notational definitions is that they leave their straightforward, recursive expansion implicit. When we write in math:

A ⇔ B = A ⇒ B ∧ B ⇒ A

what we really mean is that all occurrences of ⇔ should be recursively expanded within a term. But there's essentially an implicit structural recursion through all propositions in the logic (which is left open "until" all notational definitions have been provided) which expands any occurrences of notational definitions homomorphically through sub-propositions. We don't require anyone to go through the painstaking and virtually information-free process of explicitly marking all points of recursive expansion.

I would love a similar notational style for defining annotations. I often find myself defining an instrumentation function that inserts one or two kinds of extra pieces of information into a tree. Maybe term-rewriting would work pretty well for this. Say we're writing a function that annotates certain λ-expressions with their height. We could write

λ x . e → λ [ |e| ] x . e

and then leave the compatible, reflexive, and transitive closure of this rewriting rule implicit, since they're obvious.

Then I would really like some way to make this style of definition composable with other definitions, so for example I could define a type-checking-cum-instrumentation algorithm

Γ ⊢ e : τ → e'

where the instrumentation portion (→ e') is mostly left implicit.

How to impair a declarative

Declarative programming is a vague term but could loosely be interpreted to mean not imperative programming. It's also about defining a program by breaking it into separate, modular units of partial specification.

Of course, the language's semantics has to have some algorithmic means to combine these declarations into a complete program definition. And if the language admits recursive definitions, the combined program may contains cycles. So the implementation of a declarative language will often have an imperative flavor, combining recursive elements by incrementally updating the set of definitions.

The question is whether it is still possible for the user to understand the semantics without resorting to reasoning about its possibly-imperative implementation. Specifically, the user shouldn't have to worry about time. If the order in which definitions are combined matters, then the semantics becomes imperative. Worse, if the programming interface allows definitions in multiple files, the order of definition might not even be under the user's control--or worse, it might only be controllable through extra-linguistic means like compiler command-line arguments.

Take as an example a language with open recursion, the ability to define a recursive function in multiple, disparate pieces. If an open recursive function has overlapping cases in separate declarations, the language can handle this in one of several ways:

1. Let rules defined "later" take precedence over rules defined "earlier."
2. Define a total order on rule specificity, and let more specific rules take precedence over less specific rules.
3. Disallow overlapping cases statically.

Option #1 reintroduces the notion of time. The resulting semantics is less modular, because it requires understanding not just the individual modules, but subtle aspects of their composition. (If the algorithm for combining definitions is sophisticated--unification, for example--this order may even be a complicated dynamic notion, not just textual order.) The other two options eliminate the imperative flavor, defining time out of the semantics. This frees the programmer to reorder definitions without affecting the program's meaning, and making the program's meaning more modular.

ADTs in JavaScript

Sjoerd Visscher has written a neat post about implementing algebraic data types in JavaScript. There are lots of ways to do this, but this one looks interesting. I don't quite understand it but I thought I'd point it out.

Note the use of expression closures! Good stuff.

Clumsy existential

This might be a dumb question: I often want to prove something like this:

(∃ v . e ⇒ v) ⇔ (∃ v′ ~ v . [[e]] ⇒ v′)

except that the scope doesn't work out: v is only in scope in the first parenthesized proposition, so it can't be referred to in the second one. Of course, it's generally sufficient to prove co-termination and just leave out the relationship between the final values, since that's usually easily derivable. But it's an important part of the intuition behind correctness, so I want the relationship between answers to be in the statement of the theorem.

An awkward way to make this work is to write big clunky conjunctions like:

(e⇓ ⇔ [[e]]⇓) ∧ (∀ v . e ⇒ v . ∃ v′ ~ v . [[e]] ⇒ v′)

But it would be nice if there were some way to write it more compactly like the first pseudo-proposition I wrote. I like that it reads almost like you'd say in English: "e and [[e]] always get the same answers."

Anyone have any suggestions?