We argue that programming-language theory should face the pragmatic fact that humans develop software by interacting with computers in real time. This interaction not only relies on but also bears on the core design and tools of programming languages, so it should not be left to Eclipse plug-ins and StackOverflow. We further illustrate how this interaction could be improved by drawing from existing research on natural-language dialogue, specifically on collaborative reference.
Overloading resolution is one immediate application. Here, collaborative reference can resolve the tension between fancy polymorphism and the need to write long type annotations everywhere. The user will submit a source code fragment with few or no annotations. If the compiler gets stuck -- e.g., because of ambiguous overloading -- it will ask the user for a hint. At the successful conclusion of the dialogue, the compiler saves all relevant context, in the form of inserted type annotations or as a proof tree attached to the source code. When revisiting the code later on, the same or a different programmer may ask the compiler questions about the inferred types and the reasons for chosen overloadings. We argue that such an interactive overloading resolution should be designed already in the type system (e.g., using oracles).
Joint work with Chung-chieh Shan.
The extended abstract, submitted to the ``Off-the-beaten track'' workshop affiliated with POPL 2012.
The slides of the talk presented by Chung-chieh Shan at the
workshop. Philadelphia, PA, January 28, 2012.
Henry Baker remarked that "it is impossible to create infinite trees -- i.e., directed cycles -- without side-effects." This article shows limitations of that statement. One can construct cyclic lists and other self-referential values in a pure functional style, without resorting to mutations. Lazy evaluation -- either supported by a language, or emulated -- makes this possible. Lazy evaluation even allows an invocation of a function with an argument that refers to the function's result.
An interesting follow-up article showed various ways to simulate self-referential values and lazy computation in ML (Caml).
Furthermore, we can create DAGs and general cyclic data structures even in a strict pure functional language. The following article "On parent pointers in SXML trees" demonstrates different ways of constructing tree-like data structures with forward and backward pointers. Some of the data structures are general graphs with directed cycles, some of them are DAGs. And yet some of them are genuine trees. How can a recursive data structure have forward and backward pointers and yet only a single path between any two nodes? How can we do that in a strict pure language? The article and the accompanying source code explain. The paradoxical tree is built by a procedure add-thunk-parent-pt, which is defined in section 'Solution 3' of the source code. The procedure is deceptively simple. It took 21 lines of Scheme code to implement the algorithm and 26 (full-length) lines of comments to explain it.
A USENET article Self-referential values and
expressiveness of strict vs. non-strict languages [plain text file]
The article was posted on newsgroups comp.lang.scheme, comp.lang.functional on Mon Feb 14 20:14:49 2000 GMT
Unitary type as a self-referential set
Pure-functional transformations of cyclic graphs and the Credit Card Transform
Henry G. Baker: Equal Rights for Functional Objects or, The More Things Change, The More They Are the Same
On parent pointers in SXML trees
The article and the accompanying Scheme source code. The article also explains practical benefits of creating and manipulating cyclical structures in a side-effect-free manner.
The following article describes a real practical application:
avoiding the explosion of makefile rules in a project that executes
many test cases on many platforms. Each test target is built from its
own set of source code files. Each (Scheme) platform has its own
particular way of assembling source code files into a project; some
source code files might need be omitted from the build for a
particular platform. Because GNU make turns out to be a
functional programming system, we can reduce the number of rules from
<number-of-targets> * <number-of-platforms> to just
The language of GNU make is indeed functional, complete with combinators (map and filter), applications and anonymous abstractions. GNU make does support lambda-abstractions. The following is one example from the Makefile in question: it is a rule to build a test target for the SCM Scheme system. The list of source code files and the name of the target/root-test-file are passed as two arguments of the rule:
make-scmi= scm -b -l $(LIBDIR)/myenv-scm.scm \ $(foreach file,$(1),-l $(LIBDIR)/$(file)) \ -l $(2).scmThe rule returns an OS command to interpret or compile the target. The rule can be invoked as
$(call make-scmi,util.scm catch-error.scm,vmyenv). As in TeX, the arguments of a function are numbered (it is possible to assign them meaningful symbolic names, too). Makefile's
foreachcorresponds to Scheme's
map. The comparison with the corresponding Scheme code is striking:
(define make-scmi (lambda (arg1 arg2) `(scm -b -l ,(mks LIBDIR '/ 'myenv-scm.scm) ,@(map (lambda (file) `(-l ,(mks LIBDIR '/ file))) arg1) -l ,(mks arg2 '.scm))))
SSAX updates; Makefile as a functional program [plain text file]
A message describing the motivation for the functional Makefile to automate regression testing, and a few examples. The message was posted on the SSAX-SXML mailing list on Mon, 18 Nov 2002 12:48:41 -0800
The Makefile in question
Chapter 'Functions' from
make info pages.
Konrad Zuse's Z3 was far ahead of its time. Unlike ENIAC, it was controlled by a software program. In Z3, the numbers were represented in a floating point format greatly resembling the one in the IEEE Floating-Point standard. Z3 had two ALUs so it operated on the exponent and the mantissa of a number in parallel.
It appears Z3 was farther ahead than we might have realized. Z3 had no branch instruction and instead relied on predicated execution. The latter technique -- implemented in the most recent upscale CPUs -- is considered to be ``one of the most significant [recent] advances in the history of computer architecture and compiler design.'' It seems that advance is not recent at all: it was invented by Konrad Zuse back in 1938. The letter to Dr.Dobbs J. Editors gives more details.
Simulating Konrad Zuse's Computers
Dr. Dobbs J., September 2000, pp. 64-69.
Zuse Accolades [plain text file]
The letter to the editor regarding the above article. It was published in Dr. Dobbs J., December 2000, p. 10.
Zuse and Intel
A letter from reader Ben Laurie
Dr. Dobbs J., August 2001, p. 12.
Ben Lauri points out that Acorn's ARM chip has had the predicated execution feature more than a decade ago.
Konrad Zuse Internet Archive
The following short essay argues that the Axiom of Choice can be regarded as a deconstructor (i.e., cursor-like) API for a set. In contrast, axioms of (restricted) comprehension and of replacement are more like the enumerator API for a set. The Axiom of Choice does not reveal how the set in question has been constructed. The Axiom of Choice may also be viewed as an assertion that set's membership predicate is safe, in Datalog sense.
In a more recent discussion, Neelakantan Krishnaswami
choose function as an indispensable part of
an API for a
Set, enabling us to reason about sets
algebraically and equationally.
The essay [plain text file]
Neelakantan Krishnaswami. Re: FP-style map over set
A message posted on a newsgroup comp.lang.functional on Mon, 28 Nov 2005 23:45:27 +0000 (UTC)
This article proves by construction that sendmail rewriting rules are Turing-complete. They are expressive enough to implement a Turing machine. The article first gives an introduction to the rewriting rules, for easy reference. We then explain how to map Turing machine configuration (the content of the tape and the current position) to a character string, and machine's finite control to rewriting rules. As an example, we demonstrate two Turing machines: an adder of two natural numbers, and an even/odd decision function. We explain how to run these examples and see the result.
The USENET article itself [plain text file]
This article, Sendmail as a Turing machine, was posted on newsgroups comp.lang.functional and comp.mail.sendmail on Sun, 10 Sep 2000 22:26:33 GMT
A sendmail configuration file (sendmail.cf) augmented with rules to implement the Turing machine. This file also defines two sample Turing machines.
The following archive contains a simple implementation of Turing machine in Standard ML (SML/NJ). For illustration, the code includes three sample Turing programs: the successor function, a character substitution function, and a decision function. For example,
- turing_machine((0,["#","a","a","a","a","a","a"],"#",),prog_decision); val it = (~1,["#","Yes"],"#",["#","#","#","#","#"]) : int * string list * string * string listshows that starting the decision program (which decides if a string contains an even number of characters) with the tape
#aaaaaa###....and the head positioned at the beginning of the tape, leaves
# "YES" ####...on the tape after the machine halts (by reaching the state -1). Thus, the machine has decided the input string contained an even number of characters.
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML