There Is Such A Thing As A Declarative Language, and It’s The World’s Best DSL

July 22, 2013

In a recent post I asked whether there is any such thing as a declarative language. The main point was to argue that the standard “definitions” are, at best, not very precise, and to see whether anyone might offer a better definition. What I’m after is an explanation of why people seem to think that the phrase has meaning, even though they can’t say very clearly what they mean by it.  (One commenter analogized with “love” and “happiness”, but I would counter by saying that we’re trying to do science here, and we ought to be able to define our terms with some precision.)

As I mentioned, perhaps the best “definition” that is usually offered is to say that “declarative” is synonymous with “functional-and-logic-programming”.  This is pretty unsatisfactory, since it is not so easy to define these terms either, and because, contrary to conventional classifications, the two concepts have pretty much nothing in common with each other (but for one thing to be mentioned shortly). The propositions-as-types principle helps set them clearly apart: whereas functional programming is about executing proofs, logic programming is about the search for proofs. Functional programming is based on the dynamics of proof given by Gentzen’s inversion principle. Logic programming is based on the dynamics of provability given by cut elimination and focusing.  The two concepts of computation could not be further apart.

Yet they do have one thing in common that is usefully isolated as fundamental to what we mean by “declarative”, namely the concept of a variable.  Introduced by the ancient Hindu and Muslim mathematicians, Brahmagupta and al Kwharizmi, the variable is one of the most remarkable achievements of the human intellect.  In my previous post I had secretly hoped that someone would propose variables as being central to what we mean by “declarative”, but no one did, at least not in the comments section.  My unstated motive for writing that post was not so much to argue that the term “declarative” is empty, but to test the hypothesis that few seem to have grasp the importance of  this concept for designing a civilized, and broadly applicable, programming language.

My contention is that variables, properly so-called, are what distinguish “declarative” languages from “imperative” languages. Although the imperative languages, including all popular object-oriented languages, are based on a concept that is called a variable, they lack anything that actually is a variable.   And this is where the trouble begins, and the need for the problematic distinction arises.  The declarative concept of a variable is the mathematical concept of an unknown that is given meaning by substitution. The imperative concept of a variable, arising from low-level machine models, is instead given meaning by assignment (mutation), and, by a kind of a notational pun, allowed to appear in expressions in a way that resembles that of a proper variable.  But the concepts are so fundamentally different, that I argue in PFPL that the imperative concept be called an “assignable”, which is more descriptive, rather than “variable”, whose privileged status should be emphasized, not obscured.

The problem with purely imperative programming languages is that they have only the concept of an assignable, and attempt to make it serve also as a concept of variable. The results are a miserable mess of semantic and practical complications. Decades of work has gone into rescuing us from the colossal mistake of identifying variables with assignables. And what is the outcome? If you want to reason about assignables, what you do is (a) write a mathematical formulation of your algorithm (using variables, of course) and (b) show that the imperative code simulates the functional behavior so specified.   Under this methodology the mathematical formulation is taken as self-evidently correct, the standard against which the imperative program is judged, and is not itself in need of further verification, whereas the imperative formulation is, invariably, in need of verification.

What an odd state of affairs!  The functional “specification” is itself a perfectly good, and apparently self-evidently correct, program.  So why not just write the functional (i.e., mathematical) formulation, and call it a day?  Why indeed!  Declarative languages, being grounded in the language of mathematics, allow for the identification of the “desired behavior” with the “executable code”.  Indeed, the propositions-as-types principle elevates this identification to a fundamental organizing principle: propositions are types, and proofs are programs.  Who needs verification?  Once you have a mathematical specification of the behavior of a queue, say, you already have a running program; there is no need to relegate it to a stepping stone towards writing an awkward, and invariably intricate, imperative formulation that then requires verification to ensure that it works properly.

Functional programming languages are written in the universally applicable language of mathematics as expressed by the theory of types.  Such languages are therefore an integral part of science itself, inseparable from our efforts to understand and master the workings of the world.  Imperative programming has no role to play in this effort, and is, in my view, doomed in the long run to obsolescence, an artifact of engineering, rather than a fundamental discovery on a par with those of mathematics and science.

This brings me to my main point, the popular concept of a domain-specific language. Very much in vogue, DSL’s are offered as the solution to many of our programming woes. And yet, to borrow a phrase from my colleague Guy Blelloch, the elephant in the room is the question “what is a domain?”. I’ve yet to hear anyone explain how you decide what are the boundaries of a “domain-specific” language. Isn’t the “domain” mathematics and science itself? And does it not follow that the right language must be the language of mathematics and science? How can one rule out anything as being irrelevant to a “domain”?  I think it is impossible, or at any rate inadvisable, to make such restrictions a priori.  Indeed, full-spectrum functional languages are already the world’s best DSL’s, precisely because they are (or come closest to being) the very language of science, the ultimate “domain”.


