Library Reference
Syntax
GATlab.Syntax.Scopes.Binding — TypeBinding{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)
GATlab.Syntax.Scopes.Context — TypeA 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) -> Scopenscopes(c::Context) -> Inthastag(c::Context, tag::ScopeTag) -> Boolhasname(c::Context, name::Symbol) -> Boolgetlevel(c::Context, tag::ScopeTag) -> Intgetlevel(c::Context, name::Symbol) -> Int
GATlab.Syntax.Scopes.HasScope — TypeAn abstract type for wrappers around a single scope.
Must overload
getscope(hs::HasScope) -> Scope
GATlab.Syntax.Scopes.HasScopeList — TypeA type for things which contain a scope list.
Notably, GATs contain a scope list.
Must implement:
getscopelist(hsl::HasScopeList) -> ScopeList
GATlab.Syntax.Scopes.Ident — TypeIdent
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
GATlab.Syntax.Scopes.LID — TypeA 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.
GATlab.Syntax.Scopes.Scope — TypeScope{T, Sig}
In GATlab, we handle overloading and shadowing with a notion of scope. Anything which binds variables introduces a scope, for instance a @theory declaration or a context. For example, a scope with 3 elements:
x::Int = 3
+Library Reference · GATlab.jl Library Reference
Syntax
GATlab.Syntax.Scopes.Binding — TypeBinding{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)
sourceGATlab.Syntax.Scopes.Context — TypeA 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) -> Scopenscopes(c::Context) -> Inthastag(c::Context, tag::ScopeTag) -> Boolhasname(c::Context, name::Symbol) -> Boolgetlevel(c::Context, tag::ScopeTag) -> Intgetlevel(c::Context, name::Symbol) -> Int
sourceGATlab.Syntax.Scopes.HasScope — TypeAn abstract type for wrappers around a single scope.
Must overload
getscope(hs::HasScope) -> Scope
sourceGATlab.Syntax.Scopes.HasScopeList — TypeA type for things which contain a scope list.
Notably, GATs contain a scope list.
Must implement:
getscopelist(hsl::HasScopeList) -> ScopeList
sourceGATlab.Syntax.Scopes.Ident — TypeIdent
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
sourceGATlab.Syntax.Scopes.LID — TypeA 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.
sourceGATlab.Syntax.Scopes.Scope — TypeScope{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.
sourceGATlab.Syntax.Scopes.ScopeTag — TypeThe tag that makes reference to a specific scope possible.
sourceGATlab.Syntax.Scopes.ScopeTagError — TypeScopeTagError
An error to throw when an identifier has an unexpected scope tag
sourceBase.:+ — MethodDeterministically combine two scope tags into a third
sourceGATlab.Syntax.Scopes.equiv — MethodCompare two scopes, ignoring the difference in the top-level scope tag.
sourceGATlab.Syntax.Scopes.getlid — MethodDetermine the level of a binding given the name and possibly the signature
sourceGATlab.Syntax.Scopes.hasident — Methodhasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
sourceGATlab.Syntax.Scopes.ident — Methodident 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.
sourceGATlab.Syntax.Scopes.rename — Methodrename(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.
sourceGATlab.Syntax.Scopes.retag — Methodretag(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.
sourceGATlab.Syntax.Scopes.unsafe_addalias! — Methodunsafe_addalias! should only be used when unsafe_pushbinding! won't be called again, because new bindings won't get the old aliases.
sourceGATlab.Syntax.GATs.Judgment — TypeJudgment
A judgment is either a type constructor, term constructor, or axiom; a GAT is composed of a list of judgments.
sourceGATlab.Syntax.GATs.AbstractConstant — TypeWe need this to resolve a mutual reference loop; the only subtype is Constant
sourceGATlab.Syntax.GATs.AlgAxiom — TypeAlgAxiom
A declaration of an axiom
sourceGATlab.Syntax.GATs.AlgSort — TypeAlgSort
A sort, which is essentially a type constructor without arguments ref must be reference to a AlgTypeConstructor
sourceGATlab.Syntax.GATs.AlgSorts — TypeAlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
sourceGATlab.Syntax.GATs.AlgTerm — TypeAlgTerm
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
sourceGATlab.Syntax.GATs.AlgTermConstructor — TypeAlgTermConstructor
A declaration of a term constructor
sourceGATlab.Syntax.GATs.AlgType — TypeAlgType
One syntax tree to rule all the types. head must be reference to a AlgTypeConstructor
sourceGATlab.Syntax.GATs.AlgTypeConstructor — TypeAlgTypeConstructor
A declaration of a type constructor
sourceGATlab.Syntax.GATs.Constant — TypeConstant
A Julia value in an algebraic context. Checked elsewhere.
sourceGATlab.Syntax.GATs.GAT — TypeGAT
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.
sourceGATlab.Syntax.GATs.GATSegment — TypeGATSegment
A piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.
sourceGATlab.Syntax.GATs.JudgmentBinding — TypeJudgmentBinding
A binding of a judgment to a name and possibly a signature.
sourceGATlab.Syntax.GATs.SortScope — TypeSortScope
A scope where variables are assigned to AlgSortss, and no overloading is permitted.
sourceGATlab.Syntax.GATs.TermInCtx — TypeA term with an accompanying type scope, e.g.
(a,b)::R
a*(a+b)
sourceGATlab.Syntax.GATs.TermInCtx — MethodGet the canonical term associated with a term constructor
sourceGATlab.Syntax.GATs.TypeScope — TypeTypeScope
A scope where variables are assigned to AlgTypes, and no overloading is permitted.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodSome expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodSome expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodReturn nothing if the binding we parse has already been bound.
sourceGATlab.Syntax.GATs.argcontext — MethodLocal context of an AlgTermConstructor, including the arguments themselves
sourceGATlab.Syntax.GATs.bind_localctx — MethodTake a term constructor and determine terms of its local context.
This function is mutually recursive with infer_type.
sourceGATlab.Syntax.GATs.equations — MethodGet equations for a term or type constructor
sourceGATlab.Syntax.GATs.equations — MethodImplicit 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
sourceGATlab.Syntax.GATs.infer_type — MethodInfer 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)).
sourceGATlab.Syntax.GATs.normalize_decl — Methodaxiom=true adds a ::default to exprs like f(a,b) ⊣ [a::A, b::B]
sourceGATlab.Syntax.GATs.parsetypescope — MethodKeep 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.)
sourceGATlab.Syntax.GATs.sortcheck — Methodsortcheck(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.
sourceGATlab.Syntax.GATs.sortcheck — Methodsortcheck(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.
sourceGATlab.Syntax.GATs.substitute_term — MethodReplace idents with AlgTerms.
sourceGATlab.Syntax.Presentations.Presentation — TypeA 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.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodParse, 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.
sourceGATlab.Syntax.Scopes.ScopeTag — TypeThe tag that makes reference to a specific scope possible.
sourceGATlab.Syntax.Scopes.ScopeTagError — TypeScopeTagError
An error to throw when an identifier has an unexpected scope tag
sourceGATlab.Syntax.Scopes.ScopedBinding — TypeType for printing out bindings with colored keys
sourceBase.:+ — MethodDeterministically combine two scope tags into a third
sourceGATlab.Syntax.Scopes.equiv — MethodCompare two scopes, ignoring the difference in the top-level scope tag.
sourceGATlab.Syntax.Scopes.getlid — MethodDetermine the level of a binding given the name and possibly the signature
sourceGATlab.Syntax.Scopes.hasident — Methodhasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.
sourceGATlab.Syntax.Scopes.ident — Methodident 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.
sourceGATlab.Syntax.Scopes.rename — Methodrename(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.
sourceGATlab.Syntax.Scopes.retag — Methodretag(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.
sourceGATlab.Syntax.Scopes.unsafe_addalias! — Methodunsafe_addalias! should only be used when unsafe_pushbinding! won't be called again, because new bindings won't get the old aliases.
sourceGATlab.Syntax.GATs.Judgment — TypeJudgment
A judgment is either a type constructor, term constructor, or axiom; a GAT is composed of a list of judgments.
sourceGATlab.Syntax.GATs.AbstractConstant — TypeWe need this to resolve a mutual reference loop; the only subtype is Constant
sourceGATlab.Syntax.GATs.AlgAxiom — TypeAlgAxiom
A declaration of an axiom
sourceGATlab.Syntax.GATs.AlgSort — TypeAlgSort
A sort, which is essentially a type constructor without arguments ref must be reference to a AlgTypeConstructor
sourceGATlab.Syntax.GATs.AlgSorts — TypeAlgSorts
A description of the argument sorts for a term constructor, used to disambiguate multiple term constructors of the same name.
sourceGATlab.Syntax.GATs.AlgTerm — TypeAlgTerm
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
sourceGATlab.Syntax.GATs.AlgTermConstructor — TypeAlgTermConstructor
A declaration of a term constructor
sourceGATlab.Syntax.GATs.AlgType — TypeAlgType
One syntax tree to rule all the types. head must be reference to a AlgTypeConstructor
sourceGATlab.Syntax.GATs.AlgTypeConstructor — TypeAlgTypeConstructor
A declaration of a type constructor
sourceGATlab.Syntax.GATs.Constant — TypeConstant
A Julia value in an algebraic context. Checked elsewhere.
sourceGATlab.Syntax.GATs.GAT — TypeGAT
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.
sourceGATlab.Syntax.GATs.GATSegment — TypeGATSegment
A piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.
sourceGATlab.Syntax.GATs.InCtx — TypeA type or term with an accompanying type scope, e.g.
(a,b)::R (a,b)::Ob –––––- or ––––– a*(a+b) Hom(a,b)
sourceGATlab.Syntax.GATs.InCtx — MethodGet the canonical term + ctx associated with a term constructor.
sourceGATlab.Syntax.GATs.InCtx — MethodGet the canonical type + ctx associated with a type constructor.
sourceGATlab.Syntax.GATs.JudgmentBinding — TypeJudgmentBinding
A binding of a judgment to a name and possibly a signature.
sourceGATlab.Syntax.GATs.SortScope — TypeSortScope
A scope where variables are assigned to AlgSortss, and no overloading is permitted.
sourceGATlab.Syntax.GATs.TypeScope — TypeTypeScope
A scope where variables are assigned to AlgTypes, and no overloading is permitted.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodSome expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodSome expr may have already been bound (e.g. by an explicit context) and thus oughtn't be interpreted as default type.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodReturn nothing if the binding we parse has already been bound.
sourceGATlab.Syntax.GATs.argcontext — MethodLocal context of an AlgTermConstructor, including the arguments themselves
sourceGATlab.Syntax.GATs.bind_localctx — MethodTake a term constructor and determine terms of its local context.
This function is mutually recursive with infer_type.
sourceGATlab.Syntax.GATs.equations — MethodGet equations for a term or type constructor
sourceGATlab.Syntax.GATs.equations — MethodImplicit 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
sourceGATlab.Syntax.GATs.infer_type — MethodInfer 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)).
sourceGATlab.Syntax.GATs.normalize_decl — Methodaxiom=true adds a ::default to exprs like f(a,b) ⊣ [a::A, b::B]
sourceGATlab.Syntax.GATs.parsetypescope — MethodKeep 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.)
sourceGATlab.Syntax.GATs.sortcheck — Methodsortcheck(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.
sourceGATlab.Syntax.GATs.sortcheck — Methodsortcheck(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.
sourceGATlab.Syntax.GATs.substitute_term — MethodReplace idents with AlgTerms.
sourceGATlab.Syntax.Presentations.Presentation — TypeA 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.
sourceGATlab.Syntax.ExprInterop.fromexpr — MethodParse, e.g.:
(a,b,c)::Ob
f::Hom(a, b)
g::Hom(b, c)
h::Hom(a, c)
h′::Hom(a, c)
-compose(f, g) == h == h′
sourceGATlab.Syntax.ExprInterop.toexpr — MethodContext of presentation is the underlying GAT
sourceGATlab.Syntax.ExprInterop.fromexpr — Functionfromexpr(c::Context, e::Any, T::Type) -> Union{T,Nothing}
Converts a Julia Expr into type T, in a certain scope.
sourceGATlab.Syntax.ExprInterop.toexpr — Functiontoexpr(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.
sourceGATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP — ConstantWhen 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.
sourceModels
GATlab.Models.ModelInterface.ImplementationNotes — TypeImplementationNotes
Information 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.
sourceGATlab.Models.ModelInterface.implements — Methodimplements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
sourceGATlab.Models.ModelInterface.parse_instance_body — MethodParses the raw julia expression into JuliaFunctions
sourceGATlab.Models.ModelInterface.qualify_function — MethodAdd model kwarg (it shouldn't have it already) Qualify method name to be in theory module Add context kwargs if not already present
TODO: throw error if there's junk kwargs present already?
sourceGATlab.Models.ModelInterface.typecheck_instance — MethodThrow error if missing a term constructor. Provides default instances for type constructors and type arguments, which return true or error, respectively.
sourceGATlab.Models.ModelInterface.@instance — MacroUsage:
struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+compose(f, g) == h == h′
sourceGATlab.Syntax.ExprInterop.toexpr — MethodContext of presentation is the underlying GAT
sourceGATlab.Syntax.ExprInterop.fromexpr — Functionfromexpr(c::Context, e::Any, T::Type) -> Union{T,Nothing}
Converts a Julia Expr into type T, in a certain scope.
sourceGATlab.Syntax.ExprInterop.toexpr — Functiontoexpr(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.
sourceGATlab.Syntax.TheoryInterface.GAT_MODULE_LOOKUP — ConstantWhen 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.
sourceModels
GATlab.Models.ModelInterface.ImplementationNotes — TypeImplementationNotes
Information 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.
sourceGATlab.Models.ModelInterface.implements — Methodimplements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}
If m implements the GATSegment referred to by tag, then return the corresponding implementation notes.
sourceGATlab.Models.ModelInterface.parse_instance_body — MethodParses the raw julia expression into JuliaFunctions
sourceGATlab.Models.ModelInterface.qualify_function — MethodAdd model kwarg (it shouldn't have it already) Qualify method name to be in theory module Add context kwargs if not already present
TODO: throw error if there's junk kwargs present already?
sourceGATlab.Models.ModelInterface.typecheck_instance — MethodThrow error if missing a term constructor. Provides default instances for type constructors and type arguments, which return true or error, respectively.
sourceGATlab.Models.ModelInterface.@instance — MacroUsage:
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
sourceGATlab.Models.SymbolicModels.GATExpr — TypeBase 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.
sourceBase.nameof — MethodGet name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
sourceGATlab.Models.SymbolicModels.constructor_name — MethodName of constructor that created expression.
sourceGATlab.Models.SymbolicModels.functor — MethodFunctor 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:
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.
Explicitly map each generator term to an instance value, using the generators dictionary.
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
sourceGATlab.Models.SymbolicModels.parse_json_sexpr — MethodDeserialize expression from JSON-able S-expression.
If symbols is true (the default), strings are converted to symbols.
sourceGATlab.Models.SymbolicModels.show_latex — MethodShow the expression in infix notation using LaTeX math.
Does not include $ or \[begin|end]{equation} delimiters.
sourceGATlab.Models.SymbolicModels.show_sexpr — MethodShow the syntax expression as an S-expression.
Cf. the standard library function Meta.show_sexpr.
sourceGATlab.Models.SymbolicModels.show_unicode — MethodShow the expression in infix notation using Unicode symbols.
sourceGATlab.Models.SymbolicModels.symbolic_instance_methods — MethodJulia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides.
sourceGATlab.Models.SymbolicModels.syntax_module — MethodGet syntax module of given expression.
sourceGATlab.Models.SymbolicModels.to_json_sexpr — MethodSerialize expression as JSON-able S-expression.
The format is an S-expression encoded as JSON, e.g., "compose(f,g)" is represented as ["compose", f, g].
sourceGATlab.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.
- 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
sourceGATlab.Models.SymbolicModels.GATExpr — TypeBase 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.
sourceBase.nameof — MethodGet name of GAT generator expression as a Symbol.
If the generator has no name, returns nothing.
sourceGATlab.Models.SymbolicModels.constructor_name — MethodName of constructor that created expression.
sourceGATlab.Models.SymbolicModels.functor — MethodFunctor 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:
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.
Explicitly map each generator term to an instance value, using the generators dictionary.
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
sourceGATlab.Models.SymbolicModels.parse_json_sexpr — MethodDeserialize expression from JSON-able S-expression.
If symbols is true (the default), strings are converted to symbols.
sourceGATlab.Models.SymbolicModels.show_latex — MethodShow the expression in infix notation using LaTeX math.
Does not include $ or \[begin|end]{equation} delimiters.
sourceGATlab.Models.SymbolicModels.show_sexpr — MethodShow the syntax expression as an S-expression.
Cf. the standard library function Meta.show_sexpr.
sourceGATlab.Models.SymbolicModels.show_unicode — MethodShow the expression in infix notation using Unicode symbols.
sourceGATlab.Models.SymbolicModels.symbolic_instance_methods — MethodJulia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides.
sourceGATlab.Models.SymbolicModels.syntax_module — MethodGet syntax module of given expression.
sourceGATlab.Models.SymbolicModels.to_json_sexpr — MethodSerialize expression as JSON-able S-expression.
The format is an S-expression encoded as JSON, e.g., "compose(f,g)" is represented as ["compose", f, g].
sourceGATlab.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.
- 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
sourceUtilities
GATlab.Util.MetaUtils — ModuleGeneral-purpose tools for metaprogramming in Julia.
sourceGATlab.Util.MetaUtils.generate_docstring — MethodWrap Julia expression with docstring.
sourceGATlab.Util.MetaUtils.generate_function — MethodGenerate Julia expression for function definition.
sourceGATlab.Util.MetaUtils.parse_docstring — MethodParse Julia expression that is (possibly) annotated with docstring.
sourceGATlab.Util.MetaUtils.parse_function — MethodParse Julia function definition into standardized form.
sourceGATlab.Util.MetaUtils.parse_function_sig — MethodParse signature of Julia function.
sourceGATlab.Util.MetaUtils.replace_symbols — MethodReplace symbols occuring anywhere in a Julia expression.
sourceGATlab.Util.MetaUtils.replace_symbols — MethodReplace symbols occurring anywhere in a Julia function (except the name).
sourceGATlab.Util.MetaUtils.strip_lines — MethodRemove all LineNumberNodes from a Julia expression.
sourceSettings
This document was generated with Documenter.jl version 1.0.1 on Thursday 21 September 2023. Using Julia version 1.9.3.
Utilities
GATlab.Util.MetaUtils — ModuleGeneral-purpose tools for metaprogramming in Julia.
GATlab.Util.MetaUtils.generate_docstring — MethodWrap Julia expression with docstring.
GATlab.Util.MetaUtils.generate_function — MethodGenerate Julia expression for function definition.
GATlab.Util.MetaUtils.parse_docstring — MethodParse Julia expression that is (possibly) annotated with docstring.
GATlab.Util.MetaUtils.parse_function — MethodParse Julia function definition into standardized form.
GATlab.Util.MetaUtils.parse_function_sig — MethodParse signature of Julia function.
GATlab.Util.MetaUtils.replace_symbols — MethodReplace symbols occuring anywhere in a Julia expression.
GATlab.Util.MetaUtils.replace_symbols — MethodReplace symbols occurring anywhere in a Julia function (except the name).
GATlab.Util.MetaUtils.strip_lines — MethodRemove all LineNumberNodes from a Julia expression.