Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. Datalog is declarative, expressive, and optimizable, and has been applied successfully in a wide...
详细信息
ISBN:
(纸本)9781450342193
Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. Datalog is declarative, expressive, and optimizable, and has been applied successfully in a wide variety of problem domains. However, most use-cases require extending Datalog in an application-specific manner. In this paper we define Datafun, an analogue of Datalog supporting higher-order functionalprogramming. the key idea is to track monotonicity with types.
Analysing time complexity of functional programs in a lazy language is problematic, because the time required to evaluate a function depends on how much of the result is "needed" in the computation. Recent r...
详细信息
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We prop...
详细信息
ISBN:
(纸本)9781450308656
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We propose a safer programming interface implemented as a library. Whereas indexing the types of names and terms by a numerical bound is a famous technique, we index them by worlds, a different notion of index that is both finer and more abstract. While being more finely typed, our approach incurs no loss of expressiveness or efficiency. Via parametricity we obtain properties about functions polymorphic on worlds. For instance, well-typed world-polymorphic functions over open lambda-terms commute with any renaming of the free variables. Our whole development is conducted within Agda, from the code of the library, to its soundness proof and the properties of external functions. the soundness of our library is demonstrated via the construction of a logical relations argument.
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.
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.
this paper presents an OO style without classes, which we call interface-based object-oriented programming (IB). IB is a natural extension of closely related ideas such as traits. Abstract state operations provide a n...
详细信息
ISBN:
(纸本)9781450344463
this paper presents an OO style without classes, which we call interface-based object-oriented programming (IB). IB is a natural extension of closely related ideas such as traits. Abstract state operations provide a new way to deal with state, which allows for flexibility not available in classbased languages. In IB state can be type-refined in subtypes. the combination of a purely IB style and type-refinement enables powerful idioms using multiple inheritance and state. To introduce IB to programmers we created Classless Java: an embedding of IB directly into Java. Classless Java uses annotation processing for code generation and relies on new features of Java 8 for interfaces. the code generation techniques used in Classless Java have interesting properties, including guarantees that the generated code is type-safe and good integration with IDEs. Usefulness of IB and Classless Java is shown with examples and case studies.
Pattern matching is a high-level notation for programs to analyse the shape of data, and can be optimised to efficient low-level instructions. the Stratego language uses first-class pattern matching, a powerful form o...
详细信息
ISBN:
(纸本)9781450399197
Pattern matching is a high-level notation for programs to analyse the shape of data, and can be optimised to efficient low-level instructions. the Stratego language uses first-class pattern matching, a powerful form of pattern matching that traditional optimisation techniques do not apply to directly. In this paper, we investigate how to optimise programs that use first-class pattern matching. Concretely, we show how to map first-class pattern matching to a form close to traditional pattern matching, on which standard optimisations can be applied. through benchmarks, we demonstrate the positive effect of these optimisations on the run-time performance of Stratego programs. We conclude that the expressive power of first-class pattern matching does not hamper the optimisation potential of a language that features it.
the proceedings contain 23 papers. the topics discussed include: a multi-target, multi-paradigm DSL compiler for algorithmic graph processing;Lang-n-Prove: a DSL for language proofs;freon: an open web native language ...
ISBN:
(纸本)9781450399197
the proceedings contain 23 papers. the topics discussed include: a multi-target, multi-paradigm DSL compiler for algorithmic graph processing;Lang-n-Prove: a DSL for language proofs;freon: an open web native language workbench;the semantics of plurals;reflection as a tool to debug objects;workbench for creating block-based environments;property-based testing: climbing the stairway to verification;selective traceability for rule-based model-to-model transformations;specializing scope graph resolution queries;gradual grammars: syntax in levels and locales;property probes: source code based exploration of program analysis results;a language-parametric approach to exploratory programming environments;collection skeletons: declarative abstractions for data collections;and iCoLa: a compositional meta-language with support for incremental language development.
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. the ultrametric structure enforces causality restrictions on reactive systems and ...
详细信息
ISBN:
(纸本)9781450308656
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. the ultrametric structure enforces causality restrictions on reactive systems and allows well-founded recursive definitions by a generalization of guardedness. We capture the arbitrariness of user input (e. g., a user gets to decide the stream of clicks she sends to a program) by making use of the fact that the closed subsets of an ultrametric space themselves form an ultrametric space, allowing us to interpret nondeterminism with a "powerspace" monad. Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/non-linear domain-specific language for writing GUI programs. the non-linear part of the language is used for writing reactive stream-processing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph. We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.
One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exception...
详细信息
ISBN:
(纸本)9781450323260
One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions withthe outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations - it provides monads for capturing state, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects. Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
暂无评论