Existential Type

Polarity in Type Theory

August 25, 2012

There has recently arisen some misguided claims about a supposed opposition between functional and object-oriented programming. The claims amount to a belated recognition of a fundamental structure in type theory first elucidated by Jean-Marc Andreoli, and developed in depth by Jean-Yves Girard in the context of logic, and by Paul Blain-Levy and Noam Zeilberger in the context of programming languages. In keeping with the general principle of computational trinitarianism, the concept of polarization has meaning in proof theory, category theory, and type theory, a sure sign of its fundamental importance.

Polarization is not an issue of language design, it is an issue of type structure. The main idea is that types may be classified as being positive or negative, with the positive being characterized by their structure and the negative being characterized by their behavior. In a sufficiently rich type system one may consider, and make effective use of, both positive and negative types. There is nothing remarkable or revolutionary about this, and, truly, there is nothing really new about it, other than the terminology. But through the efforts of the above-mentioned researchers, and others, we have learned quite a lot about the importance of polarization in logic, languages, and semantics. I find it particularly remarkable that Andreoli’s work on proof search turned out to also be of deep significance for programming languages. This connection was developed and extended by Zeilberger, on whose dissertation I am basing this post.

The simplest and most direct way to illustrate the ideas is to consider the product type, which corresponds to conjunction in logic. There are two possible ways that one can formulate the rules for the product type that from the point of view of inhabitation are completely equivalent, but from the point of view of computation are quite distinct. Let us first state them as rules of logic, then equip these rules with proof terms so that we may study their operational behavior. For the time being I will refer to these as Method 1 and Method 2, but after we examine them more carefully, we will find more descriptive names for them.

Method 1 of defining conjunction is perhaps the most familiar. It consists of this introduction rule

$\displaystyle\frac{\Gamma\vdash A\;\textsf{true}\quad\Gamma\vdash B\;\textsf{true}}{\Gamma\vdash A\wedge B\;\textsf{true}}$

and the following two elimination rules

$\displaystyle\frac{\Gamma\vdash A\wedge B\;\textsf{true}}{\Gamma\vdash A\;\textsf{true}}\qquad\frac{\Gamma\vdash A\wedge B\;\textsf{true}}{\Gamma\vdash B\;\textsf{true}}$ .

Method 2 of defining conjunction is only slightly different. It consists of the same introduction

$\displaystyle \frac{\Gamma\vdash A\;\textsf{true}\quad\Gamma\vdash B\;\textsf{true}}{\Gamma\vdash A\wedge B\;\textsf{true}}$

and one elimination rule

$\displaystyle\frac{\Gamma\vdash A\wedge B\;\textsf{true} \quad \Gamma,A\;\textsf{true},B\;\textsf{true}\vdash C\;\textsf{true}}{\Gamma\vdash C\;\textsf{true}}$ .

From a logical point of view the two formulations are interchangeable in that the rules of the one are admissible with respect to the rules of the other, given the usual structural properties of entailment, specifically reflexivity and transitivity. However, one can discern a difference in “attitude” in the two formulations that will turn out to be a manifestation of the concept of polarity.

Method 1 is a formulation of the idea that a proof of a conjunction is anything that behaves conjunctively, which means that it supports the two elimination rules given in the definition. There is no commitment to the internal structure of a proof, nor to the details of how projection operates; as long as there are projections, then we are satisfied that the connective is indeed conjunction. We may consider that the elimination rules define the connective, and that the introduction rule is derived from that requirement. Equivalently we may think of the proofs of conjunction as being coinductively defined to be as large as possible, as long as the projections are available. Zeilberger calls this the pragmatist interpretation, following Count Basie’s principle, “if it sounds good, it is good.”

Method 2 is a direct formulation of the idea that the proofs of a conjunction are inductively defined to be as small as possible, as long as the introduction rule is valid. Specifically, the single introduction rule may be understood as defining the structure of the sole form of proof of a conjunction, and the single elimination rule expresses the induction, or recursion, principle associated with that viewpoint. Specifically, to reason from the fact that $A\wedge B\;\textsf{true}$ to derive $C\;\textsf{true}$ , it is enough to reason from the data that went into the proof of the conjunction to derive $C\;\textsf{true}$ . We may consider that the introduction rule defines the connective, and that the elimination rule is derived from that definition. Zeilberger calls this the verificationist interpretation.

These two perspectives may be clarified by introducing proof terms, and the associated notions of reduction that give rise to a dynamics of proofs.

When reformulated with explicit proofs, the rules of Method 1 are the familiar rules for ordered pairs:

$\displaystyle\frac{\Gamma\vdash M:A\quad\Gamma\vdash N:B}{\Gamma\vdash \langle M, N\rangle:A\wedge B}$

$\displaystyle\frac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash \textsf{fst}(M):A}\qquad\frac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash \textsf{snd}(M):B}$ .

The associated reduction rules specify that the elimination rules are post-inverse to the introduction rules:

$\displaystyle\textsf{fst}(\langle M,N\rangle)\mapsto M \qquad \textsf{snd}(\langle M,N\rangle)\mapsto N$ .

In this formulation the proposition $A\wedge B$ is often written $A\times B$ , since it behaves like a Cartesian product of proofs.

When formulated with explicit proofs, Method 2 looks like this:

$\displaystyle \frac{\Gamma\vdash M:A\quad\Gamma\vdash M:B}{\Gamma\vdash M\otimes N:A\wedge B}$

$\displaystyle\frac{\Gamma\vdash M:A\wedge B \quad \Gamma,x:A,y:B\vdash N:C}{\Gamma\vdash \textsf{split}(M;x,y.N):C}$

with the reduction rule

$\displaystyle\textsf{split}(M\otimes N;x,y.P)\mapsto [M,N/x,y]P$ .

With this formulation it is natural to write $A\wedge B$ as $A\otimes B$ , since it behaves like a tensor product of proofs.

Since the two formulations of “conjunction” have different internal structure, we may consider them as two different connectives. This may, at first, seem pointless, because it is easily seen that $x:A\times B\vdash M:A\otimes B$ for some $M$ and that $x:A\otimes B\vdash N:A\times B$ for some $N$ , so that the two connectives are logically equivalent, and hence interchangeable in any proof. But there is nevertheless a reason to draw the distinction, namely that they have different dynamics.

It is easy to see why. From the pragmatic perspective, since the projections act independently of one another, there is no reason to insist that the components of a pair be evaluated before they are used. Quite possibly we may only ever project the first component, so why bother with the second? From the verificationist perspective, however, we are pattern matching against the proof of the conjunction, and are demanding both components at once, so it makes sense to evaluate both components of a pair in anticipation of future pattern matching. (Admittedly, in a structural type theory one may immediately drop one of the variables on the floor and never use it, but then why give it a name at all? In a substructural type theory such as linear type theory, this is not a possibility, and the interpretation is forced.) Thus, the verficationist formulation corresponds to eager evaluation of pairing, and the pragmatist formulation to lazy evaluation of pairing.

