School of Computing

Publications by Dr Olaf Chitil

Also view these in the Kent Academic Repository
Articles

    Swierstra, S. Doaitse and Chitil, Olaf (2009) Linear, bounded, functional pretty-printing. Journal of Functional Programming, 19 (01). pp. 1-16. ISSN 0956-7968.

    Abstract

    We present two implementations of Oppen's pretty-printing algorithm in Haskell that meet the efficiency of Oppen's imperative solution but have a simpler, clear structure. We start with an implementation that uses lazy evaluation to simulate two co-operating processes. Then we present an implementation that uses higher-order functions for delimited continuations to simulate co-routines with explicit scheduling.

    Chitil, Olaf (2005) Pretty printing with lazy dequeues. Transactions on Programming Languages and Systems (TOPLAS), 27 (1). pp. 163-184. ISSN 0164-0925.

    Abstract

    There are several purely functional libraries for converting tree structured data into indented text, but they all make use of some backtracking. Over twenty years ago, Oppen published a more efficient imperative implementation of a pretty printer. This article shows that the same efficiency is also obtainable without destructive updates by developing a similar but purely functional Haskell implementation with the same complexity bounds. At its heart lie two lazy double ended queues.

    Chitil, Olaf (1997) The Sigma-Semantics: A Comprehensive Semantics for Functional Programs. Fundamenta Informaticae, 31. pp. 253-294.

    Abstract

    A comprehensive semantics for functional programs is presented, which generalizes the well-known call-by-value and call-by-name semantics. By permitting a separate choice between call-by value and call-by-name for every argument position of every function and parameterizing the semantics by this choice we abstract from the parameter-passing mechanism. Thus common and distinguishing features of all instances of the sigma-semantics, especially call-by-value and call-by-name semantics, are highlighted. Furthermore, a property can be validated for all instances of the sigma-semantics by a single proof. This is employed for proving the equivalence of the given denotational (fixed-point based) and two operational (reduction based) definitions of the sigma-semantics. We present and apply means for very simple proofs of equivalence with the denotational sigma-semantics for a large class of reduction-based sigma-semantics. Our basis are simple first-order constructor-based functional programs with patterns.

Book Sections

    Chitil, Olaf (2009) Functional Programming. In: Wah, Benjamin W. Encyclopedia of Computer Science and Engineering. John Wiley & Sons, Hoboken, NJ, pp. 1334-1344. ISBN 978-0-471-38393-2.

    Abstract

    Functional programming is a programming paradigm like object-oriented programming and logic programming. Functional programming comprises both a specific programming style and a class of programming languages that encourage and support this programming style. Functional programming enables the programmer to describe an algorithm on a high-level, in terms of the problem domain, without having to deal with machine-related details. A program is constructed from functions that only map inputs to outputs, without any other effect on the program state. Thus a function will always return the same output, regardless of when and in which context the function is used. These functions provide clear interfaces, separate concerns and are easy to reuse. A small and simple set of highly orthogonal language constructs assists in writing modular programs.

    Luo, Yong and Chitil, Olaf (2007) Proving the correctness of algorithmic debugging for funtional programs. In: Nilsson, Henrik Trends in Functional Programming. Trends in Functional Programming, 7. Intellect UK, United States, pp. 19-34. ISBN 978-1841501888.

    Abstract

    This paper formally presents a model of tracing for functional programs based on a small-step operational semantics. The model records the computation of a functional program in a graph which can be utilised for various purposes such as algorithmic debugging. The main contribution of this paper is to prove the correctness of algorithmic debugging for functional programs based on the model. Although algorithmic debugging for functional programs is implemented in several tracers such as Hat, the correctness has not been formally proved before. The difficulty of the proof is to find a suitable induction principle and a more general induction hypothesis.

    Chitil, Olaf and Luo, Yong (2007) Proving the Correctness of Algorithmic Debugging for Functional Programs. In: UNSPECIFIED Trends in Functional Programming. Intellect. ISBN 9781841501888.

    Abstract

    This paper formally presents a model of tracing for functional programs based on a small-step operational semantics. The model records the computation of a functional program in a graph which can be utilised for various purposes such as algorithmic debugging. The main contribution of this paper is to prove the correctness of algorithmic debugging for functional programs based on the model. Although algorithmic debugging for functional programs is implemented in several tracers such as Hat, the correctness has not been formally proved before. The difficulty of the proof is to find a suitable induction principle and a more general induction hypothesis.

