Bachelorarbeit Moritz Uhlig A Type Class Based Approach for Modeling Transformations of Abstract Petri Nets Fakultät Technik und Informatik Faculty of Engineering and Computer Science Studiendepartment Informatik Department of Computer Science Moritz Uhlig A Type Class Based Approach for Modeling Transformations of Abstract Petri Nets Bachelorarbeit eingereicht im Rahmen der Bachelorprüfung im Studiengang Bachelor of Science Angewandte Informatik am Department Informatik der Fakultät Technik und Informatik der Hochschule für Angewandte Wissenschaften Hamburg Betreuender Prüfer: Prof. Dr. Julia Padberg Zweitgutachter: Prof. Dr. Friedrich Esser Eingereicht am: 28. August 2012 Moritz Uhlig Thema der Arbeit A Type Class Based Approach for Modeling Transformations of Abstract Petri Nets Stichworte Petri-Netze, Abstrakte Petri-Netze, Funktionale Programmierung, Scala, Netztransfor- mationen, Kategorientheorie, Typklassen, Netzklassen Kurzzusammenfassung Abstrakte Petri-Netze bieten einen einheitlichen Ansatz zur Beschreibung von Struktur und Semantik unterschiedlicher Arten von Petri-Netzen. Kategorientheorie stellt ein allgemeines Modell zur Beschreibung von Phänomenen bereit, die in unterschiedlichen Zweigen der Mathematik und Wissenschaft aufzufinden sind. Diese stellt die Basis für die Theorie der Abstrakten Petri-Netze dar, findet aber auch Anwendung in der funk- tionalen Programmierung. Diese Arbeit erläutert kategorielle Konzepte und deren Zusammenhang mit Abstrakten Petri-Netze sowie der funktionalen Programmierung. Sie stellt ein Softwaredesign vor, für das diese Konzepte die Grundlage bilden. Moritz Uhlig Title of the paper A Type Class Based Approach for Modeling Transformations of Abstract Petri Nets Keywords Petri nets, Abstract Petri Nets, functional programming, Scala, net transformations, category theory, type classes, net classes Abstract Abstract Petri Nets offer a unified approach to describing the structure and seman- tics of different kinds of Petri nets. Category provides a common model for describing phenomena found in multiple branches of mathematics and science. It acts as the foun- dation for the theory of Abstract Petri Nets but also has applications in in functional programming. This thesis explains categorical concepts and their relation to both func- tional programming and the theory of Abstract Petri Nets. A software design for im- plementing transformations of Petri nets based on these concepts will be presented. Contents 1. Introduction 1 1.1. Motivation and Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2. Structure of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2. Categorical Foundations 4 2.1. Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2. Duality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3. Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.4. Free Functor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.5. Natural Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.6. Products and Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.7. Adjoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.8. Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3. Functional Programming in Scala 17 3.1. Functional Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.2. Referential Transparency and Pure Functions . . . . . . . . . . . . . . . . 17 3.3. Concepts in Scala . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.4. Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.4.1. Classes, Traits and Objects . . . . . . . . . . . . . . . . . . . . . . . 19 3.4.2. Companion Objects and Case Classes . . . . . . . . . . . . . . . . 21 3.4.3. Polymorphic Expressions . . . . . . . . . . . . . . . . . . . . . . . 22 3.4.4. Generic Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.4.5. Function Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.4.6. Algebraic Data Types and Pattern Matching . . . . . . . . . . . . 27 3.4.7. Higher Kinds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.4.8. Type Aliases and Type Members . . . . . . . . . . . . . . . . . . . 30 3.4.9. Implicit Parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.4.10. Structural Types and Type Lambdas . . . . . . . . . . . . . . . . . 38 3.5. Type classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.6. Type Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.7. The Category of Scala Types . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.7.1. Products in Scala . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.7.2. Coproducts in Scala . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.7.3. Endofunctors in Scala . . . . . . . . . . . . . . . . . . . . . . . . . 45 iv Contents 3.7.4. Natural Transformations in Scala . . . . . . . . . . . . . . . . . . . 46 4. Abstract Petri Nets 48 4.1. Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.1.1. Elementary Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.1.2. Place/Transition Nets . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.2. Low-Level Abstract Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.3. High-Level Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.3.1. Typed Algebraic High-Level Nets . . . . . . . . . . . . . . . . . . 54 4.4. Transformation of Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.4.1. Net Class Transformations . . . . . . . . . . . . . . . . . . . . . . . 57 4.4.2. Petri Net Transformations Based on Morphisms . . . . . . . . . . 58 5. Design and Implementation 60 5.1. Type Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 5.1.1. Type Classes as Evidence . . . . . . . . . . . . . . . . . . . . . . . 62 5.1.2. Net Structure as Data Type . . . . . . . . . . . . . . . . . . . . . . 64 5.2. Categorical View of Data Structures . . . . . . . . . . . . . . . . . . . . . 64 5.3. Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.4. Syntax Layer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 6. Conclusion and Prospects 80 6.1. Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 6.2. Applicability to High-Level Nets . . . . . . . . . . . . . . . . . . . . . . . 81 A. Appendix 84 A.1. Sets and Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 A.2. Semigroups, Monoids and Groups . . . . . . . . . . . . . . . . . . . . . . 84 A.3. Grothendieck Group . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 A.4. Free Commutative Monoid . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Bibliography 87 v 1. Introduction 1.1. Motivation and Goals Petri nets are used to model and analyze concurrent processes with a wide range of applications in chemistry, business and computer science. Based on the original def- inition there exist numerous variations of Petri nets reaching from low level nets like elementary nets to various high level nets with typed, distinguishable tokens. Abstract Petri nets define a mathematical model for uniformly describing the structure of dif- ferent classes of Petri nets and transformations between them. When viewed from an implementor’s perspective this enables a generic design as it is possible to abstract over the elements describing structure and operations. When looking at the tools for model- ing Petri nets it appears that most of them concentrate on graphical modeling and are often limited in the types of Petri nets they support. These types of Petri nets are also in many cases restricted to low level Petri nets, sometimes offering one type of high-level Petri net. There also exist more extensive tools like CPN Tools that are not restricted to graphical modeling but are also extensible via a programming interface. These are by far more expressive than simple graphical editing tools but are still restricted to one certain type of high-level nets. In the case of CPN Tools this is a special form of Col- ored Petri nets incorporating a custom dialect of the programming language ML for definition of behaviour. Category theory is an abstract branch of mathematics that is used to examine ab- stract properties of mathematical concepts. It offers a toolset for describing the general abstract structures in mathematics. Category theory focusses on relations between el- ements - called objects - instead of the elements themselves. It provides abstractions that are useful in many branches of mathematics and science and defines a common lan- guage when working across boundaries of these disciplines. In recent years category theory has also gained importance in both functional programming and the theory of Petri nets. Having a common foundation for modeling the problem domain and struc- turing a program that implements the model can be a valuable asset. As the concept of 1 1. Introduction functional programming is based on treating computations as the evaluation of mathe- matical functions it is a good fit for implementing solutions to mathematical problems. Scala is a multi-paradigm programming language for the Java Virtual Machine that incorporates many features from functional as well as object oriented languages. It has a very expressive type system that allows encoding much more information in types than is possible in other languages. This has lead to efforts to port libraries that are based on categorical concepts from the functional programming language Haskell to 1 Scala. Libraries like Scalaz allow expressing axioms in the type system and implement programs that act as proofs for these axioms. Influences from other programming lan- guages also lead to patterns to emulate a construct called type classes in the Scala lan- guage. Type classes are a type level construct for implementing polymorphism that sep- arates data types and operations. The use of type classes often results in more modular and more extensible code. It also limits code duplication as in combination with other Scala features a higher level of abstraction can be reached. Especially when modeling mathematical concepts in type classes this also leads to a higher degree of reusability. This thesis takes a code centric approach to modeling Petri nets opposed to the more traditional graphical approach to modeling. In particular the goals of this thesis are the following: 1. We show how Scala’s programming language features and its type system can be used to model categorical concepts. 2. We analyze how the common foundation of both functional programming and Abstract Petri Nets given by category theory can be leveraged to provide mean- ingful abstractions usable for the implementation. 3. We inspect how transformations both between two net classes and inside one class of Petri nets can be implemented. To answer these questions, we perform an in-depth analysis of the Scala program- ming language. We design and implement a softwares model for the given problem domain and evaluate it in terms of usability and general applicability. In summary, the contributions of this thesis can be summarized as follows: • We analyze category theory, functional programming and Abstract Petri Nets as well as the relationships between these disciplines. 1 Documentation Available at http://code.google.com/p/scalaz/ 2 1. Introduction • We try to leverage the common underlying ideas of category theory to deliver an abstraction applicable to multiple instantiations to multiple types of Abstract Petri Nets. • We design a framework for modeling and transforming Abstract Petri Nets and evaluate the model in terms of applicability and extensibility. 1.2. Structure of the Thesis The thesis starts off by introducing the categorical concepts used in both the theory of Abstract Petri Nets and functional programming. It continues by explaining fundamen- tal concepts of functional programming along with the Scala programming language. Advanced type system constructs of Scala that are used to implement features not pos- sible in many other languages will be discussed in more detail. Petri nets will be intro- duced by defining the properties of two distinct classes of Petri nets before the notion of Abstract Petri Nets will be presented. Two different notions of transformation on Petri nets will also be introduced in this section. The implementation part starts with showing the relationship between the concepts involved and continues by implement- ing data structures and operations. The thesis is closed by a discussion an evaluating the applicability of the model concerning high-level Petri nets and gives some ideas how extension to the model could be implemented for improved support of high-level nets. Due to the strong coherence of the fundamental theories involved and due to the abstract nature of the problem it is inevitable to also include forward references. 3 2. Categorical Foundations Category theory is a branch of mathematics that exists since the 1940s. It is an effort to use a convenient symbolism and common language to describe precisely many similar phenomena. Additionally it provides the means to simultaneously investigate con- structions with similar properties that occur in different fields of mathematics and re- lated fields such as computer science and physics. 2.1. Categories A category A consists of • a class of objects (A, B, …), • morphisms (also called arrows) between objects (f , g, …), • for each object A an identity morphism 1A called the identity and • a composition law for morphisms. For each pair (A;B) of objects of a category A there is a set hom (A;B) whose mem- bers are called A-morphisms from A to B. The sets hom (A;B) are pairwise disjoint (Adamék et al., 2009, 3.1). The source of each morphism f : A �! B is called domain, denoted dom (f) = A, the target is called codomain denoted cod (f) = B. Morphisms f; g are can be composed whenever cod (f) = dom (g) yielding a new morphism h = g � f with domain dom (h) = dom (f) and codomain cod (h) = cod (g). Composition is associative, i.e. given any morphisms f : A �! B, g : B �! C and h : C �! D the equation h � (g � f) = (h � g) � f holds. The identities are A-morphisms from an object A to itself and have to also act as identities with respect to composition: 4 2. Categorical Foundations 1B � f = f = f � 1A. Example 2.1.1. Set is the category whose objects are sets and the morphisms are func- tions between the sets. The identity is the identity function and composition is given by function composition. Example 2.1.2. Every monoid (M; �; e), i.e. a semigroup with unit (see Section A.2) can be seen as category with the underlying set M as only object and hom (M;M) = M; 1M = e; y � x = y � x. Example 2.1.3. The category of a functional programming language L consists of the types of the programming language as objects and the computable functions as mor- phisms. As in Example 2.1.1 the identity is given the identity function, composition is given by the composition of functions. A common way to represent objects and morphisms graphically are commutative di- agrams. These are directed graphs with the objects as nodes and morphism as edges. Commutative diagrams are not only used for visualization but also for proofs. The technique used is often called diagram chasing as it is possible to follow the arrows in the diagram to examine certain properties of the morphisms and their compositions. Figure 2.1 shows a diagram with three objects A, B, and C and morphisms f, g and h between them. Saying that this diagram commutes is equivalent to saying h = g � f. f A. B. . g h . C. Figure 2.1.: Commutative diagram Another commonly used notation for categories is the tuple notation. A category A can be written as the quadruple A = (OA; homA; id; �) where OA denotes the objects of the category, hom the hom-set, id the identity morphisms and � the composition. Category theory concentrates on inpecting the morphisms between objects instead of focussing on the objects of a category. 5