diff --git a/dev/api/index.html b/dev/api/index.html index 68482ec7..40ce56ed 100644 --- a/dev/api/index.html +++ b/dev/api/index.html @@ -1,12 +1,12 @@ -Library Reference · GATlab.jl

Library Reference

Syntax

GATlab.Syntax.Scopes.BindingType

Binding{T, Sig}

A binding associates some T-typed value to a name and possibly some aliases, disambiguated by a signature in Sig in the case of overloading.

primary is an optional distinguished element of aliases value is the element sig is a way of uniquely distinguishing this element from others with the same name (for example, ⊗ : Ob x Ob -> Ob and Hom x Hom -> Hom)

source
GATlab.Syntax.Scopes.ContextType

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
source
GATlab.Syntax.Scopes.IdentType

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.LIDType

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.ScopeType

Scope{T, Sig}

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. For example, a scope with 3 elements:

x::Int = 3
+Library Reference · GATlab.jl

Library Reference

Syntax

GATlab.Syntax.Scopes.BindingType

Binding{T, Sig}

A binding associates some T-typed value to a name and possibly some aliases, disambiguated by a signature in Sig in the case of overloading.

primary is an optional distinguished element of aliases value is the element sig is a way of uniquely distinguishing this element from others with the same name (for example, ⊗ : Ob x Ob -> Ob and Hom x Hom -> Hom)

source
GATlab.Syntax.Scopes.ContextType

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
source
GATlab.Syntax.Scopes.IdentType

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.LIDType

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.ScopeType

Scope{T, Sig}

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. For example, a scope with 3 elements:

x::Int = 3
 y::String = "hello"
-x::String = "ex"

This is a valid scope even though there are name collisions, because the signature (in this case, a datatype) disambiguates. Of course, it may not be wise to disambiguate by type, because it is not always possible to infer expected type. In general, one should pick something that can be inferred, and Nothing is always a reasonable choice, which disallows any name collisions.

source
GATlab.Syntax.Scopes.hasidentMethod

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.identMethod

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.
  • sig::Any. The signature of the identifier, to disambiguate between multiple identifiers with the same name within the same scope.
  • strict::Bool. If strict is true, throw an error if not found, else return nothing.
  • isunique::Bool. If isunique is true, then don't use the signature to disambiguate, instead fail if their are multiple identifiers with the same name in a scope.
source
GATlab.Syntax.Scopes.renameMethod

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.retagMethod

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.AlgSortsType

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.AlgTermType

AlgTerm

One syntax tree to rule all the terms. Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant

source
GATlab.Syntax.GATs.GATType

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.equationsMethod

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 each of the elements of context from the args, as well as checking that the args are well-typed.

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

Algorithm:

Start from the arguments. We know how to compute each of the arguments; they are given. Each argument tells us how to compute other arguments, and also elements of the context

source
GATlab.Syntax.GATs.sortcheckMethod

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.sortcheckMethod

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.Presentations.PresentationType

A presentation has a set of generators, given by a TypeScope, and a set of equations among terms which can refer to those generators. Each element of eqs is a list of terms which are asserted to be equal.

source
GATlab.Syntax.ExprInterop.fromexprMethod

Parse, e.g.:

(a,b,c)::Ob
+x::String = "ex"

This is a valid scope even though there are name collisions, because the signature (in this case, a datatype) disambiguates. Of course, it may not be wise to disambiguate by type, because it is not always possible to infer expected type. In general, one should pick something that can be inferred, and Nothing is always a reasonable choice, which disallows any name collisions.

source
Base.:+Method

Deterministically combine two scope tags into a third

source
GATlab.Syntax.Scopes.hasidentMethod

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.identMethod

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.
  • sig::Any. The signature of the identifier, to disambiguate between multiple identifiers with the same name within the same scope.
  • strict::Bool. If strict is true, throw an error if not found, else return nothing.
  • isunique::Bool. If isunique is true, then don't use the signature to disambiguate, instead fail if their are multiple identifiers with the same name in a scope.