Conference Items

    Chitil, Olaf (2012) Practical Typed Lazy Contracts. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012).

    Abstract

    Until now there has been no support for specifying and enforcing contracts within a lazy functional program. That is a shame, because contracts consist of pre- and post-conditions for functions that go beyond the standard static types. This paper presents the design and implementation of a small, easy-to-use, purely functional contract library for Haskell, which, when a contract is violated, also provides more useful information than the classical blaming of one contract partner. From now on lazy functional languages can profit from the assurances in the development of correct programs that contracts provide.

    Chitil, Olaf (2011) A semantics for lazy assertions. In: Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation.

    Abstract

    Lazy functional programming languages need lazy assertions to ensure that assertions preserve the meaning of programs. Examples in this paper demonstrate that previously proposed lazy assertions nonetheless break basic semantic equivalences, because they include a non-deterministic disjunction combinator. The objective of this paper is to determine ''correct'' definitions for lazy assertions. The starting point is our formalisation of basic properties such as laziness, taking them as axioms of our design space. We develop the first denotational semantics for lazy assertions; assertions denote subdomains. We define a weak disjunction combinator and together with a conjunction combinator assertions form a bounded distributive lattice. From the established laws we derive an efficient prototype implementation of lazy assertions for Haskell as a library.

    Chitil, Olaf and Davie, Thomas (2008) Comprehending Finite Maps for Algorithmic Debugging of Higher-Order Functional Programs. In: PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming.

    Abstract

    Algorithmic debuggers for higher-order functional languages have to display functional values. Originally functional values had been represented as partial applications of function and constructor symbols, but a recent approach represents functional values as finite maps. The two representations require the computation tree that is central to algorithmic debugging to be structured rather differently. In this paper we present a unifying framework that formally defines algorithmic debugging for both representations in an implementation-independent way. On this basis we prove the soundness of algorithmic debugging with finite maps. Our framework shows how a single implementation can support both forms of algorithmic debugging. The proof exposed that algorithmic debugging with finite maps does not handle arbitrary functional programs, but in current practice the problematic ones are excluded by Haskell's type system. Both framework and proof suggest variations of algorithmic debugging with finite maps and thus are tools for further improvement of this form of debugging.

    Chitil, Olaf and Huch, Frank (2007) Monadic prompt lazy assertions in Haskell. In: Shao, Zhong Lecture Notes in Computer Science Vol. 4807, 4807. Springer pp. 38-53. ISBN 3540766367.

    Abstract

    Assertions test expected properties of run-time values without disrupting the normal computation of a program. We present a library for enriching Haskell programs with assertions. Expected properties can be specified in a parser-combinator like language. The assertions are lazy: they do not force evaluation but only examine what is evaluated by the program. They are also prompt: assertion failure is reported as early as possible. The implementation is based on lazy observations and continuation-based coroutines.

    Chitil, Olaf and Luo, Yong (2007) Structure and Properties of Traces for Functional Programs. In: Mackie, Ian ENTCS, 176. Elsevier pp. 39-63.

    Abstract

    The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace can then be viewed in various ways to support program comprehension and debugging. The trace was named the augmented redex trail. Its structure was inspired by standard graph rewriting implementations of functional languages. Here we describe a model of the trace that captures its essential properties and allows formal reasoning. The trace is a graph constructed by graph rewriting but goes beyond simple term graphs. Although the trace is a graph whose structure is independent of any rewriting strategy, we define the trace inductively, thus giving us a powerful method for proving its properties.

    Chitil, Olaf and Huch, Frank (2007) A Pattern Logic for Prompt Lazy Assertions. In: Horváth, Zoltán and Zsok, Viktoria and Butterfield, Andrew Lecture Notes in Computer Science, 4449. Springer, Germany pp. 126-144. ISBN 978-3-540-7412909.

    Abstract

    Assertions test expected properties of run-time values without disrupting the normal computation of a program. Here we present a library for enriching programs in the lazy language Haskell with assertions. Expected properties are written in an expressive pattern logic that combines pattern matching with logical operations and predicates. The presented assertions are lazy: they do not force evaluation but only examine what is evaluated by other parts of the program. They are also prompt: assertion failure is reported as early as possible, before a faulty value is used by the main computation.

    Chitil, Olaf and Huch, Frank (2006) A Pattern Logic for Prompt Lazy Assertions in Haskell. In: Draft Proceedings of the 18th International Symposium on Implementation and Application of Functional Languages, IFL 2006.

    Abstract

    Assertions test expected properties of run-time values without disrupting the normal computation of a program. Here we present a library for enriching programs in the lazy language Haskell with assertions. Expected properties are written in an expressive pattern logic that combines pattern matching with logical operations and predicates. The presented assertions are lazy: they do not force evaluation but only examine what is evaluated by other parts of the program. They are also prompt: assertion failure is reported as early as possible, before a faulty value is used by the main computation.

    Davie, Thomas and Chitil, Olaf (2006) Display of Functional Values for Debugging. In: Draft Proceedings of the 18th International Symposium on Implementation and Application of Functional Languages, IFL 2006, Budapest, Hungary.

    Abstract

    Functional values are used naturally in higher order functional programs, as they are commonly passed around or returned by other function. As such any debugger for these languages must be capable of conveying information about functional values to the user. Current debuggers are limited to displaying the name of the function, or a partial application. In this paper we study two alternative methods of displaying functional values, and their effect on a popular debugging method (Algorithmic Debugging).

    Chitil, Olaf (2006) Promoting Non-Strict Programming. In: Draft Proceedings of the 18th International Symposium on Implementation and Application of Functional Languages, IFL 2006.

    Abstract

    In a non-strict functional programming language functions that yield the same result for all total arguments can still differ for partial arguments, that is, they differ in their strictness. Here a Haskell library is presented that enables the programmer to easily check whether a given function is least-strict; if it is not least-strict, then the tool suggests how to make it less strict.

    Luo, Yong and Chitil, Olaf (2006) Replacing Unevaluated Parts in the Traces of Functional Programs. In: Draft Proceedings of the 18th International Symposium on Implementation and Application of Functional Languages, IFL 2006.

    Abstract

    In functional programming languages such as Haskell, it happens often that some parts of a program are not evaluated because their values are not demanded. In practice, those unevaluated parts are often replaced by a placeholder (e.g. ) in order to keep the trace size smaller. For algorithmic debugging, this also makes the questions shorter and clearer. In this paper, we present a formal model of tracing in which unevaluated parts are replaced by the symbol . Some properties such as the correctness of algorithmic debugging will also be proved.

    Silva, Josep and Chitil, Olaf (2006) Combining Algorithmic Debugging and Program Slicing. In: 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, 10-12 July 2006, Venice, Italy.

    Abstract

    Currently, program slicing and algorithmic debugging are two of the most relevant debugging techniques for declarative languages. They help programmers to find bugs in a semiautomatic manner. On the one hand, program slicing is a technique to extract those program fragments that (potentially) affect the values computed at some point of interest. On the other hand, algorithmic debugging is able to locate a bug by automatically generating a series of questions and processing the programmer's answers. In this work, we show for functional languages how the combination of both techniques produces a more powerful debugging schema that reduces the number of questions that programmers must answer to locate a bug.

    Davie, Thomas and Chitil, Olaf (2006) One Right Does Make a Wrong. In: Pre-Proceedings of the Seventh Symposium on Trends in Functional Programming, TFP 2006. (submitted)

    Abstract

    Algorithmic debugging is a semi-automatic method for locating bugs in programs. An algorithmic debugger asks a user a series of questions about the intended behaviour of the program. Here we present two new methods that reduces the number of questions a user must answer to locate a bug. First, we describe a heuristic based on comparing computations of the same program with different inputs. Besides a computation that exhibits some erroneous behaviour, we use information from computations that produce correct results. The heuristic uses program slices to identify areas of code that are likely to be correct. Secondly, we describe a method of compressing the search tree that guides the questions of an algorithmic debugger. This compression is particularly successful when used in combination with our heuristic. Both heuristic and tree-compression are applicable to algorithmic debugging in general. We have implemented it for locating bugs in Haskell programs.

    Chitil, Olaf and Luo, Yong (2006) Towards a Theory of Tracing for Functional Programs based on Graph Rewriting. In: Mackie, Ian Termgraph

    Abstract

    The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace can then be viewed in various ways to support program comprehension and debugging. Here we describe a model of the trace that captures its essential properties and allows formal reasoning. The trace structure was inspired by standard graph rewriting implementations of functional languages. The trace is a graph which is constructed by graph rewriting but goes beyond simple term graphs.

    Davie, Thomas and Chitil, Olaf (2005) Hat-Delta --- One Right Does Make a Wrong. In: Hat Day 2005: work in progress on the Hat tracing system for Haskell.

    Abstract

    We outline two methods for locating bugs in a program. This is done by comparing computations of the same program with different input. At least one of these computations must produce a correct result, while exactly one must exhibit some erroneous behaviour. Firstly reductions that are thought highly likely to be correct are eliminated from the search for the bug. Secondly, a program slicing technique is used to identify areas of code that are likely to be correct. Both methods have been implemented. In combination with algorithmic debugging they provide a system that quickly and accurately identifies bugs.

    Chitil, Olaf (2005) Hat-Explore: Source-Based Trace Exploration. In: Runciman, Colin Lecture Notes in Computer Science, 3474/2. Springer Berlin / Heidelberg pp. 126-141. ISBN 978-3-540-26094-3.

    Abstract

    Experience shows that users of the Hat viewing tools find it hard to keep orientation and navigate to a point of interest in the trace. Hence this paper describes a new viewing tool where navigation through the trace is based on the program source. The tool combines ideas from algorithmic debugging, traditional stepping debuggers and dynamic program slicing.

    Chitil, Olaf (2005) Pretty Printing with Partial Continuations. In: 17th International Workshop on Implementation and Application of Functional Languages, 19-21 September 2005, Dublin, Ireland.

    Chitil, Olaf (2005) Source-based trace exploration. In: Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004.

    Abstract

    Tracing a computation is a key method for program comprehension and debugging. Hat is a tracing system for Haskell 98 programs. During a computation a trace is recorded in a file; then the user studies the trace with a collection of viewing tools. Different views are complementary and can productively be used together. Experience shows that users of the viewing tools find it hard to keep orientation and navigate to a point of interest in the trace. Hence this paper describes a new viewing tool where navigation through the trace is based on the program source. The tool combines ideas from algorithmic debugging, traditional stepping debuggers and dynamic program slicing.

    Chitil, Olaf and McNeill, Dan and Runciman, Colin (2004) Lazy Assertions. In: Implementation of Functional Languages: 15th International Workshop, IFL 2003, Sep 08-11, 2003, Edinburgh, England.

    Abstract

    Assertions test expected properties of run-time values without disrupting the normal working of a program. So in a lazy functional language assertions should be lazy - not forcing evaluation, but only examining what is evaluated by other parts of the program. We explore the subtle semantics of lazy assertions and describe sequential and concurrent variants of a method for checking lazy assertions. All variants are implemented in Haskell.

    Chitil, Olaf (2004) Source-Based Trace Exploration. In: UNSPECIFIED Lecture Notes in Computer Science. Technical Report 0408, University of Kiel pp. 239-244. ISBN 3-540-26094-3.

    Abstract

    Hat is a programmer's tool for generating a trace of a computation of a Haskell 98 program and viewing such a trace in various different ways. Applications include program comprehension and debugging. The trace viewing tools show expressions and equations of a computation, but they hardly refer to the source program. This disregard of the program is odd, because the computation follows from the program and the usually familiar source program can help orientation in a complex computation. Hence I started the development of new trace viewing tools that are based on showing the source program with various changing markings.

    Brassel, Bernd and Chitil, Olaf and Hanus, Michael et al. (2004) Observing Functional Logic Computations. In: Proc. of the Sixth International Symposium on Practical Aspects of Declarative Languages (PADL'04), JUN 18-19, 2004, Dallas, TX,.

    Abstract

    A lightweight approach to debugging functional logic programs by observations is presented, implemented for the language Curry. The Curry Object Observation System (COOSy) comprises a portable library plus a viewing tool. A programmer can observe data structures and functions by annotating expressions in his program. The possibly partial values of observed expressions that are computed during program execution are recorded in a trace file, including information on non-deterministic choices and logical variables. A separate viewing tool displays the trace content. COOSy covers all aspects of modern functional logic multiparadigm languages such as lazy evaluation, higher order functions, non-deterministic search, logical variables, concurrency and constraints. Both use and implementation of COOSy are described.

    Chitil, Olaf and Runciman, Colin and Wallace, Malcolm (2003) Transforming Haskell for Tracing. In: Ricardo, Peña and Thomas, Arts Lecture Notes in Computer Science. Springer, Berlin pp. 165-181. ISBN 3540401903.

    Abstract

    Hat is a programmer's tool for generating a trace of a computation of a Haskell 98 program and viewing such a trace in various different ways. Applications include program comprehension and debugging. A new version of Hat uses a stand-alone program transformation to produce self-tracing Haskell programs. The transformation is small and works with any Haskell 98 compiler that implements the standard foreign function interface. We present general techniques for building compiler independent tools similar to Hat based on program transformation. We also point out which features of Haskell 98 caused us particular grief.

    Claessen, Koen and Runciman, Colin and Chitil, Olaf et al. (2003) Testing and Tracing Lazy Functional Programs using QuickCheck and Hat. In: 4th Summer School in Advanced Functional Programming.

    Chitil, Olaf (2001) A Semantics for Tracing. In: Draft Proceedings of the 13th International Workshop on Implementation of Functional Languages, IFL 2001.

    Abstract

    We define a small step operational semantics for a core of Haskell. We modify this semantics to generate traces, specifically Augmented Redex Trails. This small and direct definition of Augmented Redex Trails shall improve our understanding of them and shall help to extend them systematically.

    Wallace, Malcolm and Chitil, Olaf and Brehm, Thorsten et al. (2001) Multiple-View Tracing for Haskell: a New Hat. In: Preliminary Proceedings of the 2001 ACM SIGPLAN Haskell Workshop.

    Abstract

    Different tracing systems for Haskell give different views of a program at work. In practice, several views are complementary and can productively be used together. Until now each system has generated its own trace, containing only the information needed for its particular view. Here we present the design of a trace that can serve several views. The trace is generated and written to file as the computation proceeds. We have implemented both the generation of the trace and several different viewers.

    Chitil, Olaf (2001) Compositional Explanation of Types and Algorithmic Debugging of Type Errors. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01).

    Abstract

    The type systems of most typed functional programming languages are based on the Hindley-Milner type system. A practical problem with these type systems is that it is often hard to understand why a program is not type correct or a function does not have the intended type. We suggest that at the core of this problem is the difficulty of explaining why a given expression has a certain type. The type system is not defined compositionally. We propose to explain types using a variant of the Hindley-Milner type system that defines a compositional type explanation graph of principal typings. We describe how the programmer understands types by interactive navigation through the explanation graph. Furthermore, the explanation graph can be the foundation for algorithmic debugging of type errors, that is, semi-automatic localisation of the source of a type error without even having to understand the type inference steps. We implemented a prototype of a tool to explore the usefulness of the proposed methods.

    Chitil, Olaf and Runciman, Colin and Wallace, Malcolm (2001) Freja, Hat and Hood --- A Comparative Evaluation of Three Systems for Tracing and Debugging Lazy Functional Programs. In: Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL 2000), AACHEN, GERMANY.

    Abstract

    In this paper we compare three systems for tracing and debugging Haskell programs: Freja, Hat and Hood. We evaluate their usefulness in practice by applying them to a number of moderately complex programs in which errors had deliberately been introduced. We identify the strengths and weaknesses of each system and then form ideas on how the systems can be improved further.

    Simon, Axel and Chitil, Olaf and Huch, Frank (2000) Typeview: A Tool for Understanding Type Errors. In: Draft Proceedings of the 12th International Workshop on Implementation of Functional Languages.

    Abstract

    In modern statically typed functional languages, type inference is used to determine the type of each function automatically. Whenever this fails, the compiler emits an error message that is often very complex. Sometimes the expression mentioned in the type error message is not the one that is wrong. We therefore implement an interactive tool that allows programmers to browse through the source code of their program and query the types of each expression. If a variable cannot be typed, we would like to present a set of possible types from which the user can decide which is wrong. This should help finding the origin of type errors without detailed knowledge of type inference on the user side.

    Chitil, Olaf and Runciman, Colin and Wallace, Malcolm (2000) Tracing and Debugging of Lazy Functional Programs - A Comparative Evaluation of Three Systems. In: Draft Proceedings of the 12th International Workshop on Implementation of Functional Languages.

    Abstract

    In this paper we compare three systems for tracing and debugging Haskell programs: Freja, the Redex Trail System and Hood. We identify the similarities and differences of these systems and we evaluate their usefulness in practice by applying them to a number of small to medium programs in which errors had deliberately been introduced.

    Chitil, Olaf (2000) Deforestation of Functional Programs through Type Inference. In: 17 Workshops der GI-Fachgruppe 2.1.4. Programmiersprachen und Rechenkonzepte mit Schwerpunkt Softwarecomponenten.

    Abstract

    Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. Short cut deforestation is a deforestation method which is based on a single, local transformation rule. In return, short cut deforestation expects both producer and consumer of the intermediate structure in a certain form. Starting from the fact that short cut deforestation is based on a parametricity theorem of the second-order typed lambda-calculus, we show how the required form of a list producer can be derived through the use of type inference. Type inference can also indicates which function definitions need to be inlined. Because only limited inlining across module boundaries is practically feasible, we develop a scheme for splitting a function definition into a worker definition and a wrapper definition. For deforestation we only need to inline the small wrapper definition.

    Chitil, Olaf (1999) Type Inference Builds a Short Cut to Deforestation. In: Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP '99), September 27 - September 29, 1999, Paris, France.

    Abstract

    Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. Short cut deforestation is a deforestation method which is based on a single, local transformation rule. In return, short cut deforestation expects both producer and consumer of the intermediate structure in a certain form. Warm fusion was proposed to automatically transform functions into this form. Unfortunately, it is costly and hard to implement. Starting from the fact that short cut deforestation is based on a parametricity theorem of the second-order typed lambda-calculus, we show how the required form of a list producer can be derived through the use of type inference. Typability for the second-order typed lambda-calculus is undecidable. However, we present a linear-time algorithm that solves a partial type inference problem and that, together with controlled inlining and polymorphic type instantiation, suffices for deforestation. The resulting new short cut deforestation algorithm is efficient and removes more intermediate lists than the original.

    Chitil, Olaf (1999) Denotational Semantics for Teaching Lazy Functional Programming. In: Proceedings of the Workshop on Functional and Declarative Programming in Education, 29 September 1999, Paris, France.

    Chitil, Olaf (1999) Type-Inference Based Short Cut Deforestation (nearly) without Inlining. In: 11th International Workshop on Implementation of Functional Languages, September 7th-10th 1999, Lochem, Netherlands.

    Abstract

    Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. In [ICFP'99] we presented a type-inference based deforestation algorithm which performs extensive inlining. However, across module boundaries only limited inlining is practically feasible. Furthermore, inlining is a non-trivial transformation which is therefore best implemented as a separate optimisation pass. To perform short cut deforestation (nearly) without inlining, Gill suggested to split definitions into workers and wrappers and inline only the small wrappers, which transfer the information needed for deforestation. We show that Gill's use of a function build limits deforestation and note that his reasons for using build do not apply to our approach. Hence we develop a more general worker/wrapper scheme without build. We give a type-inference based algorithm which splits definitions into workers and wrappers. Finally, we show that we can deforest more expressions with the worker/wrapper scheme than the algorithm with inlining.

    Chitil, Olaf (1997) Common Subexpression Elimination in a Lazy Functional Language. In: Draft Proceedings of the 9th International Workshop on Implementation of Functional Languages.

    Abstract

    Common subexpression elimination is a well-known compiler optimisation that saves time by avoiding the repetition of the same computation. To our knowledge it has not yet been applied to lazy functional programming languages, although there are several advantages. First, the referential transparency of these languages makes the identification of common subexpressions very simple. Second, more common subexpressions can be recognised because they can be of arbitrary type whereas standard common subexpression elimination only shares primitive values. However, because lazy functional languages decouple program structure from data space allocation and control flow, analysing its effects and deciding under which conditions the elimination of a common subexpression is beneficial proves to be quite difficult. We developed and implemented the transformation for the language Haskell by extending the Glasgow Haskell compiler and measured its effectiveness on real-world programs.

Monographs

    Abstract

    In a non-strict functional programming language functions that yield the same result for all total arguments can still differ for partial arguments, that is, they differ in their strictness. Here a tool for Haskell is presented that enables the programmer to easily check whether a given function is least-strict; if it is not least-strict, then the tool suggests how to make it less strict.

    Luo, Yong and Chitil, Olaf (2007) Algorithmic Debugging with Cyclic Traces of Lazy Functional Programs. technical_report. Computing Laboratory, University of Kent, Canterbury, Kent

    Abstract

    We have proved the correctness of algorithmic debugging if the traces are acyclic. For cyclic traces, however, does algorithmic debugging still work? There does not exist a common understanding of how to debug cyclic traces in functional programming communities for a long time. In this paper we give two small examples to demonstrate that it is extremely difficult to find a generic algorithmic debugging scheme for cyclic traces. We conjecturre that it is impossible to have a generic scheme for cyclic traces, because the examples are very small and the choices of reasonable debugging trees are very limited. We also present acyclic traces in which constants are shared unless shared constants result in a cycle. The normal algorithmic debugging scheme works fine for acyclic traces and the proof is very similar to our previous paper.

    Luo, Yong and Chitil, Olaf (2007) Algorithmic Debugging for Locally Defined Functions. technical_report. University of Kent, Canterbury, Canterbury

    Abstract

    The purpose of the document is to prove the correctness of Algorithmic Debugging where the traces for local functions are generated in a new way. The processes of generating computation graphs follow exactly what we might do by hand. Therefore, we can be confident that the graphs are correct.We do not need to justify the graphs by comparing ?-lifted programs.

    Luo, Yong and Chitil, Olaf (2007) Algorithmic debugging and trusted functions. technical_report. Computing Laboratory, University of Kent, Canterbury, Kent

    Abstract

    As the name states, trusted functions do not have bugs. It is up to user to specify which function is trusted. Commonly used functions in standard library are normally trusted. In the process of algorithmic debugging, we search for faulty nodes to locate bugs. Since a trusted function cannot be a faulty node, there is no point to keep trusted func- tions in Evaluation Dependency Trees (EDT) for algorithmic debugging. In this report, we create smaller tree structures by removing trusted func- tions. There are two different ways to achieve this: generating a smaller tree structure directly from the original trace; or creating a smaller trace first and then from which generating a smaller tree structure.

    Luo, Yong and Chitil, Olaf (2007) Replacing unevaluated parts in the traces of functional programs. technical_report. University of Kent, Canterbury, Kent, Canterbury, Kent

    Abstract

    In non-strict functional programming languages such as Haskell, it happens often that some parts of a program are not evaluated because their values are not demanded. In practice, those unevaluated parts are often replaced by a placeholder (e.g. ) in order to keep the trace size smaller. In the process of algorithmic debugging, one needs to answer several questions in order to locate a program fault. Replacing unevaluated parts makes these questions shorter and semantically clearer. In this paper, we present a formal model of tracing in which unevaluated parts are replaced by the symbol . The most important property, the correctness of algorithmic debugging, is proved.

    Chitil, Olaf (2006) Pretty Printing with Delimited Continuations Report 4-06. technical_report. University of Kent

    Abstract

    Pretty printing is the task of nicely formatting tree structured data within a given line width limit. In 1980 Oppen published a pretty printing algorithm that takes time linear in the size of the input, independent of the line width, and uses only limited look-ahead. This work inspired the development of a number of purely functional pretty printing libraries in Haskell. Here I present a new functional pretty printing algorithm that has all the nice properties of Oppen's and is surprisingly simple. A double-ended queue of delimited continuations is the key to addressing all aspects of the problem explicitly.

    Chitil, Olaf (1997) Adding an Optimisation Pass to the Glasgow Haskell Compiler. other. University of Kent at Canterbury (unpublished)

    Abstract

    The Glasgow Haskell compiler (GHC) with its over 40.000 lines of code is quite daunting for a newcomer. Here we give a short practical introduction based on our experiences in how to add an optimisation pass to GHC. Thus we hope to encourage other developers of optimisations to implement them in GHC. These notes are meant to be extended and updated from time to time. Hence observe the date shown below. Unpublished, November 4, 1997, 16 pages.

    Abstract

    A comprehensive semantics for functional programs is presented, which generalizes the well-known call-by-value and call-by-name semantics. By permitting a separate choice between call-by value and call-by-name for every argument position of every function and parameterizing the semantics by this choice we abstract from the parameter-passing mechanism. Thus common and distinguishing features of all instances of the sigma-semantics, especially call-by-value and call-by-name semantics, are highlighted. Furthermore, a property can be validated for all instances of the sigma-semantics by a single proof. This is employed for proving the equivalence of the given denotational (fixed-point based) and two operational (reduction based) definitions of the sigma-semantics. We present and apply means for very simple proofs of equivalence with the denotational sigma-semantics for a large class of reduction-based sigma-semantics. Our basis are simple first-order constructor-based functional programs with patterns.

Theses

    Chitil, Olaf (2000) Type-Inference Based Deforestation of Functional Programs. phd thesis, RWTH Aachen.

    Abstract

    In lazy functional programming modularity is often achieved by using intermediate data structures to combine separate parts of a program. Each intermediate data structure is produced by one part and consumed by another one. Deforestation optimises a functional program by transformation into a program which does not produce such intermediate data structures. In this thesis we present a new method for deforestation, which combines a known method,short cut deforestation, with a new analysis that is based on type inference. Short cut deforestation eliminates an intermediate list by a single, local transformation. In return, short cut deforestation expects both producer and consumer of the intermediate list in a certain form. Whereas the required form of the consumer is generally considered desirable in a well-structured program anyway, the required form of the producer is only a crutch to enable deforestation. Hence only the list-producing functions of the standard libraries were defined in the desired form and short cut deforestation has been confined to compositions of these functions. Here, we present an algorithm which transforms an arbitrary producer into the required form. Starting from the observation that short cut deforestation is based on a parametricity theorem of the second-order typed lambda-calculus, we show how the construction of the required form can be reduced to a type inference problem. Typability for the second-order typed lambda-calculus is undecidable, but we only need to solve a partial type inference problem. For this problem we develop an algorithm based on the well-known Hindley-Milner type inference algorithm. The transformation of a producer often requires inlining of some function definitions. Type inference even indicates which function definitions need to be inlined. However, only limited inlining across module boundaries is practically feasible. Therefore, we extend the previously developed algorithm to split a function definition into a worker definition and a wrapper definition. We only need to inline the small wrapper definition, which transfers all information required for deforestation. The flexibility of type inference allows us to remove intermediate lists which original short cut deforestation cannot remove, even with hand-crafted producers. In contrast to most previous work on deforestation, we give a detailed proof of completeness and semantic correctness of our transformation.

Total publications in KAR: 49 [See all in KAR]

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 23/10/2014