One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exception...
详细信息
ISBN:
(纸本)9781450323260
One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions withthe outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations - it provides monads for capturing state, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects. Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. the system is based on the portable Gambit Scheme programming language and provides a ...
详细信息
ISBN:
(纸本)9781450323260
A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. the system is based on the portable Gambit Scheme programming language and provides a flexible cross-platform environment for developing graphical applications on mobile devices as well as medical instrumentation interfaces running on embedded platforms. Real world applications of this framework for mobile diagnostics, telemonitoring and automated drug infusions are reported. the source code for the core framework is open source and available at: https://***/part-cw/lambdanative.
Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflowexecution must answer the following question: How can parallelism between two dependent n...
详细信息
ISBN:
(纸本)9781450368131
Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflowexecution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? this is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higher-order function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a state-of-the-art approach using monad-par and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves short-comings of the stream-based programming model for current state-of-theart big data processing systems.
the evolution of Web sites towards very dynamic applications makes it necessary to reconsider current Web programming technologies. We believe that Web development would benefit greatly from more abstract paradigms an...
详细信息
ISBN:
(纸本)9781605583327
the evolution of Web sites towards very dynamic applications makes it necessary to reconsider current Web programming technologies. We believe that Web development would benefit greatly from more abstract paradigms and that a more semantical approach would result in huge gains in expressiveness. In particular, functionalprogramming provides a really elegant solution to some important Web interaction problems, but few frameworks take advantage of it. the Ocsigen project is an attempt to provide global solutions to these needs. We present our experience in designing this general framework for Web programming, written in Objective Caml. It provides a fully featured Web server and a framework for programming Web applications, withthe aim of improving expressiveness and safety. this is done by taking advantage of functionalprogramming and static typing as much as possible.
I describe the initial attempt of experienced business software developers with minimal functionalprogramming background to write a non-trivial, business-critical application entirely in Haskell. Sonic parts of the a...
详细信息
ISBN:
(纸本)9781605583327
I describe the initial attempt of experienced business software developers with minimal functionalprogramming background to write a non-trivial, business-critical application entirely in Haskell. Sonic parts of the application domain are well suited to a mathematically-oriented language;others are more typically done in languages such as C++. I discuss the advantages and difficulties of Haskell in these circumstances, with a particular focus on issues that commercial developers find important but that may receive less attention from the academic community. I conclude that, while academic implementations of "advanced" programming languages arguably may lag somewhat behind implementations of commercial languages in certain ways important to businesses, this appears relatively easy to fix, and that the other advantages that they offer make them a good, albeit long-term, investment for companies where effective IT implementation can offer a crucial advantage to success.
the adoption of Domain-Specific Languages (DSLs) relies on the capacity of language workbenches to automate the development of advanced and customized environments. While DSLs are usually well tailored for the main sc...
详细信息
ISBN:
(纸本)9781450369817
the adoption of Domain-Specific Languages (DSLs) relies on the capacity of language workbenches to automate the development of advanced and customized environments. While DSLs are usually well tailored for the main scenarios, the cost of developing mature tools prevents the ability to develop additional capabilities for alternative scenarios targeting specific tasks (e.g., API testing) or stakeholders (e.g., education). In this paper, we propose an approach to automatically generate interactive computer programming environments from existing specifications of textual interpreted DSLs. the approach provides abstractions to complement the DSL specification, and combines static analysis and language transformations to automate the transformation of the language syntax, the execution state and the execution semantics. We evaluate the approach over a representative set of DSLs, and demonstrate the ability to automatically transform a textual syntax to load partial programs limited to a single statement, and to derive a Read-Eval-Print-Loop (REPL) from the specification of a language interpreter.
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper desc...
详细信息
ISBN:
(纸本)9781595930644
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper describes the design and implementation issues of those AOP mechanisms that give us insights into the interaction between AOP features and common features in strongly-typed functional languages such as type inference, polymorphic types and curried functions. We implemented a prototype compiler of the language and used the language for separating crosscutting concerns in application programs, including for separating descriptions of a type system from compiler descriptions.
Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tac...
详细信息
ISBN:
(纸本)9781450323260
Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers. We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulatio...
详细信息
ISBN:
(纸本)9781605587943
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive. In this paper, we present a novel approach to the problem. Our proposal can be viewed either as a programming language design or as a library: in fact, it is currently implemented within Agda. It provides a safe and expressive means of programming with names and binders. It is abstract enough to support multiple concrete implementations: we present one in nominal style and one in de Bruijn style. We use logical relations to prove that "well-typed programs do not mix names with different scope". We exhibit an adequate encoding of Pitts-style nominal terms into our system.
Analyzing software product lines is difficult, due to their inherent variability. In the past, several strategies for product-line analysis have been proposed, in particular, product-based, feature-based, and family-b...
详细信息
ISBN:
(纸本)9781450323734
Analyzing software product lines is difficult, due to their inherent variability. In the past, several strategies for product-line analysis have been proposed, in particular, product-based, feature-based, and family-based strategies. Despite recent attempts to conceptually and empirically compare different strategies, there is no work that empirically compares all of the three strategies in a controlled setting. We close this gap by extending a compiler for feature-oriented programming with support for product-based, feature-based, and family-based type checking. We present and discuss the results of a comparative performance evaluation that we conducted on a set of 12 feature-oriented, JAVA-based product lines. Most notably, we found that the family-based strategy is superior for all subject product lines: it is substantially faster, it detects all kinds of errors, and provides the most detailed information about them.
暂无评论