The idea of functional programming has played a big role in shaping today's landscape of mainstream programming languages. Another concept that dominates the current programming style is Dijkstra's structured programming. Both concepts have been successfully married, for example in the programming language Scala. This paper proposes how the same can be achieved for structured programming and PURELY functional programming via the notion of LINEAR SCOPE. One advantage of this proposal is that mainstream programmers can reap the benefits of purely functional programming like easily exploitable parallelism while using familiar structured programming syntax and without knowing concepts like monads. A second advantage is that professional purely functional programmers can often avoid hard to read functional code by using structured programming syntax that is often easier to parse mentally.
We present a marriage of functional and structured imperative programming that embeds in pure lambda calculus. We describe how we implement the core of this language in a monadic DSL which is structurally equivalent to our intended source language and which, when evaluated, generates pure lambda terms in continuation-passing-style.
Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. On the other hand, having an exact reference count of each value can enable optimizations, such as destructive updates. We explore these optimization opportunities in the context of an eager, purely functional programming language. We propose a new mechanism for efficiently reclaiming memory used by nonshared values, reducing stress on the global memory allocator. We describe an…
This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022). The meeting took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of Software (ETAPS 2022). The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. As the range of papers presented in this year's workshop shows, this continues to be a fruitful interface.
Traversal strategies á la Stratego (also á la Strafunski and 'Scrap Your Boilerplate') provide an exceptionally versatile and uniform means of querying and transforming deeply nested and heterogeneously structured data including terms in functional programming and rewriting, objects in OO programming, and XML documents in XML programming. However, the resulting traversal programs are prone to programming errors. We are specifically concerned with errors that go beyond conservative type errors; examples we examine include divergent traversals, prematurely terminated traversals, and traversals w…
This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in Dublin, Ireland on the 25th of April as a satellite event of the European Joint Conferences on Theory & Practice of Software (ETAPS 2020). Due to the COVID-19 pandemic, ETAPS 2020, and consequently MSFP 2020, has been postponed to a date yet to be determined. The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal …
In this paper, we propose an explicit, non-strict representation of search trees in constraint-logic object-oriented programming. Our search tree representation includes both the non-deterministic and deterministic behaviour during execution of an application. Introducing such a representation facilitates the use of various search strategies. In order to demonstrate the applicability of our approach, we incorporate explicit search trees into the virtual machine of the constraint-logic object-oriented programming language Muli. We then exemplarily implement three search algorithms that traverse…
This volume contains the proceedings of the Fifth Workshop on Mathematically Structured Functional Programming (MSFP 2014), taking place on 12 April, 2014 in Grenoble, France, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. As the range of papers presented in this year's workshop shows, this continues to be a fruitful …
This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. The workshop consists of two invited presentations and eight contributed papers on a range of t…
The sixth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop i…
The correctness of a structured program is, at best, plausible. Though this is a step forward compared to what came before, it falls short of verified correctness. To verify a structured program according to Hoare's method one is faced with the problem of finding assertions to fit existing code. In 1971 this mode of verification was declared by Dijkstra as too hard to be of practical use---he advised that proof and code were to grow together. A method for doing this was independently published by Reynolds in 1978 and by van Emden in 1979. The latter was further developed to attain the form of …
We demonstrate how methods in Functional Programming can be used to implement a computer algebra system. As a proof-of-concept, we present the computational-algebra package. It is a computer algebra system implemented as an embedded domain-specific language in Haskell, a purely functional programming language. Utilising methods in functional programming and prominent features of Haskell, this library achieves safety, composability, and correctness at the same time. To demonstrate the advantages of our approach, we have implemented advanced Gröbner basis algorithms, such as Faugère's $F_4$ and …
The seventh workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop…
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we set out to characterise the hierarchy NP $\subseteq$ NEXP $\subseteq$ NEXP$^{(2)}$ $\subseteq \cdots \subseteq$ NEXP$^{(k)}$ $\subseteq \cdots$ solely in terms of higher-typed, purely functional programs. Although the work is incomplete, we present an initial approach using cons-free programs with immutable functions.
We present Babel-17, the first programming language for purely functional structured programming (PFSP). Earlier work illustrated PFSP in the framework of a toy research language. Babel-17 takes this earlier work to a new level by showing how PFSP can be combined with pattern matching, object oriented programming, and features like concurrency, lazy evaluation, memoization and support for lenses.
With the growing ubiquity of Internet of Things(IoT), more complex logic is being programmed on resource-constrained IoT devices, almost exclusively using the C programming language. While C provides low-level control over memory, it lacks a number of high-level programming abstractions such as higher-order functions, polymorphism, strong static typing, memory safety, and automatic memory management. We present Hailstorm, a statically-typed, purely functional programming language that attempts to address the above problem. It is a high-level programming language with a strict typing discipline…
University of Athens（雅典大学）；University of Victoria（维多利亚大学）
We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique minimum Herbrand model which is the greatest lower bound of all Herbrand models of the program and the least fixed-point of an immediate consequence operator. We also propose an SLD-resolution proof procedure which is proven sound and complete with respect to the minimum model semantics. In other words, we provide a purely extensional theoretical framework f…
Computer Aided Design systems provide tools for building and manipulating models of solid objects. Some also provide access to programming languages so that parametrised designs can be expressed. There is a sharp distinction, therefore, between building models, a concrete graphical editing activity, and programming, an abstract, textual, algorithm-construction activity. The recently proposed Language for Structured Design (LSD) was motivated by a desire to combine the design and programming activities in one language. LSD achieves this by extending a visual logic programming language to incorp…
GP 2 is an experimental programming language for computing by graph transformation. An initial interpreter for GP 2, written in the functional language Haskell, provides a concise and simply structured reference implementation. Despite its simplicity, the performance of the interpreter is sufficient for the comparative investigation of a range of test programs. It also provides a platform for the development of more sophisticated implementations.
A multitude of different probabilistic programming languages exists today, all extending a traditional programming language with primitives to support modeling of complex, structured probability distributions. Each of these languages employs its own probabilistic primitives, and comes with a particular syntax, semantics and inference procedure. This makes it hard to understand the underlying programming concepts and appreciate the differences between the different languages. To obtain a better understanding of probabilistic programming, we identify a number of core programming concepts underly…
Macros are a common part of Lisp languages, and one of their most lauded features. Much research has gone into making macros both safer and more powerful resulting in developments in multiple areas, including maintaining hygiene, and typed program staging. However, macros do suffer from various downsides, including being second-class. Particularly egregious for eager functional programming, they are unable to be passed to higher-order functions or freely composed. Fexprs, as reformulated by John Shutt, provide a first-class and more powerful alternative to macros that meshes well with pure fun…
Both Prolog and Oz are multiparadigm languages with a logic programming core. There is a significant subset of Oz that is a syntactic variant of Prolog: pure Prolog programs with green or blue cuts and bagof/3 or setof/3 can be translated directly to Oz. Because of this close relationship between Prolog and Oz, we propose that the extensions made by Oz to logic programming can be an inspiration for the future evolution of Prolog. We explain three extensions, namely deterministic logic programming, lazy concurrent functional programming, and purely functional distributed computing. We briefly p…
Implementing a complex concept as an executable model in a strongly typed, purely functional language hits a sweet spot between mere simulation and formal specification. For research and education it is often desirable to enrich the algorithmic code with meta-logical annotations, variously embodied as assertions, theorems or test cases. Checking frameworks use the inherent logical power of the functional paradigm to approximate theorem proving by heuristic testing. Here we propose several novel idioms to enhance the practical expressivity of checking, namely meta-language marking, nominal axio…
Pull-tabbing is an evaluation technique for functional logic programs which computes all non-deterministic results in a single graph structure. Pull-tab steps are local graph transformations to move non-deterministic choices towards the root of an expression. Pull-tabbing is independent of a search strategy so that different strategies (depth-first, breadth-first, parallel) can be used to extract the results of a computation. It has been used to compile functional logic languages into imperative or purely functional target languages. Pull-tab steps might duplicate choices in case of shared sub…
We describe the design and implementation of GNU Guix, a purely functional package manager designed to support a complete GNU/Linux distribution. Guix supports transactional upgrades and roll-backs, unprivileged package management, per-user profiles, and garbage collection. It builds upon the low-level build and deployment layer of the Nix package manager. Guix uses Scheme as its programming interface. In particular, we devise an embedded domain-specific language (EDSL) to describe and compose packages. We demonstrate how it allows us to benefit from the host general-purpose programming langua…
This paper illustrates how the diagram programming language DiaPlan can be used to program visual systems. DiaPlan is a visual rule-based language that is founded on the computational model of graph transformation. The language supports object-oriented programming since its graphs are hierarchically structured. Typing allows the shape of these graphs to be specified recursively in order to increase program security. Thanks to its genericity, DiaPlan allows to implement systems that represent and manipulate data in arbitrary diagram notations. The environment for the language exploits the diagr…
Control Network Programming (CNP) is a programming paradigm which is being described with the maxim "Primitives + Control Network = Control Network program". It is a type of graphic programming. The Control Network is a recursive system of graphs; it can be a purely descriptive specification of the problem being solved. Clearly, "drawing" the control network does not include any programming. The Primitives are elementary, easily understandable and clearly specified actions. Ultimately, they have to be programmed. Historically, they are usually coded in Free Pascal. The actual code of the primi…
Concurrency has been rapidly gaining importance in general-purpose computing, caused by the recent turn towards multicore processing architectures. As a result, an increasing number of developers have to learn to write concurrent programs, a task that is known to be hard even for the expert. Language designers are therefore working on languages that promise to make concurrent programming "easier" than using traditional thread libraries. However, the claim that a new language is more usable than another cannot be supported by purely theoretical considerations, but calls for empirical studies. I…
The ability to generate natural language sequences from source code snippets has a variety of applications such as code summarization, documentation, and retrieval. Sequence-to-sequence (seq2seq) models, adopted from neural machine translation (NMT), have achieved state-of-the-art performance on these tasks by treating source code as a sequence of tokens. We present ${\rm {\scriptsize CODE2SEQ}}$: an alternative approach that leverages the syntactic structure of programming languages to better encode source code. Our model represents a code snippet as the set of compositional paths in its abst…
Scientific computation is a discipline that combines numerical analysis, physical understanding, algorithm development, and structured programming. Several yottacycles per year on the world's largest computers are spent simulating problems as diverse as weather prediction, the properties of material composites, the behavior of biomolecules in solution, and the quantum nature of chemical compounds. This article is intended to review specfic languages features and their use in computational science. We will review the strengths and weaknesses of different programming styles, with examples taken …
Many applications require complexly structured data objects. Developing new or adapting existing algorithmic solutions for creating such objects can be a non-trivial and costly task if the considered objects are subject to different application-specific constraints. Often, however, it is comparatively easy to declaratively describe the required objects. In this paper, we propose to use answer-set programming (ASP)---a well-established declarative programming paradigm from the area of artificial intelligence---for instantiating objects in standard object-oriented programming languages. In parti…
Dynamic trees, originally described by Sleator and Tarjan, have been studied deeply for non persistent structures providing $\mathcal{O}(\log n)$ time for update and lookup operations as shown in theory and practice by Werneck. However, discussions on how the most common dynamic trees operations (i.e. link and cut) are computed over a purely functional data structure have not been studied. Even more, asking whether vertices $u$ and $v$ are connected (i.e. within the same forest) assumes that corresponding indices or locations for $u$ and $v$ are taken for granted in most of the literature, and…
We present a unified framework for the declarative analysis of structured communications. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. We introduce a declarative interpretation of the language for structured communications proposed by Honda, Vasconcelos, and Kubo. Distinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; t…
In today's world of Web application development, programmers are commonly called upon to use the Hypertext Markup Language (HTML) as a programming language, something for which it was never intended and for which it is woefully inadequate. HTML is a data language, nothing more. It lacks high level programming constructions like procedures, conditions, and loops. Moreover it provides no intrinsic mechanism to insert or associate dynamic application data. Lastly, despite the visibly apparent structure of a web page when viewed in a browser, the responsible HTML code bears little to no discernibl…
The STAPLE project investigated (at the end of the eighties), a persistent architecture for functional programming. Work has been done in two directions: the development of a programming environment for a functional language within a persistent system and an experiment on transferring the expertise of functional prototyping into industry. This paper is a report on the first activity. The first section gives a general description of Absynte - the abstract syntax tree editor developed within the Project. Following sections make an attempt at measuring the effectiveness of such an editor and disc…
Memoisation, or tabling, is a well-known technique that yields large improvements in the performance of some recursive computations. Tabled resolution in Prologs such as XSB and B-Prolog can transform so called left-recursive predicates from non-terminating computations into finite and well-behaved ones. In the functional programming literature, memoisation has usually been implemented in a way that does not handle left-recursion, requiring supplementary mechanisms to prevent non-termination. A notable exception is Johnson's (1995) continuation passing approach in Scheme. This, however, relies…
Compiler-Guided Inference-Time Adaptation: Improving GPT-5 Programming Performance in Idris
Ming Hsieh Department of Electrical and Computer Engineering（明希斯部门电子与计算机工程系）；Viterbi School of Engineering, University of Southern California（维特比工程学院，南加州大学）
One of the most recent architectures of networks is Software-Defined Networks (SDNs) using a con- troller appliance to control the set of switches on the network. The controlling process includes installing or uninstalling packet-processing rules on flow tables of switches. This paper presents a high-level imperative network programming language, called ImNet, to facilitate writing efficient, yet simple, programs executed by controller to manage switches. ImNet is simply-structured, expressive, compositional, and imperative. This paper also introduces an operational semantics to ImNet. Detaile…
Stevens Institute of Technology（史蒂文斯理工学院）；University of Arizona（亚利桑那大学）
Most musical programming languages are developed purely for coding virtual instruments or algorithmic compositions. Although there has been some work in the domain of musical query languages for music information retrieval, there has been little attempt to unify the principles of musical programming and query languages with cognitive and natural language processing models that would facilitate the activity of composition by conversation. We present a prototype framework, called MusECI, that merges these domains, permitting score-level algorithmic composition in a text editor while also support…