Having distinguished the two forms of conjunction by their operational behavior, it is immediately clear that both forms are useful, and are by no means opposed to one another. This is why, for example, the concept of a lazy language makes no sense, rather one should instead speak of lazy types, which are perfectly useful, but by no means the only types one should ever consider. Similarly, the concept of an object-oriented language seems misguided, because it emphasizes the pragmatist conception, to the exclusion of the verificationist, by insisting that everything be an object characterized by its methods.

More broadly, it is useful to classify types into two polarities, the positive and the negative, corresponding to the verificationist and pragmatist perspectives. Positive types are inductively defined by their introduction forms; they correspond to colimits, or direct limits, in category theory. Negative types are coinductively defined by their elimination forms; they correspond to limits, or inverse limits, in category theory. The concept of polarity is intimately related to the concept of focusing, which in logic sharpens the concept of a cut-free proof and elucidates the distinction between synchronous and asynchronous connectives, and which in programming languages provides an elegant account of pattern matching, continuations, and effects.

As ever, enduring principles emerge from the interplay between proof theory, category theory, and type theory. Such concepts are found in nature, and do not depend on cults of personality or the fads of the computer industry for their existence or importance.

Update: word-smithing.

26 Comments | Programming, Research | Tagged: polarization, type theory | Permalink
Posted by Robert Harper

Intro Curriculum Update

August 17, 2012

In previous posts I have talked about the new introductory CS curriculum under development at Carnegie Mellon. After a year or so of planning, we began to roll out the new curriculum in the Spring of 2011, and have by now completed the transition. As mentioned previously, the main purpose is to bring the introductory sequence up to date, with particular emphasis on introducing parallelism and verification. A secondary purpose was to restore the focus on computing fundamentals, and correct the drift towards complex application frameworks that offer the students little sense of what is really going on. (The poster child was a star student who admitted that, although she had built a web crawler the previous semester, she in fact has no idea how to build a web crawler.) A particular problem is that what should have been a grounding in the fundamentals of algorithms and data structures turned into an exercise in object-oriented programming, swamping the core content with piles of methodology of dubious value to beginning students. (There is a new, separate, upper-division course on oo methodology for students interested in this topic.) A third purpose was to level the playing field, so that students who had learned about programming on the street were equally as challenged, if not more so, than students without much or any such experience. One consequence would be to reduce the concomitant bias against women entering CS, many fewer of whom having prior computing experience than the men.

The solution was a complete do-over, jettisoning the traditional course completely, and starting from scratch. The most important decision was to emphasize functional programming right from the start, and to build on this foundation for teaching data structures and algorithms. Not only does FP provide a much more natural starting point for teaching programming, it is infinitely more amenable to rigorous verification, and provides a natural model for parallel computation. Every student comes to university knowing some algebra, and they are therefore familiar with the idea of computing by calculation (after all, the word algebra derives from the Arabic al jabr, meaning system of calculation). Functional programming is a generalization of algebra, with a richer variety of data structures and a richer set of primitives, so we can build on that foundation. It is critically important that variables in FP are, in fact, mathematical variables, and not some distorted facsimile thereof, so all of their mathematical intuitions are directly applicable. So we can immediately begin discussing verification as a natural part of programming, using principles such as mathematical induction and equational reasoning to guide their thinking. Moreover, there are natural concepts of sequential time complexity, given by the number of steps required to calculate an answer, and parallel time complexity, given by the data dependencies in a computation (often made manifest by the occurrences of variables). These central concepts are introduced in the first week, and amplified throughout the semester.

Two major homework exercises embody the high points of the first-semester course, one to do with co-development of code with proof, the other to do with parallelism. Co-development of program and proof is illustrated by an online regular expression matcher. The problem is a gem for several reasons. One is that it is essentially impossible for anyone to solve by debugging a blank screen. This sets us up nicely for explaining the importance of specification and proof as part of the development process. Another is that it is very easy, almost inevitable, for students to make mistakes that are not easily caught or diagnosed by testing. We require the students to carry out a proof of the correctness of the matcher, and in the process discover a point where the proof breaks down, which then leads to a proper solution. (See my JFP paper “Proof-Directed Debugging” for a detailed development of the main ideas.) The matcher also provides a very nice lesson in the use of higher-order functions to capture patterns of control, resulting in an extremely clean and simple matcher whose correctness proof is highly non-trivial.

The main parallelism example is the Barnes-Hut algorithm for solving the n-body problem in physics. Barnes-Hut is an example of a “tree-based” method, invented by Andrew Appel, for solving this well-known problem. At a high level the main idea is to decompose space into octants (or quadrants if you’re working in the plane), recursively solving the problem for each octant and then combining the solutions to make an overall solution. The key idea is to use an approximation for bodies that are far enough away—a distant constellation can be regarded as an atomic body for the purposes of calculating the effects of its stars on the sun, say. The problem is naturally parallelizable, because of the recursive decomposition. Moreover, it provides a very nice link to their high school physics. Since FP is just an extension of mathematics, the equations specifying the force law and Newton’s Law carry over directly to the code. This is an important sense in which FP builds on and amplifies their prior mathematical experience, and shows how one may connect computer science with other sciences in a rather direct manner.

The introductory FP course establishes the basis for the new data structures and algorithms course that most students take in either the third or fourth semester. This course represents a radical departure from tradition in several ways. First, it is a highly rigorous course in algorithms that rivals the upper-division course taught at most universities (including our own) for the depth and breadth of ideas it develops. Second, it takes the stance that all algorithms are parallel algorithms, with sequential being but a special case of parallel. Of course some algorithms have a better parallelizability ratio (a precise technical characterization of the ability to make use of parallelism), and this can be greatly affected by data structure selection, among other considerations. Third, the emphasis is on persistent abstract types, which are indispensable for parallel computing. No more linked lists, no more null pointer nonsense, no more mutation. Instead we consider abstract types of graphs, trees, heaps, and so forth, all with a persistent semantics (operations create “new” ones, rather than modify “old” ones). Fourth, we build on the reasoning methods introduced in the first semester course to prove the correctness and the efficiency of algorithms. Functional programming makes all of this possible. Programs are concise and amenable to proof, they are naturally parallel, and they enjoy powerful typing properties that enforce abstraction in a mathematically rigorous manner. Fifth, there is a strong emphasis on problems of practical interest. For example, homework 1 is the shotgun method for genome sequencing, a parallel algorithm of considerable practical importance and renown.

