From f22415569bc0bf0d2ded59665d757de3f02484d9 Mon Sep 17 00:00:00 2001 From: "Documenter.jl" Date: Thu, 21 Sep 2023 00:36:31 +0000 Subject: [PATCH] build based on 06be9f0 --- dev/.documenter-siteinfo.json | 2 +- dev/api/index.html | 10 +++++----- dev/concepts/models/index.html | 2 +- dev/concepts/overview/index.html | 2 +- dev/concepts/scopes/index.html | 2 +- dev/concepts/theories/index.html | 2 +- dev/index.html | 2 +- dev/search_index.js | 2 +- dev/stdlib/index.html | 2 +- 9 files changed, 13 insertions(+), 13 deletions(-) diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index f9e54a88..0b8f01e3 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.9.3","generation_timestamp":"2023-09-21T00:18:31","documenter_version":"1.0.1"}} \ No newline at end of file +{"documenter":{"julia_version":"1.9.3","generation_timestamp":"2023-09-21T00:36:27","documenter_version":"1.0.1"}} \ No newline at end of file diff --git a/dev/api/index.html b/dev/api/index.html index 03ee0840..2c224633 100644 --- a/dev/api/index.html +++ b/dev/api/index.html @@ -1,12 +1,12 @@ -Library Reference · GATlab.jl
GitHub

Library Reference

Syntax

GATlab.Syntax.Scopes.Binding — Type

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.Context — Type

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

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

Contexts should overload:

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

Ident

An identifier.

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

source
GATlab.Syntax.Scopes.LID — Type

A LID (Local ID) indexes a given scope.

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

source
GATlab.Syntax.Scopes.Scope — Type

