Replacement for GATExpr

docs/src/concepts/models.md

@@ -16,7 +16,7 @@ Given a theory, one can declare a model family for that theory. This consists of
    This can then be applied using, for instance
 
    ```julia
-   checkvalidity(m, Category.Hom(), x, y, f)
+   checkvalidity(m, Category.Hom, x, y, f)
    ```
 
    using the singleton structs defined in [Theories](@ref)

docs/src/index.md

@@ -4,4 +4,26 @@
 CurrentModule = Gatlab
 ```
 
-`Gatlab.jl` is a Julia library for...
+`Gatlab.jl` is a computer algebra system based on Generalized Algebraic Theories.
+
+Roughly speaking, Gatlab consists of two parts. The first part is concerned with *symbolic constructs*. The prototypical symbolic construct is simply a *term*, i.e. a syntax tree. In Gatlab, every term is always relative to a *context*, in which the free variables in that term are typed. And the context and term themselves are relative to an underlying theory, which defines the allowable type and term constructors that can be used in contexts and terms, along with laws that allow one to rewrite terms into equivalent other terms.
+
+We think about a term as a symbolic representation of a function from an assignment of values to the free variables to a value for the term. I.e., the term $x^{2} + y^{2}$ represents the function $\mathbb{R}^2 \to \mathbb{R}$ given by $(x,y) \mapsto x^{2} + y^{2}$. However, Gatlab also supports higher-level symbolic constructs. For instance, we can consider "substitutions" between contexts, which map free variables in one context to terms in another, as [symbolic functions](https://blog.algebraicjulia.org/post/2023/03/algebraic-geometry-1/), and we can consider a collection of equations between terms in a context as a symbolic relation. We can use these building blocks to build [symbolic dynamical systems](https://blog.algebraicjulia.org/post/2023/05/algebraic-geometry-2/) and other things along these lines. Gatlab ensures that all of the manipulation of symbolic constructs is *well-typed*, so that you don't do something like accidently add a vector and a scalar.
+
+The second part of Gatlab is concerned with *computational semantics*. The core of computational semantics is *models* of theories. A model tells you:
+
+- When a Julia value is a valid instance of a type in a theory
+- How to apply term constructors to Julia values
+
+Given a model for a theory, a term in a context, and values for each of the free variables in that context, one can produce a new value by recursively applying the term constructors; this is known as *interpreting* the term. One can also *compile* the term by producing a Julia function that takes as its arguments values for the free variables in the context and then computes the value of the term. This can be faster than interpreting, because one only has to walk the syntax tree at runtime, not compile time. Analogous operations of interpretation and compilation can also be defined for higher level symbolic constructs. Moreover, Gatlab provides facilities for manipulation of *models themselves*. For instance, from a model of a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are `Vector`s of ring elements.
+
+Gatlab is the new backend for [Catlab](https://github.com/AlgebraicJulia/Catlab.jl), and we are currently working to replace the old implementation of GATs with this new one.
+
+There are many programs which have influenced the development of Gatlab, here we just list a few
+
+- [MMT](https://uniformal.github.io/doc/)
+- [Maude](http://maude.cs.illinois.edu/w/index.php/The_Maude_System:About)
+- [Symbolics.jl](https://symbolics.juliasymbolics.org/stable/)
+- [Metatheory.jl](https://github.com/JuliaSymbolics/Metatheory.jl)
+- [Egg](https://egraphs-good.github.ioj/)
+- [Standard ML modules](https://en.wikipedia.org/wiki/Standard_ML)

src/dsl/TheoryMacros.jl

@@ -151,9 +151,17 @@ function parse_rename(rename::Expr)
   end
 end
 
+function using_names(from::Vector, names::Vector)
+  Expr(:using, Expr(:(:), Expr(:(.), from...), Expr.(Ref(:(.)), names)...))
+end
+
+function define_nameof(name::Symbol)
+  :($(GlobalRef(Base, :nameof))(::$name) = $(Expr(:quote, name)))
+end
+
 macro theory(head, body)
-  (name, parent) = @match head begin
-    :($(name::Symbol) <: $(parent::Symbol)) => (name, parent)
+  (name, parent_module) = @match head begin
+    :($(name::Symbol) <: $(parent_module::Symbol)) => (name, parent_module)
     _ => error("expected head of @theory macro to be in the form name <: parent")
   end
   lines = @match body begin
@@ -171,33 +179,68 @@ macro theory(head, body)
       l => push!(judgments, l)
     end
   end
-  parent = macroexpand(__module__, :($parent.@theory()))
+  parent = macroexpand(__module__, :($parent_module.@theory()))
   usings = Tuple{Theory, Dict{Name, Name}}[
     (macroexpand(__module__, :($T.@theory)), renames)
     for (T, renames) in usings
   ]
   precursor = theory_precursor(parent, usings)
   theory = theory_impl(precursor, name, judgments)
+  n = length(parent.judgments)
+  new_judgments = theory.judgments[(n+1):end]
   typ_cons = [
-    (j.name.name, :(struct $(j.name.name) <: $(GlobalRef(Theories, :TypTag)){$i} end))
-    for (i,j) in enumerate(theory.judgments)
-      if (typeof(j.head) == TypCon) && (typeof(j.name) == SymLit)
+    (Symbol(j.name),
+     quote
+       struct $(Symbol(j.name)) <: $(GlobalRef(Theories, :TypTag)){$(n+i)} end
+
+       $(define_nameof(Symbol(j.name)))
+     end)
+    for (i,j) in enumerate(new_judgments)
+      if j.head isa TypCon
   ]
   trm_cons = [
-    (j.name.name, :(struct $(j.name.name) <: $(GlobalRef(Theories, :TrmTag)){$i} end))
-    for (i,j) in enumerate(theory.judgments)
-      if (typeof(j.head) == TrmCon) && (typeof(j.name) == SymLit)
+    (Symbol(j.name),
+     quote
+       struct $(Symbol(j.name)) <: $(GlobalRef(Theories, :TrmTag)){$(n+i)} end
+
+       $(define_nameof(Symbol(j.name)))
+     end)
+    for (i,j) in enumerate(new_judgments)
+      if j.head isa TrmCon
+  ]
+  typ_accessors = [
+    (Symbol(arg),
+     quote
+       struct $(Symbol(arg)) <: $(GlobalRef(Theories, :TypArgTag)){$(n+nj), $narg} end
+
+       $(define_nameof(Symbol(arg)))
+     end)
+    for (nj, j) in enumerate(new_judgments)
+      if j.head isa TypCon
+        for (narg, (arg, _)) in enumerate(j.ctx.ctx)
   ]
-  exports = [first.(typ_cons); first.(trm_cons)]
+  parent_names = exported_names(parent)
   esc(Expr(:toplevel, :(
     module $name
-    export $(exports...)
+    export $(exported_names(theory)...)
+
+    $(using_names([:(.), :(.), parent_module], parent_names))
+
+    module Types
+    $(using_names([:(.), :(.), :(.), parent_module, :Types], parent_names))
     $(last.(typ_cons)...)
     $(last.(trm_cons)...)
+    $(last.(typ_accessors)...)
+    end
+
+    $([:(const $n = Types.$n()) for (n,_) in [typ_cons; trm_cons; typ_accessors]]...)
+
     struct T <: $(GlobalRef(Theories, :AbstractTheory)) end
+
     macro theory()
       $theory
     end
+
     $(GlobalRef(Theories, :gettheory))(::T) = $theory
     end
   )))

src/models/MethodInstance.jl

@@ -11,7 +11,7 @@
   theoryname, theoryparams = parse_theory_binding_either(head)
   theory = macroexpand(__module__, :($theoryname.@theory))
   functions, ext_functions = parse_instance_body(body)
-  esc(instance_code(theory, theoryparams, functions, ext_functions))
+  esc(instance_code(theory, theoryname, theoryparams, functions, ext_functions))
 end 
 
 
@@ -45,7 +45,7 @@
   return (funs, ext_funs)
 end
 
-function instance_code(theory, instance_types, instance_fns, external_fns)
+function instance_code(theory, theoryname, instance_types, instance_fns, external_fns)
   code = Expr(:block)
   typenames = [Symbol(j.name) for j in theory.judgments if j.head isa TypCon]
   bindings = Dict(zip(typenames, instance_types))
@@ -62,7 +62,7 @@
     else
       error("Method $(f.call_expr) not implemented in $(nameof(mod)) instance")
     end
-    push!(code.args, generate_function(f_impl))
+    push!(code.args, generate_function(f_impl; rename=name->:(::$theoryname.Types.$name)))
   end
   return code
 end
@@ -74,7 +74,8 @@
 function interface(T::Theory, j::Judgment, bindings::AbstractDict)::Vector{JuliaFunction}
   h = headof(j)
   getbound(x::Typ) = bindings[Symbol(T[x.head].name)]
-  if h isa Axiom return JuliaFunction[]  
+  if h isa Axiom
+    return JuliaFunction[]
   elseif h isa TrmCon
     args = [Expr(:(::), Symbol(name), getbound(typ)) 
             for (name,typ) in getindex.(Ref(j.ctx), h.args)]
@@ -83,8 +84,10 @@
   elseif h isa TypCon
     map(argsof(h)) do arg 
       argname, argtyp = j.ctx[arg]
-      JuliaFunction(Expr(:call, Symbol(argname), Expr(:(::), bindings[Symbol(j.name)])), 
-      getbound(argtyp))
+      JuliaFunction(
+        Expr(:call, Symbol(argname), Expr(:(::), bindings[Symbol(j.name)])),
+        getbound(argtyp)
+      )
     end
   end
 end 

src/models/SymbolicModels.jl

@@ -0,0 +1,125 @@
+module SymbolicModels
+export GATExpr, @symbolic_model
+
+using ...Syntax
+
+using Base.Meta: ParseError
+using MLStyle
+
+abstract type GATExpr{T} end
+
+"""
+module FreeCategory
+export Ob,Hom
+using ..__module__
+
+theory() = ThCategory
+
+struct Ob{T} <: ObExpr{T}
+  args::Vector
+  type_args::Vector{GATExpr}
+end
+
+struct Hom{T} <: HomExpr{T}
+  args::Vector
+  type_args::Vector{GATExpr}
+end
+
+function (::typeof(ThCategory.dom))(x::Hom)::Ob
+  x.type_args[1]
+end
+
+function Ob(::Typ{Ob}, __value__::Any)::Ob
+  Ob{:generator}([__value__], [])
+end
+
+function (::typeof(ThCategory.id))(A::Ob)::Hom
+  Hom{:id}([A], [A, A])
+end
+
+end # module
+
+function (::typeof(ThCategory.Hom))(x1::Any, x2::FreeCategory.Ob, x3::FreeCategory.Ob)::FreeCategory.Hom
+  FreeCategory.Hom(x1, x2, x3)
+end
+"""
+
+
+function typname(theory::Theory, typ::Typ)
+  Symbol(theory[typ.head].name)
+end
+
+function symbolic_struct(name, abstract_type, parentmod)::Expr
+  quote
+    struct $(esc(name)){T} <: $parentmod.$(abstract_type){T}
+      args::$(Vector)
+      type_args::$(Vector){$(GlobalRef(SymbolicModels, :GATExpr))}
+    end
+  end
+end
+
+function symbolic_structs(theory::Theory, abstract_types, parentmod)::Vector{Expr}
+  Expr[
+    symbolic_struct(Symbol(j.name), abstract_type, parentmod)
+    for (j, abstract_type) in zip(typcons(theory), abstract_types)
+  ]
+end
+
+function symbolic_accessor(theoryname, argname, typname, rettypname, argindex, parentmod)
+  quote
+    function (::$(typeof)($parentmod.$theoryname.$(Symbol(argname))))(x::$(esc(typname)))::$(esc(rettypname))
+      x.type_args[$argindex]
+    end
+  end
+end
+
+function symbolic_accessors(theoryname, theory::Theory, parentmod)::Vector{Expr}
+  Expr[
+    symbolic_accessor(theoryname, argname, Symbol(j.name), typname(theory, argtyp), argindex, parentmod)
+    for j in typcons(theory) for (argindex, (argname, argtyp)) in enumerate(j.ctx.ctx)
+  ]
+end
+
+function symbolic_constructor(theoryname, j, theory, parentmod)
+  quote
+    function (::$(typeof)($parentmod.$theoryname.$(Symbol(j.name))))(
+      $([Expr(:(::), Symbol(:x, i), esc(typname(theory, j.ctx[idx][2]))) for (i, idx) in enumerate(j.head.args)]...)
+    )
+      $(esc(typname(theory, j.head.typ))){$(Expr(:quote, Symbol(j.name)))}(
+        $(Expr(:vect, [Symbol(:x, i) for i in 1:length(j.head.args)]...)),
+        $(Vector){$(GlobalRef(SymbolicModels, :GATExpr))}()
+      )
+    end
+  end
+end
+
+function symbolic_constructors(theoryname, theory::Theory, parentmod)::Vector{Expr}
+  Expr[symbolic_constructor(theoryname, judgment, theory, parentmod) for judgment in trmcons(theory)]
+end
+
+macro symbolic_model(decl, theoryname, body)
+  theory = macroexpand(__module__, :($theoryname.@theory))
+  (name, abstract_types) = @match decl begin
+    Expr(:curly, name, abstract_types...) => (name, abstract_types)
+    _ => throw(ParseError("Ill-formed head of @symbolic_model $decl"))
+  end
+
+  structs = symbolic_structs(theory, abstract_types, __module__)
+
+  accessors = symbolic_accessors(theoryname, theory, __module__)
+
+  constructors = symbolic_constructors(theoryname, theory, __module__)
+
+  Expr(:toplevel,
+    :(module $(esc(name))
+      using ..($(nameof(__module__)))
+      $(structs...)
+
+      $(accessors...)
+
+      $(constructors...)
+    end)
+  )
+end
+
+end

src/models/module.jl

@@ -6,10 +6,12 @@ include("ModelInterface.jl")
 include("Interpret.jl")
 include("MethodInstance.jl")
 include("AugmentedTheories.jl")
+include("SymbolicModels.jl")
 
 @reexport using .ModelInterface
 @reexport using .Interpret
 @reexport using .MethodInstance
 @reexport using .AugmentedTheories
+@reexport using .SymbolicModels
 
 end

src/stdlib/models/SimpleLenses.jl

@@ -174,25 +174,25 @@ end
 
 const SimpleArena = Impl.Arena
 
-Categories.compose(f::SimpleKleisliLens{T}, g::SimpleKleisliLens{T}) where {T<:AbstractTheory} =
-  SimpleKleisliLens{T}(
-    f.dom,
-    g.codom,
-    Impl.compose(
-      f.dom,
-      f.codom,
-      g.codom,
-      f.morphism,
-      g.morphism
-    )
-  )
-
-Monoidal.mcompose(f::SimpleKleisliLens{T}, g::SimpleKleisliLens{T}) where {T<:AbstractTheory} =
-  SimpleKleisliLens{T}(
-    Impl.mcompose(f.dom, g.dom),
-    Impl.mcompose(f.codom, g.codom),
-    Impl.mcompose(f.dom, g.dom, f.codom, g.codom, f.morphism, g.morphism)
-  )
+# ThCategory.compose(f::SimpleKleisliLens{T}, g::SimpleKleisliLens{T}) where {T<:AbstractTheory} =
+#   SimpleKleisliLens{T}(
+#     f.dom,
+#     g.codom,
+#     Impl.compose(
+#       f.dom,
+#       f.codom,
+#       g.codom,
+#       f.morphism,
+#       g.morphism
+#     )
+#   )
+
+# Monoidal.mcompose(f::SimpleKleisliLens{T}, g::SimpleKleisliLens{T}) where {T<:AbstractTheory} =
+#   SimpleKleisliLens{T}(
+#     Impl.mcompose(f.dom, g.dom),
+#     Impl.mcompose(f.codom, g.codom),
+#     Impl.mcompose(f.dom, g.dom, f.codom, g.codom, f.morphism, g.morphism)
+#   )
 
 function Base.show(io::IO, l::SimpleKleisliLens{T}) where {T<:AbstractTheory}
   theory = gettheory(T)

src/stdlib/models/SliceCategories.jl

@@ -15,16 +15,16 @@
   over::Ob
 
   Ob(x::SliceOb{Ob, Hom}) =
-    checkvalidity(self.cat, ThCategory.Ob(), x.ob) &&
-    checkvalidity(self.cat, ThCategory.Hom(), x.ob, self.over, x.hom)
+    checkvalidity(self.cat, ThCategory.Ob, x.ob) &&
+    checkvalidity(self.cat, ThCategory.Hom, x.ob, self.over, x.hom)
 
   Hom(x::SliceOb{Ob, Hom}, y::SliceOb{Ob, Hom}, f::Hom) =
-    checkvalidity(self.cat, ThCategory.Hom(), x.ob, y.ob, f) &&
-    ap(self.cat, ThCategory.compose(), x.ob, y.ob, self.over, f, y.hom) == x.hom
+    checkvalidity(self.cat, ThCategory.Hom, x.ob, y.ob, f) &&
+    ap(self.cat, ThCategory.compose, x.ob, y.ob, self.over, f, y.hom) == x.hom
 
-  id(x::SliceOb{Ob, Hom}) = ap(self.cat, ThCategory.id(), x.ob)
+  id(x::SliceOb{Ob, Hom}) = ap(self.cat, ThCategory.id, x.ob)
 
-  compose(x, y, z, f, g) = ap(self.cat, ThCategory.compose(), x.ob, y.ob, z.ob, f, g)
+  compose(x, y, z, f, g) = ap(self.cat, ThCategory.compose, x.ob, y.ob, z.ob, f, g)
 end
 
 end