There is a third introductory course in imperative programming, taken in either the first or second semester (alternating with the functional programming course at the student’s discretion), that teaches the “old ways” of doing things using a “safe” subset of C. Personally, I think this style of programming is obsolete, but there are many good reasons to continue to teach it, the biggest probably being the legacy problem. The emphasis is on verification, using simple assertions that are checked at run-time and which may be verified statically in some situations. It is here that students learn how to do things “the hard way” using low-level representations. This course is very much in the style of the 1970’s era data structures course, the main difference being that the current incarnation of Pascal has curly braces, rather than begin-end.

For the sake of those readers who may not be up to date on such topics, it seems important to emphasize that functional programming subsumes imperative programming. Every functional language is capable of expressing the old-fashioned sequential pointer-hacking implementation of data structures. You can even reproduce Tony Hoare’s self-described “billion dollar mistake” of the cursed “null pointer” if you’d like! But the whole point is that it is rarely useful, and almost never elegant, to work that way. (Curiously, the “monad mania” in the Haskell community stresses an imperative, sequential style of programming that is incompatible with parallelism, but this is not forced on you as it is in the imperative world.) From this point of view there no loss, and considerable gain, in teaching functional programming from the start. It puts a proper emphasis on mathematically sane programming methods, but allows for mutation-based programming where appropriate (for example, in engendering “side effects” on users).

To learn more about these courses, please see the course web pages:

I encourage readers to review the syllabi and course materials. There is quite a large body of material in place that we plan to expand into textbook-level treatments in the near future. We also plan to write a journal article documenting our experiences with these courses.

I am very grateful to my colleagues Guy Blelloch, Dan Licata, and Frank Pfenning for their efforts in helping to develop the new introductory curriculum at Carnegie Mellon, and to the teaching assistants whose hard work and dedication put the ideas into practice.

Update: Unfortunately, the homework assignments for these courses are not publicly available, because we want to minimize the temptation for students to make use of old assignments and solutions in preparing their own work. I am working with my colleagues to find some way in which we can promote the ideas without sacrificing too much of the integrity of the course materials. I apologize for the inconvenience.

10 Comments | Teaching | Tagged: functional programming, imperative programming, parallelism, verification | Permalink
Posted by Robert Harper

Extensionality, Intensionality, and Brouwer’s Dictum

August 11, 2012

There seems to be a popular misunderstanding about the propositions-as-types principle that has led some to believe that intensional type theory (ITT) is somehow preferable to or more sensible than extensional type theory (ETT). Now, as a practical matter, few would dispute that ETT is much easier to use than ITT for mechanizing everyday mathematics. Some justification for this will be given below, but I am mainly concerned with matters of principle. Specifically, I wish to dispute the claim that t ETT is somehow “wrong” compared to ITT. The root of the problem appears to be a misunderstanding of the fundamental ideas of intuitionism, which are expressed by the proposition-as-types principle.

The most popular conception appears to be the trivial one, namely that certain inductively defined formal systems of logic correspond syntactically to certain inductively defined formal systems of typing. Such correspondences are not terribly interesting, because they can easily be made to hold by construction: all you need to do is to introduce proof terms that summarize a derivation, and then note that the proofs of a proposition correspond to the terms of the associated type. In this form the propositions-as-types principle is often dubbed, rather grandly, the Curry-Howard Isomorphism. It’s a truism that most things in mathematics are named after anyone but their discoverers, and that goes double in this case. Neither Curry nor Howard discovered the principle (Howard himself disclaims credit for it), though they both did make contributions to it. Moreover, this unfortunate name deprives credit to those who did the real work in inventing the concept, including Brouwer, Heyting, Kolmogorov, deBruijn, and Martin-Löf. (Indeed, it is sometimes called the BHK Correspondence, which is both more accurate and less grandiose.) Worse, there is an “isomorphism” only in the most trivial sense of an identity by definition, hardly worth emphasizing.

The interesting conception of the propositions-as-types principle is what I call Brouwer’s Dictum, which states that all of mathematics, including the concept of a proof, is to be derived from the concept of a construction, a computation classified by a type. In intuitionistic mathematics proofs are themselves “first-class” mathematical objects that inhabit types that may as well be identified with the proposition that they prove. Proving a proposition is no different than constructing a program of a type. In this sense logic is a branch of mathematics, the branch concerned with those constructions that are proofs. And mathematics is itself a branch of computer science, since according to Brouwer’s Dictum all of mathematics is to be based on the concept of computation. But notice as well that there are many more constructions than those that correspond to proofs. Numbers, for example, are perhaps the most basic ones, as would be any inductive or coinductive types, or even more exotic objects such as Brouwer’s own choice sequences. From this point of view the judgement $M\in A$ stating that $M$ is a construction of type $A$ is of fundamental importance, since it encompasses not only the formation of “ordinary” mathematical constructions, but also those that are distinctively intuitionistic, namely mathematical proofs.

An often misunderstood point that must be clarified before we continue is that the concept of proof in intuitionism is not to be identified with the concept of a formal proof in a fixed formal system. What constitutes a proof of a proposition is a judgement, and there is no reason to suppose a priori that this judgement ought to be decidable. It should be possible to recognize a proof when we see one, but it is not required that we be able to rule out what is a proof in all cases. In contrast formal proofs are inductively defined and hence fully circumscribed, and we expect it to be decidable whether or not a purported formal proof is in fact a formal proof, that is whether it is well-formed according to the given inductively defined rules. But the upshot of Gödel’s Theorem is that as soon as we fix the concept of formal proof, it is immediate that it is not an adequate conception of proof simpliciter, because there are propositions that are true, which is to say have a proof, but have no formal proof according to the given rules. The concept of truth, even in the intuitionistic setting, eludes formalization, and it will ever be thus. Putting all this another way, according to the intuitionistic viewpoint (and the mathematical practices that it codifies), there is no truth other than that given by proof. Yet the rules of proof cannot be given in decidable form without missing the point.

It is for this reason that the first sense of the propositions-as-types principle discussed above is uninteresting, for it only ever codifies a decidable, and hence incomplete, conception of proof. Moreover, the emphasis on an isomorphism between propositions and types also misses the point, because it fails to account for the many forms of type that do not correspond to propositions. The formal correspondence is useful in some circumstances, namely those in which the object of study is a formal system. So, for example, in LF the goal is to encode formal systems, and hence it is essential in the LF methodology that type checking be decidable. But when one is talking about a general theory of computation, which is to say a general theory of mathematical constructions, there is no reason to expect either an isomorphism or decidability. (So please stop referring to propositions-as-types as “the Curry-Howard Isomorphism”!)

