We describe the Funlogic system which extends a functional language with existentially quantified declarations. An existential declaration introduces a variable and a set of constraints that its value should meet. Exi...
详细信息
It is possible to extend the basic notion of "function call" to allow functions to have multiple return points. this turns out to be a surprisingly useful mechanism. this article conducts a fairly wide-rangi...
详细信息
It is possible to extend the basic notion of "function call" to allow functions to have multiple return points. this turns out to be a surprisingly useful mechanism. this article conducts a fairly wide-ranging tour of such a feature: a formal semantics for a minimal A-calculus capturing the mechanism;motivating examples;monomorphic and parametrically polymorphic static type systems;useful transformations;implementation concerns and experience with an implementation;and comparison to related mechanisms, such as exceptions, sum-types and explicit continuations. We conclude that multiple-return function call is not only a useful and expressive mechanism, at boththe source-code and intermediate-representation levels, but also quite inexpensive to implement.
Heterogeneous programming complicates software development. We present CLOP, a platform that embeds code targeting heterogeneous compute devices in a convenient and clean way, allowing unobstructed data flow between t...
详细信息
ISBN:
(纸本)9781450336871
Heterogeneous programming complicates software development. We present CLOP, a platform that embeds code targeting heterogeneous compute devices in a convenient and clean way, allowing unobstructed data flow between the host code and the devices, reducing the amount of source code by an order of magnitude. the CLOP compiler uses the standard facilities of the D programming language to generate code strictly at compile-time. In this paper we describe the CLOP language and the CLOP compiler implementation.
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionalit...
详细信息
ISBN:
(纸本)9781450308656
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML's built-in support for state and I/O. Developers write programs using monadic values of type m T as if they were of type T, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program type checks. Our algorithm, based on Jones' qualified types, produces principal types. But principal types are sometimes problematic: the program's semantics could depend on the choice of instantiation when more than one instantiation is valid. In such situations we are able to simplify the types to remove any ambiguity but without adversely affecting typability;thus we can accept strictly more programs. Moreover, we have proved that this simplification is efficient (linear in the number of constraints) and coherent: while our algorithm induces a particular rewriting, all related rewritings will have the same semantics. We have implemented our approach for a core functional language and applied it successfully to simple examples from the domains listed above, which are used as illustrations throughout the paper.
functionalprogramming languages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. functional abstractions, such as monads, allow a...
详细信息
ISBN:
(纸本)9781450369817
functionalprogramming languages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. functional abstractions, such as monads, allow abstracting away some of the repetitive structure of a compiler, removing boilerplate code and making extensions simpler. Even so, functional languages are rarely used to implement compilers for languages of other paradigms. this paper reports on the experience of a four-year long project where we developed a compiler for a concurrent, object-oriented language using the functional language Haskell. the focus of the paper is the implementation of the type checker, but the design works well in static analysis tools, such as tracking uniqueness of variables to ensure data-race freedom. the paper starts from a simple type checker to which we add more complex features, such as type state, with minimal changes to the overall initial design.
Information Flow Control (IFC) in dynamic contexts is challenging due to different interpretations of security that arise. this paper introduces a modular framework to address this challenge. We present a dynamic floa...
详细信息
ISBN:
(纸本)9798400703843
Information Flow Control (IFC) in dynamic contexts is challenging due to different interpretations of security that arise. this paper introduces a modular framework to address this challenge. We present a dynamic floating-label enforcement mechanism that can be instantiated based on the intended security. Our approach formalizes a simply typed lambda-calculus, extended with IFC operations, and adopts an epistemic perspective on security definition.
functional Reactive programming (FRP) is a framework for reactive programming in a functional setting. FRP has been applied to a number of domains, such as graphical animation, graphical user interfaces, robotics, and...
详细信息
ISBN:
(纸本)9781581137569
functional Reactive programming (FRP) is a framework for reactive programming in a functional setting. FRP has been applied to a number of domains, such as graphical animation, graphical user interfaces, robotics, and computer vision. Recently, we have been interested in applying FRP-like principles to hybrid modeling and simulation of physical systems. As a step in that direction, we have extended an existing FRP implementation, Yampa, in two new ways that make it possible to express certain models in a very natural way, and reduces the amount of work needed to put modeling equations into a suitable form for simulation. First, we have added Dirac impulses that allow certain types of discontinuities to be handled in an easy yet rigorous manner. Second, we have adapted automatic differentiation to the setting of Yampa, and generalized it to work correctly with Dirac impulses. this allows derivatives of piecewise continuous signals to be well-defined at all points. this paper reviews the basic ideas behind automatic differentiation, in particular Jerzy Karczmarczuk's elegant version for a lazy functional language with overloading, and then considers the integration with Yampa and the addition of Dirac impulses.
functional Reactive programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports ...
详细信息
ISBN:
(纸本)9781605583327
functional Reactive programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from Most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs. Statically guaranteeing correctness properties of programs is an attractive proposition. this is true in particular for typical application domains for reactive programming such as embedded systems. To that end, many existing reactive languages have type systems or other static checks that guarantee domain-specific properties, such as feedback loops always being well-formed. However, they are limited in their capabilities to support dynamism and higher-order data-flow compared with FRP. thus, the onus of ensuring such properties of FRP programs has so far been on the programmer as established static techniques do not suffice. In this paper, we show how dependent types allow this concern to be addressed. We present an implementation of FRP embedded in the dependently-typed language Agda, leveraging the type system of the host language to craft a domain-specific (dependent) type system for FRP. the implementation constitutes a discrete, operational semantics of FRP, and as it passes the Agda type, coverage, and termination checks, we know the operational semantics is total, which means our type system is safe.
Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as alpha-equivalen...
详细信息
ISBN:
(纸本)9781450308656
Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as alpha-equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected. Furthermore, their implementations are tedious, requiring "boilerplate" code that must be updated whenever the object language definition changes. Many researchers have therefore sought to specify binding syntax declaratively, so that tools can correctly handle the details behind the scenes. this idea has been the inspiration for many new systems (such as Beluga, Delphin, FreshML, FreshOCaml, C alpha ml, FreshLib, and Ott) but there is still room for improvement in expressivity, simplicity and convenience. In this paper, we present a new domain-specific language, UNBOUND, for specifying binding structure. Our language is particularly expressive-it supports multiple atom types, pattern binders, type annotations, recursive binders, and nested binding (necessary for telescopes, a feature found in dependently-typed languages). However, our specification language is also simple, consisting of just five basic combinators. We provide a formal semantics for this language derived from a locally nameless representation and prove that it satisfies a number of desirable properties. We also present an implementation of our binding specification language as a GHC Haskell library implementing an embedded domain specific language (EDSL). By using Haskell type constructors to represent binding combinators, we implement the EDSL succinctly using datatype-generic programming. Our implementation supports a number of features necessary for practical programming, including flexibility in the treatment of user-defined types, best-effort name preservation (for error messages), and integration with Haskell's monad transformer library.
Type providers [16], pioneered in the F# programming language, are a practical and powerful means of gaining the benefits of a modern static type system when working with data schemas that are defined outside of the p...
详细信息
ISBN:
(纸本)9781450323895
Type providers [16], pioneered in the F# programming language, are a practical and powerful means of gaining the benefits of a modern static type system when working with data schemas that are defined outside of the programming language, such as relational databases. F# type providers are implemented using a form of compile-time code generation, which requires the compiler to expose an internal API and can undermine type safety. We show that with dependent types it is possible to define a type provider mechanism that does not rely on code generation. Using this mechanism, a type provider becomes a kind of generic program that is instantiated for a particular external schema, which can be represented using an ordinary datatype. Because these dependent type providers use the ordinary abstraction mechanisms of the type system, they preserve its safety properties. We evaluate the practicality of this technique and explore future extensions.
暂无评论