We present a user-friendly approach to unifying program creation and execution, based on a notion of "tangible values" (TVs), which are visual and interactive manifestations of pure values, including functio...
详细信息
ISBN:
(纸本)9781595938152
We present a user-friendly approach to unifying program creation and execution, based on a notion of "tangible values" (TVs), which are visual and interactive manifestations of pure values, including functions. programming happens by gestural composition of TVs. Our goal is to give end-users the ability to create parameterized, composable content without imposing the usual abstract and linguistic working style of programmers. We hope that such a system will put the essence of programming into the hands of many more people, and in particular people with artistic/visual creative style. In realizing this vision, we develop algebras for visual presentation and for "deep" function application, where function and argument may both be nested within a structure of tuples, functions, etc. Composition gestures are translated into chains of combinators that act simultaneously on statically typed values and their visualizations.
the bondi programming language is multi-polymorphic, in that it supports four polymorphic programming styles within a small core of computation, namely a typed pattern calculus. bondi's expressive power is illustr...
详细信息
Staging allows a programmer to write domain-specific, custom code generators. Ideally, a programming language for staging provides all necessary features for staging, and at the same time, gives static guarantee for t...
详细信息
ISBN:
(纸本)9781450355247
Staging allows a programmer to write domain-specific, custom code generators. Ideally, a programming language for staging provides all necessary features for staging, and at the same time, gives static guarantee for the safety properties of generated code including well typedness and well scopedness. We address this classic problem for the language with control operators, which allow code optimizations in a modular and compact way. Specifically, we design a staged programming language withthe expressive control operators shift0 and reset0, which let us express, for instance, multi-layer let-insertion, while keeping the static guarantee of well typedness and well scopedness. For this purpose, we extend our earlier work on refined environment classifiers which were introduced for the staging language with state. We show that our language is expressive enough to write interesting code generation techniques, and that it enjoys type soundness. We also mention a type inference algorithm for our language under reasonable restriction.
Total functionalprogramming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to term...
详细信息
ISBN:
(纸本)9781450323260
Total functionalprogramming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e. g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. the theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees. Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming. Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano's guarded recursion. Clock variables allow us to "close over" the generation of infinite codata, and to make finite observations, something that is not possible with guarded recursion alone.
Current languages for safely manipulating values with names only support term languages with simple binding syntax. As a result, no tools exist to safely manipulate code written in those languages for which name probl...
详细信息
ISBN:
(纸本)9781450328739
Current languages for safely manipulating values with names only support term languages with simple binding syntax. As a result, no tools exist to safely manipulate code written in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects alpha-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's lambda(m), but is a full-fledged binding-safe language like Pure FreshML.
We present a series of CPS-based intermediate languages suitable for functional language compilation, arguing that they have practical benefits over direct-style languages based on A-normal form (ANF) or monads. Inlin...
详细信息
ISBN:
(纸本)9781595938152
We present a series of CPS-based intermediate languages suitable for functional language compilation, arguing that they have practical benefits over direct-style languages based on A-normal form (ANF) or monads. Inlining of functions demonstrates the benefits most clearly: in ANF-based languages, inlining involves a re-normalization step that rearranges let expressions and possibly introduces a new 'join point' function, and in monadic languages, commuting conversions must be applied;in contrast, inlining in our CPS language is a simple substitution of variables for variables. We present a contification transformation implemented by simple rewrites on the intermediate language. Exceptions are modelled using so-called 'double-barrelled' CPS. Subtyping on exception constructors then gives a very straightforward effect analysis for exceptions. We also show how a graph-based representation of CPS terms can be implemented extremely efficiently, with linear-time term simplification.
the fast-and-loose, permissive semantics of dynamic programming languages limit the power of static analyses. For that reason, soundness is often traded for precision through dynamic program analysis. Dynamic analysis...
详细信息
ISBN:
(纸本)9781450399197
the fast-and-loose, permissive semantics of dynamic programming languages limit the power of static analyses. For that reason, soundness is often traded for precision through dynamic program analysis. Dynamic analysis is only as good as the available runnable code, and relying solely on test suites is fraught as they do not cover the full gamut of possible behaviors. Fuzzing is an approach for automatically exercising code, and could be used to obtain more runnable code. However, the shape of user-defined data in dynamic languages is difficult to intuit, limiting a fuzzer's reach. We propose a feedback-driven blackbox fuzzing approach which draws inputs from a database of values recorded from existing code. We implement this approach in a tool called signatr for the R language. We present the insights of its design and implementation, and assess signatr's ability to uncover new behaviors by fuzzing 4,829 R functions from 100 R packages, revealing 1,195,184 new signatures.
FranTk is a new high level library for programming Graphical User Interfaces (GUIs) in Haskell. It is based on Fran (functional Reactive Animation), and uses the notions of Behaviors and Events to structure code. Beha...
详细信息
ISBN:
(纸本)9781581132021
FranTk is a new high level library for programming Graphical User Interfaces (GUIs) in Haskell. It is based on Fran (functional Reactive Animation), and uses the notions of Behaviors and Events to structure code. Behaviors are time-varying, reactive values. they can be used to represent the state of an application. Events are streams of values that occur at discrete points in time. they can be used, for instance, to represent user input. FranTk allows user interfaces to be structured in a more declarative manner than has been possible with previous functional GUI libraries. We demonstrate, through a series of examples, how this is achieved, and why it is important. these examples are elements of a prototype, Air Traffic Control simulator. FranTk uses a binding to the popular Tcl/Tk toolkit to provide a powerful set of platform independent set of widgets. It has been released as a Haskell library that runs under Hugs and GHC.
Modern networks provide a variety of interrelated services including routing, traffic monitoring, load balancing, and access control. Unfortunately, the languages used to program today's networks lack modern featu...
详细信息
ISBN:
(纸本)9781450308656
Modern networks provide a variety of interrelated services including routing, traffic monitoring, load balancing, and access control. Unfortunately, the languages used to program today's networks lack modern features-they are usually defined at the low level of abstraction supplied by the underlying hardware and they fail to provide even rudimentary support for modular programming. As a result, network programs tend to be complicated, error-prone, and difficult to maintain. this paper presents Frenetic, a high-level language for programming distributed collections of network switches. Frenetic provides a declarative query language for classifying and aggregating network traffic as well as a functional reactive combinator library for describing high-level packet-forwarding policies. Unlike prior work in this domain, these constructs are-by design-fully compositional, which facilitates modular reasoning and enables code reuse. this important property is enabled by Frenetic's novel run-time system which manages all of the details related to installing, uninstalling, and querying low-level packet-processing rules on physical switches. Overall, this paper makes three main contributions: (1) We analyze the state-of-the art in languages for programming networks and identify the key limitations;(2) We present a language design that addresses these limitations, using a series of examples to motivate and validate our choices;(3) We describe an implementation of the language and evaluate its performance on several benchmarks.
We present a new interface for practical functional Reactive programming (FRP) that (1) is close in spirit to the original FRP ideas, (2) does not have the original space-leak problems, without using arrows or advance...
详细信息
ISBN:
(纸本)9781450336697
We present a new interface for practical functional Reactive programming (FRP) that (1) is close in spirit to the original FRP ideas, (2) does not have the original space-leak problems, without using arrows or advanced types, and (3) provides a simple and expressive way for performing I/O actions from FRP code. We also provide a denotational semantics for this new interface, and a technique (using Kripke logical relations) for reasoning about which FRP functions may "forget their past", i.e. which functions do not have an inherent space-leak. Finally, we show how we have implemented this interface as a Haskell library called FRPNow.
暂无评论