-
An Exceptional Actor System (Functional Pearl)
Authors:
Patrick Redmond,
Lindsey Kuper
Abstract:
The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways -- some more advisable than others.
We present a user-accessible actor framework hidden in plain sight within the RTS an…
▽ More
The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways -- some more advisable than others.
We present a user-accessible actor framework hidden in plain sight within the RTS and demonstrate it on a classic example from the distributed systems literature. We then extend both the framework and example to the realm of dynamic types. Finally, we raise questions about how RTS features intersect and possibly subsume one another, and suggest that GHC can guide good practice by constraining the use of some features.
△ Less
Submitted 20 July, 2023;
originally announced July 2023.
-
Inductive diagrams for causal reasoning
Authors:
Jonathan Castello,
Patrick Redmond,
Lindsey Kuper
Abstract:
The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagr…
▽ More
The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagrams and concurrent separation logic, but enjoys a graphical syntax similar to Lamport diagrams. Critically, CSDs are based on the idea that causal relationships between events are witnessed by the paths that information follows between them. To that end, we model happens-before as a dependent type of paths between events.
The inductive formulation of CSDs enables their interpretation into a variety of semantic domains. We demonstrate the interpretability of CSDs with a case study on properties of logical clocks, widely-used mechanisms for reifying causal relationships as data. We carry out this study by implementing a series of interpreters for CSDs, culminating in a generic proof of Lamport's clock condition that is parametric in a choice of clock. We instantiate this proof on Lamport's scalar clock, on Mattern's vector clock, and on the matrix clocks of Raynal et al. and of Wuu and Bernstein, yielding verified implementations of each. The CSD formalism and our case study are mechanized in the Agda proof assistant.
△ Less
Submitted 14 May, 2024; v1 submitted 19 July, 2023;
originally announced July 2023.
-
A Review of the Trends and Challenges in Adopting Natural Language Processing Methods for Education Feedback Analysis
Authors:
Thanveer Shaik,
Xiaohui Tao,
Yan Li,
Christopher Dann,
Jacquie Mcdonald,
Petrea Redmond,
Linda Galligan
Abstract:
Artificial Intelligence (AI) is a fast-growing area of study that stretching its presence to many business and research domains. Machine learning, deep learning, and natural language processing (NLP) are subsets of AI to tackle different areas of data processing and modelling. This review article presents an overview of AI impact on education outlining with current opportunities. In the education…
▽ More
Artificial Intelligence (AI) is a fast-growing area of study that stretching its presence to many business and research domains. Machine learning, deep learning, and natural language processing (NLP) are subsets of AI to tackle different areas of data processing and modelling. This review article presents an overview of AI impact on education outlining with current opportunities. In the education domain, student feedback data is crucial to uncover the merits and demerits of existing services provided to students. AI can assist in identifying the areas of improvement in educational infrastructure, learning management systems, teaching practices and study environment. NLP techniques play a vital role in analyzing student feedback in textual format. This research focuses on existing NLP methodologies and applications that could be adapted to educational domain applications like sentiment annotations, entity annotations, text summarization, and topic modelling. Trends and challenges in adopting NLP in education were reviewed and explored. Contextbased challenges in NLP like sarcasm, domain-specific language, ambiguity, and aspect-based sentiment analysis are explained with existing methodologies to overcome them. Research community approaches to extract the semantic meaning of emoticons and special characters in feedback which conveys user opinion and challenges in adopting NLP in education are explored.
△ Less
Submitted 20 January, 2023;
originally announced January 2023.
-
Verified Causal Broadcast with Liquid Haskell
Authors:
Patrick Redmond,
Gan Shen,
Niki Vazou,
Lindsey Kuper
Abstract:
Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that w…
▽ More
Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of their correctness is less common, much less machine-checked proofs about executable implementations.
We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell's underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store.
△ Less
Submitted 15 March, 2023; v1 submitted 29 June, 2022;
originally announced June 2022.
-
Toward Hole-Driven Development with Liquid Haskell
Authors:
Patrick Redmond,
Gan Shen,
Lindsey Kuper
Abstract:
Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell's support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized…
▽ More
Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell's support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized proof developments in Liquid Haskell take advantage of this capability. Adding theorem-proving capabilities to a "legacy" language like Haskell lets programmers directly verify properties of real-world Haskell programs (taking advantage of the existing highly tuned compiler, run-time system, and libraries), just by writing Haskell. However, more established proof assistants like Agda and Coq offer far better support for interactive proof development and insight into the proof state (for instance, what subgoals still need to be proved to finish a partially-complete proof). In contrast, Liquid Haskell provides only coarse-grained feedback to the user -- either it reports a type error, or not -- unfortunately hindering its usability as a theorem prover.
In this paper, we propose improving the usability of Liquid Haskell by extending it with support for Agda-style typed holes and interactive editing commands that take advantage of them. In Agda, typed holes allow programmers to indicate unfinished parts of a proof, and incrementally complete the proof in a dialogue with the compiler. While GHC Haskell already has its own Agda-inspired support for typed holes, we posit that typed holes would be especially powerful and useful if combined with Liquid Haskell's refinement types and SMT automation. We discuss how typed holes might work in Liquid Haskell, and we consider possible implementation approaches and next steps.
△ Less
Submitted 9 October, 2021;
originally announced October 2021.
