ARCHIVED
We started again in Rust: https://github.com/homotopy-io/homotopy-rs.
Build instructions
- install
purescript
compiler and spago
build tool:
nix-shellcan do this for you with the providedshell.nix- alternatively, both of these dependencies can be installed with
npm install -g purescript spago
- run
spago buildin the core and webclient directories
Tooling
purty is used to format the code in
this repository, and this is incorporated as a git
pre-commit
hook (please install with git config core.hooksPath .githooks).
purescript-language-server provides IDE-like features via the Language Server Protocol. Among other features, this provides facilities to:
- trigger builds (e.g.\ on save) --- this is vastly preferred to running
spago build;- diagnostics information (warnings, errors) resulting from the build are passed back to the editor
- apply compiler suggestions to fix warnings;
- provide autocompletion of symbols from installed packages;
- automatically adding the corresponding
importline afterwards
- automatically adding the corresponding
- provide information about a symbol on hover (type, documentation);
- provide refactoring tools;
- auto-insert case splits.
Data structure overview
In this library, we encode zigzags in the Diagram type:
data Diagram
= Diagram0 Generator
| DiagramN DiagramN
newtype DiagramN
= InternalDiagram { source :: Diagram, cospans :: List Cospan }Diagram is a sum type which distinguishes between $0$-dimensional diagrams
and $>0$-dimensional diagrams. A $0$-dimensional diagram is merely a
Generator (an element of the signature), whereas for $n >0$, a
$n$-dimensional diagram is given by its source boundary (A $n-1$-dimensional
diagram), and a list of Cospans:
type Cospan
= { forward :: Rewrite, backward :: Rewrite }
data Rewrite
= Rewrite0 { source :: Generator, target :: Generator }
| RewriteI
| RewriteN { dimension :: Int, cones :: List Cone }
type Cone
= { index :: Int
, source :: List Cospan
, target :: Cospan
, slices :: List Rewrite
}A Cospan encodes a cospan comprising of:
- a singular level $sᵢ$ --- the tip of the cospan;
- zigzag maps $rᵢ \xrightarrow{\texttt{forward}} sᵢ \xleftarrow{\texttt{backward}} r_{i+1}$.
Rewrite similarly encodes maps between diagrams (zigzag maps), with identity
rewrites being represented by RewriteI. A rewrite between $0$-dimensional
diagrams simply maps Generators to Generators (Rewrite0). A
$>0$-dimensional rewrite (RewriteN) is a non-trivial zigzag map, which is
sparsely encoded as a list of Cones.
Recall that in general, a zigzag map $f\colon Z → Z′$ is given by:
- a monotone function from the singular levels of $Z$ to the singular levels of $Z′$;
- built from morphisms of $𝒞$ (if we are working in the category $Z_𝒞$ --- zigzags of $𝒞$);
- identities between regular levels;
- such that all squares commute.
A Cone is a sparse encoding of the monotone functions between singular
levels. Suppose that we have a monotone function from a linearly ordered set
with $m$ elements (denoted $[m]$) to one with $n$ elements: $[m]
\xrightarrow{f} [n]$; this can be decomposed into a sequence of Cones as follows:
An example
Let us see how we can encode the following string diagram:
When an $n$-dimensional diagram is projected onto 2D, the $n$-cells are represented as vertices, the $n-1$-cells as edges, and the $n-2$-cells as faces. Supposing that this string diagram is 2D, this means that we have might have a signature comprising of the following:
- $0$-cells: a single $0$-cell representing the regions, which we will name “Space”;
- $1$-cells: a single $1$-cell representing the wires, $\text{Space} \xrightarrow{\text{Wire}} \text{Space}$;
- $2$-cells:
- for the monoid, a $2$-cell $\text{Wire} ⊗ \text{Wire} → \text{Wire}$;
- for the comonoid, a $2$-cell $\text{Wire} → \text{Wire} ⊗ \text{Wire}$;
- for the scalar, a $2$-cell $\text{Identity}(\text{Space}) → \text{Identity}(\text{Space})$.
In the data structure, this is represented as:
-- first, we fix generators for each cell
spaceG = Generator { id: 0, dimension: 0 }
wireG = Generator { id: 1, dimension: 1 }
monoidG = Generator { id: 2, dimension: 2 }
comonoidG = Generator { id: 3, dimension: 2 }
scalarG = Generator { id: 4, dimension: 2 }
endomorphismG = Generator { id: 5, dimension: 2 }
-- 0-diagrams
space = Diagram0 spaceG :: Diagram
-- 1-diagrams
wire = fromGenerator space space wireG :: DiagramN
-- InternalDiagram
-- { source: space
-- , cospans:
-- { forward: Rewrite0 { source: spaceG, target: wireG }
-- , backward: Rewrite0 { source: spaceG, target: wireG }
-- } : Nil
-- }
wire⊗wire = attach Target Nil wire wire :: Maybe DiagramN
-- Just $ InternalDiagram
-- { source: space
-- , cospans:
-- { forward: Rewrite0 { source: spaceG, target: wireG }
-- , backward: Rewrite0 { source: spaceG, target: wireG }
-- } :
-- { forward: Rewrite0 { source: spaceG, target: wireG }
-- , backward: Rewrite0 { source: spaceG, target: wireG }
-- } : Nil
-- }
-- 2-diagrams
monoid = fromGenerator (DiagramN $ fromJust $ wire⊗wire) (DiagramN wire) monoidG :: DiagramN
-- InternalDiagram
-- { source: (DiagramN $ fromJust $ wire⊗wire)
-- , cospans: { forward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: monoidG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: monoidG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: monoidG
-- })
-- : (Rewrite0 { source: wireG
-- , target: monoidG
-- })
-- : Nil
-- } : Nil
-- }
-- , backward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: monoidG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: monoidG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: monoidG
-- }) : Nil
-- } : Nil
-- }
-- } : Nil
-- }
comonoid = fromGenerator (DiagramN wire) (DiagramN $ fromJust $ wire⊗wire) comonoidG :: DiagramN
-- InternalDiagram
-- { source: (DiagramN $ wire)
-- , cospans: { forward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: comonoidG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: comonoidG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: comonoidG
-- })
-- : Nil
-- } : Nil
-- }
-- , backward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: comonoidG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: comonoidG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: comonoidG
-- })
-- : (Rewrite0 { source: wireG
-- , target: comonoidG
-- })
-- : Nil
-- } : Nil
-- }
-- } : Nil
-- }
scalar = fromGenerator (DiagramN $ identity space) (DiagramN $ identity space) scalarG :: DiagramN
-- InternalDiagram
-- { source: (DiagramN $ identity space)
-- , cospans: { forward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: scalarG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: scalarG
-- }
-- }
-- , slices: Nil
-- } : Nil
-- }
-- , backward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: scalarG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: scalarG
-- }
-- }
-- , slices: Nil
-- } : Nil
-- }
-- } : Nil
-- }
endomorphism = fromGenerator (DiagramN wire) (DiagramN wire) endomorphismG :: DiagramN
-- InternalDiagram
-- { source: (DiagramN $ wire)
-- , cospans: { forward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: endomorphismG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: endomorphismG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: endomorphismG
-- })
-- : Nil
-- } : Nil
-- }
-- , backward: RewriteN { dimension: 1
-- , cones: { index: 0
-- , source: { forward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: wireG
-- }
-- } : Nil
-- , target: { forward: Rewrite0 { source: spaceG
-- , target: endomorphismG
-- }
-- , backward: Rewrite0 { source: spaceG
-- , target: endomorphismG
-- }
-- }
-- , slices: (Rewrite0 { source: wireG
-- , target: endomorphismG
-- })
-- : Nil
-- } : Nil
-- }
-- } : Nil
-- }With a couple of imports, this can be tested in the repl (spago repl), and
the output can be examined to give something similar to the Pseudo-PureScript
in the comments.
Let's unpack what is going on here.
-
First, we defined a bunch of
Generators, which are essentially names (with an additionaldimensionfield) which will be bound to diagrams. -
The 0-diagram
spaceis fully determined by giving it a generator of dimension 0:spaceG, with theDiagram0constructor. -
The
wire1-diagram is constructed with thefromGeneratorfunction, and has type $\text{Space} \xrightarrow{\text{Wire}} \text{Space}$ (domain is the first argument tofromGenerator, while codomain is the second argument; the third argument is the generator we wish to bind to the resulting diagram). Internally, this gets represented as aDiagramN; it specifies asourcediagram and a list ofcospanswhich rewrite fromsourceto target. With respect to zigzags, thewire1-diagram is represented as
and this precisely corresponds to the singleton
Cospaninwire's list ofcospans, with the left arrow being theforwardcomponent and the right arrow thebackward. Just as aDiagram0is fairly trivial, aRewrite0is a fairly trivial (i.e.\ no information) relationship betweenGenerators.The other 1-diagram we need to represent is
wire⊗wire(as it is the source of the monoid, and target of the comonoid). With zigzags, it is represented as so
The only difference is that its list of
cospansis length two, instead of one. -
The monoid zigzag has one singular height, and two regular heights, looking like this:
The
sourceof this diagram iswire⊗wire, and it only contains a singleCospan(depicted vertically); however, in this case, theforwardandbackwardcomponents are not 0-dimensional rewrites. Higher dimensional rewrites are encoded by a list ofCones, which is a sparse encoding.The
forwardrewrite is depicted by the red arrows, and comprises of a single (red) cone. Theindexparameter of the cone identifies its starting position along the X-axis. Thesourceparameter identifies what is replaced bytarget, by the rewrites in theslicesparameter; the length of thesourcelist should equal that of thesliceslist, and the $i$-th index ofslicesacts on the $i$-th index ofsourceto encode the zigzag map --- observe that the firstsliceof theforwardcomponent is the left red arrow, and the secondsliceis the right one.The
backwardrewrite is similar (the only difference being it goes from a regular height to the preceding singular height), and is denoted in blue. Finally, in the zigzag formalism, there are identities between regular-regular heights, denoted in green; these are not represented explicitly in this encoding.For this particular example, no space has been saved by the sparse
Coneencoding (but it will help significantly in larger diagrams).The comonoid diagram is similar, and the scalar zigzag looks like this:
The endomorphism diagram looks like this:
Putting it together
We can identify the regular and singular levels of the big diagram:
This 2D-diagram should be captured by DiagramN, which has two constructors:
source :: Diagram--- in this instance, a 1D-diagram, which is the zigzag corresponding to $[3]$ along the bottom of the figure;cospans :: List Cospan--- this encodes rewriting to the target, i.e.\ the forward and backward rewrites vertically along the right of the figure.