the proceedings contain 10 papers. the special focus in this conference is on trends in functionalprogramming. the topics include: Towards a More Efficient Selection Monad;compositional Views in Composition...
ISBN:
(纸本)9783031745577
the proceedings contain 10 papers. the special focus in this conference is on trends in functionalprogramming. the topics include: Towards a More Efficient Selection Monad;compositional Views in Compositional Images – Category: Research –;programming with Dependent Additive Pairs;context-Free Subphrase Grammars: A Grammar Formalism for Modular Syntax Definitions;polymorphism with Typed Holes;a Preliminary Type- and Control-Flow Analysis for System Fω;error Messages for Students Taught Using a Systematic Program Design Curriculum;flattening Combinations of Arrays and Records.
Dependent types provide users withthe tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language...
详细信息
ISBN:
(纸本)9783031745577;9783031745584
Dependent types provide users withthe tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.
Flattening is known to be a performance-boosting technique to orchestrate parallel computations on arbitrarily deeply nested arrays. In this paper, we propose a flattening transformation that deals with nested data st...
详细信息
ISBN:
(纸本)9783031745577;9783031745584
Flattening is known to be a performance-boosting technique to orchestrate parallel computations on arbitrarily deeply nested arrays. In this paper, we propose a flattening transformation that deals with nested data structures that are composed of combinations of arrays and records. We choose the functional array programming language SaC as basis for this work, as it already supports flattening of homogeneously nested arrays, i.e. arrays in which all elements have the same shape. We propose an extension of SaC's syntax for records that allows records and arrays to be used in homogeneously nested form, and provide an implementation of this record transformation in the SaC compiler. Based on that extension, we show how any legal program that operates with such data structures can be transformed into an equivalent one that does not require any records at runtime.
this paper explores a novel approach to selection functions through the introduction of a generalised selection monad. the foundation is laid withthe conventional selection monad J, defined as (A -> R) -> A, to...
详细信息
ISBN:
(纸本)9783031745577;9783031745584
this paper explores a novel approach to selection functions through the introduction of a generalised selection monad. the foundation is laid withthe conventional selection monad J, defined as (A -> R) -> A, together with various combinators for computing new selection functions from old. However, inefficiencies in these combinators are identified. To address these issues, a specialised type K is introduced, and its isomorphism to J is demonstrated. the paper further generalises the K type to G, where performance improvements and enhanced intuitive usability are observed. the embeddings between J and G are established, offering a more efficient and expressive alternative to the well established J type for selection functions. the findings emphasise the advantages of the generalised selection monad and its applicability in diverse scenarios, paving the way for further exploration and optimisation.
Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of ...
详细信息
ISBN:
(纸本)9783031745577;9783031745584
Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of pairs together? And is this new pair type useful in practice? To answer these questions, we employ quantitative type theory, which can describe both substructural and dependent types simultaneously. In our previous work, we introduced dependent additive pairs. In this work, we show how these pairs can be used in three completely different scenarios: folding data structures using linear recursion schemes, computing resource-aware proofs, and defining additive versions of inductive and coinductive types. Each of these scenarios is then illustrated by an implementation in the Janus language.
this article presents a map of studies on the educational potential of robotics and programming in inclusive settings. the scoping review methodology was used based on the procedures recommended by the Joanna Briggs I...
详细信息
this paper presents stableKanren, a miniKanren extension with normal logic programming support under stable model semantics. MiniKanren is a relational programming solver implemented atop Scheme via shallow embedding,...
详细信息
ISBN:
(纸本)9798400708121
this paper presents stableKanren, a miniKanren extension with normal logic programming support under stable model semantics. MiniKanren is a relational programming solver implemented atop Scheme via shallow embedding, which means the predicate in each rule is encoded as a goal function directly. the solver utilizes the pattern matching macro in Scheme to transform the input goal function and form a static search stream through continuations to achieve the essential features, resolution and unification, in Prolog. However, the static stream only works on monotonic reasoning. Even though the core miniKanren is designed to be easily modified and extended with new features, none of the existing extensions support solving normal logic programs. Also, no normal logic program solvers are based on a functionalprogramming language. We identify and categorize the roles of resolution and unification in top-down solving. And we realize that a dynamic search stream is needed to support non-monotonic reasoning. So we evolve both resolution and unification with new roles, and we exploit the advantages of using macros and continuations further to weave the information generated during runtime into future streams dynamically. We create multiple innovative macros to compile the normal logic program into a program with its complement form, obtain the domain of a variable under different contexts, and generate the new search stream during solving. And we use the coinductive resolution to handle the loop in the normal logic program. In future work, we plan to apply bottom-up optimization to improve our top-down system performance and support various input rules.
the paper describes the 101haskell chrestomathy-a collection of Haskell programs implementing features of a hypothetical information system in a manner to represent knowledge about functionalprogramming useful for le...
详细信息
this paper shows how reflection and object-oriented programming can be used to ease the implementation of classical fault tolerance mechanisms in distributed applications. When the underlying runtime system does not p...
详细信息
this paper shows how reflection and object-oriented programming can be used to ease the implementation of classical fault tolerance mechanisms in distributed applications. When the underlying runtime system does not provide fault tolerance transparently, classical approaches to implementing fault tolerance mechanisms often imply mixing functionalprogramming with non-functionalprogramming (e.g. error processing mechanisms). the use of reflection improves the transparency of fault tolerance mechanisms to the programmer and more generally provides a clearer separation between functional and non-functionalprogramming. the implementations of some classical replication techniques using a reflective approach are presented in detail and illustrated by several examples, which have been prototyped on a network of Unix workstations. Lessons learnt from our experiments are drawn and future work is discussed.
We present a technique to embed a functional logic language in Haskell using a GHC plugin. Our approach is based on a monadic lifting that models the functional logic semantics explicitly. Using a GHC plugin, we get m...
详细信息
ISBN:
(纸本)9783031248405;9783031248412
We present a technique to embed a functional logic language in Haskell using a GHC plugin. Our approach is based on a monadic lifting that models the functional logic semantics explicitly. Using a GHC plugin, we get many language extensions that GHC provides for free in the embedded language. As a result, we obtain a seamless embedding of a functional logic language, without having to implement a full compiler. We briefly show that our approach can be used to embed other domainspecific languages as well. Furthermore, we can use such a plugin to build a full blown compiler for our language.
暂无评论