Scope{T, 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
GitHub
Library Reference
Syntax
GATlab.Syntax.Scopes.Binding — Type
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.Context — Type
A Context is anything which contains an ordered list of scopes.
Scopes within a context are referred to by level, which is their index within this list.
Contexts should overload:
  • getscope(c::Context, level::Int) -> Scope
  • nscopes(c::Context) -> Int
  • hastag(c::Context, tag::ScopeTag) -> Bool
  • hasname(c::Context, name::Symbol) -> Bool
  • getlevel(c::Context, tag::ScopeTag) -> Int
  • getlevel(c::Context, name::Symbol) -> Int
source
GATlab.Syntax.Scopes.Ident — Type
Ident
An identifier.
tag refers to the scope that this Ident is bound in lid indexes the scope that Ident is bound in name is an optional field for the sake of printing. A variable in a scope might be associated with several names
source
GATlab.Syntax.Scopes.LID — Type
A LID (Local ID) indexes a given scope.
Currently, scopes assign LIDs sequentially – this is not a stable guarantee however, and in theory scopes could have "sparse" LIDs.
source
GATlab.Syntax.Scopes.Scope — Type
Scope{T, 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
Base.:+ — Method
Deterministically combine two scope tags into a third
source
GATlab.Syntax.Scopes.hasident — Method
hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
source
GATlab.Syntax.Scopes.ident — Method
ident creates an Ident from a context and some partial data supplied as keywords.
Keywords arguments:
  • tag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.
  • name::Union{Symbol, Nothing}. The name of the identifier.
  • lid::Union{LID, Nothing}. The lid of the identifier within its scope.
  • level::Union{Int, Nothing}. The level of the scope within the context.
  • 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.rename — Method
rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T
Recurse through the structure of x, and change any name n in scope tag to get(replacements, n, n). Overload this function on structs that have names in them.
source
GATlab.Syntax.Scopes.retag — Method
retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T
Recurse through the structure of x, swapping any instance of a ScopeTag t with get(replacements, t, t). Overload this function on structs that have ScopeTags within them.
source
GATlab.Syntax.GATs.AlgSorts — Type
AlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
source
GATlab.Syntax.GATs.AlgTerm — Type
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.GAT — Type
GAT
A generalized algebraic theory. Essentially, just consists of a name and a list of GATSegments, but there is also some caching to make access faster. Specifically, there is a dictionary to map ScopeTag to position in the list of segments, and there are lists of all of the identifiers for term constructors, type constructors, and axioms so that they can be iterated through faster.
GATs allow overloading but not shadowing.
source
GATlab.Syntax.GATs.equations — Method
Implicit equations defined by a context.
This function allows a generalized algebraic theory (GAT) to be expressed as an essentially algebraic theory, i.e., as partial functions whose domains are defined by equations.
References:
  • (Cartmell, 1986, Sec 6: "Essentially algebraic theories and categories with  finite limits")
  • (Freyd, 1972, "Aspects of topoi")
This function gives expressions for computing 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_type — Method
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.parsetypescope — Method
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.sortcheck — Method
sortcheck(ctx::Context, t::AlgTerm)
Throw an error if a the head of an AlgTerm (which refers to a term constructor) has arguments of the wrong sort. Returns the sort of the term.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgType)
Throw an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.
source
GATlab.Syntax.Presentations.Presentation — Type
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.fromexpr — Method
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.hasident — Method
hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
source
GATlab.Syntax.Scopes.ident — Method
ident creates an Ident from a context and some partial data supplied as keywords.
Keywords arguments:
  • tag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.
  • name::Union{Symbol, Nothing}. The name of the identifier.
  • lid::Union{LID, Nothing}. The lid of the identifier within its scope.
  • level::Union{Int, Nothing}. The level of the scope within the context.
  • 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.rename — Method
rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::T) where {T} -> T
Recurse through the structure of x, and change any name n in scope tag to get(replacements, n, n). Overload this function on structs that have names in them.
source
GATlab.Syntax.Scopes.retag — Method
retag(replacements::Dict{ScopeTag, ScopeTag}, x::T) where {T} -> T
Recurse through the structure of x, swapping any instance of a ScopeTag t with get(replacements, t, t). Overload this function on structs that have ScopeTags within them.
source
GATlab.Syntax.GATs.AlgSorts — Type
AlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
source
GATlab.Syntax.GATs.AlgTerm — Type
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.GAT — Type
GAT
A generalized algebraic theory. Essentially, just consists of a name and a list of GATSegments, but there is also some caching to make access faster. Specifically, there is a dictionary to map ScopeTag to position in the list of segments, and there are lists of all of the identifiers for term constructors, type constructors, and axioms so that they can be iterated through faster.
GATs allow overloading but not shadowing.
source
GATlab.Syntax.GATs.InCtx — Type
A type or term with an accompanying type scope, e.g.
(a,b)::R        (a,b)::Ob –––––-  or  –––––   a*(a+b)         Hom(a,b)
source
GATlab.Syntax.GATs.equations — Method
Implicit equations defined by a context.
This function allows a generalized algebraic theory (GAT) to be expressed as an essentially algebraic theory, i.e., as partial functions whose domains are defined by equations.
References:
  • (Cartmell, 1986, Sec 6: "Essentially algebraic theories and categories with  finite limits")
  • (Freyd, 1972, "Aspects of topoi")
This function gives expressions for computing 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_type — Method
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.parsetypescope — Method
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.sortcheck — Method
sortcheck(ctx::Context, t::AlgTerm)
Throw an error if a the head of an AlgTerm (which refers to a term constructor) has arguments of the wrong sort. Returns the sort of the term.
source
GATlab.Syntax.GATs.sortcheck — Method
sortcheck(ctx::Context, t::AlgType)
Throw an error if a the head of an AlgType (which refers to a type constructor) has arguments of the wrong sort.
source
GATlab.Syntax.Presentations.Presentation — Type
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.toexpr — Function
toexpr(c::Context, t) -> Any
Converts GATlab syntax into an Expr that can be read in via fromexpr to get the same thing. Crucially, the output of this will depend on the order of the scopes in c, and if read back in with a different c may end up with different results.
source
Models
GATlab.Models.ModelInterface.implements — Method
implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
source
GATlab.Syntax.ExprInterop.toexpr — Function
toexpr(c::Context, t) -> Any
Converts GATlab syntax into an Expr that can be read in via fromexpr to get the same thing. Crucially, the output of this will depend on the order of the scopes in c, and if read back in with a different c may end up with different results.
source
Models
GATlab.Models.ModelInterface.implements — Method
implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
source
GATlab.Models.ModelInterface.@instance — Macro
Usage:
struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
   ntypes::Int
 end
 
