-
Crème de la Crem: Composable Representable Executable Machines (Architectural Pearl)
Authors:
Marco Perone,
Georgios Karachalias
Abstract:
In this paper we describe how to build software architectures as a composition of state machines, using ideas and principles from the field of Domain-Driven Design. By definition, our approach is modular, allowing one to compose independent subcomponents to create bigger systems, and representable, allowing the implementation of a system to be kept in sync with its graphical representation.
In a…
▽ More
In this paper we describe how to build software architectures as a composition of state machines, using ideas and principles from the field of Domain-Driven Design. By definition, our approach is modular, allowing one to compose independent subcomponents to create bigger systems, and representable, allowing the implementation of a system to be kept in sync with its graphical representation.
In addition to the design itself we introduce the Crem library, which provides a concrete state machine implementation that is both compositional and representable, Crem uses Haskell's advanced type-level features to allow users to specify allowed and forbidden state transitions, and to encode complex state machine -- and therefore domain-specific -- properties. Moreover, since Crem's state machines are representable, Crem can automatically generate graphical representations of systems from their domain implementations.
△ Less
Submitted 18 July, 2023;
originally announced July 2023.
-
Resolution as Intersection Subty** via Modus Ponens
Authors:
Koar Marntirosian,
Tom Schrijvers,
Bruno C. d. S. Oliveira,
Georgios Karachalias
Abstract:
Resolution and subty** are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subty** is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other.…
▽ More
Resolution and subty** are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subty** is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subty** with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subty** becomes apparent. Finally, the integration of resolution into subty** enables first-class (implicit) environments. The extension that recovers the power of resolution via subty** is the modus ponens rule of propositional logic. While it is easily added to declarative subty**, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subty**, and coherence. To materialize these ideas we develop $λ_i^{\mathsf{MP}}$, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.
△ Less
Submitted 15 October, 2020; v1 submitted 13 October, 2020;
originally announced October 2020.
-
Explicit Effect Subty**
Authors:
Georgios Karachalias,
Matija Pretnar,
Amr Hany Saleh,
Stien Vanderhallen,
Tom Schrijvers
Abstract:
As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subty**-based effect system on which an effect-aware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly error-prone because its core language is implicitly-typed,…
▽ More
As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subty**-based effect system on which an effect-aware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly error-prone because its core language is implicitly-typed, making code transformations very fragile.
To remedy this, we present an explicitly-typed polymorphic core calculus for algebraic effect handlers with a subty**-based type-and-effect system. It reifies appeals to subty** in explicit casts with coercions that witness the subty** proof, quickly exposing ty** bugs in program transformations.
Our ty**-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly-typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.
△ Less
Submitted 28 May, 2020;
originally announced May 2020.
-
Bidirectional Type Class Instances (Extended Version)
Authors:
Koen Pauwels,
Georgios Karachalias,
Michiel Derhaeg,
Tom Schrijvers
Abstract:
GADTs were introduced in Haskell's eco-system more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes.
In this paper we identify the source of this shortcoming and…
▽ More
GADTs were introduced in Haskell's eco-system more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes.
In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell's type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical bi-implications, in contrast to their traditional unidirectional interpretation.
We present a fully-fledged design of bidirectional instances, covering the specification of ty** and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proof-of-concept implementation of our algorithm, and revisit the meta-theory of type classes in the presence of our extension.
△ Less
Submitted 1 July, 2019; v1 submitted 28 June, 2019;
originally announced June 2019.
