-
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.
-
idris-ct: A Library to do Category Theory in Idris
Authors:
Fabrizio Genovese,
Alex Gryzlov,
Jelle Herold,
Andre Knispel,
Marco Perone,
Erik Post,
André Videla
Abstract:
We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for t…
▽ More
We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.
△ Less
Submitted 14 September, 2020; v1 submitted 25 November, 2019;
originally announced December 2019.
-
Computational Petri Nets: Adjunctions Considered Harmful
Authors:
Fabrizio Genovese,
Alex Gryzlov,
Jelle Herold,
Marco Perone,
Erik Post,
André Videla
Abstract:
We review some of the endeavors in trying to connect Petri nets with free symmetric monoidal categories. We give a list of requirement such connections should respect if they are meant to be useful for practical/implementation purposes. We show how previous approaches do not satisfy them, and give compelling evidence that this depends on trying to make the correspondence functorial in the directio…
▽ More
We review some of the endeavors in trying to connect Petri nets with free symmetric monoidal categories. We give a list of requirement such connections should respect if they are meant to be useful for practical/implementation purposes. We show how previous approaches do not satisfy them, and give compelling evidence that this depends on trying to make the correspondence functorial in the direction from nets to free symmetric monoidal categories, in order to produce an adjunction. We show that dropping this immediately honors our desiderata, and conclude by introducing an Idris library which implements them.
△ Less
Submitted 8 May, 2019; v1 submitted 29 April, 2019;
originally announced April 2019.