@@ -27,7 +27,7 @@
 end
 
 @instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
-end
source
GATlab.Models.SymbolicModels.GATExpr — Type
Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.
We define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)
The concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.
source
Base.nameof — Method
Get name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
source
GATlab.Models.SymbolicModels.functor — Method
Functor from GAT expression to GAT instance.
Strictly speaking, we should call these "structure-preserving functors" or, better, "model homomorphisms of GATs". But this is a category theory library, so we'll go with the simpler "functor".
A functor is completely determined by its action on the generators. There are several ways to specify this mapping:
  1. Specify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.
  2. Explicitly map each generator term to an instance value, using the generators dictionary.
  3. For each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.
The terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.
FIXME
source
GATlab.Models.SymbolicModels.@symbolic_model — Macro
@symbolic_model generates the free model of a theory, generated by symbols.
This is backwards compatible with the @syntax macro in Catlab.
One way of thinking about this is that for every type constructor, we add an additional term constructor that builds a "symbolic" element of that type from any Julia value. This term constructor is called "generator".
An invocation of @symbolic_model creates the following.
  1. A module with a struct for each type constructor, which has a single type
parameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.
For instance, in the theory of categories, we might have the following elements.
using .FreeCategory
+end
source
GATlab.Models.SymbolicModels.GATExpr — Type
Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.
We define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)
The concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.
source
Base.nameof — Method
Get name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
source
GATlab.Models.SymbolicModels.functor — Method
Functor from GAT expression to GAT instance.
Strictly speaking, we should call these "structure-preserving functors" or, better, "model homomorphisms of GATs". But this is a category theory library, so we'll go with the simpler "functor".
A functor is completely determined by its action on the generators. There are several ways to specify this mapping:
  1. Specify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.
  2. Explicitly map each generator term to an instance value, using the generators dictionary.
  3. For each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.
The terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.
FIXME
source
GATlab.Models.SymbolicModels.@symbolic_model — Macro
@symbolic_model generates the free model of a theory, generated by symbols.
This is backwards compatible with the @syntax macro in Catlab.
One way of thinking about this is that for every type constructor, we add an additional term constructor that builds a "symbolic" element of that type from any Julia value. This term constructor is called "generator".
An invocation of @symbolic_model creates the following.
  1. A module with a struct for each type constructor, which has a single type
parameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.
For instance, in the theory of categories, we might have the following elements.
using .FreeCategory
 x = Ob{:generator}([:x], [])
 y = Ob{:generator}([:y], [])
 f = Hom{:generator}([:f], [x, y])
@@ -84,4 +84,4 @@
 
 function ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)
   associate_unit(FreeCategory.compose(f, g; strict), id)
-end
source
Utilities

+end
source

Utilities

diff --git a/dev/concepts/models/index.html b/dev/concepts/models/index.html index 98ef8c79..45693362 100644 --- a/dev/concepts/models/index.html +++ b/dev/concepts/models/index.html @@ -1,2 +1,2 @@ -Model families · GATlab.jl
GitHub

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
GitHub

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 33d85f7f..c688967b 100644 --- a/dev/concepts/overview/index.html +++ b/dev/concepts/overview/index.html @@ -1,4 +1,4 @@ For Catlab users · GATlab.jl
GitHub

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 18df5ca8..1659a23f 100644 --- a/dev/concepts/scopes/index.html +++ b/dev/concepts/scopes/index.html @@ -1,2 +1,2 @@ -Scopes · GATlab.jl
GitHub

Scopes

Design rationale:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+Scopes · GATlab.jl
GitHub

Scopes

Design rationale:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

diff --git a/dev/concepts/theories/index.html b/dev/concepts/theories/index.html index 22ba9c56..2df958e5 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 cd3cc3fd..cc13a4fa 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -GATlab.jl · GATlab.jl
GitHub

GATlab.jl

GATlab.jl is a computer algebra system based on Generalized Algebraic Theories.

