(press s
for speaker notes)
3/6/24
I. Future of software engineering
II. Mini examples of the future paradigm
III. Intuition for how structural mathematics works
This starts feeling repetitive.
This feels repetitive insofar as we feel the problem classes are related.
Common abstractions are things like functions / datatypes / scripts in our language.
Future paradigm: mathematically-principled + automatic abstraction reuse
Understand structure of the abstraction + implementation + the relationship between them.
New problem expressed in terms of old problem.
"""Modify to allow it to overlap existing vertex IDs"""
function triangle!(graph, v1=nothing, v2=nothing, v3=nothing)
vs = map([v1=>"B", v2=>"R", v3=>"Y"]) do (v, color)
isnothing(v) ? add_vertex!(graph, color) : v
end
[add_edge!(graph, vs[i]...) for i in [1:2,2:3,[3,1]]]
vs
end
"""Now expressible as an abstraction of `triangle!`"""
function big_tri!(graph)
blue, red, _ = triangle!(graph)
_, _, yellow = triangle!(graph, blue)
triangle!(graph, nothing, red, yellow)
end
"""Modify to allow it to overlap existing vertex IDs"""
function triangle!(graph, v1=nothing, v2=nothing, v3=nothing)
vs = map([v1=>"B", v2=>"R", v3=>"Y"]) do (v, color)
isnothing(v) ? add_vertex!(graph, color) : v
end
[add_edge!(graph, vs[i]...) for i in [1:2,2:3,[3,1]]]
vs
end
"""Now expressible as an abstraction of `triangle!`"""
function big_tri!(graph)
blue, red, _ = triangle!(graph)
_, _, yellow = triangle!(graph, blue)
triangle!(graph, nothing, red, yellow)
end
AlgebraicJulia
"""Modify to allow it to overlap existing vertex IDs"""
function triangle!(graph, v1=nothing, v2=nothing, v3=nothing)
vs = map([v1=>"B", v2=>"R", v3=>"Y"]) do (v, color)
isnothing(v) ? add_vertex!(graph, color) : v
end
[add_edge!(graph, vs[i]...) for i in [1:2,2:3,[3,1]]]
vs
end
"""Now expressible as an abstraction of `triangle!`"""
function big_tri!(graph)
blue, red, _ = triangle!(graph)
_, _, yellow = triangle!(graph, blue)
triangle!(graph, nothing, red, yellow)
end
AlgebraicJulia
New problem expressed in terms of old problem.
prepend(pre) = s -> pre * "_" * s
US, EU, E, W =
prepend.(["US", "EU", "east", "west"])
function mult_EU(petri::PetriNet)
res = PetriNet()
for state in petri.S
us = add_state!(res, US(state))
eu = add_state!(res, EU(state))
add_transition!(res, E(state), [us]=>[eu])
add_transition!(res, W(state), [eu]=>[us])
end
for (T, (I, O)) in petri.T
add_transition!(res, US(T), US.(I)=>US.(O))
add_transition!(res, EU(T), EU.(I)=>EU.(O))
end
res
end
function multiply(r1::PetriNet, r2::PetriNet)
res = PetriNet()
for (s1, s2) in Iterators.product(r1.S, r2.S)
add_state!(res, "$(s1)_$(s2)")
end
for rx1 in r1.T
for s2 in r2.S
add_transition!(res, rename_rxn(rx1, s2))
end
end
for rx2 in r2.T
for s1 in r1.S
add_transition!(res, rename_rxn(rx2, s1))
end
end
RxnNet(rs)
end
rename_rxn(rxn, species::Symbol) = # TODO
prepend(pre) = s -> pre * "_" * s
US, EU, E, W =
prepend.(["US", "EU", "east", "west"])
function mult_EU(petri::PetriNet)
res = PetriNet()
for state in petri.S
us = add_state!(res, US(state))
eu = add_state!(res, EU(state))
add_transition!(res, E(state), [us]=>[eu])
add_transition!(res, W(state), [eu]=>[us])
end
for (T, (I, O)) in petri.T
add_transition!(res, US(T), US.(I)=>US.(O))
add_transition!(res, EU(T), EU.(I)=>EU.(O))
end
res
end
function multiply(r1::PetriNet, r2::PetriNet)
res = PetriNet()
for (s1, s2) in Iterators.product(r1.S, r2.S)
add_state!(res, "$(s1)_$(s2)")
end
for rx1 in r1.T
for s2 in r2.S
add_transition!(res, rename_rxn(rx1, s2))
end
end
for rx2 in r2.T
for s1 in r1.S
add_transition!(res, rename_rxn(rx2, s1))
end
end
RxnNet(rs)
end
rename_rxn(rxn, species::Symbol) = # TODO
prepend(pre) = s -> pre * "_" * s
US, EU, E, W =
prepend.(["US", "EU", "east", "west"])
function mult_EU(petri::PetriNet)
res = PetriNet()
for state in petri.S
us = add_state!(res, US(state))
eu = add_state!(res, EU(state))
add_transition!(res, E(state), [us]=>[eu])
add_transition!(res, W(state), [eu]=>[us])
end
for (T, (I, O)) in petri.T
add_transition!(res, US(T), US.(I)=>US.(O))
add_transition!(res, EU(T), EU.(I)=>EU.(O))
end
res
end
function multiply(r1::PetriNet, r2::PetriNet)
res = PetriNet()
for (s1, s2) in Iterators.product(r1.S, r2.S)
add_state!(res, "$(s1)_$(s2)")
end
for rx1 in r1.T
for s2 in r2.S
add_transition!(res, rename_rxn(rx1, s2))
end
end
for rx2 in r2.T
for s1 in r1.S
add_transition!(res, rename_rxn(rx2, s1))
end
end
RxnNet(rs)
end
rename_rxn(rxn, species::Symbol) = # TODO
New problem expressed in terms of old problem.
\(\Rightarrow\)
\(\Rightarrow\)
AlgebraicJulia
New problem expressed in terms of old problem.
New problem expressed in terms of old problem.
"""Species and transitions are vertices.
Inputs and outputs are edges."""
function petri_to_graph(p::PetriNet)
grph = Graph()
vs = Dict(s => add_vertex!(grph) for s in p.S)
for (t, (i, o)) in pairs(p.T)
t = add_vertex!(grph)
for eᵢ in i
add_edge!(grph, vs[eᵢ], t)
end
for eₒ in o
add_edge!(grph, t, vs[eₒ])
end
end
grph
end
Common theme: writing code vs declaring relationships between abstractions.
Problem | Julia solution | AlgebraicJulia solution |
---|---|---|
Different pieces of a model need to be glued together. | Write a script which does the gluing or modifies how pieces are constructed. | Declare how overlap relates to the building blocks. (colimits) |
Different aspects of a model need to be combined / a distinction is needed. | Write a script which creates copies of one aspect for every part of the other aspect. | Declare how the different aspects interact with each other. (limits) |
We want to integrate systems at different levels of granularity. | Refactor the original code to incorporate the more detailed subsystem. | Separate syntax/semantics. Declare how the part relates to the whole at syntax level. (operads) |
We make a new assumption and want to migrate old knowledge into our new understanding. | Write a script to convert old data into updated data. | Declare how the new way of seeing the world (i.e. schema) is related to the old way. (data migration) |
Informal definition: a category is a bunch of things that are related to each other
Key intuition: category theory is concerned with universal properties.
Consider mathematical sets which are related to each other via functions.
Definition in terms of internal properties
The empty set is the unique set which has no elements in it.
But if we we look at how the empty set relates to all the other sets, we’ll eventually notice something about these relations.
Definition in terms of external relationships (universal properties)
The empty set is the unique set which has exactly one function into every other set.
Consider colored graphs related to each other via vertex mappings which preserve color and edges.
Definition in terms of internal properties
The empty graph uniquely has no vertices nor edges in it.
But if we we look at how it relates to all the other graphs, we’ll eventually notice something characteristic.
Definition in terms of external relationships (universal properties)
The empty graph is the unique graph which has exactly one graph mapping into every other graph.
Category theory enforces good conceptual hygeine - one isn’t allowed to depend on “implementation details” of the things which feature in its definitions.
This underlies the ability of models built in AlgebraicJulia to be extended and generalized without requiring messy code refactor.
CT is useful for the same reason interfaces are generally useful.
In particular, CT provides generalized1 notions of:
These abstractions all fit very nicely with each other:
We can use them to replace a large amount of our code with high level, conceptual data.
Mission: to shape technology for public benefit by advancing sciences of connection and integration.
Three pillars of our work, from theory to practice to social impact:
Topos Institute is a 501(c)(3) non-profit organization
"""Define the multiphysics"""
Diffusion = @decapode DiffusionQuantities begin
C::Form0{X}
ϕ::Form1{X}
ϕ == k(d₀{X}(C)) # Fick's first law
end
Advection = @decapode DiffusionQuantities begin
C::Form0{X}
(V, ϕ)::Form1{X}
ϕ == ∧₀₁{X}(C,V)
end
Superposition = @decapode DiffusionQuantities begin
(C, Ċ)::Form0{X}
(ϕ, ϕ₁, ϕ₂)::Form1{X}
ϕ == ϕ₁ + ϕ₂
Ċ == ⋆₀⁻¹{X}(dual_d₁{X}(⋆₁{X}(ϕ)))
∂ₜ{Form0{X}}(C) == Ċ
end
compose_diff_adv = @relation (C, V) begin
diffusion(C, ϕ₁)
advection(C, ϕ₂, V)
superposition(ϕ₁, ϕ₂, ϕ, C)
end
"""Assign semantics to operators"""
funcs = sym2func(mesh)
funcs[:k] = Dict(:operator => 0.05 * I(ne(mesh)),
:type => MatrixFunc())
funcs[:⋆₁] = Dict(:operator => ⋆(Val{1}, mesh,
hodge=DiagonalHodge()), :type => MatrixFunc());
funcs[:∧₀₁] = Dict(:operator => (r, c, v) -> r .=
∧(Tuple{0,1}, mesh, c, v), :type => InPlaceFunc())
Focuses on relationships between things without talking about the things themselves.
Invented in the 1940’s to connect different branches of math.
A category consists of objects and morphisms (arrows).
CT studies certain shapes of combinations of arrows.
Compare to interfaces in computer science:
In some sense a category is just a particular interface.
CT is also the study of interfaces in general. It knows which are good ones.