Refactor of AlgTerm/AlgType to use good sumtypes

.editorconfig

@@ -0,0 +1,2 @@
+[*.jl]
+indent_size = 2

.gitignore

@@ -26,3 +26,4 @@ docs/site/
 # committed for packages, but should be committed for applications that require a static
 # environment.
 Manifest.toml
+/coverage/

Project.toml

@@ -4,13 +4,15 @@ authors = ["AlgebraicJulia Developers"]
 version = "0.1.3"
 
 [deps]
+AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"
 AlgebraicInterfaces = "23cfdc9f-0504-424a-be1f-4892b28e2f0c"
 Colors = "5ae59095-9a9b-59fe-a467-6f913c188581"
 Crayons = "a8cc5b0e-0ffa-5ad4-8c14-923d3ee1735f"
 DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078"
 Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a"
+OrderedCollections = "bac558e1-5e72-5ebc-8fee-abe8a469f55d"
 Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
 Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"

docs/src/concepts/theory_composition.md

@@ -0,0 +1,51 @@
+# Theory Composition
+
+As theories get larger, it becomes more and more important to not build the
+entire theory from scratch. Not only is this tedious, it is also error-prone.
+From the beginning, Catlab and GATlab have supported single inheritance, which
+helps to some extent. In this document, we lay out other approaches to composing
+theories.
+
+## Multiple Inheritance
+
+In a GATlab `@theory`, one can use `using` to take the *union* of one theory
+with another theory.
+
+The way this works is the following. Every time a new theory is created, the new
+definitions for that theory form a new scope, with a unique UUID. Union of
+theories operates on a scope tag level, taking the union of the sets of UUIDs
+and then producing a theory with all the bindings from the scopes tagged by
+those UUIDs.
+
+If we never had to parse user-supplied expressions, then the names of the
+operations in the theories wouldn't matter, because identifiers come with scope
+tags. However, as a practical matter, we disallow unioning two theories with the
+same name declaration.
+
+That being said, it is fine to union two theories which *overload* the same
+declaration. That is, if two theories have the declaration of a name in common,
+then they can overload that name as long as they don't give conflicting
+overloads, in the same way that overloading methods in Julia works.
+
+This is akin to the way multiple inheritance works in frameworks such as
+
+- Haskell typeclasses
+- [Object-oriented systems with multiple inheritance, like Scala](https://docs.scala-lang.org/scala3/book/domain-modeling-tools.html#traits)
+- [Module inclusion in OCaml](https://cs3110.github.io/textbook/chapters/modules/includes.html)
+
+## Nesting
+
+However, there are other ways of composing things like GATlab theories. In
+dependently typed languages used for theorem proving, algebraic structures are
+often represented by dependent records. For instance, in the agda unimath
+library, the [definition of a group](https://github.com/UniMath/agda-unimath/blob/master/src/group-theory/groups.lagda.md) is
+
+```agda
+Semigroup :
+  (l : Level) → UU (lsuc l)
+Semigroup l = Σ (Set l) has-associative-mul-Set
+
+Group :
+  (l : Level) → UU (lsuc l)
+Group l = Σ (Semigroup l) is-group
+```

docs/src/examples/springs.md

@@ -0,0 +1,5 @@
+# Composition of resource sharers
+
+```julia
+
+```

docs/src/nonstdlib/resource_sharers.md

@@ -0,0 +1,9 @@
+# Resource Sharers
+
+```@docs
+GATlab.NonStdlib.ResourceSharers.Rhizome
+GATlab.NonStdlib.ResourceSharers.ResourceSharer
+GATlab.NonStdlib.ResourceSharers.Variable
+GATlab.NonStdlib.ResourceSharers.PortVariable
+GATlab.NonStdlib.ResourceSharers.ocompose
+```

dynamics.md

@@ -0,0 +1,111 @@
+# The Road to Dynamical Systems
+
+## Basic steps
+
+- [x] Tuple types
+- [-] Symbolic functions
+    Data type:
+
+    ```julia
+    struct AlgebraicFunction
+        theory::GAT
+        args::TypeScope
+        ret::AlgType
+        body::AlgTerm
+    end
+    ```
+
+    Affordances:
+    - [x] DSL for writing down functions, composing, etc.
+    - [ ] A function `tcompose(t::Dtry{AlgebraicFunction})::AlgebraicFunction`, implementing the Dtry-algebra structure on morphisms
+    - [ ] Interpret/compile a symbolic function into a real function
+    - [ ] Serialize symbolic functions
+- [ ] Compilation
+- [ ] Serialization
+
+## Lens-based dynamical systems
+
+- [ ] Arenas
+    Sketch:
+    ```julia
+    struct Arena
+        in::AlgType
+        out::AlgType
+    end
+    ```
+
+    Affordances:
+    - A function `tcompose(arena::Dtry{Arena})::Arena`, implementing the Dtry-algebra structure on objects
+- [ ] Multilenses
+    Sketch:
+    ```julia
+    struct MultiLens
+        inner_boxes::Dtry{Arena}
+        outer_box::Arena
+        # used for namespacing `params` in composition, must not overlap with `inner_boxes`
+        name::Symbol 
+        params::AlgType
+        # (params, tcompose(inner_boxes[...].out)) -> outer_box.out
+        output::AlgebraicFunction
+        # (params, tcompose(inner_boxes[...].out), outer_box.in) -> tcompose(inner_boxes[...].in)
+        update::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - A function `ocompose(l::MultiLens, args::Dtry{MultiLens})::MultiLens` implementing the Dtry-multicategory structure
+- [ ] Systems
+    Sketch:
+    ```julia
+    struct System
+        interface::Arena
+        state::AlgType
+        params::AlgType
+        # (params, state) -> interface.out
+        output::AlgebraicFunction
+        # (params, state, interface.in) -> state
+        input::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - A function `oapply(l::MultiLens, args::Dtry{System})::System` implementing the action of the Dtry-multicategory of multilenses on systems.
+
+## Resource sharers
+
+- [ ] Interfaces
+- [ ] Rhizomes (epi-mono uwds)
+    ```julia
+    struct VariableType
+        type::AlgType
+        exposed::Bool
+    end
+
+    struct Rhizome
+        boxes::Dtry{Interface}
+        junctions::Dtry{VariableType}
+        mapping::Dict{DtryVar, DtryVar}
+    end
+    ```
+
+    Affordances:
+    - `ocompose(r::Rhizome, rs::Dtry{Rhizome})::Rhizome`
+
+    In `ocompose`, the names of the junctions in the top-level rhizome dominate.
+- [ ] Systems
+    ```julia
+    struct ResourceSharer
+        variables::Dtry{VariableType}
+        params::AlgType
+        output::AlgType
+        # (params, state) -> state
+        update::AlgebraicFunction
+        # (params, state) -> output
+        readout::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - `oapply(r::Rhizome, sharers::Dtry{ResourceSharer})::ResourceSharer`
+
+    In `oapply`, variables get renamed to the junctions that they are attached to.