We are now in a position to discuss the relationship between ITT and ETT, and to correct the misconception that ETT is somehow “wrong” because the typing judgement is not decidable. The best way to understand the proper relationship between the two is to place them into the broader context of homotopy type theory, or HTT. From the point of view of homotopy type theory ITT and ETT represent extremal points along a spectrum of type theories, which is to say a spectrum of conceptions of mathematical construction in Brouwer’s sense. Extensional type theory is the theory of homotopy sets, or hSets for short, which are spaces that are homotopically discrete, meaning that the only path (evidence for equivalence) of two elements is in fact the trivial self-loop between an element and itself. Therefore if we have a path between $x$ and $y$ in $A$ , which is to say a proof that they are equivalent, then $x$ and $y$ are equal, and hence interchangeable in all contexts. The bulk of everyday mathematics takes place within the universe of hSets, and hence is most appropriately expressed within ETT, and experience has born this out. But it is also interesting to step outside of this framework and consider richer conceptions of type.

For example, as soon as we introduce universes, one is immediately confronted with the need to admit types that are not hSets. A universe of hSets naturally includes non-trivial paths between elements witnessing their isomorphism as hSets, and hence their interchangeability in all contexts. Taking a single universe of hSets as the sole source of such additional structure leads to (univalent) two-dimensional type theory. In this terminology ETT is then to be considered as one-dimensional type theory. Universes are not the only source of higher dimensionality. For example, the interval has two elements, $0$ and $1$ connected by a path, the segment between them, which may be seen as evidence for their interchangeability (we can slide them along the segment one to the other). Similarly, the circle $S^1$ is a two-dimensional inductively defined type with one element, a base point, and one path, a non-reflexive self-loop from the base point to itself. It is now obvious that one may consider three-dimensional type theory, featuring types such as $S^2$ , the sphere, and so forth. Continuing this through all finite dimensions, we obtain finite-dimensional type theory, which is just ITT (type theory with no discreteness at any dimension).

From this perspective one can see more clearly why it has proved so awkward to formalize everyday mathematics in ITT. Most such work takes place in the universe of hSets, and makes no use of higher-dimensional structure. The natural setting for such things is therefore ETT, the theory of types as homotopically discrete sets. By formalizing such mathematics within ITT one is paying the full cost of higher-dimensionality without enjoying any of its benefits. This neatly confirms experience with using NuPRL as compared to using Coq for formulating the mathematics of homotopy sets, and why even die-hard ITT partisans find themselves wanting to switch to ETT for doing real work (certain ideological commitments notwithstanding). On the other hand, as higher-dimensional structure becomes more important to the work we are doing, something other than ETT is required. One candidate is a formulation of type theory with explicit levels, representing the dimensionality restriction appropriate to the problem domain. So work with discrete sets would take place within level 1, which is just extensional type theory. Level 2 is two-dimensional type theory, and so forth, and the union of all finite levels is something like ITT. To make this work requires that there be a theory of cumulativity of levels, a theory of resizing that allows us to move work at a higher level to a lower level at which it still makes sense, and a theory of truncation that allows suppression of higher-dimensional structure (generalizing proof irrelevance and “squash” types).

However this may turn out, it is clear that the resulting type theory will be far richer than merely the codification of the formal proofs of some logical system. Types such as the geometric spaces mentioned above do not arise as the types of proofs of propositions, but rather are among the most basic of mathematical constructions, in complete accordance with Brouwer’s dictum.

9 Comments | Research | Tagged: extensionality, homotopy, intensionality, type theory | Permalink
Posted by Robert Harper

Church’s Law

August 9, 2012

A new feature of this year’s summer school was a reduction in the number of lectures, and an addition of daily open problem sessions for reviewing the day’s material. This turned out to be a great idea for everyone, because it gave us more informal time together, and gave the students a better chance at digesting a mountain of material. It also turned out to be a bit of an embarrassment for me, because I posed a question off the top of my head for which I thought I had two proofs, neither of which turned out to be valid. The claimed theorem is, in fact, true, and one of my proofs is easily corrected to resolve the matter (the other, curiously, remains irredeemable for reasons I’ll explain shortly). The whole episode is rather interesting, so let me recount a version of it here for your enjoyment.

The context of the discussion was extensional type theory, or ETT, which is characterized by an identification of judgemental with propositional equality: if you can prove that two objects are equal,then they are interchangeable for all purposes without specific arrangement. The alternative, intensional type theory,or ITT, regards judgemental equality as definitional equality (symbolic evaluation), and gives computational meaning to proofs of equality of objects of a type, allowing in particular transport across two instances of a family whose indices are equal. NuPRL is an example of an ETT; CiC is an example of an ITT.

Within the framework of ETT, the principle of function extensionality comes “for free”, because you can prove it to hold within the theory. Function extensionality states that $f=g:A\to B$ whenever $x:A\vdash f(x)=g(x):B$ . That is, two functions are if they are equal on all arguments (and, implicitly, respect equality of arguments). Function extensionality holds definitionally if your definitional equivalence includes the $\eta$ and $\xi$ rules, but in any case does not have the same force as extensional equality. Function extensionality as a principle of equality cannot be derived in ITT, but must be added as an additional postulate (or derived from a stronger postulate, such as univalence or the existence of a one-dimensional interval type).

Regardless of whether we are working in an extensional or an intensional theory, it is easy to see that all functions of type $N\to N$ definable in type theory are computable. For example, we may show that all such functions may be encoded as recursive functions in the sense of Kleene, or in a more modern formulation we may give a structural operational semantics that provides a deterministic execution model for such functions (given $n:N$ , run $f:N\to N$ on $n$ until it stops, and yield that as result). Of course the proof relies on some fairly involved meta-theory, but it is all constructively valid (in an informal sense) and hence provides a legitimate computational interpretation of the theory. Another way to say the same thing is to say that the comprehension principles of type theory are such that every object deemed to exist has a well-defined computational meaning, so it follows that all functions defined within it are going to be computable.

This is all just another instance of Church’s Law, the scientific law stating that any formalism for defining computable functions will turn out to be equivalent to, say, the λ-calculus when it comes to definability of number-theoretic functions. (Ordinarily Church’s Law is called Church’s Thesis, but for reasons given in my Practical Foundations book, I prefer to give it the full status of a scientific law.) Type theory is, in this respect, no better than any other formalism for defining computable functions. By now we have such faith in Church’s Law that this remark is completely unsurprising, even boring to state explicitly.

So it may come as a surprise to learn that Church’s Law is false. I’m being provocative here, so let me explain what I mean before I get flamed to death on the internet. The point I wish to make is that there is an important distinction between the external and the internal properties of a theory. For example, in first-order logic the Löwenheim-Skolem Theorem tells us that if a first-order theory has an infinite model, then it has a countable model. This implies that, externally to ZF set theory, there are only countably many sets, even though internally to ZF set theory we can carry out Cantor’s argument to show that the powerset operation takes us to exponentially higher cardinalities far beyond the countable. One may say that the “reason” is that the evidence for the countability of sets is a bijection that is not definable within the theory, so that it cannot “understand” its own limitations. This is a good thing.

