halt
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.
FLOPS brings together practitioners, researchers and implementers of declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. This wide scope and the interplay of theory and practice is reflected in the papers of this special issue.
We are grateful to the authors for preparing the extended versions of their papers and promptly addressing reviewers' comments. We deeply thank the reviewers for all the work they have done to evaluate and improve the submissions.
Joint editing with Andy King, University of Kent, UK
FLOPS-poster.pdf [125K]
The conference poster
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.
Zuse-accolades.txt [6K]
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 (but far after Z3)
Konrad Zuse Internet Archive
<http://www.zib.de/zuse/English_Version/index.html>
A follow-up article showed various ways to simulate self-referential values and lazy computation in ML (OCaml).
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.
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 also explains practical benefits of creating and
manipulating cyclical structures in the side-effect-free manner.
number-of-targets times number-of-platforms to just
number-of-targets plus number-of-platforms.
The language of GNU make is indeed functional, complete with
combinators (map and filter), applications and anonymous
abstractions. Yes, GNU make supports 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).scm
The rule returns the OS command to interpret or compile the target.
It is to 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
foreach corresponds 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))))
Makefile [7K]
The Makefile in question
Chapter 'Functions' from make info pages
In a more recent discussion, Neelakantan Krishnaswami
introduced the function choose function as an indispensable part of
an API for Set, letting us reason about sets
algebraically and equationally.
Neelakantan Krishnaswami: Re: FP-style map over set
The message posted on the newsgroup comp.lang.functional
on Mon, 28 Nov 2005 23:45:27 +0000 (UTC)
sendmail.cf [37K]
The sendmail configuration file (sendmail.cf) augmented with rules to
implement the Turing machine. This file also defines two sample Turing
machines.
- turing_machine((0,["#","a","a","a","a","a","a"],"#",[]),prog_decision);
val it = (~1,["#","Yes"],"#",["#","#","#","#","#"])
: int * string list * string * string list
shows 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.