127,335 research outputs found
Communicating Haskell Processes
No full textConcurrent programming supports multiple threads of concurrent execution. It
is a suitable paradigm for interaction with the outside world, where many inputs
(e.g. network packets, key-presses, mouse-clicks) may arrive at any time and need
to be dealt with at the same time. Concurrent execution also potentially allows
for parallel speed-up; multicore machines are now the standard for new PCs, but
the quest to take full advantage of the available parallelism continues.
One approach to concurrent programming is process-oriented programming,
which uses message-passing and is based on Hoare and Roscoe's Communicating
Sequential Processes (CSP). CSP is a process calculus centred on concurrent processes that communicate with each other via synchronous channels. This is used
as a formal underpinning for process-oriented programming, either directly (proving behaviours of programs with a CSP model checker) or indirectly (providing
sound design principles and patterns).
Process-oriented programming has previously been provided in programming
languages such as occam-? and libraries for other mainstream languages such as
Java and C++. However, as yet process-oriented programming has failed to gain
much traction via these implementations; occam-? is rooted in the much older
language occam and thus lacks powerful data structures (among other features)
which are standard in most modern languages { while languages such as Java
and C++, where data is mutable and easily shared, can be an awkward fit to
process-oriented programming.
Haskell is a functional programming language that is notable for its purity,
type-classes, monads and lazy evaluation: modern features that provide interest-
ing and powerful ways to program, including good support for imperative pro-
gramming. Like other functional languages, it eliminates mutable data -- which
immediately removes a whole class of problems in concurrent programming.
This thesis contends that CSP and process-oriented programming ?t well with
Haskell. The thesis details the creation of a CSP library for Haskell (Commu-
nicating Haskell Processes: CHP) { which features powerful support for process
composition { and its further augmentation with capabilities such as support for
a new concurrency primitive (conjunction), tracing and the ability to generate
formal models of CHP programs. This allows programmers to build concurrent
message-passing systems with a strong formal underpinning in a modern program-
ming language, with more features and less complications than process-oriented
libraries for other languages
Formalisation of Haskell Refactorings
No full textRefactoring is a well-known technique for improving the design of existing programs without changing their external behaviour. HaRe is the refactoring tool we have built to support refactoring Haskell programs. Along with the development of HaRe, This formalisation process helps to clarify the meaning of refactorings, improves our confidence in the behaviour-preservation of refactorings, and reduces the need for testing. This paper gives an overview of HaRe, and shows our approach to the formalisation of refactorings
Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack
No full textExisting algorithmic debuggers for Haskell require a transformation of all modules in a program, even libraries that the user does not want to debug and which may use language features not supported by the debugger. This is a pity, because a promising ap- proach to debugging is therefore not applicable to many real-world programs. We use the cost centre stack from the Glasgow Haskell Compiler profiling environment together with runtime value observations as provided by the Haskell Object Observation Debugger (HOOD) to collect enough information for algorithmic debugging. Program annotations are in suspected modules only. With this technique algorithmic debugging is applicable to a much larger set of Haskell programs. This demonstrates that for functional languages in general a simple stack trace extension is useful to support tasks such as profiling and debugging
Software Metrics: Measuring Haskell
No full textSoftware metrics have been used in software engineering as a mechanism for assessing code quality and for targeting software development activities, such as testing or refactoring, at areas of a program that will most benefit from them. Haskell has many tools for software engineering, such as testing, debugging and refactoring tools, but software metrics have mostly been neglected. The work presented in this paper identifies a collection of software metrics for use with Haskell programs. These metrics are subjected to statistical analysis to assess the correlation between their values and the number of bug fixing changes occurring during the development lifetime of two case study programs. In addition to this, the relationships between the metric values is also explored, showing how combinations of metrics can be used to improve the accuracy of the measurements
Communicating Haskell Processes: Composable Explicit Concurrency Using Monads
No full textWriting concurrent programs in languages that lack explicit support for concurrency can often be awkward and difficult. Haskell's monads provide a way to explicitly specify sequence and effects in a functional language, and monadic combinators allow composition of monadic actions, for example via parallelism and choice two core aspects of Communicating Sequential Processes (CSP). We show how the use of these combinators, and being able to express processes as first-class types (monadic actions) allow for easy and elegant programming of process-oriented concurrency in a new CSP library for Haskell: Communicating Haskell Processes
A contextual semantics for concurrent Haskell with futures
No full textIn this paper we analyze the semantics of a higher-order functional language with concurrent threads, monadic IO and synchronizing variables as in Concurrent Haskell. To assure declarativeness of concurrent programming we extend the language by implicit, monadic, and concurrent futures. As semantic model we introduce and analyze the process calculus CHF, which represents a typed core language of Concurrent Haskell extended by concurrent futures. Evaluation in CHF is defined by a small-step reduction relation. Using contextual equivalence based on may- and should-convergence as program equivalence, we show that various transformations preserve program equivalence. We establish a context lemma easing those correctness proofs. An important result is that call-by-need and call-by-name evaluation are equivalent in CHF, since they induce the same program equivalence. Finally we show that the monad laws hold in CHF under mild restrictions on Haskell’s seq-operator, which for instance justifies the use of the do-notation
Feat: Functional Enumeration of Algebraic Types
No full textIn mathematics, an enumeration of a set S is a bijective function from (an initial segment of) the natural numbers to S. We define "functional enumerations" as efficiently computable such bijections. This paper describes a theory of functional enumeration and provides an algebra of enumerations closed under sums, products, guarded recursion and bijections. We partition each enumerated set into numbered, finite subsets.
We provide a generic enumeration such that the number of each part corresponds to the size of its values (measured in the number of constructors). We implement our ideas in a Haskell library called testing-feat, and make the source code freely available. Feat provides efficient "random access" to enumerated values. The primary application is property-based testing, where it is used to define both random sampling (for example QuickCheck generators) and exhaustive enumeration (in the style of SmallCheck). We claim that functional enumeration is the best option for automatically generating test cases from large groups of mutually recursive syntax tree types. As a case study we use Feat to test the pretty-printer of the Template Haskell library (uncovering several bugs)
Multiple-View Tracing for Haskell: a New Hat
No full textDifferent 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
A Pattern Logic for Prompt Lazy Assertions in Haskell
No full textAssertions 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
A principled approach to programming with nested types in Haskell
No full textInitial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell
- …
