Elementary Strong Functional Programming: Summary
Professor D. A. Turner,
Computing Laboratory,
University of Kent,
Canterbury CT2 7NF, UK.
The project, funded by the UK Engineeering and Physical Sciences Research Council (EPSRC) from 14.10.96 to 13.10.99 under grant GR/L03279, was undertaken to investigate the practical viability of a discipline of strong functional programming proposed in [8]. The research associate was Alastair Telford.
In strong functional programming all expressions are guaranteed to have normal form. In order to retain the possibility of programming with infinite structures, which is an essential feature of pure functional languages such as Haskell, a key part of the methodology of [8] is to maintain a separation in the type system between data, which is known to be finite, and codata which is permitted to be infinite. This may be contrasted with the usual situation in lazy functional programming in which infinite lists for example, have the same compile-time type as ordinary finite lists.
The separation between data and codata leads to a distinction between recursion, which to be "safe" must be well-founded, and corecursion, which must be productive. Our main achievements are the development of techniques of abstract interpretation, which we demonstrate can recognise at compile time sufficiently large classes of safe recursion and corecursion to permit a wide range of standard functional algorithms to be accepted in their "natural" form. Previous work on automatic termination detection, based for example on Walther recursion, has required even quite simple algorithms, for example gcd, to be rewritten in a special style. We believe these results substantially advance the practical viability of strong functional programming.
Our techniques for recognising productivity in corecursive definitions of infinitary structures are presented in [1,2] and those for well-founded recursion over finitary data structures in [3,4].
Alexander Kaganovsky, a PhD student associated with the group, did outstanding work on the investigation of an important class of corecursive algorithms over infinite lists of integers. The problem area he studied is the efficient implementation of unbounded precision arithmetic on real and complex numbers represented as streams of signed digits. His results, which include algorithms for many analytic functions and are a significant advance on previous work, are described in two papers and his thesis [5,6,7].
For further information contact the investigator at the University of Kent.
Final report PDF [84K].