Introducing
Your new presentation assistant.
Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.
Trending searches
Bewl's latest update
20
In the 2.0 DSL:
Topos theory is all about diagrams of (abstract) dots and arrows
dots and arrows are replaced by stars and quivers, which have a richer structure:
- a star is bound to a class
- quivers from STAR[A] to STAR[B] are interchangeable with functions A => B
- product elements are tuples
- exponential elements are functions
This makes the language far more
powerful and expressive!
Sets and functions form a topos, which means:
regarded as an abstract "category" of dots and arrows, they have extra features which let us transform different types of diagram into each other.
A topos is just a more general
workspace in which these
diagram manipulations are possible.
Bewl
a Scala DSL for topos theory
Working with dots and arrows
So, what are these
diagram transformations?
In a category with these 'optional add-ons', the language of diagrams becomes rich enough that you can do serious math.
The DSL then becomes a language for constructions and calculations, operating in a set-like way on things that aren't sets (graphs, monoid actions, fuzzy sets, etc) -
as long as they satisfy the topos axioms.
the category of sets and functions
forms a topos, because it has:
- products
- exponentials
- equalizers
- a truth object
Products
http://github/fdilke/bewl
Given dots A, B, C...
there is a "product dot"
A x B x C ...
such that:
for any object X,
a set of arrows
X -> A, X -> B, X -> C ...
is interchangeable with an arrow
X -> A x B x C ...
The other topos properties are similar
How I improved the DSL,
using some domain modelling and Scala tricks
They enable us to do various manipulations (sleight of hand with diagrams)
which form a sort of machine code powerful enough to define algebraic structures and prove theorems.
Updating the DSL
1.0 was 'diagrammatic'
2.0 is 'intrinsic'
Instead of having to do clunky manipulations with "diagram objects", it's all baked into the DSL
The 1.0 DSL had 'product diagram objects' and 'exponential diagram' objects
Exponentials
These encoded the manipulations you could do with products / exponentials, but were quite awkward to use
Given dots A and B, there is a dot called A ^ B which parameterizes arrows from A to B:
an arrow from X x A -> B
is interchangeable with an arrow
X -> A ^ B