WORKSHOPS IN COMPUTING Series edited by C. J. van Rijsbergen Also in this series Algebraic Methodology and Software Z User Workshop, Cambridge 1994 Technology (AMAST'93) Proceedings of the Eighth Z User Meeting, Proceedings of the Third International Cambridge, 29-30 June 1994 Conference on Algebraic Methodology and J.P. Bowen and J.A. Hall (Eds.) Software Technology, University of Twente, Enschede, The Netherlands, ;/.1-25 June 1993 6th Refinement Workshop M. Nivat, C. Rattray, T. Rus and G. Scollo (Eds.) Proceedings of the 6th Refinement Workshop, organised by BCS-FACS, London, Logic Program Synthesis and Transformation 5-7 January 1994 Proceedings of LOPSTR 93, International David Till (Ed.) Workshop on Logic Program Synthesis and Transformation, Louvain-la-Neuve, Belgium, Incompleteness and Uncertainty in Information 7-9 July 1993 Systems Yves Deville (Ed.) Proceedings ofth'e SOFTEKS Workshop on Incompleteness and Uncertainty in Information Database Programming Languages (DBPL-4) Systems, Concordia University, Montreal, Proceedings of the Fourth International Canada, 8-9 October 1993 Workshop on Database Programming Languages V.S. Alagar, S. Bergler and F.Q. Dong (Eds.) - Object Models and Languages, Manhattan, New York City, USA, 30 AUgUSt-1 September 1993 Rough Sets, Fuzzy Sets and Catriel Beeri, Atsushi Ohori and Knowledge Discovery Dennis E. Shasha (Eds.) Proceedings of the International Workshop on Rough Sets and Knowledge Discovery Music Education: An Artificial Intelligence (RSKD'93), Banff, Alberta, Canada, Approach, Proceedings of a Workshop held as 12-15 October 1993 part of AI-ED 93, World Conference on Artificial Wojciech P. Ziarko (Ed.) Intelligence in Education, Edinburgh, Scotland, 25 August 1993 Algebra of Communicating Processes Matt Smith, Alan Smaill and Proceeedings of ACP94, the First Workshop on Geraint A. Wiggins (Eds.) the Algebra of Communicating Processes, Utrecht, The Netherlands, Rules in Database Systems 16-17 May 1994 Proceedings of the 1st International Workshop A. Ponse, C. Verhoef and on Rules in Database Systems, Edinburgh, S.F.M. van Vlijmen (Eds.) Scotland, 30 August-1 September 1993 Norman W. Paton and Interfaces to Database Systems (IOS94) M. Howard Williams (Eds.) Proceedings of the Second International Workshop on Interfaces to Database Systems, Semantics of Specification Languages (SoSL) Lancaster University, 13-15 July 1994 Proceedings of the International Workshop on Pete Sawyer (Ed.) Semantics of Specification Languages, Utrecht, The Netherlands, 25-27 October 1993 Persistent Object Systems D.J. Andrews, J.F. Groote and Proceedings of the Sixth International Workshop C.A. Middelburg (Eds.) on Persistent Object Systems, Tarascon, Provence, France, 5-9 September 1994 Security for Object-Oriented Systems Malcolm Atkinson, David Maier and Proceedings of the OOPSLA-93 Conference Veronique Benzaken (Eds.) Workshop on Security for Object-Oriented Systems, Washington DC, USA, 26 September 1993 B. Thuraisingham, R. Sandhu and T.C. Ting (Eds.) Functional Programming, Glasgow 1993 Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Scotland, 5-7 July 1993 John T. O'Donnell and Kevin Hammond (Eds.) continued on back page. .. Kevin Hammond, David N. Turner and Patrick M. Sansom (Eds) Functional Programming, Glasgow 1994 Proceedings of the 1994 Glasgow Workshop on Functional Programming, Ayr, Scotland, 12-14 September 1994 Springer-Verlag London Ltd. Kevin Hammond, PhD David N. Turner, BSc Patrick M. Sansom, BSc, PhD Department of Computing Science, Glasgow University, Glasgow G12 8QQ, Scotland ISBN 978-3-540-19914-4 British Library Cataloguing in Publication Data Functional Programming, Glasgow 1994: Proceedings of the 1994 Glasgow Workshop on Functional Programming, Ayr, Scotland, 12-14 September 1994. - (Workshops in Computing Series) I. Hammond, Kevin II. Series 005·1 ISBN 978-3-540-19914-4 Library of Congress Cataloging-in-Publication Data Glasgow Workshop on Functional Programming (1994: Ayr, Scotland) Functional programming, Glasgow 1994: proceedings of the 1994 Glasgow Workshop on Functional Programming, Ayr, Scotland, 12-14 September 19941 Kevin Hammond, David N. Turner, and Patrick M. Sansom. p. cm. - (Workshops in computing) "Published in collaboration with the British Computer Society." Includes bibliographical references and index. ISBN 978-3-540-19914-4 ISBN 978-1-4471-3573-9 (eBook) DOI 10.1007/978-1-4471-3573-9 1. Functional programming (Computer science)-Congresses. I. Hammond, Kevin. II. Turner, David N. (David Neil), 1968- III Sansom, Patrick. IV. British Computer Society. V. Title. VI. Series. QA76.62.G58 1995 94-44476 005.1'1-dc20 CIP Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form, or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms of licences issued by the Copyright Licensing Agency. Enquiries concerning reproduction outside those terms should be sent to the publishers. © Springer-Verlag London 1995 The use of registered names, trademarks etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant laws and regulations and therefore free for general use. The publisher makes no representation, express or implied, with regard to the accuracy of the information contained in this book and cannot accept any legal responsibility or liability for any errors or omissions that may be made. Typesetting: Camera ready by contributors 34/3830-543210 Printed on acid-free paper Preface This is the proceedings of the seventh annual workshop held by the Glasgow Functional Programming Group. The purpose of the workshop is to provide a focus for new research, to foster research contacts with other functional language researchers, and to provide a platform for research students to develop their presentation skills. As in previous years, we spent three days closeted together in a pleasant seaside town, isolated from normal work commitments. We were joined by colleagues from other universities (both UK and abroad) and from industry. Workshop participants presented a short talk about their current research work, and produced a paper which appeared in a draft proceedings. These papers were then reviewed and revised in the light of discussions at the workshop and the referees' comments. A selection of those revised papers (the majority of those presented at the workshop) appears here in the published proceedings. The papers themselves cover a wide span, from theoretical work on algebras and bisimilarity to experience with a real-world medical applica tion. Unsurprisingly, given Glasgow's track record, there is a strong emphasis on compilation techniques and optimisations, and there are also several papers on concurrency and parallelism. Each year many people make significant contributions to organising the workshop, and without their efforts we would not be able to hold the workshop at all. We would particularly like to thank John O'Donnell (General Chair), Sigbj0rn Finne, Andy Gill, Cordy Hall, David King, Andrew Partridge, and Simon Peyton Jones for all their hard work this year. We would also like to thank all the reviewers who have devoted their time to help improve the papers which are published here. This year's workshop was generously sponsored by Canon UK, Harlequin, ICL Ltd., and Software AG. We are very grateful for their continued support over the years that this workshop has been running. Glasgow University Kevin Hammond December 1994 David N. Turner Patrick Sansom Contents List of Contributors ................................................................................... ix Expression Refinement: Deriving Bresenham's Algorithm A. Bunkenburg and S. Flynn ....................................................................... 1 Dynamic Algebra for Calculating Algorithms K. Clenaghan ............................................................................................... 18 On the Expressive Power of Constructor Classes L. Duponcheel and E. Meijer.................................................................... 29 Programming Reactive Systems in Haskell S.O. Finne and S.L. Peyton Jones ............................................................. 50 Techniques for Simplifying the Visualization of Graph Reduction S.P. Foubister and C. Runciman ............................................................. 66 A Tutorial on Co-Induction and Functional Programming A.D. Gordon ................................................................................................. 78 Unboxing Using Specialisation C. V. Hall, S.L. Peyton Jones and P.M. Sansom ..................................... 96 Improving Granularity in Parallel Functional Programs: A Graphical Winnowing System for Haskell K. Hammond, H. W. Loidl and A. Partridge ......................................... 111 Fold-Unfold Transformations on State Monadic Interpreters T. Johnsson ................................................................................................. 127 Functional Binomial Queues D.J. King ...................................................................................................... 141 Mechanized Reasoning About Functional Programs S. Mintchev ................................................................................................. 151 A Case Study in Parallel Program Derivation: The Heat Equation Algorithm J.T. O'Donnell and G. Runger................................................................. 167 Compilation by Transformation in the Glasgow Haskell Compiler S.L. Peyton Jones and A. Santos............................................................. 184 viii Contents Experience of Developing a Cervical Cytology Scanning System Using Gofer and Haskell 1. Poole and D. Charleston ...................................................................... 205 Binding-Time Improvement and Fold-Unfold Transformation C. Runciman .............................................................................................. 218 Data Dependent Concurrency Control P. W. Trinder .............................................................................................. 231 Type-Checked Message-Passing Between Functional Processes M. Wallace and C. Runciman ................................................................ 245 Author Index .......................................................................................... 255 List of Contributors Bunkenberg, A. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, Gil 8QQ. Charleston, D. MRC Human Genetics Unit, Crewe Rd., Edinburgh, EH4 2XU. Clenaghan, K. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, Gil 8QQ. Duponcheel, L. Vakgroep Informatika, Rijks Universitaet Utrecht, Utrecht, The Netherlands. Finne, S.O. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 8QQ. Flynn, S. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, Gil 8QQ. Foubister, S.P. Institute for Computer Based Learning, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS. Gordon, A.D. University of Cambridge Computer Laboratory, New Museums Site, Cambridge, CB2 3QG. Hall,C.V. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 8QQ. Hammond,K. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 8QQ. Johnsson, T. Department of Computer Science, Chalmers University of Technology, S-412 96 Goteborg, Sweden. King,D.J. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, Gil 8QQ. Loidl,H.W. RISC-LINZ Research Institute for Symbolic Computation, Johannes Kepler University, A-4040, Linz, Austria. Meijer, E. Vakgroep Informatika, Rijks Universitaet Utrecht, Utrecht, The Netherlands. Mintchev, S. Department of Computer Science, Victoria University of Manchester, Manchester, MI39PL. O'Donnell, J.T. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 8QQ. x List of Contributors Partridge, A. Department of Computer Science, University of Tasmania, Australia. Peyton Jones, S.L. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 SQQ. Poole, I. MRC Human Genetics Unit, Crewe Rd., Edinburgh, EH4 2XU. Runger, G. FB 14 Informatik, Universitat des Saarlandes, PF 151150, 66041 Saarbrucken, Germany. Runciman, C. Department of Computer Science, University of York, Heslington, York, Y01SDD. Sansom, P.M. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 SQQ. Santos, A. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 SQQ. Trinder, P.W. Department of Computing Science, Glasgow University, 17 Lilybank Gardens, Glasgow, G12 SQQ. Wallace, M. Department of Computer Science, University of York, Heslington, York, YOI SDD. Expression Refinement: Deriving Bresenham's Algorithm Alexander Bunkenburg* and Sharon Flynn* Computing Science Department, University of Glasgow, Scotland {bunkenba,sharon}@dcs.glasgow.ac.uk http://www.dcs.glasgow.ac. ukr {bunkenba,sharon} Abstract This paper illustrates a method of transforming an initial specification expression, which is not necessarily algorithmic, into an efficient func tional implementation using a refinement calculus for expressions. In doing this, we benefit from the ease of manipulation that state-less ex pressions allow. However, implementations of functional algorithms are not as cheap as imperative implementations. We further show how an imperative program can be derived from a functional expression using al gebraic transformations based on the state monad model. The example used to illustrate the method is Bresenham's line drawing algorithm. 1 Introduction In this paper we show how a simple specification expression can be refined to an efficient functional program and then further transformed into an imperative program which is cheaper to implement than its functional equivalent. For the purpose of derivation, expressions are easier to manipulate than statements. This can be seen, for example, in the Bird-Meertens formal ism [Mee86, Bir86, Bac89], 'Squiggol', where obviously correct functional pro grams are transformed into more efficient programs using derivation steps which are equalities and which preserve correctness. Moreover, it is often the case that problems can be specified more naturally and elegantly using expressions rather than imperative commands. The refinement calculus for expressions used in this paper, based on the refinement calculus for imperative program ming [Mor90, Mor89], is being developed to allow the refinement of possibly non-algorithmic specification expressions to executable expressions of a func tional programming language, using a set of refinement laws. Unfortunately, implementations of functional algorithms are not as cheap as imperative implementations, where cheap means fast and using predictably little memory. The use of the state monad [Wad92, PJW93, Lau93] permits the capture of imperative programming in a functional language, which guar antees a safe imperative evaluation. This paper illustrates a method of deriving a correct imperative program from a certain form of functional specification, making use of the state monad. ·Supported by a postgraduate research studentship from the Engineering and Physical Sciences Research Council.