Glasgow Functional Programming Seminars (1995-96)

An Overview of the Linear Logic Programming Language Lygon
James Harland
Royal Melbourne Institute of Technology

Recently there has been significant interest in the application of linear logic, a logic designed with bounded resources in mind, to computer science tasks, and in particular to the design of logic programming languages. Such languages provide a notion of resource-oriented programming, which leads to programs which are more concise and elegant than their equivalents in languages based on classical logic, such as Prolog. In this talk we give an overview of the linear logic programming language Lygon. In order to provide the programmer with maximum flexibility, Lygon has been designed with as few restrictions as possible in mind whilst still remaining a logic programming language. As a result, Lygon appears to contain the broadest class of features of any linear logic programming language. We describe the design, implementation and applications of the language, including several example programs. We argue that this shows that the paradigm of resource-oriented programming is natural and effective for a variety of applications.

Functions, objects and constraints in Oz
Joachim Niehren
Universität des Saarlandes

Oz is a concurrent constraint language develloped at DFKI in Saarbr"ucken during the last 4 years. Oz integrates functions, stateful concurrent objects, and encapsulated search. The usage of constraints is twofold:

1. They provide for communication over shared data structures which makes lazyness expressible in a concurrent setting.
2. They allow to prune search trees when solving combinatorical problems.

Covariant Types
Barry Jay
University of Technology, Sydney

The covariant type system is rich enough to represent polymorphism on inductive types, such as lists and trees, and yet is simple enough to have a set-theoretic semantics. Its chief novelty is to replace function types by transformation types, which denote parametric functions. Their free type variables are all in positive positions, and so can be modelled by covariant functors. The semantics is expressed in terms of data functors and arbitrary strong natural transformations between them. Each such transformation is given by a uniform algorithm, creating a tight link with the parametric polymorphism of the type system.

A Cheaper Form of Deforestation
Andy Gill
University of Glasgow

In functional languages intermediate data structures are often used as ``glue'' to connect separate parts of a program together. Deforestation is the process of automatically removing intermediate data structures. In this talk we present and analyse a new approach to deforestation. This new approach is both practical and general.

We concentrate on the problem of list removal rather than the more general problem of arbitrary data structure removal. This more limited scope allows a complete evaluation of the pragmatic aspects of using our deforestation technology.

We have an implementation in the Glasgow Haskell compiler, and this implementation has allowed practical feedback. One important conclusion is that a new analysis is required to infer function arities and the linearity of lambda abstractions. This analysis renders the basic deforestation algorithm far more effective.

In our talk we give a detailed assessment of our implementation of deforestation. We measure the effectiveness of our deforestation on a suite of real application programs. We also observe the costs of our deforestation algorithm.

The Essence of Compiling with Continuations and Monads
Phil Wadler
University of Glasgow

Amr Sabry (Chalmers) and Philip Wadler (Glasgow)

Every functional programmer knows that CPS stands for continuation- passing style. But why is CPS so popular? One reason is that translating a call-by-value program into CPS makes it easier to reason about: fewer equalities are provable between source terms than between their CPS equivalents.

Sabry and Felleisen augmented the call-by-value calculus with additional rules, and showed that the augmented calculus proves as many equalities as its CPS equivalent. Flanagan, Sabry, Duba, and Felleisen went on to relate these ideas to simplified compilers and abstract machines. Similar notions have been explored by Danvy and his colleagues. And eerily related notations appear in the Spineless Tagless G-machine.

Here we give a presentation that is simpler than the previous work, and establishes stronger results. It is based on two calculi of Moggi: the well-known monadic meta-language, lambda-m; and the less-known corresponding call-by-value calculus, lambda-c.

See and understand the deep structure of CPS! Marvel at the meaning of Plotkin's administrative reductions! Comprehend the close connection between call-by-value and call-by-need! Be astounded as adjoints are applied to compiling technology! A grand time will be had by all.