5,378 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
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
Realising nondeterministic I/O in the Glasgow Haskell Compiler
No full textIn this paper we demonstrate how to relate the semantics given by the nondeterministic call-by-need calculus FUNDIO [SS03] to Haskell. After introducing new correct program transformations for FUNDIO, we translate the core language used in the Glasgow Haskell Compiler into the FUNDIO language, where the IO construct of FUNDIO corresponds to direct-call IO-actions in Haskell. We sketch the investigations of [Sab03b] where a lot of program transformations performed by the compiler have been shown to be correct w.r.t. the FUNDIO semantics. This enabled us to achieve a FUNDIO-compatible Haskell-compiler, by turning o not yet investigated transformations and the small set of incompatible transformations. With this compiler, Haskell programs which use the extension unsafePerformIO in arbitrary contexts, can be compiled in a "safe" manner
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
Automatically Generating CSP Models for Communicating Haskell Processes
No full textTools such as FDR can check whether a CSP model of an implementation is a refinement of a given CSP specification. We present a technique for generating such CSP models of Haskell implementations that use the Communicating Haskell Processes library. Our technique avoids the need for a detailed semantics of
the Haskell language, and requires only minimal program annotation. The generated CSP-M model can be checked for deadlock or refinements by FDR, allowing easy use of formal methods without the need to maintain a model of the program implementation alongside the program itself
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
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)
- …