The situation with Church’s Law in type theory is similar. Externally we know that every function on the natural numbers is computable. But what about internally? The internal statement of Church’s Law is this: $\Pi f:N\to N.\Sigma n:N. n\Vdash f$ , where the notation $n\Vdash f$ means, informally, that $n$ is the code of a program that, when executed on input $m:N$ , evaluates to $f(m)$ . In Kleene’s original notation this would be rendered as $\Pi m:N.\Sigma p:N.T(n,m,p)\wedge Id(U(p),f(m))$ , where the $T$ predicate encodes the operational semantics, and the $U$ predicate extracts the answer from a successful computation. Note that the expansion makes use of the identity type at the type $N$ . The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction.

When I posed this as an exercise at the summer school, I had in mind two different proofs, which I will now sketch. Neither is valid, but there is a valid proof that I’ll come to afterwards.

Both proofs begin by applying the so-called Axiom of Choice. For those not familiar with type theory, the “axiom” of choice is in fact a theorem, stating that every total binary relation contains a function. Explicitly,

$(\Pi x:A.\Sigma y:B.R(x,y)) \to \Sigma f:A\to B.\Pi x:A.R(x,f(x)).$

The function $f$ is the “choice function” that associates a witness to the totality of $R$ to each argument $x$ . In the present case if we postulate Church’s Law, then by the axiom of choice we have

$\Sigma F:(N\to N)\to N.\Pi f:N\to N. F(f)\Vdash f$ .

That is, the functional $F$ picks out, for each function $f$ in $N\to N$ , a (code for a) program that witnesses the computability of $f$ . This should already seem suspicious, because by function extensionality the functional $F$ must assign the same program to any two extensionally equal functions.

We may easily see that $F$ is injective, for if $F(f)$ is $F(g)$ , then both track both $f$ and $g$ , and hence $f$ and $g$ are (extensionally) equal. Thus we have an injection from $N\to N$ into $N$ , which seems “impossible” … except that it is not! Let’s try the proof that this is impossible, and see where it breaks down. Suppose that $i:(N\to N)\to N$ is injective. Define $d(x)=i^{-1}(x)(x)+1$ , and consider $d(i(d))=i^{-1}(i(d))(i(d))+1=d(i(d))+1$ so $0=1$ and we are done. Not so fast! Since $i$ is only injective, and not necessarily surjective, it is not clear how to define $i^{-1}$ . The obvious idea is to send $x=i(f)$ to $f$ , and any $x$ outside the image of $i$ to, say, the identity. But there is no reason to suppose that the image of $i$ is decidable, so the attempted definition breaks down. I hacked around with this for a while, trying to exploit properties of $F$ to repair the proof (rather than work with a general injection, focus on the specific functional $F$ ), but failed. Andrej Bauer pointed out to me, to my surprise, that there is a model of ETT (which he constructed) that contains an injection of $N\to N$ into $N$ ! So there is no possibility of rescuing this line of argument.

(Incidentally, we can show within ETT that there is no bijection between $N$ and $N\to N$ , using surjectivity to rescue the proof attempt above. Curiously, Lawvere has shown that there can be no surjection from $N$ onto $N\to N$ , but this does not seem to help in the present situation. This shows that the concept of countability is more subtle in the constructive setting than in the classical setting.)

But I had another argument in mind, so I was not worried. The functional $F$ provides a decision procedure for equality for the type $N\to N$ : given $f,g:N\to N$ , compare $F(f)$ with $F(g)$ . Surely this is impossible! But one cannot prove within type theory that $\textrm{Id}_{N\to N}(-,-)$ is undecidable, because type theory is consistent with the law of the excluded middle, which states that every proposition is decidable. (Indeed, type theory proves that excluded middle is irrefutable for any particular proposition $P$ : $\neg\neg(P\vee\neg P)$ .) So this proof also fails!

At this point it started to seem as though Church’s Law could be independent of ETT, as startling as that sounds. For ITT it is more plausible: equality of functions is definitional, so one could imagine associating an index with each function without disrupting anything. But for ETT this seemed implausible to me. Andrej pointed me to a paper by Maietti and Sambin that states that Church’s Law is incompatible with function extensionality and choice. So there must be another proof that refutes Church’s Law, and indeed there is one based on the aforementioned decidability of function equivalence (but with a slightly different line of reasoning than the one I suggested).

First, note that we can use the equality test for functions in $N\to N$ to check for halting. Using the $T$ predicate described above, we can define a function that is constantly $0$ iff a given (code of a) program never halts on given input. We may then use the above-mentioned equality test to check for halting. So it suffices to show that the halting problem for (codes of) functions and inputs is not computable to complete the refutation of the internal form of Church’s Law.

Specifically, assume given $h:N\times N\to N$ that, given a code for a function and an input, yields $0$ or $1$ according to whether or not that function halts when applied to that input. Define $d:N\to N$ by $\lambda x:N.\neg h(x,x)$ , the usual diagonal function. Now apply the functional $F$ obtained from Church’s Law using the Axiom of Choice to obtain $n=F(d)$ , the code for the function $d$ , and consider $h(n,n)$ to derive the needed contradiction. Notice that we have used Church’s Law here to obtain a code for the type-theoretic diagonal function, which is then passed to the halting tester in the usual way.

As you can see, the revised argument follows along lines similar to what I had originally envisioned (in the second version), but requires a bit more effort to push through the proof properly. (Incidentally, I don’t think the argument can be made to work in pure ITT, but perhaps it would go through for ITT enriched with function extensionality.)

Thus, Church’s Law is false internally to extensional type theory, even though it is evidently true externally for that theory. You can see the similarity to the situation in first-order logic described earlier. Even though all functions of type $N\to N$ are computable, type theory itself is not capable of recognizing this fact (at least, not in the extensional case). And this is a good thing, not a bad thing! The whole beauty of constructive mathematics lies in the fact that it is just mathematics, free of any self-conscious recognition that we are writing programs when proving theorems constructively. We never have to reason about machine indices or any such nonsense, we just do mathematics under the discipline of not assuming that every proposition is decidable. One benefit is that the same mathematics admits interpretation not only in terms of computability, but also in terms of continuity in topological spaces, establishing a deep connection between two seemingly disparate topics.

(Hat tip to Andrej Bauer for help in sorting all this out. Here’s a link to a talk and a paper about the construction of a model of ETT in which there is an injection from $N\to N$ to $N$ .)

Update: word-smithing.

10 Comments | Research, Teaching | Tagged: Church's Law, extenionality, intensionality, type theory | Permalink
Posted by Robert Harper

There and Back Again

August 6, 2012

