programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-construction software. However, this extreme...
详细信息
ISBN:
(纸本)9781450310543
programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a datatype is the combination of a structuring medium together with a special purpose logic. these domain-specific logics hamper any effort of code reuse among similarly structured data. In this paper, we exorcise our datatypes by adapting the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. Withthis knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: the user can ask the definition of addition to be lifted to lists and she will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in a type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.
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.
A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. One way to redu...
详细信息
ISBN:
(纸本)9781450336697
A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. One way to reduce the development and maintenance effort of bidirectional transformations is to have specialized languages in which the resulting programs are bidirectional by construction-giving rise to the paradigm of bidirectional programming. In this paper, we develop a framework for applicative-style and higher-order bidirectional programming, in which we can write bidirectional transformations as unidirectional programs in standard functional languages, opening up access to the bundle of language features previously only available to conventional unidirectional languages. Our framework essentially bridges two very different approaches of bidirectional programming, namely the lens framework and Voigtlander's semantic bidirectionalization, creating a new programming style that is able to bag benefits from both.
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.
Reactis is a commercially successful testing and validation tool which is implemented almost entirely in Standard ML. Our experience using a functional language to develop a commercial product has led us to the conclu...
详细信息
ISBN:
(纸本)9781595938152
Reactis is a commercially successful testing and validation tool which is implemented almost entirely in Standard ML. Our experience using a functional language to develop a commercial product has led us to the conclusion that while functional languages have some disadvantages, in the case of Reactis the benefits of a functional language substantially outweigh the drawbacks.
We report on our experience using functionalprogramming languages in the development of a commercial GNU/Linux distribution, discussing features of several significant systems: hardware detection and system configura...
详细信息
functional Reactive programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such a...
详细信息
ISBN:
(纸本)9781450351829
functional Reactive programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and limiting the exploration of the past. In this paper we show how these constraints can be overcome, giving local control over the time domain, the direction of time and the sampling step. We study the behaviour of FRP expressions when time flows backwards, and demonstrate how to synchronize subsystems running asynchronously and at different sampling rates. We have verified the practicality of our approach with two non-trivial games in which time control is central to the gameplay.
functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource...
详细信息
ISBN:
(纸本)9781450323260
functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style. In this paper, we give a new language for higher-order reactive programming. Our language generalizes and simplifies prior type systems for reactive programming, by supporting the use of streams of streams, first-class functions, and higher-order operations. We also support many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with first-class schedulers. Furthermore, our language supports an efficient implementation strategy permitting us to eagerly deallocate old values and statically rule out spacetime leaks, a notorious source of inefficiency in reactive programs. Furthermore, these memory guarantees are achieved without the use of a complex substructural type discipline. We also show that our implementation strategy of eager deallocation is safe, by showing the soundness of our type system with a novel step-indexed Kripke logical relation.
the 17thacmsigplaninternationalconference on functionalprogramming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding pa...
详细信息
the 17thacmsigplaninternationalconference on functionalprogramming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding papers and invited their authors to submit to this special issue of Journal of functionalprogramming. Robby Findler and Satnam Singh acted as editors for these submissions. this issue includes the accepted papers, each of which provides substantial new material beyond the original conference version. [ABSTRACT FROM AUthOR]
暂无评论