Foundations of Programming Meetings 1996
School of Computer Science and ITUniversity of Nottingham
In the program transformation community, there is considerable interest in the use of relational calculi to construct functional programs from specifications. Working with relations allows specifications to be more abstract (for example, many programs have a natural specification using the converse operator on relations) and affords a natural treatment of non-determinism in specifications. In this talk I will present a novel pictorial interpretation of relational terms, and a completeness result that allows relational equations to be proved by the appealing process of reasoning using pictures. I will also give a number of practical applications of this result.
This talk is based upon joint work with Carolyn Brown.
Module systems are a powerful, practical tool for managing the
complexity of large software systems. Previous attempts to formulate a
type-theoretic foundation for modular programming have been based on
existential, dependent, or manifest types. These approaches can be
distinguished by their use of different quantifiers to package the
operations that a module exports together with appropriate
implementation types. In each case, the underlying type theory is
simple and elegant, but significant and sometimes complex extensions
are needed to account for features that are important in practical
systems, such as separate compilation and propagation of type
information between modules.
This talk presents a simple type-theoretic framework for modular
programming using parameterized signatures. The use of quantifiers is
treated as a necessary, but independent concern. Using familiar
concepts of polymorphism, the resulting module system is easy to
understand and admits true separate compilation. It is also very
powerful, supporting higher-order, polymorphic, and first-class modules
without further extension.
(Preview of a talk to be presented at POPL '96, St Petersburg, FL.)
Type systems in languages such as ML and Haskell allow programs to be written
with little or no type annotations, using extended versions of the Hindley/Milne
r
inference type system to rediscover this information. A requirment of this appro
ach
is that such languages require explicit syntax for defining polymorphic inductiv
e
data types such as products, sums and lists. Second-order type systems extend t
hese
systems with the notion of type parameters, allowing terms to be parameterized
with respect to some type. One such type system is Girard's system F-omega.
In this talk, we present an overview of a Haskell implementation of F-omega, bas
ed
upon Cardelli's language Fun. We give particular emphasis to type checking and
the
translation of our syntax into a lambda-lifted core language.
Polymorphic type systems for extensible records and variants, have been widely
studied in recent years. Initially introduced by Wand, as an approach for
modeling features of object oriented programming, it is widely recognized that
they provide a number of benefits over the monomorphic restrictions imposed by
languages such as Standard ML and Haskell. One drawback of such systems is
that it is not always straightforward to find an efficient implementation for
operations on records and variants.
In this talk we outline some early results for a qualified type system, under
development, for extensible records and variants.
This work is part of an on going project for developing an ML style type system
for polymorphic operations on record and variants.
Object oriented languages provide a range of concepts that have been
claimed to facilitate encapsulation, reuse and modularity. The aim of
this talk is to introduce these concepts through their theory, and to
describe how they correspond to concepts in functional programming
languages. In particular, various ways of encoding object oriented
concepts in functional languages will be examined.
Functors on the category SET of total functions often have a natural
generalisation to the category REL of binary relations. In this
blackboard presentation I will explain how, under certain mild conditions,
functors on SET have exactly one generalisation in REL. Similar
results also hold for natural transformations and adjunctions. From a
programming language point of view, such results indicate that there is
essentially one way to generalise functional programming to
relational programming.
Enumerating prime numbers is a standard programming exerise. The
popular method of solution is the Sieve of Eratosthenes, which in a
functional language with lazy lists can be expressed as a neat
two-liner. A little-known alternative method is the Wheel Sieve. As
originally formulated this is a fast imperative algorithm for
obtaining all primes up to a given limit, assuming destructive access
to a bit-array. The talk will describe two variants of the wheel
sieve programmed using lazy lists in a functional language. Both
variants enumerate the infinite list of primes. To find out the
difference between them, and what this has to do with spirals, come to
the talk!
Many functional programs can be viewed as representation changers,
that is, as functions that convert abstract values from one concrete
representation to another. Examples of such programs include
base-converters, binary adders and multipliers, and compilers. In
this blackboard presentation I will give a number of different
approaches to specifying representation changers (pointwise,
functional, and relational), and present a simple technique that
can be used to derive functional programs from the specifications.
This talk is based upon joint work with Erik Meijer (Utrecht).
The benefits of non-strict functional programming languages such as
higher-order functions, polymorphism and lazyness can be useful in
programming reactive systems. Aspects of reactive systems can be
modelled by making use of the infinite structures, such as streams,
that can be represented in such languages. However for these languages
to be practically viable we must be able to reason about the
space usage and termination properties of programs written in them.
Hughes, Pareto and Sabry have proposed a type system using sized
types to try and alleviate these problems. In this presentation I
will discuss their recent POPL paper, illustrating the usefulness
of sized types when building reactive systems.
A number of researchers have developed and extended the notion of subtyping in
the Girard/Reynolds polymorphic lambda calculus. Furthermore, Cardelli has shown
that F-sub provides enough machinary to capture the notion of row variables in
extensible types, in particular he encodes a calculus of extensible records in
F-sub.
In this talk we give an overview of F-sub and outline a translation of
well-typed terms for a qualified type system with extensible records and
variants into F-sub.
There have been a number of proposals for providing a denotational semantics
for the core language of Standard ML. One such approach is that presented by
Ohori, in which he views terms of core ML as pairs consisting of a raw
(untyped) lambda term and a type-scheme that type inference can derive for the
raw term. A type-scheme is interpreted as a set of simple types. The meaning
of a term is the set given by interpreting its type-scheme as an enumeration
of simple types paired with the type annotated instance of the raw term.
In this talk we give an overview of Ohori's approach to semantics for core ML,
highlighting the differences between his approach and other denotational
semantics for core ML. In particular, we focus on the differences with the
ideal model given by Milner in his seminal work on type inference, and the
later analysis given by Mitchell an Harper. In conclusion we outline the
objectives for generalizing Ohori's work to provide a framework for a
denotational semantics for qualified types, and higher-order polymorphism,
with the result of providing a semantics for constructor classes.
Particular applications most readily suit a concurrent implementation, such as
interactive systems. Various extensions to functional programming languages have
been proposed to provide support for explicit concurrent programming,
such as Concurrent Haskell, and Parallel Gofer. These systems have
all required new primitives to be built into the language. In this talk I will
present a system that provides the same level of expressiveness as these systems
but without the need for new primitives. The main advantages of this system are
that is easily portable (not needing to rely on propriety primitives), and also
allows for a better understanding of concurrency in a functional setting.
Modern functional programming languages provide sophisticated
pattern matching facilities; their implementations rely on
pattern matching compilers to break the matching process down
into more basic steps. Recently, to accomodate new features
introduced in the Haskell 1.3 standard, the pattern matching
compiler in Hugs has had to be rewritten to use a more general
algorithm. This informal talk describes a functional program
that was used to prototype the new implementation, and aims to
provide some general insights into the construction and working
of pattern matching compilers.
Traditional sound synthesis programs achieve much of their efficiency
by working with large precomputed tables of discrete sampled data.
Although this approach is very fast, it limits the expressiveness of
the system and can hinder experimentation with new synthesis methods.
In this talk I will describe a different approach to sound synthesis
where sound wave objects are represented as higher-order functions
within a functional language framework. Functions provide a very
natural way of representing arbitrarily complex continuous sound-wave
objects, and higher-order functions offer a very powerful yet intuitive
method of combining and performing operations on sound-waves.
The system I describe was implemented as my final-year project at the
University of Bath.
In functional programming, there is considerable interest in the use of
special-purpose operators such as fold and unfold to structure recursive
programs, and in the use of associated algebraic properties to reason about
programs. In this talk I will explain how recent categorical work shows
how the same techniques can be applied to structure and reason about the
semantics of concurrent languages using a functional language. This
approach gives functional programmers new insights into the semantics of
concurrency, and suggests a number of interesting avenues for further research.
This talk is based upon a forthcoming article.
This informal talk describes the design and implementation
of the Lout document formatting language, with emphasis on
its relationship with functional languages and especially
its treatment of those areas of document formatting which
appear to be poorly suited to the functional approach.