What, If Anything, Is A Declarative Language?

July 18, 2013

Back in the 1980’s it was very fashionable to talk about “declarative” programming languages.  But to my mind there was never a clear definition of a “declarative language”, and hence no way to tell what is declarative and what is not.  Lacking any clear meaning, the term came to refer to the arbitrary conflation of functional with logic programming to such an extent that “functional-and-logic-programming” almost became a Germanic thing-in-itself (ding an sich).  Later, as the logic programming wave subsided, the term “declarative”,  like “object-oriented”, came to be an expression of approval, and then, mercifully, died out.

Or so I had thought.  Earlier this week I attended a thriller of an NSF-sponsored workshop on high-level programming models for parallelism, where I was surprised by the declarative zombie once again coming to eat our brains.  This got me to thinking, again, about whether the term has any useful meaning.  For what it’s worth, and perhaps to generate useful debate, here’re some things that I think people mean, and why I don’t think they mean very much.

  1. “Declarative” means “high-level”.  This just seems to replace one vague term by another.
  2. “Declarative” means “not imperative”.  But this flies in the face of reality.  Functional languages embrace and encompass imperative programming as a special case, and even Prolog has imperative features, such as assert and retract, that have imperative meaning.
  3. “Declarative” means “functional”.  OK, but then we don’t really need another word.
  4. “Declarative” means “what, not how”.  But every language has an operational semantics that defines how to execute its programs, and you must be aware of that semantics to understand programs written in it.  Haskell has a definite evaluation order, just as much as ML has a different one, and even Prolog execution is defined by a clear operational semantics that determines the clause order and that can be influenced by “cut”.
  5. “Declarative” means “equational”.  This does not distinguish anything, because there is a well-defined notion of equivalence for any programming language, namely observational equivalence.  Different languages induce different equivalences, of course, but how does one say that one equivalence is “better” than another?  At any rate, I know of no stress on equational properties of logic programs, so either logic programs are not “declarative” or “equational reasoning” is not their defining characteristic.
  6. “Declarative” means “referentially transparent”.  The misappropriation of Quine’s terminology only confuses matters.  All I’ve been able to make of this is that “referentially transparent” means that beta-equivalence is valid.  But beta equivalence is not a property of an arbitrary programming language, nor in any case is it clear why this equivalence is first among equals.  In any case why you would decide a priori on what equivalences you want before you even know what it means to run a program?
  7. “Declarative” means “has a denotation”.  This gets closer to the point, I think, because we might well say that a declarative semantics is one that gives meaning to programs as some kind of mapping between some sort of spaces.  In other words, it would be a synonym for “denotational semantics”.  But every language has a denotational semantics (perhaps by interpretation into a Kripke structure to impose sequencing), so having one does not seem to distinguish a useful class of languages.  Moreover, even in the case of purely functional programs, the usual denotational semantics (as continuous maps) is not fully abstract, and the fully abstract semantics (as games) is highly operational.  Perhaps a language is declarative in proportion to being able to give it semantics in some “familiar” mathematical setting?
  8. “Declarative” means “implicitly parallelizable“.  This was certainly the sense intended at the NSF meeting, but no two “declarative” languages seemed to have much in common.  Charlie Garrod proposes just “implicit”, which is pretty much synonymous with “high level”, and may be the most precise sense there is to the term.

No doubt this list is not exhaustive, but I think it covers many of the most common interpretations.  It seems to me that none of them have a clear meaning or distinguish a well-defined class of languages.  Which leads me to ask, is there any such thing as a declarative programming language?

[Thanks to the late Steve Gould for inspiring the title of this post.]

[Update: wordsmithing.]

[Update: add a remark about semantics, add another candidate meaning.]

[Update: added link to previous post.]

Constructive Mathematics Is Not Metamathematics

July 10, 2013

The publication of the Homotopy Type Theory book has renewed interest in type theory as a foundation for mathematics, and spurred computer scientists to investigate the computational meaning of higher-dimensional types. As I mentioned in a previous post, what makes HoTT work so well for homotopy theory is that it is constructive, which means, at the very least, that it does not postulate that all types are decidable. By Hedberg’s Theorem any type with decidable equality is a set (homotopy 0-type), so a blanket adoption of the classical law of the excluded middle would immediately rule out any higher-dimensional structure.