Last fall it became clear to me that it was “now or never” time for completing Practical Foundations for Programming Languages, so I put just about everything else aside and made the big push to completion. The copy editing phase is now complete, the cover design (by Scott Draves) is finished, and its now in the final stages of publication. You can even pre-order a copy on Amazon; it’s expected to be out in November.

I can already think of ways to improve it, but at some point I had to declare victory and save some powder for future editions. My goal in writing the book is to organize as wide a body of material as I could manage in a single unifying framework based on structural operational semantics and structural type systems. At over 600 pages the manuscript is at the upper limit of what one can reasonably consider a single book, even though I strived for concision throughout.

Quite a lot of the technical development does not follow along traditional lines. For example, I completely decouple the concepts of assignment, reference, and storage class (heap or stack) from one another, which makes clear that one may have references to stack-allocated assignables, or make use of heap-allocated assignables without having references to them. As another example, my treatment of concurrency, while grounded in the process calculus tradition, coheres with my treatment of assignables, but differs sharply from standard accounts (and avoids some of the complications in the treatment of process equivalences).

An explicit goal was to avoid the computational cladistics that characterizes many treatments of PL concepts. For example, there are not chapters on “paradigms” such as “functional programming” or “object-oriented programming”, although many of their underlying concepts are treated in the text. So there are chapters on higher-order functions and dynamic dispatch, for example, but these are not elevated to language design principles, but rather are analyses of computational phenomena “found in nature”.

With the first edition behind me, I intend to resume blogging. I have a few topics lined up in my head, including an update on our new undergraduate curriculum at Carnegie Mellon (going smashingly), and more posts on fundamentals of logic and PL’s. So stay tuned!

Update: word-smithing.

12 Comments | Teaching | Tagged: programming languages | Permalink
Posted by Robert Harper

для моих русских читателей

February 28, 2012

Владислав Натаров <[email protected]> has kindly translated my blog posts to date into Russian. I cannot vouch for the accuracy of the translation, but I am grateful for the effort, and hope that this will be of interest to my Russian readers.

4 Comments | Programming, Research, Teaching | Permalink
Posted by Robert Harper

Referential Transparency

February 9, 2012

After reading some of the comments on my Words Matter post, I realized that it might be worthwhile to clarify the treatment of references in PFPL. Most people are surprised to learn that I have separated the concept of a reference from the concept of mutable storage. I realize that my treatment is not standard, but I consider that one thing I learned in writing the book is to divorce the concept of a reference from that to which it refers. Doing so allows for a nicely uniform account of references arising in many disparate situations, and is the basis for, among other things, a non-standard, but I think clearer, treatment of communication in process calculi. Conventional accounts of references are, in my formulation, references to assignables; I also have references to symbols, to fluids, to channels, and to classifiers, all of which arise naturally and independently of assignment.

It’s not feasible for me to reproduce the entire story here in a short post, so I will confine myself to a few remarks that will perhaps serve as encouragement to read the full story in PFPL.

There is, first of all, a general concept of a symbol, or name, on which much of the development builds. Perhaps the most important thing to realize about symbols in my account is that symbols are not forms of value. They are, rather, a indices for an infinite, open-ended (expansible) family of operators for forming expressions. For example, when one introduces a symbol a as the name of an assignable, what one is doing is introducing two new operators, get[a] and set[a], for getting and setting the contents of that assignable. Similarly, when one introduces a symbol a to be used as a channel name, then one is introducing operators send[a] and receive[a] that act on the channel named a. The point is that these operators interpret the symbol; for example, in the case of mutable state, the get[a] and set[a] operators are what make it be state, as opposed to some other use of the symbol a as an index for some other operator. There is no requirement that the state be formulated using “cells”; one could as well use the framework of algebraic effects pioneered by Plotkin and Power to give a dynamics to these operators. For present purposes I don’t care about how the dynamics is formulated; I only care about the laws that it obeys (this is the essence of the Plotkin/Power approach as I understand it).

Associated with each symbol a is a type that is, I hasten to emphasize not the type of the symbol a itself (the symbol inhabits no type), but is merely associated with it. For example, if a has the associated type nat, then get[a] will be a command returning a number, and set[a](e) will take a number, e, as argument. Similarly for channels, and other uses of symbols as indices of other operators.

Given a symbol a with associated type T, one may form a reference to a, written &a, as a value whose type, in the case of a reference to an assignable, will be, say, T assignable reference, or similar terminology. This type is interpreted by elimination forms that take a value as argument, and transition to the corresponding operator for that assignable: getref(&a) transitions to get[a], and setref(&a;e) transitions to set[a](e). Similar rules govern other uses of symbols. The “ref” operations simply dereference the symbol (determine which assignable it references, in the case of assignables), and defer to the underlying interpretation of the referenced symbol. In the case of process calculi channel passing is effected using references to channels, and there are operations that determine an event based on the referent of a value of channel reference type. (This greatly clarifies, in my view, some aspects of the π-calculus, and leads to a well-behaved theory of process equivalence.)

The scoping of symbols, or names, is handled independently of their interpretation. One may use either a scoped or a scope-free interpretation of symbols. Scoped symbols have a limited extent; free symbols have unlimited extent. The concept of a mobile type, adapted from our work on ML5, manages the interaction between scoped declarations and evaluation (for which see the book). One consequence is that one may form references to both scoped and unscoped assignables, independently of the scope discipline. In other words I am deliberately breaking the conventional linkage between the extent of an assignable and the formation of a reference to it. Usually people conflate reference with state and with global extent; I am deliberately not following that convention, because I think it muddles things up. So, for example, in my account of Algol I have no difficulty in allowing references to scoped assignables, and passing them as arguments to procedures. I found this surprising, at first, but then quite natural once I had analyzed the situation more carefully.

Finally, let me mention that the critical property of assignables (in fact, symbols in general) is that they admit disequality. Two different assignables, say a and b, can never, under any execution scenario, be aliases for one another: an assignment to one will never affect the content of the other. Aliasing is a property of references, because two references, say bound to variables x and y, may refer to the same underlying assignable, but two different assignables can never be aliases for one another. Assignables and variables are different things, and references are yet different from those.

Update: word smithing, tightening.

1 Comment | Research, Teaching | Tagged: assignables, references, variables | Permalink
Posted by Robert Harper

Words Matter

February 1, 2012

Yesterday, during a very nice presentation by Ohad Kammar at Carnegie Mellon, the discussion got derailed, in part, because of a standard, and completely needless, terminological confusion involving the word “variable”. I’m foolish enough to try to correct it.

The problem is that we’ve all been taught to confuse variables with variables—that is, program variables with mathematical variables. The distinction is basic. Since time immemorial (well, at least since al Khwarizmi) we have had the notion of a variable, properly so-called, which is given meaning by substitution. A variable is an unknown, or indeterminate, quantity that can be replaced by any value of its type (a type being, at least since Russell, the range of significance of a variable). Frege gave the first systematic study of the quantifiers, and Church exploited the crucial concept of a variable to give the most sharply original and broadly applicable model of computation, the $\lambda$ -calculus.

