We introduce the notion of compositional references into the Framework of monadic functionalprogramming and propose a set of new primitives based on this notion. They enable us to use a wide range of mutable data str...
详细信息
ISBN:
(纸本)9780897919180
We introduce the notion of compositional references into the Framework of monadic functionalprogramming and propose a set of new primitives based on this notion. They enable us to use a wide range of mutable data structures. There, references may be passed around explicitly, or mutable data structures such as arrays and tuples may be passed implicitly as hidden state. The former style is called the explicit style and is usually more expressive, while the latter is called the implicit style and has simpler semantics. We investigate the relation between the two styles and discus implementation issues.
By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program...
详细信息
ISBN:
(纸本)9781581137569
By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs. However, meta-programming, especially in an untyped setting, is notoriously error-prone. In this paper, we aim at making meta-programming less error-prone by providing a type system to facilitate the construction of correct meta-programs. We first introduce some code constructors for constructing typeful code representation in which program variables are replaced with deBruijn indices, and then formally demonstrate how such typeful code representation can be used to support meta-programming. The main contribution of the paper lies in recognition and then formalization of a novel approach to typed meta-programming that is practical, general and flexible.
In this talk, I will consider some possible extensions to existing functionalprogramming languages that would make them more suitable for the important and growing class of artificial intelligence applications. First...
详细信息
ISBN:
(纸本)9781595938152
In this talk, I will consider some possible extensions to existing functionalprogramming languages that would make them more suitable for the important and growing class of artificial intelligence applications. First, I will motivate the need for these language extensions. Then I will give some technical detail about these extensions that provide the logic programming idioms, probabilistic computation, and modal computation. Some examples will be given to illustrate these ideas which have been implemented in the Bach programming language that is an extension of Haskell.
Bluespec is a hardware-design tools startup whose core technology is developed using Haskell. Haskell is an unusual choice for a startup because it adds technical risk to the inherent business risk. In the years since...
详细信息
ISBN:
(纸本)9781595939197
Bluespec is a hardware-design tools startup whose core technology is developed using Haskell. Haskell is an unusual choice for a startup because it adds technical risk to the inherent business risk. In the years since Bluespec's founding, we have discovered that Haskell's purity is an unexpected match for the development needs of a startup. Based on Bluespec's experience, we conclude that pure programming languages can be the source of a competitive advantage for startup software companies.
To improve the quality of type error messages in functionalprogramming languages, we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form ...
详细信息
ISBN:
(纸本)9781581137569
To improve the quality of type error messages in functionalprogramming languages, we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form of externally supplied type inference directives, precluding the need to make any changes to the compiler. A second advantage is that the directives are automatically checked for soundness with respect to the underlying type system. We show how the techniques can be used to improve the type error messages reported for a combinator library. More specifically, how they can help to generate error messages which are conceptually closer to the domain for which the library was developed. The techniques have all been incorporated in the Helium compiler, which implements a large subset of Haskell.
In dependently typed languages run-time values can appear in types, making it possible to give programs more precise types than in languages without dependent types. This can range from keeping track of simple invaria...
详细信息
ISBN:
(纸本)9781450323260
In dependently typed languages run-time values can appear in types, making it possible to give programs more precise types than in languages without dependent types. This can range from keeping track of simple invariants like the length of a list, to full functional correctness. In addition to having some correctness guarantees on the final program, assigning more precise types to programs means that you can get more assistance from the type checker while writing them. This is what I focus on here, demonstrating how the programming environment of AGDA can help you when developing dependently typed 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.
A three-year study collected information bearing on the question of whether studying mathematics improves programming skills. An analysis of the data revealed significant differences in the programming effectiveness o...
详细信息
ISBN:
(纸本)9781581137569
A three-year study collected information bearing on the question of whether studying mathematics improves programming skills. An analysis of the data revealed significant differences in the programming effectiveness of two populations of students: (1) those who studied discrete mathematics through examples focused on reasoning about software and (2) those who studied the same mathematical topics illustrated with more traditional examples. functionalprogramming played a central role in the study because it provides a straightforward framework for the presentation of concepts such as predicate logic and proof by induction. Such topics can be covered in depth, staying almost entirely within the context of reasoning about software. The intricate complexities in logic that mutable variables carry with them need not arise, early on, to confuse novices struggling to understand new ideas. In addition, because functional languages provide useful and compact ways to express mathematical concepts, and because the choice of notation in mathematics courses is often at the discretion of the instructor (in contrast to the notational restrictions often fiercely guarded by the faculty in programming courses), discrete mathematics courses, as they are found in most computer science programs, provide an easy opportunity to enhance the education of students by exposing them to functionalprogramming concepts.
Pattern abstractions increase the expressiveness of pattern matching, enabling the programmer to describe a broader class of regular forests with patterns. Furthermore, pattern abstractions support code reuse and code...
详细信息
ISBN:
(纸本)9780897919180
Pattern abstractions increase the expressiveness of pattern matching, enabling the programmer to describe a broader class of regular forests with patterns. Furthermore, pattern abstractions support code reuse and code factoring, features that facilitate maintenance and evolution of code. Past research on pattern abstractions has generally ignored the aspect of compile-time checks for exhaustiveness and redundancy. In this paper we propose a class of expressive patterns that admits these compile-time checks.
functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are se...
详细信息
ISBN:
(纸本)9781605583327
functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functionalprogramming, because the existing features for non-strictness, sharing, and non-determinism in functional languages are tricky to combine. We present a practical way to write purely functional lazy non-deterministic programs that are efficient and perspicuous. We achieve this goal by embedding the programs into existing languages (such as Haskell, SML, and OCaml) with high-quality implementations, by making choices lazily and representing data with non-deterministic components, by working with custom monadic data types and search strategies, and by providing equational laws for the programmer to reason about their code.
暂无评论