Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFabULous Interoperability for ML and a Linear Language
64
0
0.0
(
0
)
Added by
Gabriel Scherer
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.
rate research
Read More
Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows. Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values. To demonstrate the efficacy of our linear type system - both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types - we implemented our type system in GHC, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions.
This volume collects the extend
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Ethereums EVM, while avoiding some of the problems they face. Simplicity comes with formal denotational semantics defined in Coq, a popular, general purpose software proof assistant. Simplicity also includes operational semantics that are defined with an abstract machine that we call the Bit Machine. The Bit Machine is used as a tool for measuring the computational space and time resources needed to evaluate Simplicity programs. Owing to its Turing incompleteness, Simplicity is amenable to static analysis that can be used to derive upper bounds on the computational resources needed, prior to execution. While Turing incomplete, Simplicity can express any finitary function, which we believe is enough to build useful smart contracts for blockchain applications.
The use of adaptive workflow management for in situ visualization and analysis has been a growing trend in large-scale scientific simulations. However, coordinating adaptive workflows with traditional procedural programming languages can be difficult because system flow is determined by unpredictable scientific phenomena, which often appear in an unknown order and can evade event handling. This makes the implementation of adaptive workflows tedious and error-prone. Recently, reactive and declarative programming paradigms have been recognized as well-suited solutions to similar problems in other domains. However, there is a dearth of research on adapting these approaches to in situ visualization and analysis. With this paper, we present a language design and runtime system for developing adaptive systems through a declarative and reactive programming paradigm. We illustrate how an adaptive workflow programming system is implemented using our approach and demonstrate it with a use case from a combustion simulation.
This paper describes the design and implementation of CRAQL (Composable Repository Analysis and Query Language), a new query language for source code. The growth of source code mining and its applications suggest the need for a query language that can fully utilize and correlate across the unique structure and metadata of parsed source code. CRAQL is built on an underlying abstraction analogous to the underpinnings of SQL, but aimed at parsed source code. Thus, while SQL queries inputs and outputs are sets of tuples, CRAQL queries inputs and outputs are sets of abstract syntax trees (ASTs). This abstraction makes CRAQL queries composable (the output of one query can become the input to another) and improves the power of the language by allowing for querying of the tree structure and metadata, as well as raw text. Furthermore, the abstraction enables tree-specific language optimizations and allows CRAQL to be easily applied to any language that is parsable into ASTs. These attributes, along with a familiar syntax similar to SQL, allow complex queries to be expressed in a compact, straightforward manner. Questions such as find the longest series of statements without any loops, find methods that are never called, find getters (0-parameter methods with a single statement that returns a member variable), or find the percentage of variables declared at the top of a block all translate to simple, understandable queries in CRAQL. In this paper we describe the language, its features and capabilities. We compare CRAQL to other languages for querying source code and find that it has potential advantages in clarity and compactness. We discuss the features and optimizations added to support searching parse tree collections effectively and efficiently. Finally, we summarize the application of the language to millions of Java source files, the details of which are in a companion paper.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