source
GATlab.Syntax.Scopes.renameMethod

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.retagMethod

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.AlgSortsType

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.AlgTermType

AlgTerm

One syntax tree to rule all the terms. Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant

source
GATlab.Syntax.GATs.GATType

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.equationsMethod

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 each of the elements of context from the args, as well as checking that the args are well-typed.

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

Algorithm:

Start from the arguments. We know how to compute each of the arguments; they are given. Each argument tells us how to compute other arguments, and also elements of the context

source
GATlab.Syntax.GATs.infer_typeMethod

Infer the type of the term of a term. If it is not in context, recurse on its arguments. The term constructor's output type yields the resulting type once its localcontext variables are substituted with the relevant AlgTerms.

          (x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z)

E.g. given ––––––––––––––––––– id(x)⋅(p⋅q)

             (a,b,c)::Ob, f::Hom(a,b), g::Hom(b,c)

and output type: –––––––––––––––––– Hom(a,c)

We first recursively find {id(x) => Hom(x,x), p⋅q => Hom(x,z)}. We ultimately want an AlgTerm for everything in the output type's context such that we can substitute into Hom(a,c) to get the final answer. It will help to also compute the AlgType for everything in the context. We work backwards, since we start by knowing {f => id(x)::Hom(x,x), g=> p⋅q :: Hom(x,z)}. For a b and c, we use equations which tell us, e.g., that a = dom(f). So we can grab the first argument of the type of f (i.e. grab x from Hom(x,x)).

source
GATlab.Syntax.GATs.parsetypescopeMethod

Keep track of variables already bound (e.g. in local context) so that they need not be redefined, e.g. compose(f,g::Hom(b,c)) ⊣ [(a,b,c)::Ob, f::Hom(a,b)] (If f were not defined in the local context, it would be parsed as default.)

source
GATlab.Syntax.GATs.sortcheckMethod

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.sortcheckMethod

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.Presentations.PresentationType

A presentation has a set of generators, given by a TypeScope, and a set of equations among terms which can refer to those generators. Each element of eqs is a list of terms which are asserted to be equal.

source
GATlab.Syntax.ExprInterop.toexprFunction

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.implementsMethod

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.Syntax.ExprInterop.toexprFunction

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.implementsMethod

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.@instanceMacro

Usage:

struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
   ntypes::Int
 end
 
@@ -27,4 +27,4 @@
 end
 
 @instance ThCategory{Tuple{Ob, Hom}, Hom} (;model::SliceCat{Ob, Hom, C}) where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
-end
source

Utilities

+end
source

Utilities

diff --git a/dev/concepts/models/index.html b/dev/concepts/models/index.html index 590ab9fd..452399c1 100644 --- a/dev/concepts/models/index.html +++ b/dev/concepts/models/index.html @@ -1,2 +1,2 @@ -Model families · GATlab.jl

Model families

The semantics part of GATlab is the model family infrastructure.

Given a theory, one can declare a model family for that theory. This consists of the following.

  1. A struct T. Each value of the struct is a model of the theory. The struct subtypes Model{Th, Tuple{Ts...}}. Th is the theory that the struct is a model family for, and Ts specifies types for each of the type constructors in Theory.

  2. For each type constructor i in Theory, an overload of checkvalidity of the form

    checkvalidity(m::T, ::TypCon{i}, args..., val) = ...

    This checks that val is a valid instance of i applied to args..., assuming that args... have been previously checked to be valid.

    This can then be applied using, for instance

    checkvalidity(m, Category.Hom, x, y, f)

    using the singleton structs defined in Theories

  3. For each term constructor i in Theory, an overload of ap of the form

    ap(m::T, ::TrmCon{i}, args...) = ...

    Here args... is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of ap might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.

+Model families · GATlab.jl

Model families

The semantics part of GATlab is the model family infrastructure.

