diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index d82b5525..13844ac6 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.10.0","generation_timestamp":"2024-01-03T17:18:08","documenter_version":"1.2.1"}} \ No newline at end of file +{"documenter":{"julia_version":"1.10.0","generation_timestamp":"2024-01-31T00:39:19","documenter_version":"1.2.1"}} \ No newline at end of file diff --git a/dev/api/index.html b/dev/api/index.html index a0bb8cb6..23a0f3b0 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,12 +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
 
@@ -48,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])
@@ -109,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 663fe66a..d26a9a55 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 8f333e88..1adb5189 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 0a90d4ef..a66c6faa 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 34b22810..d4fcff11 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 ac974aae..2d811158 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 18f6eb52..c9072999 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/search_index.js b/dev/search_index.js index e8f7112c..474869d0 100644 --- a/dev/search_index.js +++ b/dev/search_index.js @@ -1,3 +1,3 @@ var documenterSearchIndex = {"docs": -[{"location":"api/#Library-Reference","page":"Library Reference","title":"Library Reference","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [GATlab]","category":"page"},{"location":"api/#Syntax","page":"Library Reference","title":"Syntax","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Syntax,\n GATlab.Syntax.Scopes,\n GATlab.Syntax.GATs,\n GATlab.Syntax.GATContexts,\n GATlab.Syntax.ExprInterop,\n GATlab.Syntax.TheoryInterface,\n]","category":"page"},{"location":"api/#GATlab.Syntax.Scopes.Binding","page":"Library Reference","title":"GATlab.Syntax.Scopes.Binding","text":"Binding{T}\n\nA binding associates some T-typed value to a name.\n\nname is an optional distinguished name value is the element\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Context","page":"Library Reference","title":"GATlab.Syntax.Scopes.Context","text":"A Context is anything which contains an ordered list of scopes.\n\nScopes within a context are referred to by level, which is their index within this list.\n\nContexts should overload:\n\ngetscope(c::Context, level::Int) -> Scope\nnscopes(c::Context) -> Int\nhastag(c::Context, tag::ScopeTag) -> Bool\nhasname(c::Context, name::Symbol) -> Bool\ngetlevel(c::Context, tag::ScopeTag) -> Int\ngetlevel(c::Context, name::Symbol) -> Int\nalltags(c::Context) -> Set{ScopeTag}\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.HasScope","page":"Library Reference","title":"GATlab.Syntax.Scopes.HasScope","text":"An abstract type for wrappers around a single scope.\n\nMust overload\n\ngetscope(hs::HasScope) -> Scope\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.HasScopeList","page":"Library Reference","title":"GATlab.Syntax.Scopes.HasScopeList","text":"A type for things which contain a scope list.\n\nNotably, GATs contain a scope list.\n\nMust implement:\n\ngetscopelist(hsl::HasScopeList) -> ScopeList\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Ident","page":"Library Reference","title":"GATlab.Syntax.Scopes.Ident","text":"Ident\n\nAn identifier.\n\ntag 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\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.LID","page":"Library Reference","title":"GATlab.Syntax.Scopes.LID","text":"A LID (Local ID) indexes a given scope.\n\nCurrently, scopes assign LIDs sequentially – this is not a stable guarantee however, and in theory scopes could have \"sparse\" LIDs.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Scope","page":"Library Reference","title":"GATlab.Syntax.Scopes.Scope","text":"Scope{T}\n\nIn 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:\n\nx = 3\ny = \"hello\"\nz = x \n\nHere 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.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopeTag","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopeTag","text":"The tag that makes reference to a specific scope possible.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopeTagError","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopeTagError","text":"ScopeTagError\n\nAn error to throw when an identifier has an unexpected scope tag\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopedBinding","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopedBinding","text":"Type for printing out bindings with colored keys\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.getidents-Tuple{HasScope}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getidents","text":"This collects all the idents in a scope\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.getlid-Tuple{HasScope, Symbol}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getlid","text":"Determine the level of a binding given the name\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.hasident-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.hasident","text":"hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.ident-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.ident","text":"ident creates an Ident from a context and some partial data supplied as keywords.\n\nKeywords arguments:\n\ntag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.\nname::Union{Symbol, Nothing}. The name of the identifier.\nlid::Union{LID, Nothing}. The lid of the identifier within its scope.\nlevel::Union{Int, Nothing}. The level of the scope within the context.\nstrict::Bool. If strict is true, throw an error if not found, else return nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.idents-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.idents","text":"This is a broadcasted version of ident\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.rename-Tuple{ScopeTag, Dict{Symbol, Symbol}, Any}","page":"Library Reference","title":"GATlab.Syntax.Scopes.rename","text":"rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T\n\nRecurse 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.retag-Tuple{Dict{ScopeTag, ScopeTag}, Any}","page":"Library Reference","title":"GATlab.Syntax.Scopes.retag","text":"retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T\n\nRecurse 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.unsafe_pushbinding!-Union{Tuple{T}, Tuple{Scope{T}, Binding{T}}} where T","page":"Library Reference","title":"GATlab.Syntax.Scopes.unsafe_pushbinding!","text":"Add a new binding to the end of Scope s.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.AbstractConstant","page":"Library Reference","title":"GATlab.Syntax.GATs.AbstractConstant","text":"We need this to resolve a mutual reference loop; the only subtype is Constant\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AbstractDot","page":"Library Reference","title":"GATlab.Syntax.GATs.AbstractDot","text":"We need this to resolve a mutual reference loop; the only subtype is Dot\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgAccessor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgAccessor","text":"AlgAccessor\n\nThe arguments to a term constructor serve a dual function as both arguments and also methods to extract the value of those arguments.\n\nI.e., declaring Hom(dom::Ob, codom::Ob)::TYPE implicitly overloads a previous declaration for dom and codom, or creates declarations if none previously exist.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgAxiom","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgAxiom","text":"AlgAxiom\n\nA declaration of an axiom\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgDeclaration","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgDeclaration","text":"AlgDeclaration\n\nA declaration of a constructor; constructor methods in the form of AlgTermConstructors or the accessors for AlgTypeConstructors follow later in the theory.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgDot","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgDot","text":"Accessing a name from a term of tuple type\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgEqSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgEqSort","text":"AlgSort\n\nA sort for equality judgments of terms for a particular sort\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgFunction","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgFunction","text":"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.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSort","text":"AlgSort\n\nA sort, which is essentially a type constructor without arguments\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgSorts","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSorts","text":"AlgSorts\n\nA description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgStruct","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgStruct","text":"AlgStruct\n\nA declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor which constructs an element of that type, and projection term constructors. E.g.\n\nstruct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]\n apex::Ob\n i1::dom->apex\n i2::codom->apex\nend\n\nIs tantamount to (in a vanilla GAT):\n\nCospan(dom::Ob, codom::Ob)::TYPE \n\ncospan(apex, i1, i2)::Cospan(dom, codom) \n ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]\n\napex(csp::Cospan(d::Ob, c::Ob))::Ob \ni1(csp::Cospan(d::Ob, c::Ob))::(d->apex(csp))\ni2(csp::Cospan(d::Ob, c::Ob))::(c->apex(csp))\n\napex(cospan(a, i_1, i_2)) == a \n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\ni1(cospan(a, i_1, i_2)) == i_1 \n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\ni2(cospan(a, i_1, i_2)) == i_2\n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\n\ncospan(apex(csp), i1(csp), i2(csp)) == csp\n ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTerm","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTerm","text":"AlgTerm\n\nOne syntax tree to rule all the terms.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTermConstructor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTermConstructor","text":"AlgTermConstructor\n\nA declaration of a term constructor as a method of an AlgFunction.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgType","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgType","text":"AlgType\n\nOne syntax tree to rule all the types.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTypeConstructor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTypeConstructor","text":"AlgTypeConstructor\n\nA declaration of a type constructor.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.Constant","page":"Library Reference","title":"GATlab.Syntax.GATs.Constant","text":"Constant\n\nA Julia value in an algebraic context. Type checked elsewhere.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.Eq","page":"Library Reference","title":"GATlab.Syntax.GATs.Eq","text":"Eq\n\nThe type of equality judgments.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GAT","page":"Library Reference","title":"GATlab.Syntax.GATs.GAT","text":"GAT\n\nA 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.\n\nGATs allow overloading but not shadowing.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GATContext","page":"Library Reference","title":"GATlab.Syntax.GATs.GATContext","text":"GATContext\n\nA context consisting of two parts: a GAT and a TypeCtx\n\nCertain types (like AlgTerm) can only be parsed in a GATContext, because they require access to the method resolving in the GAT.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GATSegment","page":"Library Reference","title":"GATlab.Syntax.GATs.GATSegment","text":"GATSegment\n\nA piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.\n\nThis is a struct rather than just a type alias so that we can customize the show method.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{AlgType}, Tuple{GAT, Ident}} where AlgType","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical type + ctx associated with a type constructor.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{T}, Tuple{GAT, Ident}} where T<:AlgAST","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical term + ctx associated with a method.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.Judgment","page":"Library Reference","title":"GATlab.Syntax.GATs.Judgment","text":"A GAT is conceptually a bunch of Judgments strung together.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.MethodApp","page":"Library Reference","title":"GATlab.Syntax.GATs.MethodApp","text":"MethodApp\n\nAn 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.\n\nmethod either points to an AlgTermConstructor, an AlgTypeConstructor or an AlgAccessor,\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.MethodResolver","page":"Library Reference","title":"GATlab.Syntax.GATs.MethodResolver","text":"MethodResolver\n\nRight now, this just maps a sort signature to the resolved method.\n\nWhen we eventually support varargs, this will have to do something slightly fancier.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.TypeScope","page":"Library Reference","title":"GATlab.Syntax.GATs.TypeScope","text":"TypeScope\n\nA 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)}\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.show-Union{Tuple{T}, Tuple{IO, T}} where T<:Union{AlgTerm, AlgType}","page":"Library Reference","title":"Base.show","text":"Common methods for AlgType and AlgTerm\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{GAT, Any, Any}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Coerce GATs to GAT contexts\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.toexpr-Tuple{GAT, GATSegment}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"This only works when seg is a segment of theory\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.equations-Tuple{GAT, Ident}","page":"Library Reference","title":"GATlab.Syntax.GATs.equations","text":"Get equations for a term or type constructor\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.equations-Tuple{GATContext, AbstractVector{Ident}}","page":"Library Reference","title":"GATlab.Syntax.GATs.equations","text":"Implicit equations defined by a context.\n\nThis 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.\n\nReferences:\n\n(Cartmell, 1986, Sec 6: \"Essentially algebraic theories and categories with finite limits\")\n(Freyd, 1972, \"Aspects of topoi\")\n\nThis function gives expressions for computing the elements of c.context which can be inferred from applying accessor functions to elements of args.\n\nExample:\n\nequations({f::Hom(a,b), g::Hom(b,c)}, {a::Ob, b::Ob, c::Ob}, ThCategory)\n\nwaysofcomputing = Dict(a => [dom(f)], b => [codom(f), dom(g)], c => [codom(g)], f => [f], g => [g])\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.normalize_judgment-Tuple{Any}","page":"Library Reference","title":"GATlab.Syntax.GATs.normalize_judgment","text":"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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.parse_scope!-Tuple{Function, Scope, AbstractVector}","page":"Library Reference","title":"GATlab.Syntax.GATs.parse_scope!","text":"f(pushbinding!, expr) should inspect expr and call pushbinding! 0 or more times with two arguments: the name and value of a new binding.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.sortcheck-Tuple{Context, AlgTerm}","page":"Library Reference","title":"GATlab.Syntax.GATs.sortcheck","text":"sortcheck(ctx::Context, t::AlgTerm)\n\nThrow 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.sortcheck-Tuple{Context, AlgType}","page":"Library Reference","title":"GATlab.Syntax.GATs.sortcheck","text":"sortcheck(ctx::Context, t::AlgType)\n\nThrow an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.structs-Tuple{GAT}","page":"Library Reference","title":"GATlab.Syntax.GATs.structs","text":"Get all structs in a theory\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.substitute_funs-Tuple{Context, AlgTerm}","page":"Library Reference","title":"GATlab.Syntax.GATs.substitute_funs","text":"Replace all functions with their desugared expressions\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.substitute_term-Union{Tuple{T}, Tuple{T, Dict{Ident, AlgTerm}}} where T<:AlgAST","page":"Library Reference","title":"GATlab.Syntax.GATs.substitute_term","text":"Replace idents with AlgTerms. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{GATContext, Any, Type{GATContext}}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Parse, e.g.:\n\n(a,b,c)::Ob\nf::Hom(a, b)\ng::Hom(b, c)\nh::Hom(a, c)\nh′::Hom(a, c)\ncompose(f, g) == h == h′\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"fromexpr(c::Context, e::Any, T::Type) -> Union{T,Nothing}\n\nConverts a Julia Expr into type T, in a certain scope.\n\n\n\n\n\n","category":"function"},{"location":"api/#GATlab.Syntax.ExprInterop.toexpr","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"toexpr(c::Context, t) -> Any\n\nConverts 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.\n\n\n\n\n\n","category":"function"},{"location":"api/#GATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP","text":"When we declare a new theory, we add the scope tag of its new segment to this dictionary pointing to the module corresponding to the new theory.\n\n\n\n\n\n","category":"constant"},{"location":"api/#GATlab.Syntax.TheoryInterface.fqmn-Tuple{Module}","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.fqmn","text":"Fully Qualified Module Name\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.TheoryInterface.mk_struct-Tuple{AlgStruct, Any}","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.mk_struct","text":"\n\n\n\n","category":"method"},{"location":"api/#Models","page":"Library Reference","title":"Models","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Models,\n GATlab.Models.ModelInterface,\n GATlab.Models.SymbolicModels,\n ]","category":"page"},{"location":"api/#GATlab.Models.ModelInterface.ImplementationNotes","page":"Library Reference","title":"GATlab.Models.ModelInterface.ImplementationNotes","text":"ImplementationNotes\n\nInformation about how a model implements a GATSegment. Right now, just the docstring attached to the @instance macro, but could contain more info in the future.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Models.ModelInterface.implements-Union{Tuple{tag}, Tuple{Module, Type{Val{tag}}}} where tag","page":"Library Reference","title":"GATlab.Models.ModelInterface.implements","text":"implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}\n\nIf m implements the GATSegment referred to by tag, then return the corresponding implementation notes.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.parse_instance_body-Tuple{Expr, GAT}","page":"Library Reference","title":"GATlab.Models.ModelInterface.parse_instance_body","text":"Parses the raw julia expression into JuliaFunctions\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.qualify_function-Tuple{JuliaFunction, Any, Union{Nothing, Expr, Symbol}, Any, Any}","page":"Library Reference","title":"GATlab.Models.ModelInterface.qualify_function","text":"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\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.to_call_impl-Tuple{AlgTerm, GAT, Union{Module, Symbol}, Bool}","page":"Library Reference","title":"GATlab.Models.ModelInterface.to_call_impl","text":"Compile an AlgTerm into a Julia call Expr where termcons (e.g. f) are interpreted as mod.f[model.model](...).\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.typecheck_instance-Tuple{GAT, Vector{JuliaFunction}, Vector{Symbol}, Dict{AlgSort}}","page":"Library Reference","title":"GATlab.Models.ModelInterface.typecheck_instance","text":"Throw error if missing a term constructor. Provides default instances for type constructors and type arguments, which return true or error, respectively.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.TheoryMaps.migrator-NTuple{5, Any}","page":"Library Reference","title":"GATlab.Syntax.TheoryMaps.migrator","text":"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.\n\nFuture 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.@instance-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.ModelInterface.@instance","text":"Usage:\n\nstruct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}\n ntypes::Int\nend\n\n@instance ThCategory{Vector{Int}, Vector{Int}} [model::TypedFinSetC] begin\n Ob(v::Vector{Int}) = all(1 <= j <= model.ntypes for j in v)\n Hom(f::Vector{Int}, v::Vector{Int}, w::Vector{Int}) =\n length(f) == length(v) && all(1 <= y <= length(w) for y in f)\n\n id(v::Vector{Int}) = collect(eachindex(v))\n compose(f::Vector{Int}, g::Vector{Int}) = g[f]\n\n dom(f::Vector{Int}; context) = context.dom\n codom(f::Vector{Int}; context) = context.codom\nend\n\nstruct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Hom}, Hom}}\n c::C\nend\n\n@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#GATlab.Models.SymbolicModels.GATExpr","page":"Library Reference","title":"GATlab.Models.SymbolicModels.GATExpr","text":"Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.\n\nWe 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.)\n\nThe 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.\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.nameof-Tuple{GATExpr{:generator}}","page":"Library Reference","title":"Base.nameof","text":"Get name of GAT generator expression as a Symbol.\n\nIf the generator has no name, returns nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.constructor_name-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.constructor_name","text":"Name of constructor that created expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.functor-Tuple{Tuple, GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.functor","text":"Functor from GAT expression to GAT instance.\n\nStrictly 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\".\n\nA functor is completely determined by its action on the generators. There are several ways to specify this mapping:\n\nSpecify 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.\nExplicitly map each generator term to an instance value, using the generators dictionary.\nFor 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.\n\nThe 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.\n\nFIXME\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.generator_like-Tuple{GATExpr, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.generator_like","text":"Create generator of the same type as the given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.parse_json_sexpr-Tuple{Module, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.parse_json_sexpr","text":"Deserialize expression from JSON-able S-expression.\n\nIf symbols is true (the default), strings are converted to symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_latex-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_latex","text":"Show the expression in infix notation using LaTeX math.\n\nDoes not include $ or \\[begin|end]{equation} delimiters.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_sexpr","text":"Show the syntax expression as an S-expression.\n\nCf. the standard library function Meta.show_sexpr.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_unicode-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_unicode","text":"Show the expression in infix notation using Unicode symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.symbolic_instance_methods-Tuple{GAT, Any, Symbol, Dict{Ident, JuliaFunction}}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.symbolic_instance_methods","text":"Julia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.syntax_module-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.syntax_module","text":"Get syntax module of given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.to_json_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.to_json_sexpr","text":"Serialize expression as JSON-able S-expression.\n\nThe format is an S-expression encoded as JSON, e.g., \"compose(f,g)\" is represented as [\"compose\", f, g].\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.@symbolic_model-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.@symbolic_model","text":"@symbolic_model generates the free model of a theory, generated by symbols.\n\nThis is backwards compatible with the @syntax macro in Catlab.\n\nOne 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\".\n\nAn invocation of @symbolic_model creates the following.\n\nA module with a struct for each type constructor, which has a single type\n\nparameter 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.\n\nFor instance, in the theory of categories, we might have the following elements.\n\nusing .FreeCategory\nx = Ob{:generator}([:x], [])\ny = Ob{:generator}([:y], [])\nf = Hom{:generator}([:f], [x, y])\ng = Hom{:generator}([:g], [y, x])\nh = Hom{:compose}([f, g], [x, x])\n\nMethods inside the module (not exported) for all of the term constructors and\n\nfield accessors (i.e. stuff like compose, id, dom, codom), which construct terms.\n\nA default instance (i.e., without a model parameter) of the theory using the\n\ntypes in this generated model. Methods in this instance can be overridden by the body of @symbolic_model to perform rewriting for the sake of normalization, for instance flattening associative and unital operations.\n\nCoercion methods of the type constructors that allow one to introduce generators.\n\nx = ThCategory.Ob(FreeCategory.Ob, :x)\ny = ThCategory.Ob(FreeCategory.Ob, :y)\nf = ThCategory.Hom(:f, x, y)\n\nNote that in both the instance and in these coercion methods, we must give the expected type as the first argument when it cannot be infered by the other arguments. For instance, instead of\n\nmunit() = ...\n\nwe have\n\nmunit(::Type{FreeSMC.Ob}) = ...\n\nand likewise instead of\n\nThCategory.Ob(x::Any) = ...\n\nwe have\n\nThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...\n\nExample:\n\n@symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)\nend\n\nThis generates:\n\nmodule FreeCategory\nexport Ob, Hom\nusing ..__module__\n\nmodule Meta\n const theory_module = ThCategory\n const theory = ThCategory.Meta.theory\n const theory_type = ThCategory.Meta.T\nend\n\nstruct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol\n args::Vector\n type_args::Vector{GATExpr}\nend\n\nstruct Hom{T} <: __module__.HomExpr{T}\n args::Vector\n type_args::Vector{GATExpr}\nend\n\ndom(x::Hom) = x.type_args[1]\n\ncodom(x::Hom) = x.type_args[2]\n\nfunction compose(f::Hom, g::Hom; strict=true)\n if strict && !(codom(f) == dom(g))\n throw(SyntaxDomainError(:compose, [f, g]))\n end\n Hom{:compose}([f, g], [dom(f), codom(g)])\nend\n\nfunction id(x::Ob)\n Ob{:id}([x], [x, x])\nend\nend\n\n# default implementations \n\nfunction ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob\n FreeCategory.dom(x)\nend\n\nfunction ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob\n FreeCategory.Ob{:generator}([__value__], [])\nend\n\nfunction ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom\n FreeCategory.id(A)\nend\n\nfunction ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)\n associate_unit(FreeCategory.compose(f, g; strict), id)\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#Utilities","page":"Library Reference","title":"Utilities","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Util,\n GATlab.Util.MetaUtils,\n ]","category":"page"},{"location":"api/#GATlab.Util.MetaUtils","page":"Library Reference","title":"GATlab.Util.MetaUtils","text":"General-purpose tools for metaprogramming in Julia.\n\n\n\n\n\n","category":"module"},{"location":"api/#GATlab.Util.MetaUtils.JuliaFunctionSigNoWhere","page":"Library Reference","title":"GATlab.Util.MetaUtils.JuliaFunctionSigNoWhere","text":"For comparing JuliaFunctionSigs modulo the where parameters\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Util.MetaUtils.concat_expr-Tuple{Expr, Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.concat_expr","text":"Concatenate two Julia expressions into a block expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.generate_docstring-Tuple{Expr, Union{Nothing, String}}","page":"Library Reference","title":"GATlab.Util.MetaUtils.generate_docstring","text":"Wrap Julia expression with docstring.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.generate_function-Tuple{JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.generate_function","text":"Generate Julia expression for function definition.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_docstring-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_docstring","text":"Parse Julia expression that is (possibly) annotated with docstring.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_function-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_function","text":"Parse Julia function definition into standardized form.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_function_sig-Tuple{JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_function_sig","text":"Parse signature of Julia function.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.replace_symbols-Tuple{AbstractDict, Any}","page":"Library Reference","title":"GATlab.Util.MetaUtils.replace_symbols","text":"Replace symbols occuring anywhere in a Julia expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.replace_symbols-Tuple{AbstractDict, JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.replace_symbols","text":"Replace symbols occurring anywhere in a Julia function (except the name).\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.strip_lines-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.strip_lines","text":"Remove all LineNumberNodes from a Julia expression.\n\n\n\n\n\n","category":"method"},{"location":"concepts/catlab_differences/#Changes-from-Catlab-GATs","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#1.-Models-as-values","page":"Changes from Catlab GATs","title":"1. Models as values","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"struct FinSetInt\n n::Int\nend","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#2.-E-Graphs","page":"Changes from Catlab GATs","title":"2. E-Graphs","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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_1ldotsx_n) sim f(x_1ldotsx_n) for any term constructor f. E-graphs are used for a variety of purposes, including:","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"finding simple representations of terms\ndeciding whether two terms are equal","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#3.-Indexed-dependent-types-in-models","page":"Changes from Catlab GATs","title":"3. Indexed dependent types in models","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"A morphism between the finite sets 1ldotsn and 1ldotsm is simply a length-n vector whose entries are in 1ldotsm. 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}.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/models/#Models-and-instances","page":"Models and instances","title":"Models and instances","text":"","category":"section"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"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.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"When a model m implements Th, the following methods should be defined.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"For every type constructor X in Th\nTh.X[m::typeof(m)](x, args...) = ...\nThis 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.\nFor 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.\nThis 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.\nFor each argument a to a type constructor (i.e. dom and codom for Hom), an overload of\nTh.a[m::typeof(m)](x) = ...\nThis 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.\nFor each term constructor f in Theory\nTh.f[m::typeof(m)](args...) = ...\nThis 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,\nThCategory.compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]\nTerm 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.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"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.","category":"page"},{"location":"concepts/scopes/#Scopes","page":"Scopes","title":"Scopes","text":"","category":"section"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Design rationale:","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"(the name \"local identifier\" and also some of this philosophy is taken from chit)","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"We name the failure of this relation to be a bijection in several ways.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one symbol is related to a single binding, we say that this","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"binding has aliases. In this case, we should also have a primary alias used as a default.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one binding is related to a single symbol, we have name overlap.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Name overlap can be resolved by overloading and shadowing, we will talk about this later on.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no symbol is related to a binding, such as when the binding is created","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no binding is related to a symbol, then we have a name error; this name","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"is not valid in the current context and we must throw an error.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"The most important thing to get right is name overlap; we discuss this first.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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\".","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/theories/#Theories","page":"Theories","title":"Theories","text":"","category":"section"},{"location":"concepts/theories/#What-is-a-GAT?","page":"Theories","title":"What is a GAT?","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Generalized Algebraic Theories (GATs) are the backbone of GATlab so let's expand a bit on GATs and how they fit into the bigger picture of algebra.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"An algebraic structure, like a group or category, is a mathematical object whose axioms all take the form of equations that are universally quantified (the equations have no exceptions). That’s not a formal definition but it’s a good heuristic. There are different ways to make this precise. The oldest, going back to universal algebra in the early 20th centrury, are algebraic theories.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples (\"models\") of algebraic structures. For instance, rather than take particular groups as the object of study, in universal algebra one takes the class of groups as an object of study. In an algebraic theory, you have a collection of (total) operations and they obey a set of equational axioms. Classically, there is only a single generating type, but there are also typed or multi-sorted versions of algebraic theories. Most of the classical structures of abstract algebra, such as groups, rings, and modules, can be defined as algebraic theories.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Importantly, the theory of categories is not algebraic. In other words, a category cannot be defined as a (multi-sorted) algebraic theory. The reason is that the operation of composition is partial, since you can only compose morphisms with compatible (co)domains. Now, categories sure feel like algebraic structures, so people have come up with generalizations of algebraic theories that accomodate categories and related structures.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"The first of these was Freyd’s essentially algebraic theories. In an essentially algebraic theory, you can have partially defined operations; however, to maintain the equational character of the system, the domains of operations must themselves be defined equationally. For example, the theory of categories would be defined as having two types, Ob and Hom, and the composition operation compose(f::Hom,g::Hom)::Hom would have domain given by the equation codom(f) == dom(g). As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Later, Cartmell proposed generalized algebraic theories, which solves the same problem but in a different way. Rather than having partial operations, you have total operations but on dependent types (types that are parameterized by values). So now the composition operation has signature compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) ⊣ [A::Ob, B::Ob, C::Ob] exactly as appears in GATlab. This is closer to the way that mathematicians actually think and write about categories. For example, if you look at the definitions of category, functor, and natural transformation in Emily Riehl’s textbook, you will see that they are already essentially in the form of a GAT, whereas they require translation into an essentially algebraic theory. Nevertheless, GATs and essentially algebraic theories have the same expressive power, at least in their standard set-based semantics. GATs provide a version of the computer scientist's type theory that plays well with the mathematician's algebra, thus, providing a perfect opportunity for computer algebra systems.","category":"page"},{"location":"concepts/theories/#The-@theory-macro","page":"Theories","title":"The @theory macro","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"GATlab implements a version of the GAT formalism on top of Julia's type system, taking advantage of Julia macros to provide a pleasant syntax. GATs are defined using the @theory macro.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"For example, the theory of categories could be defined by:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"using GATlab","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"@theory ThCategory begin\n @op begin\n (→) := Hom\n (⋅) := compose\n end\n Ob::TYPE\n Hom(dom::Ob, codom::Ob)::TYPE\n id(A::Ob)::(A → A)\n compose(f::(A → B), g::(B → C))::(A → C) ⊣ [A::Ob, B::Ob, C::Ob]\n (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob,\n f::(A → B), g::(B → C), h::(C → D)]\n f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)]\n id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)]\nend\nnothing # hide","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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).","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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).","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"The result of the @theory macro is a module with the following members:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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, ⋅, →.\nA submodule called Meta with members:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"T: a zero-field struct that serves as a type-level signifier for the theory.\ntheory: a constant of type GAT which stores the data of the theory.\n@theory: a macro which expands directly to theory, which is used to pass around the data of the theory at macro-expand time.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"note: Note\nIn 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.","category":"page"},{"location":"concepts/theories/#References","page":"Theories","title":"References","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Cartmell, 1986: Generalized algebraic theories and contextual categories, DOI:10.1016/0168-0072(86)90053-9\nCartmell, 1978, PhD thesis: Generalized algebraic theories and contextual categories\nPitts, 1995: Categorical logic, Sec 6: Dependent types","category":"page"},{"location":"stdlib/#Standard-Library","page":"Standard Library","title":"Standard Library","text":"","category":"section"},{"location":"stdlib/#Categories","page":"Standard Library","title":"Categories","text":"","category":"section"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"Our friend ThCategory is the main theory in this module.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThCategory","text":"ThCategory\n\nThe theory of a category with composition operations and associativity and identity axioms.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"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.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThThinCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThThinCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThThinCategory","text":"ThThinCategory\n\nThe 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.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/#Category-Building-Blocks","page":"Standard Library","title":"Category Building Blocks","text":"","category":"section"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"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.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThClass","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThClass","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThClass","text":"ThClass\n\nA Class is just a Set that doesn't worry about foundations.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThLawlessCat","text":"ThLawlessCat\n\nThe data of a category without any axioms of associativity or identities.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThAscCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThAscCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThAscCat","text":"ThAsCat\n\nThe theory of a category with the associative law for composition.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThIdLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThIdLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThIdLawlessCat","text":"ThIdLawlessCat\n\nThe theory of a category without identity axioms.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"Modules = [GATlab.Stdlib,\n GATlab.Stdlib.StdTheories,\n GATlab.Stdlib.StdModels,\n ]","category":"page"},{"location":"concepts/symbolic_models/#Symbolic-Models","page":"Symbolic Models","title":"Symbolic Models","text":"","category":"section"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Theories can also be instantiated as systems of symbolic expressions, using the @symbolic_model macro. The symbolic expressions are expression trees, as commonly used in computer algebra systems. They are similar to Julia's Expr type but they are instead subtyped from GATlab's GATExpr type and they have a more refined type hierarchy.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"A single theory can have different syntax systems, treating different terms as primitive or performing different simplication or normalization procedures. GATlab tries to make it easy to define new syntax systems. Many of the theories included with GATlab have default syntax systems, but the user is encouraged to define their own to suit their needs.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"To get started, you can always call the @symbolic_model macro with an empty body. Below, we subtype from GATlab's abstract types ObExpr and HomExpr to enable LaTeX pretty-printing and other convenient features, but this is not required.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CategoryExprs{ObExpr, HomExpr} ThCategory begin\nend\nA, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\ncompose(compose(f,g),h)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"The resulting symbolic expressions perform no simplification. For example, the associativity law is not satisfied:","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Thus, unlike instances of a theory, syntactic expressions are not expected to obey all the axioms of the theory.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"However, the user may supply logic in the body of the @symbolic_model macro to enforce the axioms or perform other kinds of simplification. Below, we use the associate function provided by GATlab to convert the binary expressions representing composition into n-ary expressions for any number n. The option strict=true tells GATlab to check that the domain and codomain objects are strictly equal and throw an error if they are not.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model SimplifyingCategoryExprs{ObExpr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))\nend\nA, B, C, D = [ Ob(SimplifyingCategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\ncompose(compose(f,g),h)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Now the associativity law is satisfied:","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"concepts/symbolic_models/#Primitive-versus-derived-operations","page":"Symbolic Models","title":"Primitive versus derived operations","text":"","category":"section"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"In some algebraic structures, there is a choice as to which operations should be considered primitive and which should be derived. For example, in a cartesian monoidal category, the copy operation Delta_X X to X otimes X can be defined in terms of the pairing operation langle f g rangle, or vice versa. In addition, the projections pi_XY X otimes Y to X and pi_XY X otimes Y to Y can be defined in terms of the deleting operation (terminal morphism) or left as primitive.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"In GATlab, the recommended way to deal with such situations is to define all the operations in the theory and then allow particular syntax systems to determine which operations, if any, will be derived from others. In the case of the cartesian monoidal category, we could define a signature CartesianCategory by inheriting from the builtin theory SymmetricMonoidalCategory.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"using GATlab","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@signature ThCartesianCategory <: ThSymmetricMonoidalCategory begin\n mcopy(A::Ob)::(A → (A ⊗ A))\n delete(A::Ob)::(A → munit())\n pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)\n proj1(A::Ob, B::Ob)::((A ⊗ B) → A)\n proj2(A::Ob, B::Ob)::((A ⊗ B) → B)\nend\nnothing # hide","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"We could then define the copying operation in terms of the pairing.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CartesianCategoryExprsV1{ObExpr,HomExpr} ThCartesianCategory begin\n mcopy(A::Ob) = pair(id(A), id(A))\nend\nA = Ob(CartesianCategoryExprsV1.Ob, :A)\nmcopy(A)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Alternatively, we could define the pairing and projections in terms of the copying and deleting operations.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CartesianCategoryExprsV2{ObExpr,HomExpr} ThCartesianCategory begin\n pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))\n proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))\n proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))\nend\nA, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ]\nf, g = Hom(:f, A, B), Hom(:g, A, C)\npair(f, g)","category":"page"},{"location":"#GATlab.jl","page":"GATlab.jl","title":"GATlab.jl","text":"","category":"section"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"CurrentModule = GATlab","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"GATlab.jl is a computer algebra system based on Generalized Algebraic Theories.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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 mathbbR^2 to mathbbR given by (xy) 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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"The second part of GATlab is concerned with computational semantics. The core of computational semantics is models of theories. A model tells you:","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"When a Julia value is a valid instance of a type in a theory\nHow to apply term constructors to Julia values","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"There are many programs which have influenced the development of GATlab; here we just list a few:","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"MMT\nMaude\nSymbolics.jl\nMetatheory.jl\nEgg\nStandard ML modules","category":"page"}] +[{"location":"api/#Library-Reference","page":"Library Reference","title":"Library Reference","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [GATlab]","category":"page"},{"location":"api/#Syntax","page":"Library Reference","title":"Syntax","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Syntax,\n GATlab.Syntax.Scopes,\n GATlab.Syntax.GATs,\n GATlab.Syntax.GATContexts,\n GATlab.Syntax.ExprInterop,\n GATlab.Syntax.TheoryInterface,\n]","category":"page"},{"location":"api/#GATlab.Syntax.Scopes.Binding","page":"Library Reference","title":"GATlab.Syntax.Scopes.Binding","text":"Binding{T}\n\nA binding associates some T-typed value to a name.\n\nname is an optional distinguished name value is the element\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Context","page":"Library Reference","title":"GATlab.Syntax.Scopes.Context","text":"A Context is anything which contains an ordered list of scopes.\n\nScopes within a context are referred to by level, which is their index within this list.\n\nContexts should overload:\n\ngetscope(c::Context, level::Int) -> Scope\nnscopes(c::Context) -> Int\nhastag(c::Context, tag::ScopeTag) -> Bool\nhasname(c::Context, name::Symbol) -> Bool\ngetlevel(c::Context, tag::ScopeTag) -> Int\ngetlevel(c::Context, name::Symbol) -> Int\nalltags(c::Context) -> Set{ScopeTag}\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.HasScope","page":"Library Reference","title":"GATlab.Syntax.Scopes.HasScope","text":"An abstract type for wrappers around a single scope.\n\nMust overload\n\ngetscope(hs::HasScope) -> Scope\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.HasScopeList","page":"Library Reference","title":"GATlab.Syntax.Scopes.HasScopeList","text":"A type for things which contain a scope list.\n\nNotably, GATs contain a scope list.\n\nMust implement:\n\ngetscopelist(hsl::HasScopeList) -> ScopeList\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Ident","page":"Library Reference","title":"GATlab.Syntax.Scopes.Ident","text":"Ident\n\nAn identifier.\n\ntag 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\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.LID","page":"Library Reference","title":"GATlab.Syntax.Scopes.LID","text":"A LID (Local ID) indexes a given scope.\n\nCurrently, scopes assign LIDs sequentially – this is not a stable guarantee however, and in theory scopes could have \"sparse\" LIDs.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.Scope","page":"Library Reference","title":"GATlab.Syntax.Scopes.Scope","text":"Scope{T}\n\nIn 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:\n\nx = 3\ny = \"hello\"\nz = x \n\nHere 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.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopeTag","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopeTag","text":"The tag that makes reference to a specific scope possible.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopeTagError","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopeTagError","text":"ScopeTagError\n\nAn error to throw when an identifier has an unexpected scope tag\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.ScopedBinding","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopedBinding","text":"Type for printing out bindings with colored keys\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.Scopes.getidents-Tuple{HasScope}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getidents","text":"This collects all the idents in a scope\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.getlid-Tuple{HasScope, Symbol}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getlid","text":"Determine the level of a binding given the name\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.hasident-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.hasident","text":"hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.ident-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.ident","text":"ident creates an Ident from a context and some partial data supplied as keywords.\n\nKeywords arguments:\n\ntag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.\nname::Union{Symbol, Nothing}. The name of the identifier.\nlid::Union{LID, Nothing}. The lid of the identifier within its scope.\nlevel::Union{Int, Nothing}. The level of the scope within the context.\nstrict::Bool. If strict is true, throw an error if not found, else return nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.idents-Tuple{Context}","page":"Library Reference","title":"GATlab.Syntax.Scopes.idents","text":"This is a broadcasted version of ident\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.rename-Tuple{ScopeTag, Dict{Symbol, Symbol}, Any}","page":"Library Reference","title":"GATlab.Syntax.Scopes.rename","text":"rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T\n\nRecurse 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.retag-Tuple{Dict{ScopeTag, ScopeTag}, Any}","page":"Library Reference","title":"GATlab.Syntax.Scopes.retag","text":"retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T\n\nRecurse 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.unsafe_pushbinding!-Union{Tuple{T}, Tuple{Scope{T}, Binding{T}}} where T","page":"Library Reference","title":"GATlab.Syntax.Scopes.unsafe_pushbinding!","text":"Add a new binding to the end of Scope s.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.AbstractConstant","page":"Library Reference","title":"GATlab.Syntax.GATs.AbstractConstant","text":"We need this to resolve a mutual reference loop; the only subtype is Constant\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AbstractDot","page":"Library Reference","title":"GATlab.Syntax.GATs.AbstractDot","text":"We need this to resolve a mutual reference loop; the only subtype is Dot\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgAccessor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgAccessor","text":"AlgAccessor\n\nThe arguments to a term constructor serve a dual function as both arguments and also methods to extract the value of those arguments.\n\nI.e., declaring Hom(dom::Ob, codom::Ob)::TYPE implicitly overloads a previous declaration for dom and codom, or creates declarations if none previously exist.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgAxiom","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgAxiom","text":"AlgAxiom\n\nA declaration of an axiom\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgDeclaration","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgDeclaration","text":"AlgDeclaration\n\nA declaration of a constructor; constructor methods in the form of AlgTermConstructors or the accessors for AlgTypeConstructors follow later in the theory.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgDot","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgDot","text":"Accessing a name from a term of tuple type\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgEqSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgEqSort","text":"AlgSort\n\nA sort for equality judgments of terms for a particular sort\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgFunction","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgFunction","text":"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.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSort","text":"AlgSort\n\nA sort, which is essentially a type constructor without arguments\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgSorts","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSorts","text":"AlgSorts\n\nA description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgStruct","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgStruct","text":"AlgStruct\n\nA declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor which constructs an element of that type, and projection term constructors. E.g.\n\nstruct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]\n apex::Ob\n i1::dom->apex\n i2::codom->apex\nend\n\nIs tantamount to (in a vanilla GAT):\n\nCospan(dom::Ob, codom::Ob)::TYPE \n\ncospan(apex, i1, i2)::Cospan(dom, codom) \n ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]\n\napex(csp::Cospan(d::Ob, c::Ob))::Ob \ni1(csp::Cospan(d::Ob, c::Ob))::(d->apex(csp))\ni2(csp::Cospan(d::Ob, c::Ob))::(c->apex(csp))\n\napex(cospan(a, i_1, i_2)) == a \n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\ni1(cospan(a, i_1, i_2)) == i_1 \n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\ni2(cospan(a, i_1, i_2)) == i_2\n ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]\n\ncospan(apex(csp), i1(csp), i2(csp)) == csp\n ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTerm","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTerm","text":"AlgTerm\n\nOne syntax tree to rule all the terms.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTermConstructor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTermConstructor","text":"AlgTermConstructor\n\nA declaration of a term constructor as a method of an AlgFunction.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgType","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgType","text":"AlgType\n\nOne syntax tree to rule all the types.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.AlgTypeConstructor","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTypeConstructor","text":"AlgTypeConstructor\n\nA declaration of a type constructor.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.Constant","page":"Library Reference","title":"GATlab.Syntax.GATs.Constant","text":"Constant\n\nA Julia value in an algebraic context. Type checked elsewhere.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.Eq","page":"Library Reference","title":"GATlab.Syntax.GATs.Eq","text":"Eq\n\nThe type of equality judgments.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GAT","page":"Library Reference","title":"GATlab.Syntax.GATs.GAT","text":"GAT\n\nA 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.\n\nGATs allow overloading but not shadowing.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GATContext","page":"Library Reference","title":"GATlab.Syntax.GATs.GATContext","text":"GATContext\n\nA context consisting of two parts: a GAT and a TypeCtx\n\nCertain types (like AlgTerm) can only be parsed in a GATContext, because they require access to the method resolving in the GAT.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.GATSegment","page":"Library Reference","title":"GATlab.Syntax.GATs.GATSegment","text":"GATSegment\n\nA piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.\n\nThis is a struct rather than just a type alias so that we can customize the show method.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{AlgType}, Tuple{GAT, Ident}} where AlgType","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical type + ctx associated with a type constructor.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{T}, Tuple{GAT, Ident}} where T<:AlgAST","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical term + ctx associated with a method.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.Judgment","page":"Library Reference","title":"GATlab.Syntax.GATs.Judgment","text":"A GAT is conceptually a bunch of Judgments strung together.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.MethodApp","page":"Library Reference","title":"GATlab.Syntax.GATs.MethodApp","text":"MethodApp\n\nAn 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.\n\nmethod either points to an AlgTermConstructor, an AlgTypeConstructor or an AlgAccessor,\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.MethodResolver","page":"Library Reference","title":"GATlab.Syntax.GATs.MethodResolver","text":"MethodResolver\n\nRight now, this just maps a sort signature to the resolved method.\n\nWhen we eventually support varargs, this will have to do something slightly fancier.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.TypeScope","page":"Library Reference","title":"GATlab.Syntax.GATs.TypeScope","text":"TypeScope\n\nA 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)}\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.show-Union{Tuple{T}, Tuple{IO, T}} where T<:Union{AlgTerm, AlgType}","page":"Library Reference","title":"Base.show","text":"Common methods for AlgType and AlgTerm\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{GAT, Any, Any}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Coerce GATs to GAT contexts\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.toexpr-Tuple{GAT, GATSegment}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"This only works when seg is a segment of theory\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.equations-Tuple{GAT, Ident}","page":"Library Reference","title":"GATlab.Syntax.GATs.equations","text":"Get equations for a term or type constructor\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.equations-Tuple{GATContext, AbstractVector{Ident}}","page":"Library Reference","title":"GATlab.Syntax.GATs.equations","text":"Implicit equations defined by a context.\n\nThis 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.\n\nReferences:\n\n(Cartmell, 1986, Sec 6: \"Essentially algebraic theories and categories with finite limits\")\n(Freyd, 1972, \"Aspects of topoi\")\n\nThis function gives expressions for computing the elements of c.context which can be inferred from applying accessor functions to elements of args.\n\nExample:\n\nequations({f::Hom(a,b), g::Hom(b,c)}, {a::Ob, b::Ob, c::Ob}, ThCategory)\n\nwaysofcomputing = Dict(a => [dom(f)], b => [codom(f), dom(g)], c => [codom(g)], f => [f], g => [g])\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.normalize_judgment-Tuple{Any}","page":"Library Reference","title":"GATlab.Syntax.GATs.normalize_judgment","text":"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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.parse_scope!-Tuple{Function, Scope, AbstractVector}","page":"Library Reference","title":"GATlab.Syntax.GATs.parse_scope!","text":"f(pushbinding!, expr) should inspect expr and call pushbinding! 0 or more times with two arguments: the name and value of a new binding.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.sortcheck-Tuple{Context, AlgTerm}","page":"Library Reference","title":"GATlab.Syntax.GATs.sortcheck","text":"sortcheck(ctx::Context, t::AlgTerm)\n\nThrow 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.sortcheck-Tuple{Context, AlgType}","page":"Library Reference","title":"GATlab.Syntax.GATs.sortcheck","text":"sortcheck(ctx::Context, t::AlgType)\n\nThrow an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.structs-Tuple{GAT}","page":"Library Reference","title":"GATlab.Syntax.GATs.structs","text":"Get all structs in a theory\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.substitute_funs-Tuple{Context, AlgTerm}","page":"Library Reference","title":"GATlab.Syntax.GATs.substitute_funs","text":"Replace all functions with their desugared expressions\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.substitute_term-Union{Tuple{T}, Tuple{T, Dict{Ident, AlgTerm}}} where T<:AlgAST","page":"Library Reference","title":"GATlab.Syntax.GATs.substitute_term","text":"Replace idents with AlgTerms. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{GATContext, Any, Type{GATContext}}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Parse, e.g.:\n\n(a,b,c)::Ob\nf::Hom(a, b)\ng::Hom(b, c)\nh::Hom(a, c)\nh′::Hom(a, c)\ncompose(f, g) == h == h′\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATContexts.@symbolic-Tuple{Any, Any}","page":"Library Reference","title":"GATlab.Syntax.GATContexts.@symbolic","text":"@symbolic ThRing function v(a, b, c)\n (a*b, c, b)\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"fromexpr(c::Context, e::Any, T::Type) -> Union{T,Nothing}\n\nConverts a Julia Expr into type T, in a certain scope.\n\n\n\n\n\n","category":"function"},{"location":"api/#GATlab.Syntax.ExprInterop.toexpr","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"toexpr(c::Context, t) -> Any\n\nConverts 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.\n\n\n\n\n\n","category":"function"},{"location":"api/#GATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP","text":"When we declare a new theory, we add the scope tag of its new segment to this dictionary pointing to the module corresponding to the new theory.\n\n\n\n\n\n","category":"constant"},{"location":"api/#GATlab.Syntax.TheoryInterface.fqmn-Tuple{Module}","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.fqmn","text":"Fully Qualified Module Name\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.TheoryInterface.mk_struct-Tuple{AlgStruct, Any}","page":"Library Reference","title":"GATlab.Syntax.TheoryInterface.mk_struct","text":"\n\n\n\n","category":"method"},{"location":"api/#Models","page":"Library Reference","title":"Models","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Models,\n GATlab.Models.ModelInterface,\n GATlab.Models.SymbolicModels,\n ]","category":"page"},{"location":"api/#GATlab.Models.ModelInterface.ImplementationNotes","page":"Library Reference","title":"GATlab.Models.ModelInterface.ImplementationNotes","text":"ImplementationNotes\n\nInformation about how a model implements a GATSegment. Right now, just the docstring attached to the @instance macro, but could contain more info in the future.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Models.ModelInterface.implements-Union{Tuple{tag}, Tuple{Module, Type{Val{tag}}}} where tag","page":"Library Reference","title":"GATlab.Models.ModelInterface.implements","text":"implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}\n\nIf m implements the GATSegment referred to by tag, then return the corresponding implementation notes.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.parse_instance_body-Tuple{Expr, GAT}","page":"Library Reference","title":"GATlab.Models.ModelInterface.parse_instance_body","text":"Parses the raw julia expression into JuliaFunctions\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.qualify_function-Tuple{JuliaFunction, Any, Union{Nothing, Expr, Symbol}, Any, Any}","page":"Library Reference","title":"GATlab.Models.ModelInterface.qualify_function","text":"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\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.to_call_impl-Tuple{AlgTerm, GAT, Union{Module, Symbol}, Bool}","page":"Library Reference","title":"GATlab.Models.ModelInterface.to_call_impl","text":"Compile an AlgTerm into a Julia call Expr where termcons (e.g. f) are interpreted as mod.f[model.model](...).\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.typecheck_instance-Tuple{GAT, Vector{JuliaFunction}, Vector{Symbol}, Dict{AlgSort}}","page":"Library Reference","title":"GATlab.Models.ModelInterface.typecheck_instance","text":"Throw error if missing a term constructor. Provides default instances for type constructors and type arguments, which return true or error, respectively.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.TheoryMaps.migrator-NTuple{5, Any}","page":"Library Reference","title":"GATlab.Syntax.TheoryMaps.migrator","text":"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.\n\nFuture 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.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.ModelInterface.@instance-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.ModelInterface.@instance","text":"Usage:\n\nstruct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}\n ntypes::Int\nend\n\n@instance ThCategory{Vector{Int}, Vector{Int}} [model::TypedFinSetC] begin\n Ob(v::Vector{Int}) = all(1 <= j <= model.ntypes for j in v)\n Hom(f::Vector{Int}, v::Vector{Int}, w::Vector{Int}) =\n length(f) == length(v) && all(1 <= y <= length(w) for y in f)\n\n id(v::Vector{Int}) = collect(eachindex(v))\n compose(f::Vector{Int}, g::Vector{Int}) = g[f]\n\n dom(f::Vector{Int}; context) = context.dom\n codom(f::Vector{Int}; context) = context.codom\nend\n\nstruct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Hom}, Hom}}\n c::C\nend\n\n@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#GATlab.Models.SymbolicModels.GATExpr","page":"Library Reference","title":"GATlab.Models.SymbolicModels.GATExpr","text":"Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.\n\nWe 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.)\n\nThe 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.\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.nameof-Tuple{GATExpr{:generator}}","page":"Library Reference","title":"Base.nameof","text":"Get name of GAT generator expression as a Symbol.\n\nIf the generator has no name, returns nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.constructor_name-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.constructor_name","text":"Name of constructor that created expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.functor-Tuple{Tuple, GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.functor","text":"Functor from GAT expression to GAT instance.\n\nStrictly 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\".\n\nA functor is completely determined by its action on the generators. There are several ways to specify this mapping:\n\nSpecify 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.\nExplicitly map each generator term to an instance value, using the generators dictionary.\nFor 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.\n\nThe 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.\n\nFIXME\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.generator_like-Tuple{GATExpr, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.generator_like","text":"Create generator of the same type as the given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.parse_json_sexpr-Tuple{Module, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.parse_json_sexpr","text":"Deserialize expression from JSON-able S-expression.\n\nIf symbols is true (the default), strings are converted to symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_latex-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_latex","text":"Show the expression in infix notation using LaTeX math.\n\nDoes not include $ or \\[begin|end]{equation} delimiters.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_sexpr","text":"Show the syntax expression as an S-expression.\n\nCf. the standard library function Meta.show_sexpr.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_unicode-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_unicode","text":"Show the expression in infix notation using Unicode symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.symbolic_instance_methods-Tuple{GAT, Any, Symbol, Dict{Ident, JuliaFunction}}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.symbolic_instance_methods","text":"Julia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.syntax_module-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.syntax_module","text":"Get syntax module of given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.to_json_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.to_json_sexpr","text":"Serialize expression as JSON-able S-expression.\n\nThe format is an S-expression encoded as JSON, e.g., \"compose(f,g)\" is represented as [\"compose\", f, g].\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.@symbolic_model-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.@symbolic_model","text":"@symbolic_model generates the free model of a theory, generated by symbols.\n\nThis is backwards compatible with the @syntax macro in Catlab.\n\nOne 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\".\n\nAn invocation of @symbolic_model creates the following.\n\nA module with a struct for each type constructor, which has a single type\n\nparameter 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.\n\nFor instance, in the theory of categories, we might have the following elements.\n\nusing .FreeCategory\nx = Ob{:generator}([:x], [])\ny = Ob{:generator}([:y], [])\nf = Hom{:generator}([:f], [x, y])\ng = Hom{:generator}([:g], [y, x])\nh = Hom{:compose}([f, g], [x, x])\n\nMethods inside the module (not exported) for all of the term constructors and\n\nfield accessors (i.e. stuff like compose, id, dom, codom), which construct terms.\n\nA default instance (i.e., without a model parameter) of the theory using the\n\ntypes in this generated model. Methods in this instance can be overridden by the body of @symbolic_model to perform rewriting for the sake of normalization, for instance flattening associative and unital operations.\n\nCoercion methods of the type constructors that allow one to introduce generators.\n\nx = ThCategory.Ob(FreeCategory.Ob, :x)\ny = ThCategory.Ob(FreeCategory.Ob, :y)\nf = ThCategory.Hom(:f, x, y)\n\nNote that in both the instance and in these coercion methods, we must give the expected type as the first argument when it cannot be infered by the other arguments. For instance, instead of\n\nmunit() = ...\n\nwe have\n\nmunit(::Type{FreeSMC.Ob}) = ...\n\nand likewise instead of\n\nThCategory.Ob(x::Any) = ...\n\nwe have\n\nThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...\n\nExample:\n\n@symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)\nend\n\nThis generates:\n\nmodule FreeCategory\nexport Ob, Hom\nusing ..__module__\n\nmodule Meta\n const theory_module = ThCategory\n const theory = ThCategory.Meta.theory\n const theory_type = ThCategory.Meta.T\nend\n\nstruct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol\n args::Vector\n type_args::Vector{GATExpr}\nend\n\nstruct Hom{T} <: __module__.HomExpr{T}\n args::Vector\n type_args::Vector{GATExpr}\nend\n\ndom(x::Hom) = x.type_args[1]\n\ncodom(x::Hom) = x.type_args[2]\n\nfunction compose(f::Hom, g::Hom; strict=true)\n if strict && !(codom(f) == dom(g))\n throw(SyntaxDomainError(:compose, [f, g]))\n end\n Hom{:compose}([f, g], [dom(f), codom(g)])\nend\n\nfunction id(x::Ob)\n Ob{:id}([x], [x, x])\nend\nend\n\n# default implementations \n\nfunction ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob\n FreeCategory.dom(x)\nend\n\nfunction ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob\n FreeCategory.Ob{:generator}([__value__], [])\nend\n\nfunction ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom\n FreeCategory.id(A)\nend\n\nfunction ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)\n associate_unit(FreeCategory.compose(f, g; strict), id)\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#Utilities","page":"Library Reference","title":"Utilities","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Util,\n GATlab.Util.MetaUtils,\n ]","category":"page"},{"location":"api/#GATlab.Util.MetaUtils","page":"Library Reference","title":"GATlab.Util.MetaUtils","text":"General-purpose tools for metaprogramming in Julia.\n\n\n\n\n\n","category":"module"},{"location":"api/#GATlab.Util.MetaUtils.JuliaFunctionSigNoWhere","page":"Library Reference","title":"GATlab.Util.MetaUtils.JuliaFunctionSigNoWhere","text":"For comparing JuliaFunctionSigs modulo the where parameters\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Util.MetaUtils.concat_expr-Tuple{Expr, Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.concat_expr","text":"Concatenate two Julia expressions into a block expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.generate_docstring-Tuple{Expr, Union{Nothing, String}}","page":"Library Reference","title":"GATlab.Util.MetaUtils.generate_docstring","text":"Wrap Julia expression with docstring.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.generate_function-Tuple{JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.generate_function","text":"Generate Julia expression for function definition.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_docstring-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_docstring","text":"Parse Julia expression that is (possibly) annotated with docstring.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_function-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_function","text":"Parse Julia function definition into standardized form.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.parse_function_sig-Tuple{JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.parse_function_sig","text":"Parse signature of Julia function.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.replace_symbols-Tuple{AbstractDict, Any}","page":"Library Reference","title":"GATlab.Util.MetaUtils.replace_symbols","text":"Replace symbols occuring anywhere in a Julia expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.replace_symbols-Tuple{AbstractDict, JuliaFunction}","page":"Library Reference","title":"GATlab.Util.MetaUtils.replace_symbols","text":"Replace symbols occurring anywhere in a Julia function (except the name).\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Util.MetaUtils.strip_lines-Tuple{Expr}","page":"Library Reference","title":"GATlab.Util.MetaUtils.strip_lines","text":"Remove all LineNumberNodes from a Julia expression.\n\n\n\n\n\n","category":"method"},{"location":"concepts/catlab_differences/#Changes-from-Catlab-GATs","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#1.-Models-as-values","page":"Changes from Catlab GATs","title":"1. Models as values","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"struct FinSetInt\n n::Int\nend","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#2.-E-Graphs","page":"Changes from Catlab GATs","title":"2. E-Graphs","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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_1ldotsx_n) sim f(x_1ldotsx_n) for any term constructor f. E-graphs are used for a variety of purposes, including:","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"finding simple representations of terms\ndeciding whether two terms are equal","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/#3.-Indexed-dependent-types-in-models","page":"Changes from Catlab GATs","title":"3. Indexed dependent types in models","text":"","category":"section"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"A morphism between the finite sets 1ldotsn and 1ldotsm is simply a length-n vector whose entries are in 1ldotsm. 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}.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/catlab_differences/","page":"Changes from Catlab GATs","title":"Changes from Catlab GATs","text":"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.","category":"page"},{"location":"concepts/models/#Models-and-instances","page":"Models and instances","title":"Models and instances","text":"","category":"section"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"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.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"When a model m implements Th, the following methods should be defined.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"For every type constructor X in Th\nTh.X[m::typeof(m)](x, args...) = ...\nThis 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.\nFor 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.\nThis 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.\nFor each argument a to a type constructor (i.e. dom and codom for Hom), an overload of\nTh.a[m::typeof(m)](x) = ...\nThis 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.\nFor each term constructor f in Theory\nTh.f[m::typeof(m)](args...) = ...\nThis 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,\nThCategory.compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]\nTerm 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.","category":"page"},{"location":"concepts/models/","page":"Models and instances","title":"Models and instances","text":"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.","category":"page"},{"location":"concepts/scopes/#Scopes","page":"Scopes","title":"Scopes","text":"","category":"section"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Design rationale:","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"(the name \"local identifier\" and also some of this philosophy is taken from chit)","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"We name the failure of this relation to be a bijection in several ways.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one symbol is related to a single binding, we say that this","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"binding has aliases. In this case, we should also have a primary alias used as a default.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one binding is related to a single symbol, we have name overlap.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Name overlap can be resolved by overloading and shadowing, we will talk about this later on.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no symbol is related to a binding, such as when the binding is created","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no binding is related to a symbol, then we have a name error; this name","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"is not valid in the current context and we must throw an error.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"The most important thing to get right is name overlap; we discuss this first.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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\".","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"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.","category":"page"},{"location":"concepts/theories/#Theories","page":"Theories","title":"Theories","text":"","category":"section"},{"location":"concepts/theories/#What-is-a-GAT?","page":"Theories","title":"What is a GAT?","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Generalized Algebraic Theories (GATs) are the backbone of GATlab so let's expand a bit on GATs and how they fit into the bigger picture of algebra.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"An algebraic structure, like a group or category, is a mathematical object whose axioms all take the form of equations that are universally quantified (the equations have no exceptions). That’s not a formal definition but it’s a good heuristic. There are different ways to make this precise. The oldest, going back to universal algebra in the early 20th centrury, are algebraic theories.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples (\"models\") of algebraic structures. For instance, rather than take particular groups as the object of study, in universal algebra one takes the class of groups as an object of study. In an algebraic theory, you have a collection of (total) operations and they obey a set of equational axioms. Classically, there is only a single generating type, but there are also typed or multi-sorted versions of algebraic theories. Most of the classical structures of abstract algebra, such as groups, rings, and modules, can be defined as algebraic theories.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Importantly, the theory of categories is not algebraic. In other words, a category cannot be defined as a (multi-sorted) algebraic theory. The reason is that the operation of composition is partial, since you can only compose morphisms with compatible (co)domains. Now, categories sure feel like algebraic structures, so people have come up with generalizations of algebraic theories that accomodate categories and related structures.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"The first of these was Freyd’s essentially algebraic theories. In an essentially algebraic theory, you can have partially defined operations; however, to maintain the equational character of the system, the domains of operations must themselves be defined equationally. For example, the theory of categories would be defined as having two types, Ob and Hom, and the composition operation compose(f::Hom,g::Hom)::Hom would have domain given by the equation codom(f) == dom(g). As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Later, Cartmell proposed generalized algebraic theories, which solves the same problem but in a different way. Rather than having partial operations, you have total operations but on dependent types (types that are parameterized by values). So now the composition operation has signature compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) ⊣ [A::Ob, B::Ob, C::Ob] exactly as appears in GATlab. This is closer to the way that mathematicians actually think and write about categories. For example, if you look at the definitions of category, functor, and natural transformation in Emily Riehl’s textbook, you will see that they are already essentially in the form of a GAT, whereas they require translation into an essentially algebraic theory. Nevertheless, GATs and essentially algebraic theories have the same expressive power, at least in their standard set-based semantics. GATs provide a version of the computer scientist's type theory that plays well with the mathematician's algebra, thus, providing a perfect opportunity for computer algebra systems.","category":"page"},{"location":"concepts/theories/#The-@theory-macro","page":"Theories","title":"The @theory macro","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"GATlab implements a version of the GAT formalism on top of Julia's type system, taking advantage of Julia macros to provide a pleasant syntax. GATs are defined using the @theory macro.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"For example, the theory of categories could be defined by:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"using GATlab","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"@theory ThCategory begin\n @op begin\n (→) := Hom\n (⋅) := compose\n end\n Ob::TYPE\n Hom(dom::Ob, codom::Ob)::TYPE\n id(A::Ob)::(A → A)\n compose(f::(A → B), g::(B → C))::(A → C) ⊣ [A::Ob, B::Ob, C::Ob]\n (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob,\n f::(A → B), g::(B → C), h::(C → D)]\n f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)]\n id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)]\nend\nnothing # hide","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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).","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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).","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"The result of the @theory macro is a module with the following members:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"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, ⋅, →.\nA submodule called Meta with members:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"T: a zero-field struct that serves as a type-level signifier for the theory.\ntheory: a constant of type GAT which stores the data of the theory.\n@theory: a macro which expands directly to theory, which is used to pass around the data of the theory at macro-expand time.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"note: Note\nIn 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.","category":"page"},{"location":"concepts/theories/#References","page":"Theories","title":"References","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Cartmell, 1986: Generalized algebraic theories and contextual categories, DOI:10.1016/0168-0072(86)90053-9\nCartmell, 1978, PhD thesis: Generalized algebraic theories and contextual categories\nPitts, 1995: Categorical logic, Sec 6: Dependent types","category":"page"},{"location":"stdlib/#Standard-Library","page":"Standard Library","title":"Standard Library","text":"","category":"section"},{"location":"stdlib/#Categories","page":"Standard Library","title":"Categories","text":"","category":"section"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"Our friend ThCategory is the main theory in this module.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThCategory","text":"ThCategory\n\nThe theory of a category with composition operations and associativity and identity axioms.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"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.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThThinCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThThinCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThThinCategory","text":"ThThinCategory\n\nThe 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.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/#Category-Building-Blocks","page":"Standard Library","title":"Category Building Blocks","text":"","category":"section"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"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.","category":"page"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThClass","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThClass","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThClass","text":"ThClass\n\nA Class is just a Set that doesn't worry about foundations.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThLawlessCat","text":"ThLawlessCat\n\nThe data of a category without any axioms of associativity or identities.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThAscCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThAscCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThAscCat","text":"ThAsCat\n\nThe theory of a category with the associative law for composition.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"GATlab.Stdlib.StdTheories.ThIdLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.ThIdLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.ThIdLawlessCat","text":"ThIdLawlessCat\n\nThe theory of a category without identity axioms.\n\n\n\n\n\n","category":"module"},{"location":"stdlib/","page":"Standard Library","title":"Standard Library","text":"Modules = [GATlab.Stdlib,\n GATlab.Stdlib.StdTheories,\n GATlab.Stdlib.StdModels,\n ]","category":"page"},{"location":"concepts/symbolic_models/#Symbolic-Models","page":"Symbolic Models","title":"Symbolic Models","text":"","category":"section"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Theories can also be instantiated as systems of symbolic expressions, using the @symbolic_model macro. The symbolic expressions are expression trees, as commonly used in computer algebra systems. They are similar to Julia's Expr type but they are instead subtyped from GATlab's GATExpr type and they have a more refined type hierarchy.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"A single theory can have different syntax systems, treating different terms as primitive or performing different simplication or normalization procedures. GATlab tries to make it easy to define new syntax systems. Many of the theories included with GATlab have default syntax systems, but the user is encouraged to define their own to suit their needs.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"To get started, you can always call the @symbolic_model macro with an empty body. Below, we subtype from GATlab's abstract types ObExpr and HomExpr to enable LaTeX pretty-printing and other convenient features, but this is not required.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CategoryExprs{ObExpr, HomExpr} ThCategory begin\nend\nA, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\ncompose(compose(f,g),h)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"The resulting symbolic expressions perform no simplification. For example, the associativity law is not satisfied:","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Thus, unlike instances of a theory, syntactic expressions are not expected to obey all the axioms of the theory.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"However, the user may supply logic in the body of the @symbolic_model macro to enforce the axioms or perform other kinds of simplification. Below, we use the associate function provided by GATlab to convert the binary expressions representing composition into n-ary expressions for any number n. The option strict=true tells GATlab to check that the domain and codomain objects are strictly equal and throw an error if they are not.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model SimplifyingCategoryExprs{ObExpr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))\nend\nA, B, C, D = [ Ob(SimplifyingCategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\ncompose(compose(f,g),h)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Now the associativity law is satisfied:","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"concepts/symbolic_models/#Primitive-versus-derived-operations","page":"Symbolic Models","title":"Primitive versus derived operations","text":"","category":"section"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"In some algebraic structures, there is a choice as to which operations should be considered primitive and which should be derived. For example, in a cartesian monoidal category, the copy operation Delta_X X to X otimes X can be defined in terms of the pairing operation langle f g rangle, or vice versa. In addition, the projections pi_XY X otimes Y to X and pi_XY X otimes Y to Y can be defined in terms of the deleting operation (terminal morphism) or left as primitive.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"In GATlab, the recommended way to deal with such situations is to define all the operations in the theory and then allow particular syntax systems to determine which operations, if any, will be derived from others. In the case of the cartesian monoidal category, we could define a signature CartesianCategory by inheriting from the builtin theory SymmetricMonoidalCategory.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"using GATlab","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@signature ThCartesianCategory <: ThSymmetricMonoidalCategory begin\n mcopy(A::Ob)::(A → (A ⊗ A))\n delete(A::Ob)::(A → munit())\n pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)\n proj1(A::Ob, B::Ob)::((A ⊗ B) → A)\n proj2(A::Ob, B::Ob)::((A ⊗ B) → B)\nend\nnothing # hide","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"We could then define the copying operation in terms of the pairing.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CartesianCategoryExprsV1{ObExpr,HomExpr} ThCartesianCategory begin\n mcopy(A::Ob) = pair(id(A), id(A))\nend\nA = Ob(CartesianCategoryExprsV1.Ob, :A)\nmcopy(A)","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"Alternatively, we could define the pairing and projections in terms of the copying and deleting operations.","category":"page"},{"location":"concepts/symbolic_models/","page":"Symbolic Models","title":"Symbolic Models","text":"@symbolic_model CartesianCategoryExprsV2{ObExpr,HomExpr} ThCartesianCategory begin\n pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))\n proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))\n proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))\nend\nA, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ]\nf, g = Hom(:f, A, B), Hom(:g, A, C)\npair(f, g)","category":"page"},{"location":"#GATlab.jl","page":"GATlab.jl","title":"GATlab.jl","text":"","category":"section"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"CurrentModule = GATlab","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"GATlab.jl is a computer algebra system based on Generalized Algebraic Theories.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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 mathbbR^2 to mathbbR given by (xy) 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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"The second part of GATlab is concerned with computational semantics. The core of computational semantics is models of theories. A model tells you:","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"When a Julia value is a valid instance of a type in a theory\nHow to apply term constructors to Julia values","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"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.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"There are many programs which have influenced the development of GATlab; here we just list a few:","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"MMT\nMaude\nSymbolics.jl\nMetatheory.jl\nEgg\nStandard ML modules","category":"page"}] } diff --git a/dev/stdlib/index.html b/dev/stdlib/index.html index 62189ba8..52a6aa21 100644 --- a/dev/stdlib/index.html +++ b/dev/stdlib/index.html @@ -1,2 +1,2 @@ -Standard Library · GATlab.jl
GitHub

Standard Library

Categories

Our friend ThCategory is the main theory in this module.

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)]

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.

+Standard Library · GATlab.jl
GitHub

Standard Library

Categories

Our friend ThCategory is the main theory in this module.

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)]

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.