Since the dawn of Fortran something that is not a variable has come to be called a variable. A program variable, in the sense of Fortran and every imperative language since, is not given meaning by substitution. Rather, it is given meaning by (at least) two operations associated with it, one to get its contents and one to put new contents into it. (And, maybe, an operation to form a reference to it, as in C or even Algol.) Now as many of you know, I think that the concept of a program variable in this sense is by and large a bad idea, or at any rate not nearly as important as it has been made out to be in conventional (including object-oriented) languages, but that’s an argument for another occasion.

Instead, I’m making a plea. Let’s continue to call variables variables. It’s a perfectly good name, and refers to what is perhaps one of the greatest achievements of the human mind, the fundamental concept of algebra, the variable. But let’s stop calling those other things variables! In my Practical Foundations for Programming Languages I coined (as far as I know) a word that seems perfectly serviceable, namely an assignable. The things called variables in imperative languages should, rather, be called assignables. The word is only a tad longer than variable, and rolls off the tongue just as easily, and has the advantage of being an accurate description of what it really is. What’s not to like?

Why bother? For one thing, some languages have both concepts, a necessity if you want your language to be mathematically civilized (and you do). For another, in the increasingly important world of program verification, the specification formalisms, being mathematical in nature, make use of variables, which most definitely are not assignables! But the real reason to make the distinction is, after all, because words matter. Two different things deserve to have two different names, and it only confuses matters to use the same word for both. This week’s confusion was only one example of many that I have seen over the years.

So, my suggestion: let’s call variables variables, and let’s call those other things assignables. In the fullnesss of time (i.e., once the scourge of imperative programming has been lifted) we may not need the distinction any longer. But until then, why not draw the distinction properly?

Update: remove forward reference.

30 Comments | Programming, Research, Teaching | Tagged: functional programming, imperative programming | Permalink
Posted by Robert Harper

Of Course ML Has Monads!

May 1, 2011

A popular meme in the world of PL’s is that “Haskell has monads”, with the implication that this is a distinctive feature of the language, separate from all others. While it is true that Haskell has popularized the use of monads as a program structuring device, the idea of a monad is not so much an issue of language design (apart from the ad hoc syntactic support provided by Haskell), but rather one of library design. After all, a monad is just one of a zillion signatures (type classes) with which to structure programs, and there is no particular reason why this one cannot be used in any language that supports even a modicum of modularity.

Examined from the point of view of ML, monads are but a particular of use of modules. The signature of monads is given by the definition

signature MONAD = sig
  type 'a monad
  val ret : 'a -> 'a monad
  val bnd : 'a monad -> ('a -> 'b monad) -> 'b monad
end

There are many, many, many structures that satisfy this signature; I needn’t (and, in any case, can’t) rehearse them all here. One particularly simple example should suffice to give the general idea:

structure Option : MONAD = struct
  type 'a monad = 'a option
  fun ret x = SOME x
  fun bnd (SOME x) k = k x
    | bnd NONE k = NONE
end

This is of course the option monad, which is sometimes used to model the data flow aspects of exceptions, perhaps with some elaboration of the NONE case to associate an exceptional value with a non-result. (The control flow aspects are not properly modeled this way, however. For that one needs, in addition, access to some sort of jump mechanism.)

Examples like this one proliferate. A monad is represented by a structure. Any structure that provides the facilities specified by the MONAD signature gives rise to the characteristic sequentialization mechanisms codified by it. Monad transformers are functors that transform one monad into another, with no fuss or bother, and no ad hoc mechanisms required. Standard modular programming techniques suffice to represent monads; moreover, the techniques involved are fully general, and are equally applicable to other signatures of interest (arrows, or quivers, or bows, or what have you). Moreover, it is shown in my paper with Chakravarty, Dreyer, and Keller how to integrate modules into the type inference mechanism of ML so that one can get automatic functor instantiation in those limited cases where it is self-evident what is intended. This has been implemented by Karl Crary in a prototype compiler for an extension of Standard ML, and it would be good to see this supported in more broadly available compilers for the language.

The bulk of the mania about monads is therefore accounted for by modules. I have no doubt, however, that you are wondering about the IO monad in Haskell. Isn’t that a fundamental feature of the language that cannot be replicated in ML? Hardly! It’s entirely a matter of designing the signatures of the standard basis library modules, and nothing more. The default basis library does not attempt to segregate effects into a monad, but it is perfectly straightforward to do this yourself, by providing your own layer over the standard basis, or to reorganize the standard basis to enforce the separation. For example, the signature of reference cells might look like this:

signature REF = sig
  type 'a ref
  val ref : 'a -> 'a ref IO.monad
  val ! : 'a ref -> 'a IO.monad
  val := : 'a ref -> 'a -> unit IO.monad
end

Here we are presuming that we have a fixed declaration

structure IO : MONAD = ...

that packages up the basic IO primitives that are already implemented in the run-time system of ML, more or less like in Haskell. The other signatures, such as those for mutable arrays or for performing input and output, would be modified in a similar manner to push effects into the IO monad. Et voila, you have monadic effects.

There’s really nothing to it. In fact, the whole exercise was carried out by a Carnegie Mellon student, Phillippe Ajoux, a couple of years ago. He also wrote a number of programs in this style just to see how it all goes: swimmingly. He also devised syntactic extensions to the Moscow ML compiler that provide a nicer notation for programming with monads, much as in Haskell, but better aligned with ML’s conventions. (Ideally it should be possible to provide syntactic support for any signature, not just monads, but I’m not aware of a worked-out design for the general case, involving as it would an intermixing of parsing and elaboration.)

My point is that the ML module system can be deployed by you to impose the sorts of effect segregation imposed on you by default in Haskell. There is nothing special about Haskell that makes this possible, and nothing special about ML that inhibits it. It’s all a mode of use of modules.

So why don’t we do this by default? Because it’s not such a great idea. Yes, I know it sounds wonderful at first, but then you realize that it’s pretty horrible. Once you’re in the IO monad, you’re stuck there forever, and are reduced to Algol-style imperative programming. You cannot easily convert between functional and monadic style without a radical restructuring of code. And you are deprived of the useful concept of a benign effect.

The moral of the story is that of course ML “has monads”, just like Haskell. Whether you want to use them is up to you; they are just as useful, and just as annoying, in ML as they are in Haskell. But they are not forced on you by the language designers!

Update: This post should’ve been called “ML Has Monads, Why Not?”, or “Of Course ML Has Comonads!”, but then no one was wondering about that.