Given a theory, one can declare a model family for that theory. This consists of the following.

  1. A struct T. Each value of the struct is a model of the theory. The struct subtypes Model{Th, Tuple{Ts...}}. Th is the theory that the struct is a model family for, and Ts specifies types for each of the type constructors in Theory.

  2. For each type constructor i in Theory, an overload of checkvalidity of the form

    checkvalidity(m::T, ::TypCon{i}, args..., val) = ...

    This checks that val is a valid instance of i applied to args..., assuming that args... have been previously checked to be valid.

    This can then be applied using, for instance

    checkvalidity(m, Category.Hom, x, y, f)

    using the singleton structs defined in Theories

  3. For each term constructor i in Theory, an overload of ap of the form

    ap(m::T, ::TrmCon{i}, args...) = ...

    Here args... is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of ap might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.

diff --git a/dev/concepts/overview/index.html b/dev/concepts/overview/index.html index 86e83165..10ab7551 100644 --- a/dev/concepts/overview/index.html +++ b/dev/concepts/overview/index.html @@ -1,4 +1,4 @@ For Catlab users · GATlab.jl

For Catlab users

GATlab is a refactoring of the core GAT system in Catlab. 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.

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. Typechecking in general for a GAT requires deciding the equality of arbitrary terms, which is 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. I.e., 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. Typechecking in general for a GAT requires deciding the equality of arbitrary terms, which is 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. I.e., 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/scopes/index.html b/dev/concepts/scopes/index.html index 6cecdd0c..2301bfb5 100644 --- a/dev/concepts/scopes/index.html +++ b/dev/concepts/scopes/index.html @@ -1,2 +1,2 @@ -Scopes · GATlab.jl

Scopes

Design rationale:

Namespacing should be first class. This doesn't play nicely with deBruijn levels; we don't want to do a bunch of math to convert between flattened and unflattened versions of contexts. There is an accepted solution to the problem of organizing names: use refs! Mathematically speaking, a ref is just a list of deBruijn levels.

However, deBruijn levels are unfriendly for users; we want to be able to give names to our variables!

In general, naming is given by a relation between symbols and bindings (as referred to by deBruijn levels). 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 deBruijn level 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 deBruijn level) 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

Scopes

Design rationale:

Namespacing should be first class. This doesn't play nicely with deBruijn levels; we don't want to do a bunch of math to convert between flattened and unflattened versions of contexts. There is an accepted solution to the problem of organizing names: use refs! Mathematically speaking, a ref is just a list of deBruijn levels.

However, deBruijn levels are unfriendly for users; we want to be able to give names to our variables!

In general, naming is given by a relation between symbols and bindings (as referred to by deBruijn levels). 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 deBruijn level 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 deBruijn level) 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/theories/index.html b/dev/concepts/theories/index.html index 6df85f3e..57cdaca1 100644 --- a/dev/concepts/theories/index.html +++ b/dev/concepts/theories/index.html @@ -11,4 +11,4 @@ struct compose <: TrmCon{3} end ... -end +end diff --git a/dev/index.html b/dev/index.html index 39f126e7..764af997 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -GATlab.jl · GATlab.jl

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. I.e., the term $x^{2} + y^{2}$ represents the function $\mathbb{R}^2 \to \mathbb{R}$ given by $(x,y) \mapsto x^{2} + y^{2}$. However, GATlab also supports higher-level symbolic constructs. For instance, we can consider "substitutions" between contexts, which map free variables in one context to terms in another, as symbolic functions, 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 a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are Vectors of ring elements.

GATlab is the new 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

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. I.e., the term $x^{2} + y^{2}$ represents the function $\mathbb{R}^2 \to \mathbb{R}$ given by $(x,y) \mapsto x^{2} + y^{2}$. However, GATlab also supports higher-level symbolic constructs. For instance, we can consider "substitutions" between contexts, which map free variables in one context to terms in another, as symbolic functions, 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 a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are Vectors of ring elements.

GATlab is the new 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.html b/dev/search/index.html index 54a9e49a..359e9629 100644 --- a/dev/search/index.html +++ b/dev/search/index.html @@ -1,2 +1,2 @@ -Search · GATlab.jl