Roughly speaking, GATlab consists of two parts. The first part is concerned with symbolic constructs. The prototypical symbolic construct is simply a term, i.e. a syntax tree. In GATlab, every term is always relative to a context, in which the free variables in that term are typed. And the context and term themselves are relative to an underlying theory, which defines the allowable type and term constructors that can be used in contexts and terms, along with laws that allow one to rewrite terms into equivalent other terms.

We think about a term as a symbolic representation of a function from an assignment of values to the free variables to a value for the term. 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
GitHub

GATlab.jl

GATlab.jl is a computer algebra system based on Generalized Algebraic Theories.

Roughly speaking, GATlab consists of two parts. The first part is concerned with symbolic constructs. The prototypical symbolic construct is simply a term, i.e. a syntax tree. In GATlab, every term is always relative to a context, in which the free variables in that term are typed. And the context and term themselves are relative to an underlying theory, which defines the allowable type and term constructors that can be used in contexts and terms, along with laws that allow one to rewrite terms into equivalent other terms.

We think about a term as a symbolic representation of a function from an assignment of values to the free variables to a value for the term. 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.js b/dev/search_index.js index c3da47ab..97f27477 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.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/#GATlab.Models.SymbolicModels.GATExpr","page":"Library Reference","title":"GATlab.Models.SymbolicModels.GATExpr","text":"Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.\n\nWe define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)\n\nThe concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.nameof-Tuple{GATExpr{:generator}}","page":"Library Reference","title":"Base.nameof","text":"Get name of GAT generator expression as a Symbol.\n\nIf the generator has no name, returns nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.constructor_name-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.constructor_name","text":"Name of constructor that created expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.functor-Tuple{Tuple, GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.functor","text":"Functor from GAT expression to GAT instance.\n\nStrictly speaking, we should call these \"structure-preserving functors\" or, better, \"model homomorphisms of GATs\". But this is a category theory library, so we'll go with the simpler \"functor\".\n\nA functor is completely determined by its action on the generators. There are several ways to specify this mapping:\n\nSpecify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.\nExplicitly map each generator term to an instance value, using the generators dictionary.\nFor each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.\n\nThe terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.\n\nFIXME\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.parse_json_sexpr-Tuple{Module, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.parse_json_sexpr","text":"Deserialize expression from JSON-able S-expression.\n\nIf symbols is true (the default), strings are converted to symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_latex-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_latex","text":"Show the expression in infix notation using LaTeX math.\n\nDoes not include $ or \\[begin|end]{equation} delimiters.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_sexpr","text":"Show the syntax expression as an S-expression.\n\nCf. the standard library function Meta.show_sexpr.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_unicode-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_unicode","text":"Show the expression in infix notation using Unicode symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.symbolic_instance_methods-Tuple{GAT, Any, Symbol, Dict{Ident, JuliaFunction}}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.symbolic_instance_methods","text":"Julia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.syntax_module-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.syntax_module","text":"Get syntax module of given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.to_json_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.to_json_sexpr","text":"Serialize expression as JSON-able S-expression.\n\nThe format is an S-expression encoded as JSON, e.g., \"compose(f,g)\" is represented as [\"compose\", f, g].\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.@symbolic_model-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.@symbolic_model","text":"@symbolic_model generates the free model of a theory, generated by symbols.\n\nThis is backwards compatible with the @syntax macro in Catlab.\n\nOne way of thinking about this is that for every type constructor, we add an additional term constructor that builds a \"symbolic\" element of that type from any Julia value. This term constructor is called \"generator\".\n\nAn invocation of @symbolic_model creates the following.\n\nA module with a struct for each type constructor, which has a single type\n\nparameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.\n\nFor instance, in the theory of categories, we might have the following elements.\n\nusing .FreeCategory\nx = Ob{:generator}([:x], [])\ny = Ob{:generator}([:y], [])\nf = Hom{:generator}([:f], [x, y])\ng = Hom{:generator}([:g], [y, x])\nh = Hom{:compose}([f, g], [x, x])\n\nMethods inside the module (not exported) for all of the term constructors and\n\nfield accessors (i.e. stuff like compose, id, dom, codom), which construct terms.\n\nA default instance (i.e., without a model parameter) of the theory using the\n\ntypes in this generated model. Methods in this instance can be overridden by the body of @symbolic_model to perform rewriting for the sake of normalization, for instance flattening associative and unital operations.\n\nCoercion methods of the type constructors that allow one to introduce generators.\n\nx = ThCategory.Ob(FreeCategory.Ob, :x)\ny = ThCategory.Ob(FreeCategory.Ob, :y)\nf = ThCategory.Hom(:f, x, y)\n\nNote that in both the instance and in these coercion methods, we must give the expected type as the first argument when it cannot be infered by the other arguments. For instance, instead of\n\nmunit() = ...\n\nwe have\n\nmunit(::Type{FreeSMC.Ob}) = ...\n\nand likewise instead of\n\nThCategory.Ob(x::Any) = ...\n\nwe have\n\nThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...\n\nExample:\n\n@symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)\nend\n\nThis generates:\n\nmodule FreeCategory\nexport Ob, Hom\nusing ..__module__\n\nconst THEORY_MODULE = ThCategory\n\nstruct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol\n args::Vector\n type_args::Vector{GATExpr}\nend\n\nstruct Hom{T} <: __module__.HomExpr{T}\n args::Vector\n type_args::Vector{GATExpr}\nend\n\ndom(x::Hom) = x.type_args[1]\n\ncodom(x::Hom) = x.type_args[2]\n\nfunction compose(f::Hom, g::Hom; strict=true)\n if strict && !(codom(f) == dom(g))\n throw(SyntaxDomainError(:compose, [f, g]))\n end\n Hom{:compose}([f, g], [dom(f), codom(g)])\nend\n\nfunction id(x::Ob)\n Ob{:id}([x], [x, x])\nend\nend\n\n# default implementations \n\nfunction ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob\n FreeCategory.dom(x)\nend\n\nfunction ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob\n FreeCategory.Ob{:generator}([__value__], [])\nend\n\nfunction ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom\n FreeCategory.id(A)\nend\n\nfunction ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)\n associate_unit(FreeCategory.compose(f, g; strict), id)\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#Utilities","page":"Library Reference","title":"Utilities","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Util,\n GATlab.Util.MetaUtils,\n ]","category":"page"},{"location":"api/#GATlab.Util.MetaUtils","page":"Library Reference","title":"GATlab.Util.MetaUtils","text":"General-purpose tools for metaprogramming in Julia.\n\n\n\n\n\n","category":"module"},{"location":"api/#GATlab.Util.MetaUtils.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, i.e. references which look like britain.economy.GDP, should be first class. This doesn't play nicely with the internal representation of names via deBruijn levels; we don't want to do a bunch of math to convert between flattened and nested versions of contexts. Conceptually, we should then switch our identifiers to be lists of deBruijn levels.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"But there are also significant subtleties in the translation between named and nameless representations of identifiers. Also in practice if we are referencing something that might change over time, like a C-set, we don't want to use deBruijn levels, because we don't want have to change all of our identifiers when we delete something, so in the rest of this I will instead say \"local identifier\" instead of deBruijn level to refer to a nameless representation of an identifier.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"(the name \"local identifier\" and also some of this philosophy is taken from chit)","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In general, naming is given by a relation between symbols and bindings (as refered to by local identifiers). Each binding may be associated with zero or more symbols, and each symbol might be associated with zero or more bindings.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"We name the failure of this relation to be a bijection in several ways.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one symbol is related to a single binding, we say that this","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"binding has aliases. In this case, we should also have a primary alias used as a default.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one binding is related to a single symbol, we have name overlap.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Name overlap can be resolved by overloading and shadowing, we will talk about this later on.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no symbol is related to a binding, such as when the binding is created","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no binding is related to a symbol, then we have a name error; this name","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"is not valid in the current context and we must throw an error.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"The most important thing to get right is name overlap; we discuss this first.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"There are two ways in which to resolve name overlap. The first way is via overloading. In overloading, we disambiguate an ambiguous name via its context, for instance what type it is expected to be, or what arguments is it receiving. The second way is via shadowing. In shadowing, a name is resolved by making it point to the \"most recently defined\" thing with that name.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In GATlab, we handle overloading and shadowing with a notion of scope. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. Each scope is identified with a ScopeTag, which is an opaque identifier (i.e. a UUID). We take this idea from Racket, but we don't need the more complex \"scope sets\" from Racket because GATs don't need to process the syntax of other GATs; if we start doing this we'll have to rethink the design, but we'll probably have bigger problems too.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Two variables with the same name within a single scope are meant to overload one another. For instance, this is what happens with mcompose in the theory of monoidal categories; it is overloaded for Hom and Ob, and this is what happens with d in the discrete exterior calculus; it is overloaded for all of the (k+1)-forms. Variables in different scopes with the same name shadow one another. When we parse an expression a + b, we do so in an ordered list of scopes, and the most recent scope \"wins\".","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Parsing turns a Symbol into an Ident. The Ident contains the original Symbol for printing, but it also contains a reference to a scope via ScopeTag, and an local identifier (\"lid\") within that scope. Thus, the name in the Ident is never needed for later stages of programatic manipulation.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Scopes cache the relation between names and bindings, by providing a way to go from binding (as reified by local identifier) to a set of aliases with distinguished primary alias, and to go from name to the set of bindings that have that name that we need to disambiguate between in the case of an overload.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Because Idents are fully unambiguous even without their name, it is also possible to create an Ident with no name, which solves the problem of nameless references.","category":"page"},{"location":"concepts/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.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.ScopedBinding","page":"Library Reference","title":"GATlab.Syntax.Scopes.ScopedBinding","text":"Type for printing out bindings with colored keys\n\n\n\n\n\n","category":"type"},{"location":"api/#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.InCtx","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"A type or term with an accompanying type scope, e.g.\n\n(a,b)::R (a,b)::Ob –––––- or ––––– a*(a+b) Hom(a,b)\n\n\n\n\n\n","category":"type"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{AlgTerm}, Tuple{GAT, Ident}} where AlgTerm","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical term + ctx associated with a term constructor.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.InCtx-Union{Tuple{AlgType}, Tuple{GAT, Ident}} where AlgType","page":"Library Reference","title":"GATlab.Syntax.GATs.InCtx","text":"Get the canonical type + ctx associated with a type constructor.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Syntax.GATs.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.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-Union{Tuple{T}, Tuple{GAT, InCtx{T}}} where T","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-Union{Tuple{T}, Tuple{T, Dict{Ident, AlgTerm}}} where T<:GATlab.Syntax.GATs.TrmTyp","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/#GATlab.Models.SymbolicModels.GATExpr","page":"Library Reference","title":"GATlab.Models.SymbolicModels.GATExpr","text":"Base type for expressions in the syntax of a GAT. This is an alternative to AlgTerm used for backwards compatibility with Catlab.\n\nWe define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)\n\nThe concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.nameof-Tuple{GATExpr{:generator}}","page":"Library Reference","title":"Base.nameof","text":"Get name of GAT generator expression as a Symbol.\n\nIf the generator has no name, returns nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.constructor_name-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.constructor_name","text":"Name of constructor that created expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.functor-Tuple{Tuple, GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.functor","text":"Functor from GAT expression to GAT instance.\n\nStrictly speaking, we should call these \"structure-preserving functors\" or, better, \"model homomorphisms of GATs\". But this is a category theory library, so we'll go with the simpler \"functor\".\n\nA functor is completely determined by its action on the generators. There are several ways to specify this mapping:\n\nSpecify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.\nExplicitly map each generator term to an instance value, using the generators dictionary.\nFor each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.\n\nThe terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.\n\nFIXME\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.parse_json_sexpr-Tuple{Module, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.parse_json_sexpr","text":"Deserialize expression from JSON-able S-expression.\n\nIf symbols is true (the default), strings are converted to symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_latex-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_latex","text":"Show the expression in infix notation using LaTeX math.\n\nDoes not include $ or \\[begin|end]{equation} delimiters.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_sexpr","text":"Show the syntax expression as an S-expression.\n\nCf. the standard library function Meta.show_sexpr.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.show_unicode-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.show_unicode","text":"Show the expression in infix notation using Unicode symbols.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.symbolic_instance_methods-Tuple{GAT, Any, Symbol, Dict{Ident, JuliaFunction}}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.symbolic_instance_methods","text":"Julia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides. \n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.syntax_module-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.syntax_module","text":"Get syntax module of given expression.\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.to_json_sexpr-Tuple{GATExpr}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.to_json_sexpr","text":"Serialize expression as JSON-able S-expression.\n\nThe format is an S-expression encoded as JSON, e.g., \"compose(f,g)\" is represented as [\"compose\", f, g].\n\n\n\n\n\n","category":"method"},{"location":"api/#GATlab.Models.SymbolicModels.@symbolic_model-Tuple{Any, Any, Any}","page":"Library Reference","title":"GATlab.Models.SymbolicModels.@symbolic_model","text":"@symbolic_model generates the free model of a theory, generated by symbols.\n\nThis is backwards compatible with the @syntax macro in Catlab.\n\nOne way of thinking about this is that for every type constructor, we add an additional term constructor that builds a \"symbolic\" element of that type from any Julia value. This term constructor is called \"generator\".\n\nAn invocation of @symbolic_model creates the following.\n\nA module with a struct for each type constructor, which has a single type\n\nparameter T and two fields, args and type_args. Instances of this struct are thought of as elements of the type given by the type constructor applied to type_args. The type parameter refers to the term constructor that was used to generate the element, including the special term constructor :generator, which has as its single argument an Any.\n\nFor instance, in the theory of categories, we might have the following elements.\n\nusing .FreeCategory\nx = Ob{:generator}([:x], [])\ny = Ob{:generator}([:y], [])\nf = Hom{:generator}([:f], [x, y])\ng = Hom{:generator}([:g], [y, x])\nh = Hom{:compose}([f, g], [x, x])\n\nMethods inside the module (not exported) for all of the term constructors and\n\nfield accessors (i.e. stuff like compose, id, dom, codom), which construct terms.\n\nA default instance (i.e., without a model parameter) of the theory using the\n\ntypes in this generated model. Methods in this instance can be overridden by the body of @symbolic_model to perform rewriting for the sake of normalization, for instance flattening associative and unital operations.\n\nCoercion methods of the type constructors that allow one to introduce generators.\n\nx = ThCategory.Ob(FreeCategory.Ob, :x)\ny = ThCategory.Ob(FreeCategory.Ob, :y)\nf = ThCategory.Hom(:f, x, y)\n\nNote that in both the instance and in these coercion methods, we must give the expected type as the first argument when it cannot be infered by the other arguments. For instance, instead of\n\nmunit() = ...\n\nwe have\n\nmunit(::Type{FreeSMC.Ob}) = ...\n\nand likewise instead of\n\nThCategory.Ob(x::Any) = ...\n\nwe have\n\nThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...\n\nExample:\n\n@symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin\n compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)\nend\n\nThis generates:\n\nmodule FreeCategory\nexport Ob, Hom\nusing ..__module__\n\nconst THEORY_MODULE = ThCategory\n\nstruct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol\n args::Vector\n type_args::Vector{GATExpr}\nend\n\nstruct Hom{T} <: __module__.HomExpr{T}\n args::Vector\n type_args::Vector{GATExpr}\nend\n\ndom(x::Hom) = x.type_args[1]\n\ncodom(x::Hom) = x.type_args[2]\n\nfunction compose(f::Hom, g::Hom; strict=true)\n if strict && !(codom(f) == dom(g))\n throw(SyntaxDomainError(:compose, [f, g]))\n end\n Hom{:compose}([f, g], [dom(f), codom(g)])\nend\n\nfunction id(x::Ob)\n Ob{:id}([x], [x, x])\nend\nend\n\n# default implementations \n\nfunction ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob\n FreeCategory.dom(x)\nend\n\nfunction ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob\n FreeCategory.Ob{:generator}([__value__], [])\nend\n\nfunction ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom\n FreeCategory.id(A)\nend\n\nfunction ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)\n associate_unit(FreeCategory.compose(f, g; strict), id)\nend\n\n\n\n\n\n","category":"macro"},{"location":"api/#Utilities","page":"Library Reference","title":"Utilities","text":"","category":"section"},{"location":"api/","page":"Library Reference","title":"Library Reference","text":"Modules = [\n GATlab.Util,\n GATlab.Util.MetaUtils,\n ]","category":"page"},{"location":"api/#GATlab.Util.MetaUtils","page":"Library Reference","title":"GATlab.Util.MetaUtils","text":"General-purpose tools for metaprogramming in Julia.\n\n\n\n\n\n","category":"module"},{"location":"api/#GATlab.Util.MetaUtils.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, i.e. references which look like britain.economy.GDP, should be first class. This doesn't play nicely with the internal representation of names via deBruijn levels; we don't want to do a bunch of math to convert between flattened and nested versions of contexts. Conceptually, we should then switch our identifiers to be lists of deBruijn levels.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"But there are also significant subtleties in the translation between named and nameless representations of identifiers. Also in practice if we are referencing something that might change over time, like a C-set, we don't want to use deBruijn levels, because we don't want have to change all of our identifiers when we delete something, so in the rest of this I will instead say \"local identifier\" instead of deBruijn level to refer to a nameless representation of an identifier.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"(the name \"local identifier\" and also some of this philosophy is taken from chit)","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In general, naming is given by a relation between symbols and bindings (as refered to by local identifiers). Each binding may be associated with zero or more symbols, and each symbol might be associated with zero or more bindings.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"We name the failure of this relation to be a bijection in several ways.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one symbol is related to a single binding, we say that this","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"binding has aliases. In this case, we should also have a primary alias used as a default.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If more than one binding is related to a single symbol, we have name overlap.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Name overlap can be resolved by overloading and shadowing, we will talk about this later on.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no symbol is related to a binding, such as when the binding is created","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"programmatically, we need nameless references to be able to refer to the binding, which are also created programmatically.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"If no binding is related to a symbol, then we have a name error; this name","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"is not valid in the current context and we must throw an error.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"The most important thing to get right is name overlap; we discuss this first.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"There are two ways in which to resolve name overlap. The first way is via overloading. In overloading, we disambiguate an ambiguous name via its context, for instance what type it is expected to be, or what arguments is it receiving. The second way is via shadowing. In shadowing, a name is resolved by making it point to the \"most recently defined\" thing with that name.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"In GATlab, we handle overloading and shadowing with a notion of scope. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. Each scope is identified with a ScopeTag, which is an opaque identifier (i.e. a UUID). We take this idea from Racket, but we don't need the more complex \"scope sets\" from Racket because GATs don't need to process the syntax of other GATs; if we start doing this we'll have to rethink the design, but we'll probably have bigger problems too.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Two variables with the same name within a single scope are meant to overload one another. For instance, this is what happens with mcompose in the theory of monoidal categories; it is overloaded for Hom and Ob, and this is what happens with d in the discrete exterior calculus; it is overloaded for all of the (k+1)-forms. Variables in different scopes with the same name shadow one another. When we parse an expression a + b, we do so in an ordered list of scopes, and the most recent scope \"wins\".","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Parsing turns a Symbol into an Ident. The Ident contains the original Symbol for printing, but it also contains a reference to a scope via ScopeTag, and an local identifier (\"lid\") within that scope. Thus, the name in the Ident is never needed for later stages of programatic manipulation.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Scopes cache the relation between names and bindings, by providing a way to go from binding (as reified by local identifier) to a set of aliases with distinguished primary alias, and to go from name to the set of bindings that have that name that we need to disambiguate between in the case of an overload.","category":"page"},{"location":"concepts/scopes/","page":"Scopes","title":"Scopes","text":"Because Idents are fully unambiguous even without their name, it is also possible to create an Ident with no name, which solves the problem of nameless references.","category":"page"},{"location":"concepts/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 9925806c..e38f1c5d 100644 --- a/dev/stdlib/index.html +++ b/dev/stdlib/index.html @@ -1,2 +1,2 @@ -Standard Library · GATlab.jl
GitHub

Standard Library

Categories

Our friend ThCategory is the main theory in this module.

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

thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]

Category Building Blocks

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

+Standard Library · GATlab.jl
GitHub

Standard Library

Categories

Our friend ThCategory is the main theory in this module.

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

thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]

Category Building Blocks

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