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].

References

  1. A.J.Telford, D.A.Turner " Ensuring Streams Flow" Johnson, ed, Algebraic Methodology and Software Technology - AMAST '97. LNCS 1349, pages 509-523, Springer, 1997.
  2. A.J.Telford, D.A.Turner " Ensuring the Productivity of Infinite Structures" Technical Report TR 14-97, 37 pages, Computing Laboratory, University of Kent, March 1998.
  3. A.J.Telford, D.A.Turner " Ensuring Termination in ESFP", Journal of Universal Computer Science 6(4):474-488, April 2000 (originally presented at 15th British Colloquium in Theoretical Computer Science, Keele, April 1999).
  4. A.J.Telford, D.A.Turner " A Hierarchy of Elementary Languages with Strong Normalisation Properties", Technical Report TR 2-00, 66 pages, University of Kent Computing Laboratory, January 2000.
  5. A.Y.Kaganovsky " Exact Complex Arithmetic in an Imaginary Radix System", Technical Report TR 9-99, 30 pages, Computing Laboratory, University of Kent, July 1999.
  6. A.Y.Kaganovsky