Loading search...

    +Search · GATlab.jl

    Loading search...

      diff --git a/dev/search_index.js b/dev/search_index.js index e7a7eacb..e5d67079 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.Presentations,\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, Sig}\n\nA binding associates some T-typed value to a name and possibly some aliases, disambiguated by a signature in Sig in the case of overloading.\n\nprimary is an optional distinguished element of aliases value is the element sig is a way of uniquely distinguishing this element from others with the same name (for example, ⊗ : Ob x Ob -> Ob and Hom x Hom -> Hom)\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\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.Reference","page":"Library Reference","title":"GATlab.Syntax.Scopes.Reference","text":"Reference\n\nA path of identifiers. We optimize for the (frequent) case where there is only one identifier by making this a linked list.\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, Sig}\n\nIn 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. For example, a scope with 3 elements:\n\nx::Int = 3\ny::String = \"hello\"\nx::String = \"ex\"\n\nThis is a valid scope even though there are name collisions, because the signature (in this case, a datatype) disambiguates. Of course, it may not be wise to disambiguate by type, because it is not always possible to infer expected type. In general, one should pick something that can be inferred, and Nothing is always a reasonable choice, which disallows any name collisions.\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.getlid-Union{Tuple{Sig}, Tuple{T}, Tuple{HasScope{T, Sig}, Symbol}} where {T, Sig}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getlid","text":"Determine the level of a binding given the name and possibly the signature\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.\nsig::Any. The signature of the identifier, to disambiguate between multiple identifiers with the same name within the same scope.\nstrict::Bool. If strict is true, throw an error if not found, else return nothing.\nisunique::Bool. If isunique is true, then don't use the signature to disambiguate, instead fail if their are multiple identifiers with the same name in a scope.\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_addalias!-Tuple{Scope, Symbol, Symbol}","page":"Library Reference","title":"GATlab.Syntax.Scopes.unsafe_addalias!","text":"unsafe_addalias! should only be used when unsafe_pushbinding! won't be called again, because new bindings won't get the old aliases.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.Judgment","page":"Library Reference","title":"GATlab.Syntax.GATs.Judgment","text":"Judgment\n\nA judgment is either a type constructor, term constructor, or axiom; a GAT is composed of a list of judgments.\n\n\n\n\n\n","category":"type"},{"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.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.AlgSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSort","text":"AlgSort\n\nA sort, which is essentially a type constructor without arguments ref must be reference to a AlgTypeConstructor\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.AlgTerm","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTerm","text":"AlgTerm\n\nOne syntax tree to rule all the terms. Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant\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\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. head must be reference to a AlgTypeConstructor\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. Checked elsewhere.\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.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\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.JudgmentBinding","page":"Library Reference","title":"GATlab.Syntax.GATs.JudgmentBinding","text":"JudgmentBinding\n\nA binding of a judgment to a name and possibly a signature.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.SortScope","page":"Library Reference","title":"GATlab.Syntax.GATs.SortScope","text":"SortScope\n\nA scope where variables are assigned to AlgSortss, and no overloading is permitted.\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, and no overloading is permitted.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.equations-Tuple{Scope{AlgType, Nothing}, Scope{AlgType, Nothing}, GAT}","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 each of the elements of context from the args, as well as checking that the args are well-typed.\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\nAlgorithm:\n\nStart from the arguments. We know how to compute each of the arguments; they are given. Each argument tells us how to compute other arguments, and also elements of the context\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.Presentations.Presentation","page":"Library Reference","title":"GATlab.Syntax.Presentations.Presentation","text":"A presentation has a set of generators, given by a TypeScope, and a set of equations among terms which can refer to those generators. Each element of eqs is a list of terms which are asserted to be equal.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{Context, Any, Type{Presentation}}","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.toexpr-Tuple{Presentation}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"Context of presentation is the underlying GAT\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/#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}","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}","page":"Library Reference","title":"GATlab.Models.ModelInterface.qualify_function","text":"Add model kwarg (it shouldn't have it already) Qualify method name to be in theory module Add context kwargs if not already present\n\nTODO: throw error if there's junk kwargs present already?\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.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/#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.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/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 should be first class. This doesn't play nicely with deBruijn levels; we don't want to do a bunch of math to convert between flattened and unflattened versions of contexts. There is an accepted solution to the problem of organizing names: use refs! Mathematically speaking, a ref is just a list of deBruijn levels.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"However, deBruijn levels are unfriendly for users; we want to be able to give names to our variables!","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In general, naming is given by a relation between symbols and bindings (as referred to by deBruijn levels). 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 deBruijn level 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 deBruijn level) 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/models/#Model-families","page":"Model families","title":"Model families","text":"","category":"section"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"The semantics part of GATlab is the model family infrastructure.","category":"page"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"Given a theory, one can declare a model family for that theory. This consists of the following.","category":"page"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"A struct T. Each value of the struct is a model of the theory. The struct subtypes Model{Th, Tuple{Ts...}}. Th is the theory that the struct is a model family for, and Ts specifies types for each of the type constructors in Theory.\nFor each type constructor i in Theory, an overload of checkvalidity of the form\ncheckvalidity(m::T, ::TypCon{i}, args..., val) = ...\nThis checks that val is a valid instance of i applied to args..., assuming that args... have been previously checked to be valid.\nThis can then be applied using, for instance\ncheckvalidity(m, Category.Hom, x, y, f)\nusing the singleton structs defined in Theories\nFor each term constructor i in Theory, an overload of ap of the form\nap(m::T, ::TrmCon{i}, args...) = ...\nHere args... is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of ap might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.","category":"page"},{"location":"concepts/theories/#Theories","page":"Theories","title":"Theories","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A theory in GATlab consists of two parts.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A Julia value of type Theory that describes the theory.\nA module named by the theory with various Julia types that give us handles","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"for metaprogramming.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"These metaprogramming types include:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A singleton struct named Th and subtyping AbstractTheory that has an overload of gettheory on it returning the Julia value from 1. This is used to pass around the entire theory at the type level.\nA singleton struct for each type constructor and term constructor in the theory. These are used in place of Lvl in types, so that backtraces are more readable.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Example:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"module Category\nusing GATlab.Theories\n\nstruct Th <: AbstractTheory end\n\nTheories.gettheory(::Th) = ...\n\nstruct Ob <: TypCon{1} end\nstruct Hom <: TypCon{2} end\n\nstruct compose <: TrmCon{3} end\n...\nend","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.Categories.ThCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThThinCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThThinCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThClass","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThClass","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThAscCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThAscCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.ThAscCat","text":"ThAscCat\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.Categories.ThIdLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThIdLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.StdTheories.Algebra,\n GATlab.Stdlib.StdTheories.Monoidal,\n GATlab.Stdlib.StdTheories.Naturals,\n GATlab.Stdlib.StdModels,\n GATlab.Stdlib.StdModels.FinSets,\n ]","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. I.e., 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 a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are Vectors of ring elements.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"GATlab is the new 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":"concepts/overview/#For-Catlab-users","page":"For Catlab users","title":"For Catlab users","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","text":"GATlab is a refactoring of the core GAT system in Catlab. 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/overview/#.-Models-as-values","page":"For Catlab users","title":"1. Models as values","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"struct FinSetInt\n n::Int\nend","category":"page"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/#.-E-Graphs","page":"For Catlab users","title":"2. E-Graphs","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"finding simple representations of terms\ndeciding whether two terms are equal","category":"page"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"Additionally, it allows us to perform a weak form of typechecking. Typechecking in general for a GAT requires deciding the equality of arbitrary terms, which is 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/overview/#.-Indexed-dependent-types-in-models","page":"For Catlab users","title":"3. Indexed dependent types in models","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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. I.e., 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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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":"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.Presentations,\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, Sig}\n\nA binding associates some T-typed value to a name and possibly some aliases, disambiguated by a signature in Sig in the case of overloading.\n\nprimary is an optional distinguished element of aliases value is the element sig is a way of uniquely distinguishing this element from others with the same name (for example, ⊗ : Ob x Ob -> Ob and Hom x Hom -> Hom)\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\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.Reference","page":"Library Reference","title":"GATlab.Syntax.Scopes.Reference","text":"Reference\n\nA path of identifiers. We optimize for the (frequent) case where there is only one identifier by making this a linked list.\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, Sig}\n\nIn 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. For example, a scope with 3 elements:\n\nx::Int = 3\ny::String = \"hello\"\nx::String = \"ex\"\n\nThis is a valid scope even though there are name collisions, because the signature (in this case, a datatype) disambiguates. Of course, it may not be wise to disambiguate by type, because it is not always possible to infer expected type. In general, one should pick something that can be inferred, and Nothing is always a reasonable choice, which disallows any name collisions.\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/#Base.:+-Tuple{ScopeTag, ScopeTag}","page":"Library Reference","title":"Base.:+","text":"Deterministically combine two scope tags into a third\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.equiv-Tuple{Scope, Scope}","page":"Library Reference","title":"GATlab.Syntax.Scopes.equiv","text":"Compare two scopes, ignoring the difference in the top-level scope tag.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.Scopes.getlid-Union{Tuple{Sig}, Tuple{T}, Tuple{HasScope{T, Sig}, Symbol}} where {T, Sig}","page":"Library Reference","title":"GATlab.Syntax.Scopes.getlid","text":"Determine the level of a binding given the name and possibly the signature\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.\nsig::Any. The signature of the identifier, to disambiguate between multiple identifiers with the same name within the same scope.\nstrict::Bool. If strict is true, throw an error if not found, else return nothing.\nisunique::Bool. If isunique is true, then don't use the signature to disambiguate, instead fail if their are multiple identifiers with the same name in a scope.\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_addalias!-Tuple{Scope, Symbol, Symbol}","page":"Library Reference","title":"GATlab.Syntax.Scopes.unsafe_addalias!","text":"unsafe_addalias! should only be used when unsafe_pushbinding! won't be called again, because new bindings won't get the old aliases.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.Judgment","page":"Library Reference","title":"GATlab.Syntax.GATs.Judgment","text":"Judgment\n\nA judgment is either a type constructor, term constructor, or axiom; a GAT is composed of a list of judgments.\n\n\n\n\n\n","category":"type"},{"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.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.AlgSort","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgSort","text":"AlgSort\n\nA sort, which is essentially a type constructor without arguments ref must be reference to a AlgTypeConstructor\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.AlgTerm","page":"Library Reference","title":"GATlab.Syntax.GATs.AlgTerm","text":"AlgTerm\n\nOne syntax tree to rule all the terms. Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant\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\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. head must be reference to a AlgTypeConstructor\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. Checked elsewhere.\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.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\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.JudgmentBinding","page":"Library Reference","title":"GATlab.Syntax.GATs.JudgmentBinding","text":"JudgmentBinding\n\nA binding of a judgment to a name and possibly a signature.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.SortScope","page":"Library Reference","title":"GATlab.Syntax.GATs.SortScope","text":"SortScope\n\nA scope where variables are assigned to AlgSortss, and no overloading is permitted.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.TermInCtx","page":"Library Reference","title":"GATlab.Syntax.GATs.TermInCtx","text":"A term with an accompanying type scope, e.g.\n\n(a,b)::R\n\na*(a+b)\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.TermInCtx-Tuple{GAT, Ident}","page":"Library Reference","title":"GATlab.Syntax.GATs.TermInCtx","text":"Get the canonical term associated with a term constructor\n\n\n\n\n\n","category":"method"},{"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, and no overloading is permitted.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{Context, Any, Type{AlgTerm}}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Some expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{Context, Any, Type{AlgType}}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Some expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{Context, Any, Type{Binding{AlgType, Nothing}}}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.fromexpr","text":"Return nothing if the binding we parse has already been bound.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.argcontext-Tuple{Union{AlgTermConstructor, AlgTypeConstructor}}","page":"Library Reference","title":"GATlab.Syntax.GATs.argcontext","text":"Local context of an AlgTermConstructor, including the arguments themselves\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.bind_localctx-Tuple{GAT, TermInCtx}","page":"Library Reference","title":"GATlab.Syntax.GATs.bind_localctx","text":"Take a term constructor and determine terms of its local context.\n\nThis function is mutually recursive with infer_type. \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{Scope{AlgType, Nothing}, Scope{AlgType, Nothing}, GAT}","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 each of the elements of context from the args, as well as checking that the args are well-typed.\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\nAlgorithm:\n\nStart from the arguments. We know how to compute each of the arguments; they are given. Each argument tells us how to compute other arguments, and also elements of the context\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.infer_type-Tuple{GAT, TermInCtx}","page":"Library Reference","title":"GATlab.Syntax.GATs.infer_type","text":"Infer the type of the term of a term. If it is not in context, recurse on its arguments. The term constructor's output type yields the resulting type once its localcontext variables are substituted with the relevant AlgTerms. \n\n (x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z)\n\nE.g. given ––––––––––––––––––– id(x)⋅(p⋅q)\n\n (a,b,c)::Ob, f::Hom(a,b), g::Hom(b,c)\n\nand output type: –––––––––––––––––– Hom(a,c)\n\nWe first recursively find {id(x) => Hom(x,x), p⋅q => Hom(x,z)}. We ultimately want an AlgTerm for everything in the output type's context such that we can substitute into Hom(a,c) to get the final answer. It will help to also compute the AlgType for everything in the context. We work backwards, since we start by knowing {f => id(x)::Hom(x,x), g=> p⋅q :: Hom(x,z)}. For a b and c, we use equations which tell us, e.g., that a = dom(f). So we can grab the first argument of the type of f (i.e. grab x from Hom(x,x)). \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.normalize_decl-Tuple{Any}","page":"Library Reference","title":"GATlab.Syntax.GATs.normalize_decl","text":"axiom=true adds a ::default to exprs like f(a,b) ⊣ [a::A, b::B]\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.parsetypescope-Tuple{Context, AbstractVector}","page":"Library Reference","title":"GATlab.Syntax.GATs.parsetypescope","text":"Keep track of variables already bound (e.g. in local context) so that they need not be redefined, e.g. compose(f,g::Hom(b,c)) ⊣ [(a,b,c)::Ob, f::Hom(a,b)] (If f were not defined in the local context, it would be parsed as default.)\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.substitute_term-Tuple{GATlab.Syntax.GATs.TrmTyp, Dict{Ident, AlgTerm}}","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.Presentations.Presentation","page":"Library Reference","title":"GATlab.Syntax.Presentations.Presentation","text":"A presentation has a set of generators, given by a TypeScope, and a set of equations among terms which can refer to those generators. Each element of eqs is a list of terms which are asserted to be equal.\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.ExprInterop.fromexpr-Tuple{Context, Any, Type{Presentation}}","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.toexpr-Tuple{Presentation}","page":"Library Reference","title":"GATlab.Syntax.ExprInterop.toexpr","text":"Context of presentation is the underlying GAT\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/#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}","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}","page":"Library Reference","title":"GATlab.Models.ModelInterface.qualify_function","text":"Add model kwarg (it shouldn't have it already) Qualify method name to be in theory module Add context kwargs if not already present\n\nTODO: throw error if there's junk kwargs present already?\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.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/#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.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/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 should be first class. This doesn't play nicely with deBruijn levels; we don't want to do a bunch of math to convert between flattened and unflattened versions of contexts. There is an accepted solution to the problem of organizing names: use refs! Mathematically speaking, a ref is just a list of deBruijn levels.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"However, deBruijn levels are unfriendly for users; we want to be able to give names to our variables!","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In general, naming is given by a relation between symbols and bindings (as referred to by deBruijn levels). 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 deBruijn level 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 deBruijn level) 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/models/#Model-families","page":"Model families","title":"Model families","text":"","category":"section"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"The semantics part of GATlab is the model family infrastructure.","category":"page"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"Given a theory, one can declare a model family for that theory. This consists of the following.","category":"page"},{"location":"concepts/models/","page":"Model families","title":"Model families","text":"A struct T. Each value of the struct is a model of the theory. The struct subtypes Model{Th, Tuple{Ts...}}. Th is the theory that the struct is a model family for, and Ts specifies types for each of the type constructors in Theory.\nFor each type constructor i in Theory, an overload of checkvalidity of the form\ncheckvalidity(m::T, ::TypCon{i}, args..., val) = ...\nThis checks that val is a valid instance of i applied to args..., assuming that args... have been previously checked to be valid.\nThis can then be applied using, for instance\ncheckvalidity(m, Category.Hom, x, y, f)\nusing the singleton structs defined in Theories\nFor each term constructor i in Theory, an overload of ap of the form\nap(m::T, ::TrmCon{i}, args...) = ...\nHere args... is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of ap might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.","category":"page"},{"location":"concepts/theories/#Theories","page":"Theories","title":"Theories","text":"","category":"section"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A theory in GATlab consists of two parts.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A Julia value of type Theory that describes the theory.\nA module named by the theory with various Julia types that give us handles","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"for metaprogramming.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"These metaprogramming types include:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"A singleton struct named Th and subtyping AbstractTheory that has an overload of gettheory on it returning the Julia value from 1. This is used to pass around the entire theory at the type level.\nA singleton struct for each type constructor and term constructor in the theory. These are used in place of Lvl in types, so that backtraces are more readable.","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"Example:","category":"page"},{"location":"concepts/theories/","page":"Theories","title":"Theories","text":"module Category\nusing GATlab.Theories\n\nstruct Th <: AbstractTheory end\n\nTheories.gettheory(::Th) = ...\n\nstruct Ob <: TypCon{1} end\nstruct Hom <: TypCon{2} end\n\nstruct compose <: TrmCon{3} end\n...\nend","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.Categories.ThCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThThinCategory","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThThinCategory","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThClass","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThClass","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.Categories.ThAscCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThAscCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.ThAscCat","text":"ThAscCat\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.Categories.ThIdLawlessCat","category":"page"},{"location":"stdlib/#GATlab.Stdlib.StdTheories.Categories.ThIdLawlessCat","page":"Standard Library","title":"GATlab.Stdlib.StdTheories.Categories.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.StdTheories.Algebra,\n GATlab.Stdlib.StdTheories.Monoidal,\n GATlab.Stdlib.StdTheories.Naturals,\n GATlab.Stdlib.StdModels,\n GATlab.Stdlib.StdModels.FinSets,\n ]","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. I.e., 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 a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are Vectors of ring elements.","category":"page"},{"location":"","page":"GATlab.jl","title":"GATlab.jl","text":"GATlab is the new 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":"concepts/overview/#For-Catlab-users","page":"For Catlab users","title":"For Catlab users","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","text":"GATlab is a refactoring of the core GAT system in Catlab. 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/overview/#.-Models-as-values","page":"For Catlab users","title":"1. Models as values","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"struct FinSetInt\n n::Int\nend","category":"page"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/#.-E-Graphs","page":"For Catlab users","title":"2. E-Graphs","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"finding simple representations of terms\ndeciding whether two terms are equal","category":"page"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","text":"Additionally, it allows us to perform a weak form of typechecking. Typechecking in general for a GAT requires deciding the equality of arbitrary terms, which is 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/overview/#.-Indexed-dependent-types-in-models","page":"For Catlab users","title":"3. Indexed dependent types in models","text":"","category":"section"},{"location":"concepts/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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. I.e., 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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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/overview/","page":"For Catlab users","title":"For Catlab users","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"}] } diff --git a/dev/stdlib/index.html b/dev/stdlib/index.html index 89dc6b17..4321c045 100644 --- a/dev/stdlib/index.html +++ b/dev/stdlib/index.html @@ -1,2 +1,2 @@ -Standard Library · GATlab.jl

      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

      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.