Art Sci. Eng. Program., vol. 10, issue 3: "Filling the Gaps of Polarity: ..."
Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments
Bohdan Liesnikov, David Binder, and Tim Süberkrüb
(Delft University of Technology, Netherlands; University of Kent, Canterbury, UK; University of Tübingen, Germany)
The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new constructors, such as by adding a new object implementing an interface in object-oriented programming.Most dependently typed languages have good support for the former style through inductive types, but support for the latter style through coinductive types is usually much poorer. Polarity is a language that treats both kinds of types symmetrically and allows the developer to switch between type representations.However, it currently lacks several features expected of a state-of-the-art dependently typed language, such as implicit arguments. The central aim of this paper is to provide an algorithmic type system and inference algorithm for implicit arguments that respect the core symmetry of the language. Our work provides two key contributions: a complete algorithmic description of the type system backing Polarity, and a comprehensive description of a unification algorithm that covers arbitrary inductive and coinductive types. We give rules for reduction semantics, conversion checking, and a unification algorithm for pattern-matching, which are essential for a usable implementation. A work-in-progress implementation of the algorithms in this paper is available at polarity-lang.github.io. We expect that the comprehensive account of the unification algorithm and our design decisions can serve as a blueprint for other dependently typed languages that support inductive and coinductive types symmetrically.
Publisher's Version
Info
Art Sci. Eng. Program., vol. 10, issue 3: "BlueScript: A Disaggregated ..."
BlueScript: A Disaggregated Virtual Machine for Microcontrollers
Fumika Mochizuki, Tetsuro Yamazaki, and Shigeru Chiba
(University of Tokyo, Tokyo, Japan)
Virtual machines (VMs) are highly beneficial for microcontroller development. In particular, interactive programming environments greatly facilitate iterative development processes, and higher execution speeds expand the range of applications that can be developed. However, due to their limited memory size, microcontroller VMs provide a limited set of features. Widely used VMs for microcontrollers often lack interactive responsiveness and/or high execution speed. While researchers have investigated offloading certain VM components to other machines,the types of components that can be offloaded are still restricted.
In this paper, we propose a disaggregated VM that offloads as many components as possible to a host machine. This makes it possible to exploit the abundant memory of the host machine and its powerful processing capability to provide rich features through the VM. As an instance of a disaggregated VM, we design and implement a BlueScript VM. The BlueScript VM is a virtual machine for microcontrollers that provides an interactive development environment. We offload most of the components of the BlueScript VM to a host machine. To reduce communication overhead between the host machine and the microcontroller, we employed a data structure called a shadow machine on the host machine, which mirrors the execution state of the microcontroller.
Through our experiments, we confirmed that offloading components does not seriously compromise their expected benefits. We assess that an offloaded incremental compiler results in faster execution speed than MicroPython and Espruino, while keeping interactivity comparable with MicroPython. In addition, our experiments observe that the offloaded dynamic compiler improves VM performance. Through this investigation, we demonstrate the feasibility of providing rich features even on VMs for memory-limited microcontrollers.
Publisher's Version
Published Artifact
Artifact Available v2.0
Artifact Supports Claims v2.0
Art Sci. Eng. Program., vol. 10, issue 3: "Chorex: Restartable, Language-Integrated ..."
Chorex: Restartable, Language-Integrated Choreographies
Ashton Wiersdorf and Ben Greenman
(University of Utah, USA)
We built Chorex, a language that brings choreographic programming to Elixir as a path toward robust distributed applications. Chorex is unique among choreographic languages because it tolerates failure among actors: when an actor crashes, Chorex spawns a new process, restores state using a checkpoint, and updates the network configuration for all actors. Chorex also proves that full-featured choreographies can be implemented via metaprogramming, and that doing so achieves tight integration with the host language. For example, mismatches between choreography requirements and an actor implementation are reported statically and in terms of source code rather than macro-expanded code. This paper illustrates Chorex on several examples, ranging from a higher-order bookseller to a secure remote password protocol, details its implementation, and measures the overhead of checkpointing. We conjecture that Chorex’s projection strategy, which outputs sets of stateless functions, is a viable approach for other languages to support restartable actors.
Publisher's Version
Published Artifact
Artifact Available v2.0
Artifact Supports Claims v2.0
Art Sci. Eng. Program., vol. 10, issue 3: "Filling the Gaps of Polarity: ..."
Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments
Bohdan Liesnikov, David Binder, and Tim Süberkrüb
(Delft University of Technology, Netherlands; University of Kent, Canterbury, UK; University of Tübingen, Germany)
The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new constructors, such as by adding a new object implementing an interface in object-oriented programming.Most dependently typed languages have good support for the former style through inductive types, but support for the latter style through coinductive types is usually much poorer. Polarity is a language that treats both kinds of types symmetrically and allows the developer to switch between type representations.However, it currently lacks several features expected of a state-of-the-art dependently typed language, such as implicit arguments. The central aim of this paper is to provide an algorithmic type system and inference algorithm for implicit arguments that respect the core symmetry of the language. Our work provides two key contributions: a complete algorithmic description of the type system backing Polarity, and a comprehensive description of a unification algorithm that covers arbitrary inductive and coinductive types. We give rules for reduction semantics, conversion checking, and a unification algorithm for pattern-matching, which are essential for a usable implementation. A work-in-progress implementation of the algorithms in this paper is available at polarity-lang.github.io. We expect that the comprehensive account of the unification algorithm and our design decisions can serve as a blueprint for other dependently typed languages that support inductive and coinductive types symmetrically.
Publisher's Version
Info
Art Sci. Eng. Program., vol. 10, issue 3: "BlueScript: A Disaggregated ..."
BlueScript: A Disaggregated Virtual Machine for Microcontrollers
Fumika Mochizuki, Tetsuro Yamazaki, and Shigeru Chiba
(University of Tokyo, Tokyo, Japan)
Virtual machines (VMs) are highly beneficial for microcontroller development. In particular, interactive programming environments greatly facilitate iterative development processes, and higher execution speeds expand the range of applications that can be developed. However, due to their limited memory size, microcontroller VMs provide a limited set of features. Widely used VMs for microcontrollers often lack interactive responsiveness and/or high execution speed. While researchers have investigated offloading certain VM components to other machines,the types of components that can be offloaded are still restricted.
In this paper, we propose a disaggregated VM that offloads as many components as possible to a host machine. This makes it possible to exploit the abundant memory of the host machine and its powerful processing capability to provide rich features through the VM. As an instance of a disaggregated VM, we design and implement a BlueScript VM. The BlueScript VM is a virtual machine for microcontrollers that provides an interactive development environment. We offload most of the components of the BlueScript VM to a host machine. To reduce communication overhead between the host machine and the microcontroller, we employed a data structure called a shadow machine on the host machine, which mirrors the execution state of the microcontroller.
Through our experiments, we confirmed that offloading components does not seriously compromise their expected benefits. We assess that an offloaded incremental compiler results in faster execution speed than MicroPython and Espruino, while keeping interactivity comparable with MicroPython. In addition, our experiments observe that the offloaded dynamic compiler improves VM performance. Through this investigation, we demonstrate the feasibility of providing rich features even on VMs for memory-limited microcontrollers.
Publisher's Version
Published Artifact
Artifact Available v2.0
Artifact Supports Claims v2.0
Art Sci. Eng. Program., vol. 10, issue 3: "Filling the Gaps of Polarity: ..."
Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments
Bohdan Liesnikov, David Binder, and Tim Süberkrüb
(Delft University of Technology, Netherlands; University of Kent, Canterbury, UK; University of Tübingen, Germany)
The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new constructors, such as by adding a new object implementing an interface in object-oriented programming.Most dependently typed languages have good support for the former style through inductive types, but support for the latter style through coinductive types is usually much poorer. Polarity is a language that treats both kinds of types symmetrically and allows the developer to switch between type representations.However, it currently lacks several features expected of a state-of-the-art dependently typed language, such as implicit arguments. The central aim of this paper is to provide an algorithmic type system and inference algorithm for implicit arguments that respect the core symmetry of the language. Our work provides two key contributions: a complete algorithmic description of the type system backing Polarity, and a comprehensive description of a unification algorithm that covers arbitrary inductive and coinductive types. We give rules for reduction semantics, conversion checking, and a unification algorithm for pattern-matching, which are essential for a usable implementation. A work-in-progress implementation of the algorithms in this paper is available at polarity-lang.github.io. We expect that the comprehensive account of the unification algorithm and our design decisions can serve as a blueprint for other dependently typed languages that support inductive and coinductive types symmetrically.
Publisher's Version
Info
Art Sci. Eng. Program., vol. 10, issue 3: "Chorex: Restartable, Language-Integrated ..."
Chorex: Restartable, Language-Integrated Choreographies
Ashton Wiersdorf and Ben Greenman
(University of Utah, USA)
We built Chorex, a language that brings choreographic programming to Elixir as a path toward robust distributed applications. Chorex is unique among choreographic languages because it tolerates failure among actors: when an actor crashes, Chorex spawns a new process, restores state using a checkpoint, and updates the network configuration for all actors. Chorex also proves that full-featured choreographies can be implemented via metaprogramming, and that doing so achieves tight integration with the host language. For example, mismatches between choreography requirements and an actor implementation are reported statically and in terms of source code rather than macro-expanded code. This paper illustrates Chorex on several examples, ranging from a higher-order bookseller to a secure remote password protocol, details its implementation, and measures the overhead of checkpointing. We conjecture that Chorex’s projection strategy, which outputs sets of stateless functions, is a viable approach for other languages to support restartable actors.
Publisher's Version
Published Artifact
Artifact Available v2.0
Artifact Supports Claims v2.0
Art Sci. Eng. Program., vol. 10, issue 3: "BlueScript: A Disaggregated ..."
BlueScript: A Disaggregated Virtual Machine for Microcontrollers
Fumika Mochizuki, Tetsuro Yamazaki, and Shigeru Chiba
(University of Tokyo, Tokyo, Japan)
Virtual machines (VMs) are highly beneficial for microcontroller development. In particular, interactive programming environments greatly facilitate iterative development processes, and higher execution speeds expand the range of applications that can be developed. However, due to their limited memory size, microcontroller VMs provide a limited set of features. Widely used VMs for microcontrollers often lack interactive responsiveness and/or high execution speed. While researchers have investigated offloading certain VM components to other machines,the types of components that can be offloaded are still restricted.
In this paper, we propose a disaggregated VM that offloads as many components as possible to a host machine. This makes it possible to exploit the abundant memory of the host machine and its powerful processing capability to provide rich features through the VM. As an instance of a disaggregated VM, we design and implement a BlueScript VM. The BlueScript VM is a virtual machine for microcontrollers that provides an interactive development environment. We offload most of the components of the BlueScript VM to a host machine. To reduce communication overhead between the host machine and the microcontroller, we employed a data structure called a shadow machine on the host machine, which mirrors the execution state of the microcontroller.
Through our experiments, we confirmed that offloading components does not seriously compromise their expected benefits. We assess that an offloaded incremental compiler results in faster execution speed than MicroPython and Espruino, while keeping interactivity comparable with MicroPython. In addition, our experiments observe that the offloaded dynamic compiler improves VM performance. Through this investigation, we demonstrate the feasibility of providing rich features even on VMs for memory-limited microcontrollers.
Publisher's Version
Published Artifact
Artifact Available v2.0
Artifact Supports Claims v2.0