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.
Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. this can lead programmers to accidental...
详细信息
ISBN:
(纸本)9781450386159
Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. this can lead programmers to accidentally violate those assumptions if they are not careful. To address this issue, we encode the memory locations that are accessed by a given computation using a graded monad. We use the data flow dependencies which arise from this to construct a type-level graph that we analyse to automatically order the computations so that no dependencies are violated. this also allows for computations which have no dependencies on each other to be run concurrently.
A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. the system is based on the portable Gambit Scheme programming language and provides a ...
详细信息
ISBN:
(纸本)9781450323260
A modular framework for the development of medical applications that promotes deterministic, robust and correct code is presented. the system is based on the portable Gambit Scheme programming language and provides a flexible cross-platform environment for developing graphical applications on mobile devices as well as medical instrumentation interfaces running on embedded platforms. Real world applications of this framework for mobile diagnostics, telemonitoring and automated drug infusions are reported. the source code for the core framework is open source and available at: https://***/part-cw/lambdanative.
Software Defined Networking (SDN) programs are written with respect to assumptions on software and hardware facilities and protocol definitions. Silent mismatches between the expected feature set and implemented featu...
详细信息
ISBN:
(纸本)9781450336871
Software Defined Networking (SDN) programs are written with respect to assumptions on software and hardware facilities and protocol definitions. Silent mismatches between the expected feature set and implemented feature set of SDN artifacts can easily lead to hard to debug network configurations, decreased network performance, outages, or worse, security vulnerabilities. We show how the paradigm of axiomatic programming, supported by practical dependent types, provides effective support for SDN executable specifications and verification.
C-Rules is a business rules management system developed by Constraint Technologies international(1) (CTI), designed for use in transportation problems. Users define rules describing various aspects of a problem, such ...
详细信息
ISBN:
(纸本)9781595938152
C-Rules is a business rules management system developed by Constraint Technologies international(1) (CTI), designed for use in transportation problems. Users define rules describing various aspects of a problem, such as solution costs and legality, which are then queried from a host application, typically an optimising solver. At its core, C-Rules provides a functional expression language which affords users both power and flexibility when formulating rules. In this paper we will describe our experiences of using functionalprogramming both at the end-user level, as well as at the implementation level. We highlight some of the benefits we, and the product's users, have enjoyed from the decision to base our rule system on features such as: higher-order functions, referential transparency, and static, polymorphic typing. We also outline some of our experiences in using Haskell to build an efficient compiler for the core language.
this paper reports on our industry-academia project of using a functional language in business software production. the general motivation behind the project is our ultimate goal of adopting an ML-style higher-order t...
详细信息
ISBN:
(纸本)9781450328739
this paper reports on our industry-academia project of using a functional language in business software production. the general motivation behind the project is our ultimate goal of adopting an ML-style higher-order typed functional language in a wide range of ordinary software development in industry. To probe the feasibility and identify various practical problems and needs, we have conducted a 15 month pilot project for developing an enterprise resource planning (ERP) system in SML#. the project has successfully completed as we have planned, demonstrating the feasibility of SML#. In particular, seamless integration of SQL and direct C language interface are shown to be useful in reliable and efficient development of a data intensive business application. During the program development, we have found several useful functionalprogramming patterns and a number of possible extensions of an ML-style language with records. this paper reports on the project details and the lessons learned from the project.
the proceedings contain 10 papers. the topics discussed include: deadlock-free session types in linear Haskell;evaluating linear functions to symmetric monoidal categories;graded monads and type-level programming for ...
ISBN:
(纸本)9781450386159
the proceedings contain 10 papers. the topics discussed include: deadlock-free session types in linear Haskell;evaluating linear functions to symmetric monoidal categories;graded monads and type-level programming for dependence analysis;practical normalization by evaluation for EDSLs;design patterns for parser combinators (functional pearl);seeking stability by being lazy and shallow: lazy and shallow instantiation is user friendly;express: applications of dynamically typed Haskell expressions;Chesskell: a two-player game at the type level;and safe mutation with algebraic effects.
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper desc...
详细信息
ISBN:
(纸本)9781595930644
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper describes the design and implementation issues of those AOP mechanisms that give us insights into the interaction between AOP features and common features in strongly-typed functional languages such as type inference, polymorphic types and curried functions. We implemented a prototype compiler of the language and used the language for separating crosscutting concerns in application programs, including for separating descriptions of a type system from compiler descriptions.
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.
暂无评论