added basic packages data structure

named tuple types

sketch of road to dynamical systems

updated roadmap

resource sharers sketch

ENH: basic @algebraic macro

In order to make symbolic ODEs, we first have to have symbolic functions.

This commit is the first step towards that, introducing the `@algebraic` macro
which makes a DSL for introducing symbolic functions.

These hook into the Julia scope system, so they can conveniently call
other symbolic functions which happen to be in scope.

BUG: return the closure not the method from @algebraic

This is a very small change to the previous commit.

We still need to write some extensive tests for `@algebraic`

rhizome composition initiated

ocompose is written, but we have to make an easy way of
writing down rhizomes before we can test it in any serious way.

Along the way, several useful utilities to work with Tries have been
added.

rhizome macro

oapply for resource sharers works on the happy path!

added docs for resource sharers

started nonemptytrie refactor

more principled approach to empty tries

We want a trie to be uniquely determined by the set of valid TrieVars
that it supports. If we allow there to be empty branches, i.e. corresponding
to the named tuple `(a::(b::()))`, then this has no valid paths in it,
but is different from `()`. To solve this, we make two types: `Trie`
and `NonEmptyTrie`. The recursive case is `NonEmptyTrie`: a `Trie`
is just a wrapper around `Union{Nothing, NonEmptyTrie{A}}`.

This was inspired by the way yuujinchou works.

Also new in this commit is the use of MLStyle active patterns to
make pattern matching on tries cleaner. This is a huge upgrade to the
previous way we were doing things, and I think that we should use more
active patterns in the future throughout GATlab, for pattern matching
on unityped data. See the active patterns Leaf, Node, Empty, Root, Nested
in src/syntax/Tries.jl for more information.

fixup: make more things work for the trie refactor

fixup: add tests and docs for Trie methods

fix: wrapped dot accessor in quotenode

The code `a.b` is represented as a Julia expression by
`Expr(:(.), :a, QuoteNode(:b))`, not `Expr(:(.), :a, :b)`. The former
will produce a undefined variable error because it tries to look up `b`.

fix: move tries to util and include tries tests

fixup: added resource sharers to nonstdlib tests

test: addressed missing coverage for Tries.jl

fix: can't use keys as a variable name at the top level

fix: added orderedcollections to test env

doc+test

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::Trie{AlgebraicFunction})::AlgebraicFunction`, implementing the Trie-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::Trie{Arena})::Arena`, implementing the Trie-algebra structure on objects
+- [ ] Multilenses
+    Sketch:
+    ```julia
+    struct MultiLens
+        inner_boxes::Trie{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::Trie{MultiLens})::MultiLens` implementing the Trie-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::Trie{System})::System` implementing the action of the Trie-multicategory of multilenses on systems.
+
+## Resource sharers
+
+- [ ] Interfaces
+- [ ] Rhizomes (epi-mono uwds)
+    ```julia
+    struct VariableType
+        type::AlgType
+        exposed::Bool
+    end
+
+    struct Rhizome
+        boxes::Trie{Interface}
+        junctions::Trie{VariableType}
+        mapping::Dict{TrieVar, TrieVar}
+    end
+    ```
+
+    Affordances:
+    - `ocompose(r::Rhizome, rs::Trie{Rhizome})::Rhizome`
+
+    In `ocompose`, the names of the junctions in the top-level rhizome dominate.
+- [ ] Systems
+    ```julia
+    struct ResourceSharer
+        variables::Trie{VariableType}
+        params::AlgType
+        output::AlgType
+        # (params, state) -> state
+        update::AlgebraicFunction
+        # (params, state) -> output
+        readout::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - `oapply(r::Rhizome, sharers::Trie{ResourceSharer})::ResourceSharer`
+
+    In `oapply`, variables get renamed to the junctions that they are attached to.

src/models/ModelInterface.jl

@@ -644,12 +644,12 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
   _x = gensym("val")
 
   # Map CODOM sorts to whereparam symbols
-  whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
+  whereparamdict = OrderedDict(s=>gensym(headof(s).name) for s in sorts(codom_theory))
   # New model is parameterized by these types
   whereparams = collect(values(whereparamdict))
   # Julia types of domain sorts determined by theorymap 
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v
-    v => whereparamdict[AlgSort(tmap(v.method).val)]
+    v => whereparamdict[AlgSort(tmap(methodof(v)).val)]
   end)
 
   # Create input for instance_code
@@ -758,13 +758,9 @@ function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrat
   b = bodyof(t)
   if GATs.isvariable(t)
     nameof(b)
-  elseif  GATs.isdot(t)
+  elseif GATs.isdot(t)
     impl = to_call_impl(b.body, theory, mod, migrate)
-    if isnamed(b.head)
-      Expr(:., impl, QuoteNode(nameof(b.head)))
-    else 
-      Expr(:ref, impl, getlid(b.head).val)
-    end
+    Expr(:., impl, QuoteNode(b.head))
   else
     args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
     name = nameof(headof(b))

src/models/SymbolicModels.jl

@@ -328,13 +328,13 @@ end
 
 function internal_accessors(theory::GAT)
   map(theory.sorts) do sort
-    typecon = getvalue(theory[sort.method])
-    map(collect(pairs(theory.accessors[sort.method]))) do (i, acc)
+    typecon = getvalue(theory[methodof(sort)])
+    map(collect(pairs(theory.accessors[methodof(sort)]))) do (i, acc)
       accessor = getvalue(theory[acc])
       return_type = getvalue(typecon[typecon.args[i]])
       JuliaFunction(
         name=esc(nameof(getdecl(accessor))),
-        args=[:(x::$(esc(nameof(sort.head))))],
+        args=[:(x::$(esc(nameof(sort))))],
         return_type = typename(theory, return_type),
         impl=:(x.type_args[$i])
       )
@@ -415,11 +415,11 @@ function symbolic_instance_methods(
   type_con_funs = []
   accessors_funs = []
   for sort in sorts(theory)
-    type_con = getvalue(theory[sort.method])
-    symgen = symbolic_generator(theorymodule, syntaxname, sort.method, type_con, theory)
+    type_con = getvalue(theory[methodof(sort)])
+    symgen = symbolic_generator(theorymodule, syntaxname, methodof(sort), type_con, theory)
     push!(type_con_funs, symgen)
     for binding in argsof(type_con)
-      push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, sort.method, binding))
+      push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, methodof(sort), binding))
     end
   end
 
@@ -614,7 +614,7 @@ function parse_json_sexpr(syntax_module::Module, sexpr;
   theory = theory_module.Meta.theory
   type_lens = Dict(
     nameof(getdecl(getvalue(binding))) => length(getvalue(binding).args)
-    for binding in [theory[sort.method] for sort in sorts(theory)]
+    for binding in [theory[methodof(sort)] for sort in sorts(theory)]
   )
 
   function parse_impl(sexpr::Vector, ::Type{Val{:expr}})