916 papers · page 35 of 46
This pearl is about some functions whose definitions seem to require a language with dependent types. We describe a technique for defining them in Haskell or ML, which are languages without dependent types. Consider, for example, the scheme defining zipWith in figure 1. When this…
This paper introduces a sequence of λ-expressions modeling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system, i.e. one in which a…
Kamareddine, F., & Ríos (1997) conjecture that the λ s e -calculus preserves the strong normalisation of the λ-calculus. We prove here that this conjecture is false.
We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete . The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of indepen…
We present our experience in implementing a group communication toolkit in Objective Caml, a dialect of the ML family of programming languages. We compare the toolkit both quantitatively and qualitatively to a predecessor toolkit which was implemented in C. Our experience shows t…
One well known algorithm is the Fast Fourier Transform (FFT). An efficient iterative version of the FFT algorithm performs as a first step a bit-reversal permutation of the input list. The bit-reversal permutation swaps elements whose indices have binary representations that are …
A trie is a search tree scheme that employs the structure of search keys to organize information. Tries were originally devised as a means to represent a collection of records indexed by strings over a fixed alphabet. Based on work by C. P. Wadsworth and others, R. H. Connelly an…
A program derivation is said to be polytypic if some of its parameters are data types. Often these data types are container types, whose elements store data. Polytypic program derivations necessitate a general, non-inductive definition of ‘container (data) type’. Here we propose …
The understanding of polymorphic typechecking and type errors is poorly supported by contemporary functional language implementations. Here, a novel visualisation of functions and their types is presented based on the generation of function specific icons with graphical type repr…
A simple implementation of an SML-like module system is presented as a module parameterized by a base language and its type-checker. This implementation is useful both as a detailed tutorial on the Harper–Lillibridge–Leroy module system and its implementation, and as a constructi…
The Common Gateway Interface (CGI) for generating dynamic documents on web servers imposes much accidental complexity on the programmer. The Haskell/CGI library documented in this paper hides all this unpleasantness by using the common sense ‘design pattern’ of separating model a…
Indeterminism is typical for concurrent computation. If several concurrent actors compete for the same resource then at most one of them may succeed, whereby the choice of the successful actor is indeterministic. As a consequence, the execution of a concurrent program may be nonc…
The presence of side effects in even a very simple language of expressions gives rise to a number of semantic questions. The issue of evaluation order becomes a crucial one and, unless a specific order is enforced, the language becomes non-deterministic. In this paper we study th…
The Bee is an integrated development environment for the Scheme programming language. It provides the user with a connection between Scheme and the C programming language, a symbolic debugger, a profiler, an interpreter, an optimizing compiler that delivers stand alone executable…
Every functional programmer knows the technique of “replacing failure by a list of successes” (Wadler, 1985), but wise programmers are aware also of the possibility that the list will be empty or (worse) divergent. In fact, the “lists of successes” technique is equivalent to the …
This paper uses the Fran system for functional reactive animation to give a simulation of a lift – or elevator – with many floors. The paper first introduces a two-floor version, and then indicates in detail how this is extended to give a simulation with an arbitrary number of fl…
Kleisli is a modern data integration system that has made a significant impact on bioinformatics data integration. This paper contains a brief introduction to the Kleisli system and an example to illustrate its uses in the bioinformatics arena. The primary query language provided…
Injective pure type systems form a large class of pure type systems for which one can compute by purely syntactic means two sorts elmt(Γ[mid ] M ) and sort(Γ[mid ] M ), where Γ is a pseudo-context and M is a pseudo-term, and such that for every sort s , formula here By eliminatin…
“I have no data yet. It is a capital mistake to theorise before one has data.” Sir Arthur Conan Doyle The Adventures of Sherlock Holmes de Bruijn notation is a coding of lambda terms in which each occurrence of a bound variable x is replaced by a natural number, indicating the ‘d…
The LCF system was the first mechanical theorem prover to be user-programmable via a metalanguage, ML, from which the functional programming language Standard ML has been developed. Paulson has demonstrated how a modular rewriting engine can be implemented in LCF. This provides b…