To my way of thinking, the denial of the universal validity of the excluded middle is not the defining feature of constructivity, but rather a characteristic feature of constructivity—it is the smoke, not the locomotive. But what, then, is the deeper meaning of constructivity that gives rise to the denial of many classical patterns of reasoning, such as proof by contradiction or reasoning by cases on whether a proposition is true or not? Although the full story is not yet completely clear, a necessary condition is that a constructive theory be proof relevant, meaning that proofs are mathematical objects like any other, and that they play a role in the development of constructive mathematics unlike their role in classical mathematics.

The most obvious manifestation of proof relevance is the defining characteristic of HoTT, that proofs of equality correspond to paths in a space. Paths may be thought of as evidence for the equality of their endpoints. That this is a good notion of equality follows from the homotopy invariance of the constructs of type theory: everything in sight respects paths (that is, respect the groupoid structure of types). More generally, theorems in HoTT tend to characterize the space of proofs of a proposition, rather than simply state that the corresponding type is inhabited. For example, the univalence axiom itself states an equivalence between proofs of equivalence of types in a universe and equivalences between these types. This sort of reasoning may take some getting used to, but its beauty is, to my way of thinking, undeniable. Classical modes of thought may be recovered by explicitly obliterating the structure of proofs using truncation. Sometimes this is the best or only available way to state a theorem, but usually one tends to say more than just that a type is inhabited, or that two types are mutually inhabited. In this respect the constructive viewpoint enriches, rather than diminishes, classical mathematics, a point that even the greatest mathematician of the 20th century, David Hilbert, seems to have missed.

The concept of proof relevance in HoTT seems to have revived a very common misunderstanding about the nature of proofs. Many people have been trained to think that a proof is a derivation in an axiomatic theory, such as set theory, a viewpoint often promoted in textbooks and bolstered by the argument that an informal proof can always be written out in full in this form, even if we don’t do that as a matter of course. It is a short step from there to the conclusion that proofs are therefore mathematical objects, even in classical set theory, because we can treat the derivations as elements of an inductively defined set (famously, the set of natural numbers, but more realistically using more natural representations of abstract syntax such as the s-expression formalism introduced by McCarthy in 1960 for exactly this purpose). From this point of view many people are left confused about the stress on “proofs as mathematical objects” as a defining characteristic of HoTT, and wonder what could be original about that.

The key to recognize that a proof is not a formal proof. To avoid further confusion, I hasten to add that by “formal” I do not mean “rigorous”, but rather “represented in a formal system” such as the axiomatic theory of sets. A formal proof is an element of a computably enumerable set generated by the axioms and rules of the formal theory. A proof is an argument that demonstrates the truth of a proposition. While formal proofs are always proofs (at least, under the assumption of consistency of the underlying formal theory), a proof need not be, or even have a representation as, a formal proof. The principal example of this distinction is Goedel’s Theorem, which proves that the computably enumerable set of formal provable propositions in axiomatic arithmetic is not decidable. The key step is to devise a self-referential proposition that (a) is not formally provable, but (b) has a proof that shows that it is true. The crux of the argument is that once you fix the rules of proof, you automatically miss out true things that are not provable in that fixed system.

Now comes the confusing part. HoTT is defined as a formal system, so why doesn’t the same argument apply? It does, pretty much verbatim! But this has no bearing on “proof relevance” in HoTT, because the proofs that are relevant are not the formal proofs (derivations) defining HoTT as a formal system. Rather proofs are formulated internally as objects of the type theory, and there is no commitment a priori to being the only forms of proof there are. Thus, for example, we may easily see that there are only countably many functions definable in HoTT from the outside (because it is defined by a formal system), but within the theory any function space on an infinite type has uncountably many elements. There is no contradiction, because the proofs of implications, being internal functions, are not identified with codes of formal derivations, and hence are not denumerable.

There is a close analogy, previously noted in this blog, with Church’s Law. Accepting Church’s Law internally amounts to fixing the programming language used to define functions in advance, permitting us to show, for example, that certain programs are not expressible in that language. But HoTT does not commit to Church’s Law, so such arguments amount to showing that, for example, there is no Turing machine to decide halting for Turing machines, but allowing that there could be constructive functions (say, equipped with oracles) that make such decisions.

The theory of formal proofs, often called proof theory, was dubbed metamathematics by Kleene. Until the development of type theory the study of proofs was confined to metamathematics. But now in the brave new world of constructive mathematics as embodied in HoTT, proofs (not just formal proofs) have pride of place in mathematics, and provide opportunities for expressing concepts clearly and cleanly that were hitherto obscured or even hidden from our view.

Update: Corrected silly wording mistake.