Trends in Functional Programming Volume 5

Description

IgZcYh ^c ;jcXi^dcVa Egd\gVbb^c\ KdajbZ * :Y^iZY Wn =Vch"Lda[\Vc\ Ad^Ya I]^h Wdd` egZhZcih aViZhi gZhZVgX] YZkZadebZcih ^c i]Z VgZV d[ [jcXi^dcVa egd\gVbb^c\# I]Z Xdcig^Wji^dch ^c i]^h kdajbZ XdkZg V l^YZ gVc\Z d[ ide^Xh [gdb i]Zdgn! [dgbVa VheZXih d[ [jcXi^dcVa egd\gVbb^c\! \gVe]^Xh VcY k^hjVa egd\gVbb^c\ id Y^hig^WjiZY Xdbeji^c\ VcY Xdbe^aZg YZh^\c# 6h ^h d[iZc i]Z XVhZ ^c i]^h Xdbbjc^in! i]Z bdhi egda^[^X ldg` XdbZh dji d[ i]Z XdbW^cVi^dc d[ i]ZdgZi^XVa ldg` l^i] ^ih Veea^XVi^dc dc XaVhh^XVa egdWaZbh ^c XdbejiZg hX^ZcXZ# EVgi^XjaVg igZcYh ^c i]^h kdajbZ VgZ/ gZVhdc^c\ VWdji [jcXi^dcVa egd\gVbh VjidbViZY i]ZdgZb egdk^c\ [dg ]^\]"aZkZa egd\gVbb^c\ aVc\jV\Zh aVc\jV\Z hjeedgi [dg XdcXjggZcXn VcY Y^hig^Wji^dc# I]Z I;E hZg^Zh ^h YZY^XViZY id egdbdi^c\ cZl gZhZVgX] Y^gZXi^dch gZaViZY id i]Z [^ZaY d[ [jcXi^dcVa egd\gVbb^c\ VcY id ^ckZhi^\ViZ i]Z gZaVi^dch]^eh d[ [jcXi^dcVa egd\gVbb^c\ l^i] di]Zg WgVcX]Zh d[ XdbejiZg hX^ZcXZ# >i ^h YZh^\cZY id WZ V eaVi[dgb [dg cdkZa VcY jeXdb^c\ gZhZVgX]# 9g# =Vch"Lda[\Vc\ Ad^Ya^h V gZhZVgX] VhhdX^ViZ ^c i]Z I]ZdgZi^XVa 8dbejiZg HX^ZcXZ \gdje Vi i]Z 9ZeVgibZci [dg >c[dgbVi^Xh! AjYl^\"BVm^b^a^Vch Jc^kZgh^in! Bjc^X]# ^ciZaaZXiED 7dm -+'! 7g^hida 7H.. &9:!

Sujets

• Programming
• Computers
• Informatique
• General officer
• Computer programming
• General

Informations

• Publié par: Intellect Books
• Date de parution: 01 janvier 2006
• Nombre de lectures: 0
• EAN13: 9781841509563
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

i ^h YZh^\cZY id WZ V eaVi[dgb [dg cdkZa VcY jeXdb^c\ gZhZVgX]# 9g# =Vch"Lda[\Vc\ Ad^Ya^h V gZhZVgX] VhhdX^ViZ ^c i]Z I]ZdgZi^XVa 8dbejiZg HX^ZcXZ \gdje Vi i]Z 9ZeVgibZci [dg >c[dgbVi^Xh! AjYl^\"BVm^b^a^Vch Jc^kZgh^in! Bjc^X]# ^ciZaaZXiED 7dm -+'! 7g^hida 7H.. &9:!" />

Trends in Functional Programming Volume 5

Edited by Hans-Wolfgang Loidl

This book presents latest research developments in the area of functional programming. The contributions in this volume cover a wide range of topics from theory, formal aspects of functional programming, graphics and visual programming to distributed computing and compiler design. As is often the case in this community, the most prolific work comes out of the combination of theoretical work with its application on classical problems in computer science. Particular trends in this volume are: Treasoning about functional programs Tautomated theorem proving for high-level programming languages Tlanguage support for concurrency and distribution.

The TFP series is dedicated to promoting new research directions related to the field of functional programming and to investigate the relationships of functional programming with other branches of computer science. It is designed to be a platform for novel and upcoming research.

Dr. Hans-Wolfgang Loidlis a research associate in the Theoretical Computer Science group at the Department for Informatics, Ludwig-Maximilians University, Munich.

intellectPO Box 862, Bristol BS99 1DE, United Kingdom/www.intellectbooks.com

ISBN 1-84150-144-1

9 781841 501444

Loidl Trends in Functional ProgrammingVolume 5 Edited by Hans-Wolfgang Loidl Trends in Functional Programming

Volume 5

intellect

intellect Bristol, UK Portland, OR, USA

First published in the UK in 2006 by Intellect Books, PO Box 862, Bristol BS99 1DE, UK. First published in the USA in 2006 by Intellect Books, ISBS, 920 NE 58th Ave. Suite 300, Portland, Oregon 972133786, USA.

Copyright ©2006 Intellect Ltd.

All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording, or otherwise, without written permission.

A catalogue record for this book is available from the British Library

Electronic ISBN 1-84150-956-6 / ISBN1841501441 ISSN 17434505 (Print)

Printed and bound in Great Britain by 4edge Ltd.

Contents

1

2

3

Proof Support for General Type Classes Ron van Kesteren, Marko van Eekelen, Maarten de Mol 1.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2Sparkle. . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . 1.3Preliminaries. . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4Structural induction. . . . . . . . . . . . . . . . . . . . . . . . . 1.5Induction on instances. . . . . . . . . . . . . . . . . . . . . . . 1.6Multiple class constraints. . . . . . . . . . . . . . . . . . . . . . 1.7Implementation. . . . . . . . . . . . . . . . . . . . . . . . . . . 1.8Related and future work. . . . . . . . . . . . . . . . . . . . . . . 1.9Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Generic Proofs for Combinator-based Generic Programs Fermı ´ nReig 2.1Introduction. . . . . . . . . . . . . . . . . . . . . . . 2.2`Boilerplate' combinators as generic functions. . . . . 2.3Generic proofs for `boilerplate' combinators. . . . . . 2.4A proof of the fusion law forgmapT. . . . . . . . . . 2.5A theorem aboutoccurs. . . . . . . . . . . . . . . . . 2.6A fusion law foreverywhere. . . . . . . . . . . . . . 2.7Conclusions and further work. . . . . . . . . . . . . . 2.8Proof of lemma 2.1. . . . . . . . . . . . . . . . . . . 2.9Proof of lemma 2.2. . . . . . . . . . . . . . . . . . . 2.10Proof of lemma 2.3. . . . . . . . . . . . . . . . . . . 2.11Proof of theorem 2.5 (continued). . . . . . . . . . . . References . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

Building certified components within FOCAL Catherine Dubois, Thérèse Hardin, Véronique Viguié Donzeau Gouge 3.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 FOCAL requirements and design principles. . . . . . . . . . . . . 3.3Overview of FOCAL . . . . . . . . . . . . . . . . . . . . . . . . .

1

4 5 7 8 10 14 14 15 15

17

17 19 20 21 22 25 28 29 29 30 30 31

33

33 34 35

4

5

6

7

3.4A complete example. . . . . . . . . . . . . . . . . . . . . . . . 3.5Compiling. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6Applications. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8Conclusion and future work. . . . . . . . . . . . . . . . . . . . . References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Calculating an Exceptional Machine Graham Hutton, Joel Wright 4.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2Abstract machines. . . . . . . . . . . . . . . . . . . . . . . . . . 4.3Arithmetic expressions. . . . . . . . . . . . . . . . . . . . . . . 4.4Adding exceptions. . . . . . . . . . . . . . . . . . . . . . . . . 4.5Further work. . . . . . . . . . . . . . . . . . . . . . . . . . . . References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Generalizing the AUGMENT Combinator Neil Ghani, Tarmo Uustalu, Varmo Vene 5.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2Semantics of FOLD / BUILD . . . . . . . . . . . . . . . . . . . . . 5.3The AUGMENT of free monads. . . . . . . . . . . . . . . . . . . 5.4A generalized AUGMENT combinator. . . . . . . . . . . . . . . . 5.5Conclusion and future work. . . . . . . . . . . . . . . . . . . . . References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

38 43 45 46 46 47

49

49 50 51 58 63 64

65

65 66 69 72 77 77

Alice Through the Looking Glass79 Andreas Rossberg, Didier Le Botlan, Guido Tack, Th. Brunklaus, Gert Smolka 6.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 6.2Futures80. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.3Higher-order modules83. . . . . . . . . . . . . . . . . . . . . . . . 6.4Packages. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 6.5Components86. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.6Decomposing components88. . . . . . . . . . . . . . . . . . . . . 6.7Distribution. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 6.8Implementation92. . . . . . . . . . . . . . . . . . . . . . . . . . . 6.9 Related work92. . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.10Outlook. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

Experiments with GHC's Optimiser László Németh 7.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2Contributions of the paper. . . . . . . . . . . . . . . . . . . . . 7.3The setup. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4The method. . . . . . . . . . . . . . . . . . . . . . . . . . . . .

97

97 98 98 99

8

9

7.5Evaluation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 7.6Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 7.7Conclusions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108

Disjoint Forms in Graphical User Interfaces113 Sander Evers, Peter Achten, Rinus Plasmeijer 8.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 8.2 FunctionalForms summary. . . . . . . . . . . . . . . . . . . . . 114 8.3Combinators for disjoint forms. . . . . . . . . . . . . . . . . . . 116 8.4Implementation. . . . . . . . . . . . . . . . . . . . . . . . . . . 119 8.5Safety. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 8.6Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 8.7Conclusions and future work. . . . . . . . . . . . . . . . . . . . 126 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127

A Graphic Functional-Dataflow Language129 Silvia Clerici, Cristina Zoltan 9.1Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 9.2Outline of the NiMo language. . . . . . . . . . . . . . . . . . . 131 9.3The NiMo environment. . . . . . . . . . . . . . . . . . . . . . . 138 9.4Current state and future work. . . . . . . . . . . . . . . . . . . . 142 9.5Concluding remarks. . . . . . . . . . . . . . . . . . . . . . . . . 143 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144

Preface

The fifth installment of the `Trends in Functional Programming' series was the first one to be organised outside Scotland, the homeland of functional program- ming that hosted previous installments of TFP and the precursor series, the `Scot- tish Functional Programming Workshops', going back to 1989 . In November 2004, Ludwig-Maximilians University, Munich was the host for TFP04. With the change of venue we had a broad spectrum of submissions both in terms of con- tents and nationality of the authors: in total 22 papers have been submitted for presentation, and TFP04 itself was attended by 36 participants from 13 countries. The Symposium on Trends in Functional Programming (TFP) is dedicated to promoting new research directions related to the field of functional program- ming and to investigate the relationships of functional programming with other branches of computer science. It is designed to be a platform for novel and up- coming research, combined with a post-event refereeing process and a formal pub- lication of selected papers as a book. The presentations submitted this year show a wide spectrum of current research within this scope, from theoretical work on foundations of programming languages to practical usage of functional languages in many different domains. Reflecting our dedication to promote the work by young researchers in this field, the programme committee for TFP has selected this year for the first time a student paper for the `Best Student Paper' award. We are glad to announce that for TFP04 this award goes to:

Ron van Kesteren, Marko van Eekelen, Maarten de Mol `Proof Support for General Type Classes'

We hope that this award will be even more motivation for all young researchers to produce high-quality papers describing their work and to present it in an interna- tional forum. The papers in this volume of TFP cover a wide range of topics from theory, formal aspects of functional programming, graphics and visual programming to distributed computing and compiler design. As is often the case in this commu- nity, the most prolific work comes out of the combination of theoretical work with its application on classical problems in functional programming. The distinguished paper by van Kesteren et al. in Chapter 1 is a good exam- ple of this combination, developing proof methods in the SPARKLE system in

i

ii

Trends in Functional Programming 2004

order to prove properties common to all instances of a Haskell type class. One fruitful and very active area of functional languages at the moment is generic programming. In Chapter 2, Reig presents a methodology for proving common properties of such generic programs, phrased in type classes within Haskell. The work of Dubois et al. on the FOCAL system in Chapter 3 follows a similar over- all direction, integrating proving support into a high-level functional language and supporting advanced language features in the proving component of the integrated system. Any formal treatment of modern programming languages has to cope with the presence of many different language concepts, and thus concrete formalisa- tions often become unwieldy. In Chapter 4, Hutton and Wright demonstrate how to introduce exceptions into a simple abstract machine by performing equational reasoning on its high-level specification. In Chapter 5, Ghani et al. discuss the cat- egory theoretic foundations of combinators such as fold and augment, and extend their results to a wider class of inductive types using these combinators. The core areas for the TFP series of programming language design and imple- mentation are covered by several papers. In Chapter 6, Rossberg et al. present a functional language for distributed computation, using classical concepts such as futures for synchronisation. In Chapter 7, Németh presents a detailed empirical analysis of the performance of the GHC Haskell compiler, with varying orderings of the optimisation phases, and identifies orderings that consistently improve per- formance over the default setting for maximal optimisation. In Chapter 8, Evers et al. present a method for the better separation of the logic and the layout of GUI-level forms, and present a library providing an added level of abstraction. Finally, Clerici and Zoltan present in Chapter 9 NiMo, a graphic programming language based on dataflow graphs using lazy evaluation, which provides support for debugging and step-wise program development in its visual programming en- vironment.

Hans-Wolfgang Loidl, Munich

Acknowledgements

I would like to thank Martin Hofmann and the other members of the Theoreti- cal Computer Science group of the Department for Informatics at the Ludwig- Maximilians University, Munich, for the help in promoting and organising TFP04. I am indebted to Max Jakob and Spyridon Iliopoulos for valiant on-site help dur- ing TFP04. I am particularly grateful to the members of the programme commit- tee and all the referees for a smooth refereeing process. The programme commit- tee for TFP04 was comprised of: •Stephen Gilmore, University of Edinburgh •Gaetan Hains, Universite d'Orleans •Kevin Hammond, University of St Andrews •John Hughes, Chalmers University •Hans-Wolfgang Loidl, Ludwig-Maximilians-University Munich (Chair) •Rita Loogen, Philipps-University Marburg •Greg Michaelson, Heriot-Watt University Edinburgh •John O'Donnell, University of Glasgow •Ricardo Pena, Universidad Complutense de Madrid •Phil Trinder, Heriot-Watt University Edinburgh •Marko van Eekelen, University of Nijmegen •Phil Wadler, University of Edinburgh Further thanks go to the members of the TFP steering committee for general ad- vice and concrete help in running this event. Last, but not least, I want to thank all participants of TFP04 for making this year's symposium such a lively event and for making it worth the while for me to organise it. I am happy to acknowledge financial support by the EU through the APPSEM II Thematic Network and the Mobile Resource Guarantees project, funded as IST- 2001-33149 under the European Commission's Fifth Framewor k Programme.