Skip to content

Instantly share code, notes, and snippets.

@kenwebb
Last active November 2, 2017 14:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kenwebb/5e51afd9f6abccbb0055f9c2266bdaea to your computer and use it in GitHub Desktop.
Save kenwebb/5e51afd9f6abccbb0055f9c2266bdaea to your computer and use it in GitHub Desktop.
Category Theory and Programming
<?xml version="1.0" encoding="UTF-8"?>
<!--Xholon Workbook http://www.primordion.com/Xholon/gwt/ MIT License, Copyright (C) Ken Webb, Tue Oct 17 2017 09:52:02 GMT-0400 (EDT)-->
<XholonWorkbook>
<Notes><![CDATA[
Xholon
------
Title: Category Theory and Programming
Description:
Url: http://www.primordion.com/Xholon/gwt/
InternalName: 5e51afd9f6abccbb0055f9c2266bdaea
Keywords:
My Notes
--------
October 17, 2017
search: Category Theory and Programming
References
----------
() https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory
Relating Category Theory to Programming Language Theory
"I'm wondering what the relation of category theory to programming language theory is."
() http://blog.sigfpe.com/
DAN PIPONI
KSW I like the answer he provided for the mathoverflow question:
"a category consisting of types as objects and functions as arrows"
"One place where it starts getting deeper is when you consider polymorphic functions. A polymorphic function is essentially a family of functions, parameterised by types. Or categorically, a family of arrows, parameterised by objects."
"Category theory also meshes nicely with the notion of an 'interface' in programming. Category theory encourages us not to look at what an object is made of, but how it interacts with other objects, and itself."
"There is also a beautiful relationship between pure typed lambda calculus and cartesian closed categories (CCC)."
() http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.362&rep=rep1&type=pdf
A Categorical Manifesto, Joseph A. Goguen
"To each species of mathematical structure, there corresponds a category whose objects have that structure, and whose morphisms preserve it."
KSW how does this relate to starting with a tree structure, pasting in a subtree, and ending up with a tree
"If we take sets to be objects, then their morphisms are clearly going to be functions."
() book: Categories for Software Engineering, By Jose Luiz Fiadeiro
see books.google.ca, https://books.google.ca/books?id=QXojiwovK7oC&lr=
http://orbis.uottawa.ca/search/i3540209093 the book is in the library
the "social life" of objects
quotes from the book:
categories for software engineering
Concepts in set theory are typically formalized extensionally, in the sense that a set is defined by its elements, category Theory provides a more implicit way of characterizing objects.
It does so in terms of of the relationships that each object exhibits to the other objects in the universe of discourse.
Category Theory characterizes objects in terms of their social lives. (see Jean-Yves Girard)
In my opinion, this focus on social aspects of object lives is exactly the reason for the applicability of category Theory to Computing in general, and software engineering in particular.
To realize why this is so, one just needs to thank the current software development methods, namely object-oriented ones, typically model of the universe as a society of the interacting objects.
Agent oriented methods are based on the same societal metaphor.
This focus on interaction is not accidental
it is an attempt at tackling the increasing complexity of modern software systems.
In this context. Complexity does not necessarily arise from the computational or algorithmic Natura systems, but results from the fact that their behavior can only be explained as emerging from the interconnections that are established between their components.
point in the definition of the structure of a system, one also bring software to the realm of natural, physical and social systems, something that seems to be essential for the development of well Integrated Systems.
Category theory is advocated as a good mathematical structure for this integration precisely because it focuses on relationships and interactions
this is why many of the examples that are used throughout this book address what has become known in software engineering at software architecture
that is precisely the study of the gross modular ization principles that should allow us to Design Systems as possibly standard structures of smaller components and the interconnections between them.
The focus that category Theory puts on morphisms a structure preserving mappings is Paramount for software architectures because it is the morphisms that determine the nature of the interconnections that can be established between objects system components.
Hence, the choice of a particular category can be seen to reflect, in some sense, the choice of a particular architectural style.
Moreover, category Theory provides techniques for manipulating and reasoning about system configurations represented as diagrams.
As a consequence, it becomes possible to establish allowing systems to be used as components of even more complex systems that is to use diagrams is objects, and for inferring properties of systems from their configurations.
The ultimate conclusion that we would like the reader to draw is that high school education could well evolve in a way that equips our future generations with tools that are more adequate for the kind of systems that they are likely to have to develop and interact with.
We believe that the teaching of mathematics could progressively shift from the set theoretical approach that made it modern some decades ago to one that is centered on interactions.
This is of course a big challenge, mainly because it is not enough for the mathematical Theory to be there, the right way needs to be found for it to be transmitted.
We believe that recent books such as 75 are putting us on a path towards meeting this Challenge, and we hope this book makes it further contribution.
1.2 categories versus sets
4 Universal constructions
we have already hinted to the fact that category Theory provides a totally different approach to the characterization of the given domain of objects, namely to the fact that objects are characterized by their social life, or interactions, as captured by morphisms.
in this chapter, we take this few one step further by showing how certain objects, or constructions, can be characterized in terms of standard relationships that they exhibit with respect to the rest of the universe irrelevant constructions.
It is in this sense that these constructions are usually called Universal.
At the same time we shift our Focus From the social life of individual objects to that of groups or societies interacting objects.
Indeed in this chapter we should have some of the emphasis from the manipulation of objects to that of diagrams as models of complex systems.
Diagrams can be taken as expressions of water often called configurations, be at configurations of running systems as networks of simpler components, the way complex systems or specifications are put together for modules, The Inheritance structures According to which program modules are organized, Etc.
one of our goals with this book is to make the software Community aware that, like in the other domains of Science and Engineering, there are universal laws or dogmas in our area they can manifest themselves in different ways but the unified under a categorical roof.
4.1 initial and terminal objects
at least at First Sight the first Universal constructions that we Define our not so much constructions but identifications of distinguish two objects. What distinguishes them from the other objects or what are usually called Universal properties, term that is associated, and used interchangeably in the literature, with universal Construction.
An object x of a category C is said to be initial if and only if, for every object y of C, there is a unique morphism from x to y.
in set, the initial object is the empty set.
terminal objects
inset, the terminal objects are The Singletons.
1.3.4 software architectures
applications of categorical techniques to the semantics of interfaced description and module interconnection languages were developed by Goguen in the early 1980s [55] and more recently recast in the context of the emerging interest in software architecture [59].
this more recent Trend focuses instead on the organization of the behavior of systems as compositions of components ruled by protocols for communication and synchronization.
This kind of organization is founded on interaction in the behavioral sense, which explains why formalisms like the chemical abstract machine (CHAM) are preferred to the functional flavor of equational logic for the specification of Architectural Components.
category theory is not another semantic domain in which to formalize the description of components and connectors.
Instead, through its Universal constructions, it provides the very semantics of the interconnection, configuration, instantiation and composition, that is that which is related to the gross modular ization of complex systems.
1.3.5
category theory is definitely the mathematics of the internet age and Beyond
2.2 categories
categories provide an abstraction over graphs by making Paths the basic working elements - what are called morphisms, Paths provide richer information about social life than just one-to-one relationships.
categories add two graphs and identity map that converts nodes to morphisms no pads, and a composition law on morphisms internalizes path Construction.
morphism composition is required to be associative as for path concatenation. This means that morphisms have no internal structure that can be derived from the order of composition.
whereas objects and morphisms provide the main elements of the vocabulary that one uses in category Theory, diagrams provide the basic sentences that one can build to express Concepts.
In turn, most properties that one can assert in this language are expressed in terms of commutator of diagrams.
3.2 adding structure
the most typical way of building a new category is, perhaps, by adding structure to the objects of a given category or a subset thereof. The expression "adding structure" has a broad meaning that the reader will only fully apprehend after building a few categories. The morphisms of the new category are then the morphisms of the old category that preserve the additional structure.
The following example
() http://www.fiadeiro.org/jose
Jose Luiz Fiadeiro
) https://repository.royalholloway.ac.uk/file/7e175821-b603-a854-f4f1-26946a520b1f/7/CC_Fiadeiro_paper.pdf
The Many Faces of Complexity in Software Design, Jose Luiz Fiadeiro
) http://www.cs.le.ac.uk/srml/
SRML — A Service Modelling Language
() search: category theory and programming
) http://web.cs.iastate.edu/~lumpe/ComS541/Resources/Lectures/CategoryTheoryAndMonads.pdf
) categories_for_programmers.pdf
) https://yogsototh.github.io/Category-Theory-Presentation/
) http://lambda-the-ultimate.org/node/2604
book: "Conceptual Math" by Lawvere and Schanuel
) http://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf
CATEGORIES TYPES AND STRUCTURES - An Introduction to Category Theory for the working computer scientist, by Andrea Asperti, Giuseppe Longo
) https://johncarlosbaez.wordpress.com/2014/02/05/category-theory-for-better-spreadsheets/
) http://cseweb.ucsd.edu/~goguen/
) http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.4296&rep=rep1&type=pdf
Sheaf Semantics for Concurrent Interacting Objects, Joseph A. Goguen
"The approach is declarative and constraint based , and does not require distinguishing inputs
and outputs. This makes it easy to treat applications such as constraint logic programming and
electrical circuits that are essentially relational , in the sense that they involve finding solutions
for a number of simultaneous relations (which are not just functions); in particular, there may be
more than one solution, or no solution. It seems possible that functional input/output thinking
has held back progress in this area, by making it more difficult to treat systems that involve the
interdependent origination of their observed behaviour. Another goal has been to obtain a general
model theoretic framework, within which general concepts such as deadlock and non-interference
can be defined independent of formalism, and within which a wide variety of approaches can be
compared. It may be worth emphasising that true concurrency can be modeled, and that we are
not at all dependent upon interleaving. In particular, Lilius [34] has shown how to model Petri
nets in our sheaf theoretic framework."
]]></Notes>
<_-.XholonClass>
<!-- domain objects -->
<PhysicalSystem/>
<Block/>
<Brick/>
<!-- quantities -->
<Height superClass="Quantity"/>
</_-.XholonClass>
<xholonClassDetails>
<Block>
<port name="height" connector="Height"/>
</Block>
</xholonClassDetails>
<PhysicalSystem>
<Block>
<Height>0.1 m</Height>
</Block>
<Brick multiplicity="2"/>
</PhysicalSystem>
<Blockbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
var a = 123;
var b = 456;
var c = a * b;
if (console) {
console.log(c);
}
]]></Blockbehavior>
<Heightbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
var myHeight, testing;
var beh = {
postConfigure: function() {
testing = Math.floor(Math.random() * 10);
myHeight = this.cnode.parent();
},
act: function() {
myHeight.println(this.toString());
},
toString: function() {
return "testing:" + testing;
}
}
]]></Heightbehavior>
<Brickbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
$wnd.xh.Brickbehavior = function Brickbehavior() {}
$wnd.xh.Brickbehavior.prototype.postConfigure = function() {
this.brick = this.cnode.parent();
this.iam = " red brick";
};
$wnd.xh.Brickbehavior.prototype.act = function() {
this.brick.println("I am a" + this.iam);
};
]]></Brickbehavior>
<Brickbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
console.log("I'm another brick behavior");
]]></Brickbehavior>
<SvgClient><Attribute_String roleName="svgUri"><![CDATA[data:image/svg+xml,
<svg width="100" height="50" xmlns="http://www.w3.org/2000/svg">
<g>
<title>Block</title>
<rect id="PhysicalSystem/Block" fill="#98FB98" height="50" width="50" x="25" y="0"/>
<g>
<title>Height</title>
<rect id="PhysicalSystem/Block/Height" fill="#6AB06A" height="50" width="10" x="80" y="0"/>
</g>
</g>
</svg>
]]></Attribute_String><Attribute_String roleName="setup">${MODELNAME_DEFAULT},${SVGURI_DEFAULT}</Attribute_String></SvgClient>
</XholonWorkbook>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment