diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index 32a83766..7d7f3027 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-03-27T21:55:02","documenter_version":"1.3.0"}} \ No newline at end of file +{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-04-23T23:29:58","documenter_version":"1.4.0"}} \ No newline at end of file diff --git a/dev/api/index.html b/dev/api/index.html index a0c97316..a7abfd80 100644 --- a/dev/api/index.html +++ b/dev/api/index.html @@ -1,7 +1,7 @@ -Library Reference · GATlab.jl
GitHub

Library Reference

Syntax

GATlab.Syntax.Scopes.Context — Type

A Context is anything which contains an ordered list of scopes.

Scopes within a context are referred to by level, which is their index within this list.

Contexts should overload:

  • getscope(c::Context, level::Int) -> Scope
  • nscopes(c::Context) -> Int
  • hastag(c::Context, tag::ScopeTag) -> Bool
  • hasname(c::Context, name::Symbol) -> Bool
  • getlevel(c::Context, tag::ScopeTag) -> Int
  • getlevel(c::Context, name::Symbol) -> Int
  • alltags(c::Context) -> Set{ScopeTag}
source
GATlab.Syntax.Scopes.Ident — Type

Ident

An identifier.

tag refers to the scope that this Ident is bound in lid indexes the scope that Ident is bound in name is an optional field for the sake of printing. A variable in a scope might be associated with several names

source
GATlab.Syntax.Scopes.LID — Type

A LID (Local ID) indexes a given scope.

Currently, scopes assign LIDs sequentially – this is not a stable guarantee however, and in theory scopes could have "sparse" LIDs.

source
GATlab.Syntax.Scopes.Scope — Type

Scope{T}

In GATlab, we handle shadowing with a notion of scope. Names shadow between scopes. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. For example, here is a scope with 3 elements:

x = 3
+Library Reference · GATlab.jl
GitHub
Library Reference
Syntax
GATlab.Syntax.Scopes.Context — Type
A Context is anything which contains an ordered list of scopes.
Scopes within a context are referred to by level, which is their index within this list.
Contexts should overload:
  • getscope(c::Context, level::Int) -> Scope
  • nscopes(c::Context) -> Int
  • hastag(c::Context, tag::ScopeTag) -> Bool
  • hasname(c::Context, name::Symbol) -> Bool
  • getlevel(c::Context, tag::ScopeTag) -> Int
  • getlevel(c::Context, name::Symbol) -> Int
  • alltags(c::Context) -> Set{ScopeTag}
source
GATlab.Syntax.Scopes.Ident — Type
Ident
An identifier.
tag refers to the scope that this Ident is bound in lid indexes the scope that Ident is bound in name is an optional field for the sake of printing. A variable in a scope might be associated with several names
source
GATlab.Syntax.Scopes.LID — Type
A LID (Local ID) indexes a given scope.
Currently, scopes assign LIDs sequentially – this is not a stable guarantee however, and in theory scopes could have "sparse" LIDs.
source
GATlab.Syntax.Scopes.Scope — Type
Scope{T}
In GATlab, we handle shadowing with a notion of scope. Names shadow between scopes. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. For example, here is a scope with 3 elements:
x = 3
 y = "hello"
-z = x 
Here z is introduced as an alias for x. It is illegal to shadow within a scope. Overloading is not explicitly treated but can be managed by having values which  refer to identifiers earlier / the present scope. See GATs.jl, for example.
source
GATlab.Syntax.Scopes.hasident — Method
hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
source
GATlab.Syntax.Scopes.ident — Method
ident creates an Ident from a context and some partial data supplied as keywords.
Keywords arguments:
  • tag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.
  • name::Union{Symbol, Nothing}. The name of the identifier.
  • lid::Union{LID, Nothing}. The lid of the identifier within its scope.
  • level::Union{Int, Nothing}. The level of the scope within the context.
  • strict::Bool. If strict is true, throw an error if not found, else return nothing.
source
GATlab.Syntax.Scopes.rename — Method
rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T
Recurse through the structure of x, and change any name n in scope tag to get(replacements, n, n). Overload this function on structs that have names in them.
source
GATlab.Syntax.Scopes.retag — Method
retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T
Recurse through the structure of x, swapping any instance of a ScopeTag t with get(replacements, t, t). Overload this function on structs that have ScopeTags within them.
source
GATlab.Syntax.GATs.AlgAccessor — Type
AlgAccessor
The arguments to a term constructor serve a dual function as both arguments and also methods to extract the value of those arguments.
I.e., declaring Hom(dom::Ob, codom::Ob)::TYPE implicitly overloads a previous declaration for dom and codom, or creates declarations if none previously exist.
source
GATlab.Syntax.GATs.AlgDeclaration — Type
AlgDeclaration
A declaration of a constructor; constructor methods in the form of AlgTermConstructors or the accessors for AlgTypeConstructors follow later in the theory.
source
GATlab.Syntax.GATs.AlgFunction — Type
A shorthand for a function, such as "square(x) := x * x".  It is relevant for  models but can be ignored by theory maps, as it is fully determined by other  judgments in the theory.
source
GATlab.Syntax.GATs.AlgSorts — Type
AlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
source
GATlab.Syntax.GATs.AlgStruct — Type
AlgStruct
A declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor  which constructs an element of that type, and projection term constructors. E.g.
struct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]
+z = x 
Here z is introduced as an alias for x. It is illegal to shadow within a scope. Overloading is not explicitly treated but can be managed by having values which  refer to identifiers earlier / the present scope. See GATs.jl, for example.
source
GATlab.Syntax.Scopes.hasident — Method
hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
source
GATlab.Syntax.Scopes.ident — Method
ident creates an Ident from a context and some partial data supplied as keywords.
Keywords arguments:
  • tag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.
  • name::Union{Symbol, Nothing}. The name of the identifier.
  • lid::Union{LID, Nothing}. The lid of the identifier within its scope.
  • level::Union{Int, Nothing}. The level of the scope within the context.
  • strict::Bool. If strict is true, throw an error if not found, else return nothing.
source
GATlab.Syntax.Scopes.rename — Method
rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T
Recurse through the structure of x, and change any name n in scope tag to get(replacements, n, n). Overload this function on structs that have names in them.
source
GATlab.Syntax.Scopes.retag — Method
retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T
Recurse through the structure of x, swapping any instance of a ScopeTag t with get(replacements, t, t). Overload this function on structs that have ScopeTags within them.
source
GATlab.Syntax.GATs.AlgAccessor — Type
AlgAccessor
The arguments to a term constructor serve a dual function as both arguments and also methods to extract the value of those arguments.
I.e., declaring Hom(dom::Ob, codom::Ob)::TYPE implicitly overloads a previous declaration for dom and codom, or creates declarations if none previously exist.
source
GATlab.Syntax.GATs.AlgDeclaration — Type
AlgDeclaration
A declaration of a constructor; constructor methods in the form of AlgTermConstructors or the accessors for AlgTypeConstructors follow later in the theory.
source
GATlab.Syntax.GATs.AlgFunction — Type
A shorthand for a function, such as "square(x) := x * x".  It is relevant for  models but can be ignored by theory maps, as it is fully determined by other  judgments in the theory.
source
GATlab.Syntax.GATs.AlgSorts — Type
AlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
source
GATlab.Syntax.GATs.AlgStruct — Type
AlgStruct
A declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor  which constructs an element of that type, and projection term constructors. E.g.
struct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]
   apex::Ob
   i1::dom->apex
   i2::codom->apex
@@ -22,14 +22,14 @@
   ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
 
 cospan(apex(csp), i1(csp), i2(csp)) == csp
-  ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]
source
GATlab.Syntax.GATs.GAT — Type
GAT
A generalized algebraic theory. Essentially, just consists of a name and a list of GATSegments, but there is also some caching to make access faster. Specifically, there is a dictionary to map ScopeTag to position in the list of segments, and there are lists of all of the identifiers for term constructors, type constructors, and axioms so that they can be iterated through faster.
GATs allow overloading but not shadowing.
source
GATlab.Syntax.GATs.GATContext — Type
GATContext
A context consisting of two parts: a GAT and a TypeCtx
Certain types (like AlgTerm) can only be parsed in a GATContext, because they require access to the method resolving in the GAT.
source
GATlab.Syntax.GATs.GATSegment — Type
GATSegment
A piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.
This is a struct rather than just a type alias so that we can customize the show method.
source
GATlab.Syntax.GATs.MethodApp — Type
MethodApp
An application of a method of a constructor to arguments. We need a type parameter T because AlgTerm hasn't been defined yet, but the only type used for T will in fact be AlgTerm.
method either points to an AlgTermConstructor, an AlgTypeConstructor or an AlgAccessor,
source
GATlab.Syntax.GATs.MethodResolver — Type
MethodResolver
Right now, this just maps a sort signature to the resolved method.
When we eventually support varargs, this will have to do something slightly fancier.
source
GATlab.Syntax.GATs.TypeScope — Type
TypeScope
A scope where variables are assigned to AlgTypes. We use a wrapper here so that it pretty prints as [a::B] instead of {a => AlgType(B)}
source
GATlab.Syntax.GATs.equations — Method
Implicit equations defined by a context.
This function allows a generalized algebraic theory (GAT) to be expressed as an essentially algebraic theory, i.e., as partial functions whose domains are defined by equations.
References:
  • (Cartmell, 1986, Sec 6: "Essentially algebraic theories and categories with  finite limits")
  • (Freyd, 1972, "Aspects of topoi")
This function gives expressions for computing the elements of c.context   which can be inferred from applying accessor functions to elements of args.
Example:
equations({f::Hom(a,b), g::Hom(b,c)}, {a::Ob, b::Ob, c::Ob}, ThCategory)
waysofcomputing = Dict(a => [dom(f)], b => [codom(f), dom(g)], c => [codom(g)],                          f => [f], g => [g])
source
GATlab.Syntax.GATs.normalize_judgment — Method
This is necessary because the intuitive precedence rules for the symbols that we use do not match the Julia precedence rules. In theory, this could be written with some algorithm that recalculates precedence, but I am too lazy to write that, so instead I just special case everything.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgTerm)
Throw an error if a the head of an AlgTerm (which refers to a term constructor) has arguments of the wrong sort. Returns the sort of the term.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgType)
Throw an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.
source
GATlab.Syntax.GATs.GAT — Type
GAT
A generalized algebraic theory. Essentially, just consists of a name and a list of GATSegments, but there is also some caching to make access faster. Specifically, there is a dictionary to map ScopeTag to position in the list of segments, and there are lists of all of the identifiers for term constructors, type constructors, and axioms so that they can be iterated through faster.
GATs allow overloading but not shadowing.
source
GATlab.Syntax.GATs.GATContext — Type
GATContext
A context consisting of two parts: a GAT and a TypeCtx
Certain types (like AlgTerm) can only be parsed in a GATContext, because they require access to the method resolving in the GAT.
source
GATlab.Syntax.GATs.GATSegment — Type
GATSegment
A piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.
This is a struct rather than just a type alias so that we can customize the show method.
source
GATlab.Syntax.GATs.MethodApp — Type
MethodApp
An application of a method of a constructor to arguments. We need a type parameter T because AlgTerm hasn't been defined yet, but the only type used for T will in fact be AlgTerm.
method either points to an AlgTermConstructor, an AlgTypeConstructor or an AlgAccessor,
source
GATlab.Syntax.GATs.MethodResolver — Type
MethodResolver
Right now, this just maps a sort signature to the resolved method.
When we eventually support varargs, this will have to do something slightly fancier.
source
GATlab.Syntax.GATs.TypeScope — Type
TypeScope
A scope where variables are assigned to AlgTypes. We use a wrapper here so that it pretty prints as [a::B] instead of {a => AlgType(B)}
source
GATlab.Syntax.GATs.equations — Method
Implicit equations defined by a context.
This function allows a generalized algebraic theory (GAT) to be expressed as an essentially algebraic theory, i.e., as partial functions whose domains are defined by equations.
References:
  • (Cartmell, 1986, Sec 6: "Essentially algebraic theories and categories with  finite limits")
  • (Freyd, 1972, "Aspects of topoi")
This function gives expressions for computing the elements of c.context   which can be inferred from applying accessor functions to elements of args.
Example:
equations({f::Hom(a,b), g::Hom(b,c)}, {a::Ob, b::Ob, c::Ob}, ThCategory)
waysofcomputing = Dict(a => [dom(f)], b => [codom(f), dom(g)], c => [codom(g)],                          f => [f], g => [g])
source
GATlab.Syntax.GATs.normalize_judgment — Method
This is necessary because the intuitive precedence rules for the symbols that we use do not match the Julia precedence rules. In theory, this could be written with some algorithm that recalculates precedence, but I am too lazy to write that, so instead I just special case everything.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgTerm)
Throw an error if a the head of an AlgTerm (which refers to a term constructor) has arguments of the wrong sort. Returns the sort of the term.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgType)
Throw an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.
source
GATlab.Syntax.ExprInterop.toexpr — Function
toexpr(c::Context, t) -> Any
Converts GATlab syntax into an Expr that can be read in via fromexpr to get the same thing. Crucially, the output of this will depend on the order of the scopes in c, and if read back in with a different c may end up with different results.
source
Models
GATlab.Models.ModelInterface.implements — Method
implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
source
GATlab.Models.ModelInterface.qualify_function — Method
Add WithModel param first, if this is not an old instance (it shouldn't have it already) Qualify method name to be in theory module Qualify args to struct types Add context kwargs if not already present
source
GATlab.Syntax.TheoryMaps.migrator — Method
Given a Theory Morphism T->U and a model Mᵤ which implements U, obtain a model Mₜ which wraps Mᵤ and is a model of T.
Future work: There is some subtlety in how accessor functions should be handled. TODO: The new instance methods do not yet handle the context keyword argument.
source
GATlab.Syntax.ExprInterop.toexpr — Function
toexpr(c::Context, t) -> Any
Converts GATlab syntax into an Expr that can be read in via fromexpr to get the same thing. Crucially, the output of this will depend on the order of the scopes in c, and if read back in with a different c may end up with different results.
source
Models
GATlab.Models.ModelInterface.implements — Method
implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
source
GATlab.Models.ModelInterface.qualify_function — Method
Add WithModel param first, if this is not an old instance (it shouldn't have it already) Qualify method name to be in theory module Qualify args to struct types Add context kwargs if not already present
source
GATlab.Syntax.TheoryMaps.migrator — Method
Given a Theory Morphism T->U and a model Mᵤ which implements U, obtain a model Mₜ which wraps Mᵤ and is a model of T.
Future work: There is some subtlety in how accessor functions should be handled. TODO: The new instance methods do not yet handle the context keyword argument.
source
GATlab.Models.ModelInterface.@instance — Macro
Usage:
struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
   ntypes::Int
 end
 
@@ -50,7 +50,7 @@
 end
 
 @instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
-end
source
GATlab.Models.SymbolicModels.GATExpr — Type
Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.
We define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)
The concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.
source
Base.nameof — Method
Get name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
source
GATlab.Models.SymbolicModels.functor — Method
Functor from GAT expression to GAT instance.
Strictly speaking, we should call these "structure-preserving functors" or, better, "model homomorphisms of GATs". But this is a category theory library, so we'll go with the simpler "functor".
A functor is completely determined by its action on the generators. There are several ways to specify this mapping:
  1. Specify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.
  2. Explicitly map each generator term to an instance value, using the generators dictionary.
  3. For each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.
The terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.
FIXME
source
GATlab.Models.SymbolicModels.@symbolic_model — Macro
@symbolic_model generates the free model of a theory, generated by symbols.
This is backwards compatible with the @syntax macro in Catlab.
One way of thinking about this is that for every type constructor, we add an additional term constructor that builds a "symbolic" element of that type from any Julia value. This term constructor is called "generator".
An invocation of @symbolic_model creates the following.
  1. A module with a struct for each type constructor, which has a single type
parameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.
For instance, in the theory of categories, we might have the following elements.
using .FreeCategory
+end
source
GATlab.Models.SymbolicModels.GATExpr — Type
Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.
We define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)
The concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.
source
Base.nameof — Method
Get name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
source
GATlab.Models.SymbolicModels.functor — Method
Functor from GAT expression to GAT instance.
Strictly speaking, we should call these "structure-preserving functors" or, better, "model homomorphisms of GATs". But this is a category theory library, so we'll go with the simpler "functor".
A functor is completely determined by its action on the generators. There are several ways to specify this mapping:
  1. Specify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.
  2. Explicitly map each generator term to an instance value, using the generators dictionary.
  3. For each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.
The terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.
FIXME
source
GATlab.Models.SymbolicModels.@symbolic_model — Macro
@symbolic_model generates the free model of a theory, generated by symbols.
This is backwards compatible with the @syntax macro in Catlab.
One way of thinking about this is that for every type constructor, we add an additional term constructor that builds a "symbolic" element of that type from any Julia value. This term constructor is called "generator".
An invocation of @symbolic_model creates the following.
  1. A module with a struct for each type constructor, which has a single type
parameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.
For instance, in the theory of categories, we might have the following elements.
using .FreeCategory
 x = Ob{:generator}([:x], [])
 y = Ob{:generator}([:y], [])
 f = Hom{:generator}([:f], [x, y])
@@ -111,4 +111,4 @@
 
 function ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)
   associate_unit(FreeCategory.compose(f, g; strict), id)
-end
source
Utilities

+end
source

Utilities

diff --git a/dev/concepts/catlab_differences/index.html b/dev/concepts/catlab_differences/index.html index 22a4f262..2c1d7223 100644 --- a/dev/concepts/catlab_differences/index.html +++ b/dev/concepts/catlab_differences/index.html @@ -1,4 +1,4 @@ Changes from Catlab GATs · GATlab.jl
GitHub

Changes from Catlab GATs

GATlab is a refactoring of the core GAT system from Catlab versions older than 0.16. There are three main differences between the GATlab GAT system and the Catlab GAT system, in addition to a variety of new features enabled by these differences.

However, GATlab has a full backward compatibility layer with the GAT system as used to be used in Catlab; the new features are mostly only opt-in.

1. Models as values

Instances (or models) of GATs in Catlab worked on a system analogous to Haskell type classes. That is, given a type and a GAT, that type could be involved in at most one instance of the GAT. However, there are many, many categories that have, for instance, integers as objects. The way to fix this was to make lots of "newtype" wrappers, like

struct FinSetInt
   n::Int
-end

This is not ideal, but the larger problem is that this made it difficult to have models of a GAT that were parameterized by other models, because there was no way of referring to a particular model. So constructions like slice categories, dual categories, or cospan categories were not easy to do.

In GATlab, we instead do models of GATs in a more "Standard ML" style. That is, each model is a value that can be passed around dynamically. Then the implementations of the GAT term constructors are attached via multiple dispatch to that value. In simple cases, that value might be the unique instance of a zero-field struct, but more generally there could be more data inside the value, as is the case for slice categories. If the struct has fields, then we can think of it like a "functor" in ML parlance (which has little to do with the standard categorical use of the word functor); i.e. it is a parameterized model of the theory.

Sometimes we refer to this by "categories as contexts", because the category (i.e., the model of the theory of categories) serves as a context for disambiguating which method to use, and this is a pun off of the famous category theory book "Categories in Context" by Emily Riehl.

2. E-Graphs

An e-graph is a data structure used to store congruence relations on a collections of terms. A congruence relation is an equivalence relation with the property that if $x_{i} \sim x_{i}'$, then $f(x_{1},\ldots,x_{n}) \sim f(x_{1}',\ldots,x_{n}')$ for any term constructor $f$. E-graphs are used for a variety of purposes, including:

  • finding simple representations of terms
  • deciding whether two terms are equal

The syntax systems we use for GATs in GATlab are built from the ground-up to be compatible with a purpose-built e-graph implementation. This allows us to make use of the axioms in a GAT to rewrite terms and perform equational reasoning.

Additionally, it allows us to perform a weak form of typechecking. Fully general typechecking in a GAT is undecidable, as types may depend on terms and term equality is certainly undecidable. However, we can typecheck "up to" the collection of equivalences that we have recorded in an e-graph. Any well-typed term can be typechecked using this procedure by first placing the necessary equalities in the e-graph and then running the type-checking algorithm. Moreover, whenever this algorithm finds a positive result, one can be sure that the term does in fact typecheck. This is analogous to the termination-checking in proof assistants; we circumvent undecidability by putting the burden on the user to give us some additional data to show that their program is valid. And in many circumstances, very little additional data is required. For instance, in the bare theory of categories, there are no term constructors that produce objects. So checking whether two objects are equal in a presentation of a category is a simple problem of computing an equivalence relation (instead of a congruence relation). Thus, typechecking is very easy in this circumstance.

3. Indexed dependent types in models

A morphism between the finite sets $\{1,\ldots,n\}$ and $\{1,\ldots,m\}$ is simply a length-$n$ vector whose entries are in $\{1,\ldots,m\}$. However, in Catlab we cannot make a model of the theory of categories which has Vector{Int} as its type for morphisms. This is because we require an implementation of dom and codom to have a model, and it is not possible to infer the size of the codomain from a Vector{Int}.

Mathematically, this can be interpreted as a requirement that models of GATs interpret the dependent types as fibered. I.e. the dependent type Hom(a::Ob,b::Ob) gets interpreted as a Julia type Hom with functions dom, codom from Hom to Ob.

The practical downside to this is that if you want to store several morphisms that have the same domain/codomain, you have to redundantly store the domain and codomain. So although a C-set consists of a collection of objects and morphisms in FinSet, we do not actually define it in this way in Catlab, because we don't want to redundantly store the objects in each morphism.

In GATlab, we fix this in the following way. When you declares a model in GATlab, you associate types to it that correspond to the "bare" data. E.g., we would just associate Vector{Int} to Hom in an implementation of FinSet. Then various methods expect you to pass in the domain and codomain of a morphism in addition to the data of the morphism, rather than assuming that you can infer the domain and codomain from the data.

Mathematically, we interpret this by saying that we interpret the dependent types as indexed. That is, we assign a set to each pair of objects, and those sets can intersect. I.e., Hom(a,b) could intersect non-trivially Hom(c,d). So whenever we handle a morphism, we need external data that tells us what the domain and codomain is.

Notice that from such an implementation, we can automatically derive a wrapper type which contains domain, codomain, and data. But we can't go the other way; we can't automatically "pick out" what is data and what is just recording domain/codomain from the fibered implementation.

Although mathematically, fibered and indexed dependent types are equivalent, they have different implementations, and we hope that the indexed point of view will end up being more natural for our purposes.

+end

This is not ideal, but the larger problem is that this made it difficult to have models of a GAT that were parameterized by other models, because there was no way of referring to a particular model. So constructions like slice categories, dual categories, or cospan categories were not easy to do.

In GATlab, we instead do models of GATs in a more "Standard ML" style. That is, each model is a value that can be passed around dynamically. Then the implementations of the GAT term constructors are attached via multiple dispatch to that value. In simple cases, that value might be the unique instance of a zero-field struct, but more generally there could be more data inside the value, as is the case for slice categories. If the struct has fields, then we can think of it like a "functor" in ML parlance (which has little to do with the standard categorical use of the word functor); i.e. it is a parameterized model of the theory.

Sometimes we refer to this by "categories as contexts", because the category (i.e., the model of the theory of categories) serves as a context for disambiguating which method to use, and this is a pun off of the famous category theory book "Categories in Context" by Emily Riehl.

2. E-Graphs

An e-graph is a data structure used to store congruence relations on a collections of terms. A congruence relation is an equivalence relation with the property that if $x_{i} \sim x_{i}'$, then $f(x_{1},\ldots,x_{n}) \sim f(x_{1}',\ldots,x_{n}')$ for any term constructor $f$. E-graphs are used for a variety of purposes, including:

The syntax systems we use for GATs in GATlab are built from the ground-up to be compatible with a purpose-built e-graph implementation. This allows us to make use of the axioms in a GAT to rewrite terms and perform equational reasoning.

Additionally, it allows us to perform a weak form of typechecking. Fully general typechecking in a GAT is undecidable, as types may depend on terms and term equality is certainly undecidable. However, we can typecheck "up to" the collection of equivalences that we have recorded in an e-graph. Any well-typed term can be typechecked using this procedure by first placing the necessary equalities in the e-graph and then running the type-checking algorithm. Moreover, whenever this algorithm finds a positive result, one can be sure that the term does in fact typecheck. This is analogous to the termination-checking in proof assistants; we circumvent undecidability by putting the burden on the user to give us some additional data to show that their program is valid. And in many circumstances, very little additional data is required. For instance, in the bare theory of categories, there are no term constructors that produce objects. So checking whether two objects are equal in a presentation of a category is a simple problem of computing an equivalence relation (instead of a congruence relation). Thus, typechecking is very easy in this circumstance.

3. Indexed dependent types in models

A morphism between the finite sets $\{1,\ldots,n\}$ and $\{1,\ldots,m\}$ is simply a length-$n$ vector whose entries are in $\{1,\ldots,m\}$. However, in Catlab we cannot make a model of the theory of categories which has Vector{Int} as its type for morphisms. This is because we require an implementation of dom and codom to have a model, and it is not possible to infer the size of the codomain from a Vector{Int}.

Mathematically, this can be interpreted as a requirement that models of GATs interpret the dependent types as fibered. I.e. the dependent type Hom(a::Ob,b::Ob) gets interpreted as a Julia type Hom with functions dom, codom from Hom to Ob.

The practical downside to this is that if you want to store several morphisms that have the same domain/codomain, you have to redundantly store the domain and codomain. So although a C-set consists of a collection of objects and morphisms in FinSet, we do not actually define it in this way in Catlab, because we don't want to redundantly store the objects in each morphism.

In GATlab, we fix this in the following way. When you declares a model in GATlab, you associate types to it that correspond to the "bare" data. E.g., we would just associate Vector{Int} to Hom in an implementation of FinSet. Then various methods expect you to pass in the domain and codomain of a morphism in addition to the data of the morphism, rather than assuming that you can infer the domain and codomain from the data.

Mathematically, we interpret this by saying that we interpret the dependent types as indexed. That is, we assign a set to each pair of objects, and those sets can intersect. I.e., Hom(a,b) could intersect non-trivially Hom(c,d). So whenever we handle a morphism, we need external data that tells us what the domain and codomain is.

Notice that from such an implementation, we can automatically derive a wrapper type which contains domain, codomain, and data. But we can't go the other way; we can't automatically "pick out" what is data and what is just recording domain/codomain from the fibered implementation.

Although mathematically, fibered and indexed dependent types are equivalent, they have different implementations, and we hope that the indexed point of view will end up being more natural for our purposes.

diff --git a/dev/concepts/models/index.html b/dev/concepts/models/index.html index 83d11789..2387eedb 100644 --- a/dev/concepts/models/index.html +++ b/dev/concepts/models/index.html @@ -1,2 +1,2 @@ -Models and instances · GATlab.jl
GitHub

Models and instances

A model is any julia value m that satisfies m :: Model. A model may implement one or more theories; to check if a model m is implements a theory Th, one can run implements(m, Th), which returns nothing if m does not implement Th, and returns an ImplementationNotes struct if m does implement Th.

When a model m implements Th, the following methods should be defined.

  1. For every type constructor X in Th

    Th.X[m::typeof(m)](x, args...) = ...

    This attempts to coerce x into a valid element of the type constructor X applied to args args..., and throws an error if this is not possible.

    For instance, ThCategory.Hom[FinSetC()](xs::Vector{Int}, dom::Int, codom::Int) returns xs if and only if length(xs) == dom and all(1 .<= xs .<= codom), and otherwise errors.

    This is syntactic sugar (via an overload of Base.getindex(::typeof(ThCategory.Hom), ::Model)) for calling ThCategory.Hom(TheoryInterface.WithModel(FinSetC()), xs, dom, codom). The reason that we do not simply have ThCategory.Hom(FinSetC(), xs, dom, codom) is a long story; essentially it has to do with maintaining compatibility with Catlab. But one advantage of this is that you can define Hom = ThCategory.Hom[FinSetC()], and then use that locally.

  2. For each argument a to a type constructor (i.e. dom and codom for Hom), an overload of

    Th.a[m::typeof(m)](x) = ...

    This opportunistically attempts to retrieve the type argument for x. For instance, ThCategory.dom[FinSetC()]([1,2,3]) = 3. However, this may return an error, as for instance ThCategory.codom[FinSetC()]([1,2,3]) is uncertain; it could be a morphism into any n >= 3. This is because morphisms don't have to know their domain and codomain.

  3. For each term constructor f in Theory

    Th.f[m::typeof(m)](args...) = ...

    This applies the term constructor to arguments that are assumed to be a valid type (i.e., they have previously been coerced by the type constructors). For instance,

    ThCategory.compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]

    Term constructors sometimes need to know the values of elements of their context that are not arguments. For instance, compose(f::Hom(A,B), g::Hom(B,C)) might need access to the values of A, B or C, which might not be able to be inferred from f and g. In this case, we support passing a named tuple called context to provide these additional values, named with their variables names in the theory. So for instance, we would allow ThCategory.compose[FinSetC()]([1,3,2], [1,3,2]; (;B=3)). It is rare that this is needed, however.

In order to make a model implement a theory, one can either manually implement all of the methods, or use the @instance macro. You can see examples of using the @instance macro in src/stdlib/models.

+Models and instances · GATlab.jl
GitHub

Models and instances

A model is any julia value m that satisfies m :: Model. A model may implement one or more theories; to check if a model m is implements a theory Th, one can run implements(m, Th), which returns nothing if m does not implement Th, and returns an ImplementationNotes struct if m does implement Th.

When a model m implements Th, the following methods should be defined.

  1. For every type constructor X in Th

    Th.X[m::typeof(m)](x, args...) = ...

    This attempts to coerce x into a valid element of the type constructor X applied to args args..., and throws an error if this is not possible.

    For instance, ThCategory.Hom[FinSetC()](xs::Vector{Int}, dom::Int, codom::Int) returns xs if and only if length(xs) == dom and all(1 .<= xs .<= codom), and otherwise errors.

    This is syntactic sugar (via an overload of Base.getindex(::typeof(ThCategory.Hom), ::Model)) for calling ThCategory.Hom(TheoryInterface.WithModel(FinSetC()), xs, dom, codom). The reason that we do not simply have ThCategory.Hom(FinSetC(), xs, dom, codom) is a long story; essentially it has to do with maintaining compatibility with Catlab. But one advantage of this is that you can define Hom = ThCategory.Hom[FinSetC()], and then use that locally.

  2. For each argument a to a type constructor (i.e. dom and codom for Hom), an overload of

    Th.a[m::typeof(m)](x) = ...

    This opportunistically attempts to retrieve the type argument for x. For instance, ThCategory.dom[FinSetC()]([1,2,3]) = 3. However, this may return an error, as for instance ThCategory.codom[FinSetC()]([1,2,3]) is uncertain; it could be a morphism into any n >= 3. This is because morphisms don't have to know their domain and codomain.

  3. For each term constructor f in Theory

    Th.f[m::typeof(m)](args...) = ...

    This applies the term constructor to arguments that are assumed to be a valid type (i.e., they have previously been coerced by the type constructors). For instance,

    ThCategory.compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]

    Term constructors sometimes need to know the values of elements of their context that are not arguments. For instance, compose(f::Hom(A,B), g::Hom(B,C)) might need access to the values of A, B or C, which might not be able to be inferred from f and g. In this case, we support passing a named tuple called context to provide these additional values, named with their variables names in the theory. So for instance, we would allow ThCategory.compose[FinSetC()]([1,3,2], [1,3,2]; (;B=3)). It is rare that this is needed, however.

In order to make a model implement a theory, one can either manually implement all of the methods, or use the @instance macro. You can see examples of using the @instance macro in src/stdlib/models.

diff --git a/dev/concepts/scopes/index.html b/dev/concepts/scopes/index.html index edffdf69..bccd7cb2 100644 --- a/dev/concepts/scopes/index.html +++ b/dev/concepts/scopes/index.html @@ -1,2 +1,2 @@ -Scopes · GATlab.jl
GitHub

Scopes

Design rationale:

Namespacing, i.e. references which look like britain.economy.GDP, should be first class. This doesn't play nicely with the internal representation of names via deBruijn levels; we don't want to do a bunch of math to convert between flattened and nested versions of contexts. Conceptually, we should then switch our identifiers to be lists of deBruijn levels.

But there are also significant subtleties in the translation between named and nameless representations of identifiers. Also in practice if we are referencing something that might change over time, like a C-set, we don't want to use deBruijn levels, because we don't want have to change all of our identifiers when we delete something, so in the rest of this I will instead say "local identifier" instead of deBruijn level to refer to a nameless representation of an identifier.

(the name "local identifier" and also some of this philosophy is taken from chit)

In general, naming is given by a relation between symbols and bindings (as refered to by local identifiers). Each binding may be associated with zero or more symbols, and each symbol might be associated with zero or more bindings.

We name the failure of this relation to be a bijection in several ways.

  • If more than one symbol is related to a single binding, we say that this

binding has aliases. In this case, we should also have a primary alias used as a default.

  • If more than one binding is related to a single symbol, we have name overlap.

Name overlap can be resolved by overloading and shadowing, we will talk about this later on.

  • If no symbol is related to a binding, such as when the binding is created

programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.

  • If no binding is related to a symbol, then we have a name error; this name

is not valid in the current context and we must throw an error.

The most important thing to get right is name overlap; we discuss this first.

There are two ways in which to resolve name overlap. The first way is via overloading. In overloading, we disambiguate an ambiguous name via its context, for instance what type it is expected to be, or what arguments is it receiving. The second way is via shadowing. In shadowing, a name is resolved by making it point to the "most recently defined" thing with that name.

In GATlab, we handle overloading and shadowing with a notion of scope. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. Each scope is identified with a ScopeTag, which is an opaque identifier (i.e. a UUID). We take this idea from Racket, but we don't need the more complex "scope sets" from Racket because GATs don't need to process the syntax of other GATs; if we start doing this we'll have to rethink the design, but we'll probably have bigger problems too.

Two variables with the same name within a single scope are meant to overload one another. For instance, this is what happens with mcompose in the theory of monoidal categories; it is overloaded for Hom and Ob, and this is what happens with d in the discrete exterior calculus; it is overloaded for all of the (k+1)-forms. Variables in different scopes with the same name shadow one another. When we parse an expression a + b, we do so in an ordered list of scopes, and the most recent scope "wins".

Parsing turns a Symbol into an Ident. The Ident contains the original Symbol for printing, but it also contains a reference to a scope via ScopeTag, and an local identifier ("lid") within that scope. Thus, the name in the Ident is never needed for later stages of programatic manipulation.

Scopes cache the relation between names and bindings, by providing a way to go from binding (as reified by local identifier) to a set of aliases with distinguished primary alias, and to go from name to the set of bindings that have that name that we need to disambiguate between in the case of an overload.

Because Idents are fully unambiguous even without their name, it is also possible to create an Ident with no name, which solves the problem of nameless references.

+Scopes · GATlab.jl
GitHub

Scopes

Design rationale:

Namespacing, i.e. references which look like britain.economy.GDP, should be first class. This doesn't play nicely with the internal representation of names via deBruijn levels; we don't want to do a bunch of math to convert between flattened and nested versions of contexts. Conceptually, we should then switch our identifiers to be lists of deBruijn levels.

But there are also significant subtleties in the translation between named and nameless representations of identifiers. Also in practice if we are referencing something that might change over time, like a C-set, we don't want to use deBruijn levels, because we don't want have to change all of our identifiers when we delete something, so in the rest of this I will instead say "local identifier" instead of deBruijn level to refer to a nameless representation of an identifier.

(the name "local identifier" and also some of this philosophy is taken from chit)

In general, naming is given by a relation between symbols and bindings (as refered to by local identifiers). Each binding may be associated with zero or more symbols, and each symbol might be associated with zero or more bindings.

We name the failure of this relation to be a bijection in several ways.

  • If more than one symbol is related to a single binding, we say that this

binding has aliases. In this case, we should also have a primary alias used as a default.

  • If more than one binding is related to a single symbol, we have name overlap.

Name overlap can be resolved by overloading and shadowing, we will talk about this later on.

  • If no symbol is related to a binding, such as when the binding is created

programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.

  • If no binding is related to a symbol, then we have a name error; this name

is not valid in the current context and we must throw an error.

The most important thing to get right is name overlap; we discuss this first.

There are two ways in which to resolve name overlap. The first way is via overloading. In overloading, we disambiguate an ambiguous name via its context, for instance what type it is expected to be, or what arguments is it receiving. The second way is via shadowing. In shadowing, a name is resolved by making it point to the "most recently defined" thing with that name.

In GATlab, we handle overloading and shadowing with a notion of scope. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. Each scope is identified with a ScopeTag, which is an opaque identifier (i.e. a UUID). We take this idea from Racket, but we don't need the more complex "scope sets" from Racket because GATs don't need to process the syntax of other GATs; if we start doing this we'll have to rethink the design, but we'll probably have bigger problems too.

Two variables with the same name within a single scope are meant to overload one another. For instance, this is what happens with mcompose in the theory of monoidal categories; it is overloaded for Hom and Ob, and this is what happens with d in the discrete exterior calculus; it is overloaded for all of the (k+1)-forms. Variables in different scopes with the same name shadow one another. When we parse an expression a + b, we do so in an ordered list of scopes, and the most recent scope "wins".

Parsing turns a Symbol into an Ident. The Ident contains the original Symbol for printing, but it also contains a reference to a scope via ScopeTag, and an local identifier ("lid") within that scope. Thus, the name in the Ident is never needed for later stages of programatic manipulation.

Scopes cache the relation between names and bindings, by providing a way to go from binding (as reified by local identifier) to a set of aliases with distinguished primary alias, and to go from name to the set of bindings that have that name that we need to disambiguate between in the case of an overload.

Because Idents are fully unambiguous even without their name, it is also possible to create an Ident with no name, which solves the problem of nameless references.

diff --git a/dev/concepts/symbolic_models/index.html b/dev/concepts/symbolic_models/index.html index e082713a..af8a16e2 100644 --- a/dev/concepts/symbolic_models/index.html +++ b/dev/concepts/symbolic_models/index.html @@ -26,4 +26,4 @@ end A, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ] f, g = Hom(:f, A, B), Hom(:g, A, C) -pair(f, g) +pair(f, g) diff --git a/dev/concepts/theories/index.html b/dev/concepts/theories/index.html index 233d92cc..655d6fdd 100644 --- a/dev/concepts/theories/index.html +++ b/dev/concepts/theories/index.html @@ -12,4 +12,4 @@ f::(A → B), g::(B → C), h::(C → D)] f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)] id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)] -end

The code is simplified only slightly from the official GATlab definition of ThCategory. The theory has two type constructors, Ob (object) and Hom (morphism). The type Hom is a dependent type, depending on two objects, named dom (domain) and codom (codomain). The theory has two term constructors, id (identity) and compose (composition).

Notice how the return types of the term constructors depend on the argument values. For example, the term id(A) has type Hom(A,A). The term constructor compose also uses context variables, listed to the right of the ⊣ symbol. These context variables can also be defined after a where clause, but the left hand side must be surrounded by parentheses. This allows us to write compose(f,g), instead of the more verbose compose(A,B,C,f,g) (for discussion, see Cartmell, 1986, Sec 10: Informal syntax).

Notice the @op call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as @op (⋅) := compose to define a single alias. Here we utilize this functionality by replacing the Hom and compose methods with their equivalent Unicode characters, → and ⋅ respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.

The result of the @theory macro is a module with the following members:

  1. For each declaration in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like dom and codom), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use Base.+ as a method for a theory. For instance, ThCategory has functions Ob, Hom, dom, codom, compose, id, ⋅, →.

  2. A submodule called Meta with members:

Note

In general, a GAT consists of a signature, defining the types and terms of the theory, and a set of axioms, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, GATlab supports the specification of both signatures and the axioms, but only uses the axioms as part of rewriting via e-graphs: it is not automatically checked that models of a GAT satisfy the axioms. It is the responsibility of the programmer to ensure this.

References

+end

The code is simplified only slightly from the official GATlab definition of ThCategory. The theory has two type constructors, Ob (object) and Hom (morphism). The type Hom is a dependent type, depending on two objects, named dom (domain) and codom (codomain). The theory has two term constructors, id (identity) and compose (composition).

Notice how the return types of the term constructors depend on the argument values. For example, the term id(A) has type Hom(A,A). The term constructor compose also uses context variables, listed to the right of the ⊣ symbol. These context variables can also be defined after a where clause, but the left hand side must be surrounded by parentheses. This allows us to write compose(f,g), instead of the more verbose compose(A,B,C,f,g) (for discussion, see Cartmell, 1986, Sec 10: Informal syntax).

Notice the @op call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as @op (⋅) := compose to define a single alias. Here we utilize this functionality by replacing the Hom and compose methods with their equivalent Unicode characters, → and ⋅ respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.

The result of the @theory macro is a module with the following members:

  1. For each declaration in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like dom and codom), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use Base.+ as a method for a theory. For instance, ThCategory has functions Ob, Hom, dom, codom, compose, id, ⋅, →.

  2. A submodule called Meta with members:

Note

In general, a GAT consists of a signature, defining the types and terms of the theory, and a set of axioms, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, GATlab supports the specification of both signatures and the axioms, but only uses the axioms as part of rewriting via e-graphs: it is not automatically checked that models of a GAT satisfy the axioms. It is the responsibility of the programmer to ensure this.

References

diff --git a/dev/index.html b/dev/index.html index f6372d67..4c380a30 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -GATlab.jl · GATlab.jl
GitHub

GATlab.jl

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. E.g., 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, 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 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 the theory of a rings, one can construct a model of the theory of modules over that ring where the scalars are ring elements and the vectors are Vectors of ring elements. This corresponds mathematically to the infinite direct sum of copies of the ring with itself.

GATlab is the new (as of Catlab 0.16) backend for Catlab, 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:

+GATlab.jl · GATlab.jl
GitHub

GATlab.jl

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. E.g., 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, 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 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 the theory of a rings, one can construct a model of the theory of modules over that ring where the scalars are ring elements and the vectors are Vectors of ring elements. This corresponds mathematically to the infinite direct sum of copies of the ring with itself.

GATlab is the new (as of Catlab 0.16) backend for Catlab, 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:

diff --git a/dev/stdlib/index.html b/dev/stdlib/index.html index 7fcdd996..df1db1f8 100644 --- a/dev/stdlib/index.html +++ b/dev/stdlib/index.html @@ -22,7 +22,7 @@ (idl := compose(id(a), f) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] (idr := compose(f, id(b)) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] ``` -

source

You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.

thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
GATlab.Stdlib.StdTheories.ThThinCategory — Module

``` +

source

You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.

thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
GATlab.Stdlib.StdTheories.ThThinCategory — Module

``` ThThinCategory ``` @@ -47,7 +47,7 @@ (thineq := f == g) ⊣ [a::Ob, b::Ob, f::Hom(a, b), g::Hom(a, b)] ``` -

source

Category Building Blocks

The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.

GATlab.Stdlib.StdTheories.ThClass — Module

``` +

source

Category Building Blocks

The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.

GATlab.Stdlib.StdTheories.ThClass — Module

``` ThClass ``` @@ -57,7 +57,7 @@ ``` Ob::TYPE ⊣ [] ``` -

source
GATlab.Stdlib.StdTheories.ThLawlessCat — Module

``` +

source
GATlab.Stdlib.StdTheories.ThLawlessCat — Module

``` ThLawlessCat ``` @@ -73,7 +73,7 @@ #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:33 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] ``` -

source
GATlab.Stdlib.StdTheories.ThAscCat — Module

``` +

source
GATlab.Stdlib.StdTheories.ThAscCat — Module

``` ThAsCat ``` @@ -91,7 +91,7 @@ (assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)] ``` -

source
GATlab.Stdlib.StdTheories.ThIdLawlessCat — Module

``` +

source
GATlab.Stdlib.StdTheories.ThIdLawlessCat — Module

``` ThIdLawlessCat ``` @@ -111,4 +111,4 @@ id(a)::Hom(a, a) ⊣ [a::Ob] ``` -

source
GATlab.Stdlib.StdTheories.##865 — Constant
ThClass

A Class is just a Set that doesn't worry about foundations.

source
GATlab.Stdlib.StdTheories.##866 — Constant
ThGraph

A graph where the edges are typed depending on dom/codom. Contains all necessary types for the theory of categories.

source
GATlab.Stdlib.StdTheories.##867 — Constant
ThLawlessCat

The data of a category without any axioms of associativity or identities.

source
GATlab.Stdlib.StdTheories.##868 — Constant
ThAsCat

The theory of a category with the associative law for composition.

source
GATlab.Stdlib.StdTheories.##869 — Constant
ThIdLawlessCat

The theory of a category without identity axioms.

source
GATlab.Stdlib.StdTheories.##870 — Constant
ThCategory

The theory of a category with composition operations and associativity and identity axioms.

source
GATlab.Stdlib.StdTheories.##871 — Constant
ThThinCategory

The theory of a thin category meaning that if two morphisms have the same domain and codomain they are equal as morphisms. These are equivalent to preorders.

source
GATlab.Stdlib.StdTheories.##873 — Constant

The theory of a set with no operations

A base theory for all algebraic theories so that multiple inheritance doesn't create multiple types.

source
GATlab.Stdlib.StdTheories.##874 — Constant

The theory of a set with a binary operation which does not guarantee associativity

Examples:

  • The integers with minus operation is not associative.

    (a ⋅ b) ⋅ c = a - b - c

    a ⋅ (b ⋅ c) = a - b + c

source
GATlab.Stdlib.StdTheories.##875 — Constant

This theory contains an associative binary operation called multiplication.

Examples:

  • The integers under multiplication
  • Nonempty lists under concatenation
source
GATlab.Stdlib.StdTheories.##876 — Constant

The theory of a semigroup with identity.

Examples:

  • The integers under multiplication
  • Lists (nonempty and empty) under concatenation
source
GATlab.Stdlib.StdTheories.##877 — Constant

The theory of a monoid with multiplicative inverse.

Examples:

  • The rationals (excluding zero) under multiplication
  • E(n), the group of rigid transformations (translation and rotation)
  • Bₙ, the braid group of n strands
source
GATlab.Stdlib.StdTheories.##878 — Constant

The theory of a monoid where multiplication enjoys commutativity.

Examples:

  • The set of classical 1-knots under "knot sum"
source
GATlab.Stdlib.StdTheories.##879 — Constant

The theory of sets which have a preorder.

This is equivalent to the theory of thin categories (ThThinCategory) where ≤ is the composition operation.

Examples:

  • The set of natural numbers ordered by b-a ≥ 0
  • The set of natural numbers ordered by "a divides b"
source
GATlab.Stdlib.StdTheories.##880 — Constant

The theory of monoidal categories

mcompose is usually denoted with ⊗ and the munit is usually denoted by 1 or I.

source
GATlab.Stdlib.StdTheories.##881 — Constant

The theory of monoidal categories with strict associativity

source
GATlab.Stdlib.StdTheories.##882 — Constant

The theory of natural numbers

source
GATlab.Stdlib.StdTheories.##883 — Constant

The theory of natural numbers with addition as repeated succession

source
GATlab.Stdlib.StdTheories.##884 — Constant

The theory of nat-plus with multiplication

source
+

source
GATlab.Stdlib.StdTheories.##865 — Constant
ThClass

A Class is just a Set that doesn't worry about foundations.

source
GATlab.Stdlib.StdTheories.##866 — Constant
ThGraph

A graph where the edges are typed depending on dom/codom. Contains all necessary types for the theory of categories.

source
GATlab.Stdlib.StdTheories.##867 — Constant
ThLawlessCat

The data of a category without any axioms of associativity or identities.

source
GATlab.Stdlib.StdTheories.##868 — Constant
ThAsCat

The theory of a category with the associative law for composition.

source
GATlab.Stdlib.StdTheories.##869 — Constant
ThIdLawlessCat

The theory of a category without identity axioms.

source
GATlab.Stdlib.StdTheories.##870 — Constant
ThCategory

The theory of a category with composition operations and associativity and identity axioms.

source
GATlab.Stdlib.StdTheories.##871 — Constant
ThThinCategory

The theory of a thin category meaning that if two morphisms have the same domain and codomain they are equal as morphisms. These are equivalent to preorders.

source
GATlab.Stdlib.StdTheories.##873 — Constant

The theory of a set with no operations

A base theory for all algebraic theories so that multiple inheritance doesn't create multiple types.

source
GATlab.Stdlib.StdTheories.##874 — Constant

The theory of a set with a binary operation which does not guarantee associativity

Examples:

  • The integers with minus operation is not associative.

    (a ⋅ b) ⋅ c = a - b - c

    a ⋅ (b ⋅ c) = a - b + c

source
GATlab.Stdlib.StdTheories.##875 — Constant

This theory contains an associative binary operation called multiplication.

Examples:

  • The integers under multiplication
  • Nonempty lists under concatenation
source
GATlab.Stdlib.StdTheories.##876 — Constant

The theory of a semigroup with identity.

Examples:

  • The integers under multiplication
  • Lists (nonempty and empty) under concatenation
source
GATlab.Stdlib.StdTheories.##877 — Constant

The theory of a monoid with multiplicative inverse.

Examples:

  • The rationals (excluding zero) under multiplication
  • E(n), the group of rigid transformations (translation and rotation)
  • Bₙ, the braid group of n strands
source
GATlab.Stdlib.StdTheories.##878 — Constant

The theory of a monoid where multiplication enjoys commutativity.

Examples:

  • The set of classical 1-knots under "knot sum"
source
GATlab.Stdlib.StdTheories.##879 — Constant

The theory of sets which have a preorder.

This is equivalent to the theory of thin categories (ThThinCategory) where ≤ is the composition operation.

Examples:

  • The set of natural numbers ordered by b-a ≥ 0
  • The set of natural numbers ordered by "a divides b"
source
GATlab.Stdlib.StdTheories.##880 — Constant

The theory of monoidal categories

mcompose is usually denoted with ⊗ and the munit is usually denoted by 1 or I.

source
GATlab.Stdlib.StdTheories.##881 — Constant

The theory of monoidal categories with strict associativity

source
GATlab.Stdlib.StdTheories.##882 — Constant

The theory of natural numbers

source
GATlab.Stdlib.StdTheories.##883 — Constant

The theory of natural numbers with addition as repeated succession

source
GATlab.Stdlib.StdTheories.##884 — Constant

The theory of nat-plus with multiplication

source