Update: I now think that the last sentence is excessive. My main point is simply that it’s very simple to go one way or the other with effects, if you have modules to structure things; it’s all a matter of library design. A variant of ML that enforced the separation of effects is very easily constructed; the question is whether it is useful or not. I’ve suggested that the monadic separation is beguiling, but not clearly a great idea. Alternatively, one can say that we’re not that far away from eliminating laziness from Haskell, at least in this respect: just re-do the standard basis library in ML, and you’re a good ways there. Plus you have modules, and we understand how to integrate type classes with modules, so the gap is rather small.

Update: Removed inaccurate remarks about unsafePerformIO.

64 Comments | Programming | Tagged: functional programming, imperative programming, modularity | Permalink
Posted by Robert Harper

The Point of Laziness

April 24, 2011

As I’ve discussed previously, there are a number of good reasons why Haskell is not suitable for teaching introductory functional programming. Chief among these is laziness, which in the context of a pure functional language has fatal side effects. First, Haskell suffers from a paucity of types. It is not possible in Haskell to define the type of natural numbers, nor the type of lists of natural numbers (or lists of anything else), nor any other inductive type! (In Carollian style there are types called naturals and lists, but that’s only what they’re called, it’s not what they are.) Second, the language has a problematic cost model. It is monumentally difficult to reason about the time, and especially space, usage of a Haskell program. Worse, parallelism arises naturally in an eager, not a lazy, language—for example, computing every element of a finite sequence is fundamental to parallel computing, yet is not compatible with the ideology of laziness, which specifies that we should only compute those elements that are required later.

The arguments in favor of laziness never seem convincing to me. One claim is that the equational theory of lazy programs is said to be more convenient; for example, beta reduction holds without restriction. But this is significant only insofar as you ignore the other types in the language. As Andrzej Filinski pointed out decades ago, whereas lazy languages have products, but not sums, eager languages have sums, but not products. Take your pick. Similarly, where lazy languages rely on strictness conditions, eager languages rely on totality conditions. The costs and benefits are dual, and there seems to be no reason to insist a priori on one set of equations as being more important than the other.

Another claim is that laziness supports the definition of infinite data types, such as infinite sequences of values of some type. But laziness is not essential, or even particularly useful, for this purpose. For example, the type nat->nat is a natural representation of infinite sequences of natural numbers that supports many, but not all, of the operations that finite sequences (but not, for example, operations such a reverse, which make no sense in the infinite case). More generally, there is no inherent connection between laziness and such infinitary types. Noam Zeilberger has developed an elegant theory of eager and lazy types based on distinguishing positive from negative polarities of type constructors, the positive including the inductive and the negative including the coinductive. Coinductive types are no more about laziness than inductive types are about pointers.

I wish to argue that laziness is important, but not for pure functional programming, but rather only in conjunction with effects. This is the Kahn-MacQueen Principle introduced in the 1970’s by Gilles Kahn and David MacQueen in their seminal paper on recursive networks of stream transducers. Dan Licata and I have emphasized this viewpoint in our lectures on laziness in our new course on functional programming for freshmen.

Let’s use streams as a motivating example, contrasting them with lists, with which they are confused in lazy languages. A list is an example of a positive type, one that is defined by its membership conditions (constructors). Defining a function on a list amounts to pattern matching, giving one case for each constructor (nil and cons), and using recursion to apply the function to the tail of the list. A stream is an example of a negative type, one that is defined by its behavioral conditions (destructors). Defining a stream amounts to defining how it behaves when its head and tail are computed. The crucial thing about lists, or any positive type, is that they are colimits; we know as part of their semantics how a value of list type are constructed. The crucial thing about streams, or any negative type, is that they are limits; we know as part of their semantics how they behave when destructed.

Since we have no access to the “inside” of a stream, we should think of it not as a static data structure, but as a dynamic process that produces, upon request, successive elements of the stream. Internally, the stream keeps track of whatever is necessary to determine successive outputs; it has its own state that is not otherwise visible from the outside. But if a stream is to be thought of as given by a process of generation, then it is inherently an ephemeral data structure. Interacting with a stream changes its state; the “old” stream is lost when the “new” stream is created. But, as we have discussed previously, ephemeral data structures are of limited utility. The role of memoization is to transform an ephemeral process into a persistent data structure by recording the successive values produced by the process so that they can be “replayed” as necessary to permit the stream to have multiple futures. Thus, rather than being a matter of efficiency, memoization is a matter of functionality, providing a persistent interface to an underlying ephemeral process.

To see how this works in practice, let’s review the signatures PROCESS and STREAM that Dan Licata and I developed for our class. Here’s a snippet of the signature of processes:

signature PROCESS = sig
  type 'a process = unit -> 'a option
  val stdin : char process
  val random : real process
end

A process is a function that, when applied, generates a value of some type, or indicates that it is finished. The process stdin represents the Unix standard input; the process random is a random number generator. The signature of streams looks essentially like this:

signature STREAM = sig
  type 'a stream
  datatype 'a front = Nil | Cons of 'a * 'a stream
  val expose : 'a stream -> 'a front
  val memo : 'a Process.process -> 'a stream
  val fix : ('a stream -> 'a stream) -> 'a stream
end

The type ‘a front is the type of values that arise when a stream is exposed; it can either terminate, or present an element and another stream. The memo constructor creates a persistent stream from an ephemeral process of creation for its elements. The fix operation is used to create recursive networks of streams. There are other operations as well, but these illustrate the essence of the abstraction.

Using these signatures as a basis, it is extremely easy to put together a package of routines for scripting. The fundamental components are processes that generate the elements of a stream. Combinators on streams, such as composition or mapping and reducing, are readily definable, and may be deployed to build up higher levels of abstraction. For example, Unix utilities, such as grep, are stream transducers that take streams as inputs and produce streams as outputs. These utilities do not perform input/output; they merely transform streams. Moreover, since streams are persistent, there is never any issue with “buffering” or “lookahead” or “backtracking”; you just manipulate the stream like any other (persistent) data structure, and everything works automagically. The classical Bell Labs style of intermixing I/O with processing is eliminated, leading not only to cleaner code, but also greater flexibility and re-use. This is achieved not by the double-backflips required by the inheritance mechanisms of oopl’s, but rather by making a crisp semantic distinction between the processing of streams and the streaming of processes. True reuse operates at the level of abstractions, not at the level of the code that gives rise to them.

Update: It seems worthwhile to point out that memoization to create a persistent from an ephemeral data structure is a premier example of a benign effect, the use of state to evince functional behavior. But benign effects are not programmable in Haskell, because of the segregation of effects into the IO monad.

Update: Lennart Augustsson gives his reasons for liking laziness.

Update: word smithing.

56 Comments | Programming, Teaching | Tagged: laziness, processes, streams | Permalink
Posted by Robert Harper