Glasgow has been heavily involved in the design and implementation of the new common functional programming language Haskell. This work has several complementary goals: (a) to produce a useful compiler, so that people can use Haskell for real applications, and so that we can use their feedback to guide our research priorities; and (b) to provide a realistic setting within which to study design and implementation choices.
Functional languages are typically poor at expressing computations where state plays an essential role, or applications where input/output is a major feature. In both cases the absence of side effects seems more of a handicap than a benefit, yet the introduction of unrestricted side effects would destroy most of the advantages enjoyed by functional languages. We have now discovered a very fruitful approach to these difficulties, based on monads, which has given rise to several strands of research:
High level programming languages require powerful compilers in order to produce efficient code, and finding opportunities to perform optimisation is important. Traditionally, however, optimisation is seen to be dangerous, as the optimisation phase of many compilers can introduce bugs into otherwise correct programs.
There is a class of optimisation that can be guaranteed not to introduce bugs, namely those which preserve the meaning (or semantics) of the program. By manipulating an abstract version of the semantics of a source program, a compiler is able to guarantee only to introduce semantics-preserving optimisations.
Glasgow has been a partner in the ESPRIT basic research action Semantique which has focused both on the theory and practice of semantic analysis and program transformation, including such areas as, strictness analysis (determining when certain context-dependent optimisations may be performed), binding-time analysis (allowing compile-time computation to be performed), closure analysis (determining which functions might be passed as parameters to a given function), and update-avoidance analysis (allowing a faster computational model to be adopted in places).
Fundamental work on logic by Turing, in the 1930s, led directly to the notion of the stored-programme computer in the 1940s. Related work by Church and Curry, also in the 1930s, led directly to functional programming in the 1960s. This make clear two things: first, logic is a fertile source of ideas for computer scientists; and, second, for those ideas to percolate from logic into computing takes quite a while.
As a case in point, consider category theory. It was developed in the 1940s to generalise concepts arising in topology and logic, and it took computer scientists until the late 1980s to apply it. Type theory is a close cousin of category theory and, like it, has old roots in logic, and has recently come into vogue among computer scientists.
Work in Glasgow has centred on finding practical applications of concepts arising in category theory and type theory. One such application, described above, is our extensive use of monads, especially to describe state-ful computation and input/output.
Functional languages such as Standard ML and Haskell use a polymorphic type system. It has long been known that this had close ties to ideas in logic, but only recently was it realised that it also had close ties with category theory. This connection led to the realisation that from the type of a polymorphic function one could automatically deduce useful properties that it must satisfy - a method christened 'theorems for free'. The same method has proven useful in semantics-based program manipulation and analysis.
The French mathematician Girard has recently devised a new form of logic called linear logic. Linear logic treats truth as an expendable resource - it caters to facts that can be used exactly once. We are using linear logic to design type systems that control the way in which objects are used, resulting in more efficient functional programs. In particular, we have new solutions based on type systems to two old (and related problems): When is it safe not to update a closure? When is it safe to update a data structure in place? We are currently implementing and testing these solutions in the Glasgow Haskell compiler.
The absence of side-effects in pure functional languages makes them particularly suitable for parallel execution. Despite this potential, it has proved quite difficult to build a parallel implementation of Haskell with good performance compared to a state-of-the art compiler for a uniprocessor; indeed no such implementations are readily available.
Based on our earlier work on a purpose-built multiprocessor called GRIP, we are now developing the Glasgow Haskell compiler into a portable implementation of Haskell for parallel machines, including both shared-memory and distributed-memory architectures.
An early target will be the ICL Goldrush machine, on which we plan to build a parallel database engine in Haskell. Using a functional language for this purpose opens up new opportunities for both inter-transaction and intra-transaction parallelism, for instantaneous checkpointing, and for distributed locking.
Massively parallel architectures and functional languages fit very well together. These machines offer standard primitives for communication and computation that correspond directly to higher order functions that are central to functional programming (map, fold, scan, etc.). This means that massively parallel programs can be expressed very naturally in a functional language.
The key advantage of functional programming is that it supports equational reasoning, which helps us to derive and prove the correctness of parallel programs. This approach has been successfully applied to the implementation of parallel scan, sorting algorithms and list processing algorithms.
We're now implementing Connection Machine Haskell and applying it to several programming problems. This is an interface between the Glasgow Haskell Compiler and the CM-200. It exploits the monadic I/O supported by GHC, and links C object code from Haskell with the C* libraries on the Connection Machine. Presently the Connection Machine must be programmed in C, Lisp or FORTRAN; our aim is to add Haskell to that list.
We have been using functional languages to cast elegant specifications of digital synchronous systems. Traditional hardware or VLSI design uses schematic diagrams to represent circuits. These diagrams are difficult to maintain, it is hard to express generality and they are difficult to manipulate or reason about. Traditional hardware description languages have complicated semantics and are difficult to transform and are awkward to use with formal verification techniques.
We use a functional language notation for our research for a variety of compelling reasons. Functional languages capture nicely the data flow through digital circuits. Function composition corresponds to component interconnection. Our notation is easy to transform, and the semantics of our descriptions is well understood. We have developed a library of transformation laws that allow us to manipulate circuits whilst preserving behaviour. The style of descriptions we use are similar to those developed by John O'Donnell (see formal methods section). Transformation is a particularly useful for exploring space time tradeoffs. Our functional language hardware descriptions are automatically translated into VHDL which is then used as input into commercial VLSI CAD tools to actually produce VLSI programming information.
The Glasgow Haskell compiler group wants to see Haskell used for large, real world applications, and regards this as a significant measure of the project's success. In our view, the experience of supporting real applications uniquely exposes new research problems, and guides research priorities.
The DEAR project (Database Easy Retrieval), developed at Durham University by Roberto Garigliano and Rick Morgan, is a good example of the applications we have in mind. It integrates LOLITA (one of the world's most powerful natural language processing systems) with the Glasgow Haskell compiler and a large commercial database contributed by the Atomic Energy Authority. It will be executed on a parallel machine, which requires that the compiler produce good code for a Sun shared-memory multiprocessor. Another recent application is the SADLI project (Safety Assurance in Diagnostic Laboratory Imaging) at the MRC Human Genetics Unit in Edinburgh. SADLI uses Haskell to implement a system for screening microscope images for indications of cervical cancer. The emphasis of the project is on the exploitation of function languages to support formal specification and software development processes. The project also makes extensive use of Glasgow Haskell's foreign language interface, and indeed was a driving force in the development of this interface.
The group continues actively to seek and support real-world applications of Haskell.
Functional Programming Group,
Last changed: $Date: 1996/05/13 10:10:59 $