Library Reference

Binding{T}

A binding associates some T-typed value to a name.

name is an optional distinguished name value is the element

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

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

Contexts should overload:

• getscope(c::Context, level::Int) -> Scope
• nscopes(c::Context) -> Int
• hastag(c::Context, tag::ScopeTag) -> Bool
• hasname(c::Context, name::Symbol) -> Bool
• getlevel(c::Context, tag::ScopeTag) -> Int
• getlevel(c::Context, name::Symbol) -> Int
• alltags(c::Context) -> Set{ScopeTag}

An abstract type for wrappers around a single scope.

Must overload

getscope(hs::HasScope) -> Scope

A type for things which contain a scope list.

Notably, GATs contain a scope list.

Must implement:

getscopelist(hsl::HasScopeList) -> ScopeList

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

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.

Scope{T}

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

x = 3
y = "hello"
z = x 

Here z is introduced as an alias for x. It is illegal to shadow within a scope. Overloading is not explicitly treated but can be managed by having values which refer to identifiers earlier / the present scope. See GATs.jl, for example.

The tag that makes reference to a specific scope possible.

ScopeTagError

An error to throw when an identifier has an unexpected scope tag

Type for printing out bindings with colored keys

This collects all the idents in a scope

Determine the level of a binding given the name

hasident checks whether an identifier with specified data exists, by attempting to create it and returning whether or not that attempt failed.

ident creates an Ident from a context and some partial data supplied as keywords.

Keywords arguments:

• tag::Union{ScopeTag, Nothing}. The tag of the scope that the Ident is in.
• name::Union{Symbol, Nothing}. The name of the identifier.
• lid::Union{LID, Nothing}. The lid of the identifier within its scope.
• level::Union{Int, Nothing}. The level of the scope within the context.
• strict::Bool. If strict is true, throw an error if not found, else return nothing.

This is a broadcasted version of ident

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.

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.

Add a new binding to the end of Scope s.

We need this to resolve a mutual reference loop; the only subtype is Constant

We need this to resolve a mutual reference loop; the only subtype is Dot

AlgAccessor

The arguments to a term constructor serve a dual function as both arguments and also methods to extract the value of those arguments.

I.e., declaring Hom(dom::Ob, codom::Ob)::TYPE implicitly overloads a previous declaration for dom and codom, or creates declarations if none previously exist.

AlgAxiom

A declaration of an axiom

AlgDeclaration

A declaration of a constructor; constructor methods in the form of AlgTermConstructors or the accessors for AlgTypeConstructors follow later in the theory.

Accessing a name from a term of tuple type

AlgSort

A sort for equality judgments of terms for a particular sort

A shorthand for a function, such as "square(x) := x * x". It is relevant for models but can be ignored by theory maps, as it is fully determined by other judgments in the theory.

AlgSort

A sort, which is essentially a type constructor without arguments

AlgStruct

A declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor which constructs an element of that type, and projection term constructors. E.g.

struct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]
  apex::Ob
  i1::dom->apex
  i2::codom->apex
end

Is tantamount to (in a vanilla GAT):

Cospan(dom::Ob, codom::Ob)::TYPE 

cospan(apex, i1, i2)::Cospan(dom, codom) 
  ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]

apex(csp::Cospan(d::Ob, c::Ob))::Ob            
i1(csp::Cospan(d::Ob, c::Ob))::(d->apex(csp))
i2(csp::Cospan(d::Ob, c::Ob))::(c->apex(csp))

apex(cospan(a, i_1, i_2)) == a  
  ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
i1(cospan(a, i_1, i_2)) == i_1 
  ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
i2(cospan(a, i_1, i_2)) == i_2
  ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]

cospan(apex(csp), i1(csp), i2(csp)) == csp
  ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]

AlgTerm

One syntax tree to rule all the terms.

AlgTermConstructor

A declaration of a term constructor as a method of an AlgFunction.

AlgType

One syntax tree to rule all the types.

AlgTypeConstructor

A declaration of a type constructor.

Constant

A Julia value in an algebraic context. Type checked elsewhere.

Eq

The type of equality judgments.

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.

GATContext

A context consisting of two parts: a GAT and a TypeCtx

Certain types (like AlgTerm) can only be parsed in a GATContext, because they require access to the method resolving in the GAT.

GATSegment

A piece of a GAT, consisting of a scope that binds judgments to names, possibly disambiguated by argument sorts.

This is a struct rather than just a type alias so that we can customize the show method.

Get the canonical type + ctx associated with a type constructor.

Get the canonical term + ctx associated with a method.

A GAT is conceptually a bunch of Judgments strung together.

MethodApp

An application of a method of a constructor to arguments. We need a type parameter T because AlgTerm hasn't been defined yet, but the only type used for T will in fact be AlgTerm.

method either points to an AlgTermConstructor, an AlgTypeConstructor or an AlgAccessor,

MethodResolver

Right now, this just maps a sort signature to the resolved method.

When we eventually support varargs, this will have to do something slightly fancier.

TypeScope

A scope where variables are assigned to AlgTypes. We use a wrapper here so that it pretty prints as [a::B] instead of {a => AlgType(B)}

Get equations for a term or type constructor

Implicit equations defined by a context.

This function allows a generalized algebraic theory (GAT) to be expressed as an essentially algebraic theory, i.e., as partial functions whose domains are defined by equations.

References:

• (Cartmell, 1986, Sec 6: "Essentially algebraic theories and categories with finite limits")
• (Freyd, 1972, "Aspects of topoi")

This function gives expressions for computing the elements of c.context which can be inferred from applying accessor functions to elements of args.

Example:

equations({f::Hom(a,b), g::Hom(b,c)}, {a::Ob, b::Ob, c::Ob}, ThCategory)

waysofcomputing = Dict(a => [dom(f)], b => [codom(f), dom(g)], c => [codom(g)], f => [f], g => [g])

Common methods for AlgType and AlgTerm

Coerce GATs to GAT contexts

This only works when seg is a segment of theory

This is necessary because the intuitive precedence rules for the symbols that we use do not match the Julia precedence rules. In theory, this could be written with some algorithm that recalculates precedence, but I am too lazy to write that, so instead I just special case everything.

f(pushbinding!, expr) should inspect expr and call pushbinding! 0 or more times with two arguments: the name and value of a new binding.

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.

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.

Get all structs in a theory

Replace all functions with their desugared expressions

Replace idents with AlgTerms.

Parse, 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′

@symbolic ThRing function v(a, b, c)
  (a*b, c, b)
end

fromexpr(c::Context, e::Any, T::Type) -> Union{T,Nothing}

Converts a Julia Expr into type T, in a certain scope.

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.

Each theory corresponds to a module, which has the following items.

For each new term constructor in the theory, a newly declared function with the name of that term constructor.

For each new type constructor in the theory, a newly declared function with the name of that type constructor.

For each type parameter to a new type constructor in the theory, a function with the name of that type parameter.

For all of the old term constructors/type constructors/type parameters, imports from the modules that define them.

For all aliases, const declarations that make them equal to their primaries.

A macro called @theory which expands to the GAT data structure for the module.

A constant called Meta.theory which is the GAT data structure.

A struct called Meta.Wrapper which is a smart constructor for Julia types which implement the theory.

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.

The Dispatch model defers to type-dispatch

The Initial model assigns Union{} to all AlgSorts. There is one implementation for any given theory.

The Terminal model assigns Nothing to all AlgSorts. There is one implementation for any given theory.

Accepts a name, a theory body and returns a theory

Fully Qualified Module Name

Parse markdown coming out of @doc programatically.

Any Julia struct can be a model of a GAT. A model m::M is marked as implementing a theory iff, for all operations f(::A,::B,...), we have:

hasmethod(f, (WithModel{M}, A, B) == true

Then we expect the following.

Let M be the module corresponding to seg.

Then for each type constructor ty in seg, we must overload

M.ty(wm::WithModel{typeof(m)}, x, args...; context::Union{Nothing, NamedTuple})::Bool

to attempt to coerce x to a valid element of tc(args...) with explicit context context according to m (it is rare that you need a context for a type constructor; notable examples include 2-cells for a bicategory).

For each argument a to ty, we must overload

M.a(wm::WithModel{typeof(m)}, x;, context::Union{Nothing, NamedTuple})

to either error or return the argument a of x. It is perfectly valid for this to always error, (e.g. CSetTransformations which do not store their domain / codomain) but it is sometimes useful and convenient to define this, and additionally sometimes necessary for backwards compatibility.

Finally, for each term constructor tc in seg, we must overload

M.tc(wm::WithModel{typeof(m)}, args...; context::Union{Nothing, NamedTuple})

to apply the term constructor to the args. The implementation of M.tc should do no validity checking; that should be assumed to have already been done. In general, it is acceptable to error if context does not contain every element of the context. However, one may in fact only need certain elements of context, and so it is possible to get away without providing the context when you are writing code that is not generic across models, and you know that, for instance, composition of FinFunctions does not need the domains and codomains of the FinFunctions explicitly supplied.

A model implements a theory iff it implements all of the GATSegments in the theory.

Create an @instance for a model M whose methods are determined by type dispatch, e.g.:

@instance ThCategory{O,H} [model::M] begin
  id(x::O) = id(x)
  compose(f::H, g::H)::H = compose(f, g)
end

Use this with caution! For example, using this with two different models of the same theory with the same types would cause a conflict.

Create an @instance for a model M whose methods are determined by the implementation of another model, M2, e.g.:

@instance ThCategory{O,H} [model::M] begin
  id(x::O) = id[M2](x)
  compose(f::H, g::H)::H = compose[M2](f, g)
end

Returns two lists of JuliaFunctions: one for aliases of type constructors, one for aliases of term constructors.

Optional methodnames argument restricts aliases to only being generated if the name they are an alias for is included in this list.

Given a theory map A -> B, construct a new struct type which wraps a model of theory B and is itself a model of theory A. The name of the struct can be optionally given, otherwise it is gensym'd. The resulting expression is an instance of that struct type.

Future work: There is some subtlety in how accessor functions should be handled. TODO: The new instance methods do not yet handle the context keyword argument.

Parses the raw julia expression into JuliaFunctions

Add WithModel param first, if this is not an old instance (it shouldn't have it already) Qualify method name to be in theory module Qualify args to struct types Add context kwargs if not already present

Compile an AlgTerm into a Julia call Expr where termcons (e.g. f) are interpreted as mod.f[model.model](...).

Check if a method exists

A canonical implementation that just calls the method with type dispatch.

A canonical implementation that just calls the method with the implementation of another model, m.

If m implements a GAT with a type constructor (identified by ident id), mapped to a Julia type, this function returns that Julia type.

This can error if called on a symbol that matches a declaration that has more than one method

Check whether a model implements a particular theory.

If no types are provided, then we look up whether or not impl_type methods exist for this model + theory. If not, we will get a MethodError and assume that the model does not implement the theory. (WARNING: occasionally one has a complex type, such as foo(Int,String) which itself leads to a MethodError, and this can be confusing because it looks like the model doesn't implement the theory at all rather than just being an error in how it was implemented).

Once types are provided, we can check whether the theory is implemented by checking for each term constructor whether or not the model implements that (handled by a different implements method).

Machine-friendly access to checking if a model implements a particular operation. The types vector is in bijection with the AlgSorts of the whole theory.

User-friendly access to checking if a model implements an operation.

Throws an error if the name is overloaded. Anything programmatic should be calling a method which accepts method Idents rather than Symbols.

Usage:

struct TypedFinSetC
  ntypes::Int
end

@instance ThCategory{Vector{Int}, Vector{Int}} [model::TypedFinSetC] begin
  Ob(v::Vector{Int}) = all(1 <= j <= model.ntypes for j in v)
  Hom(f::Vector{Int}, v::Vector{Int}, w::Vector{Int}) =
     length(f) == length(v) && all(1 <= y <= length(w) for y in f)

  id(v::Vector{Int}) = collect(eachindex(v))
  compose(f::Vector{Int}, g::Vector{Int}) = g[f]

  dom(f::Vector{Int}; context) = context.dom
  codom(f::Vector{Int}; context) = context.codom
end

struct SliceC{ObT, HomT, C}
  cat::C
  over::ObT
  function SliceC(cat::C, over) where C
    implements(cat, ThCategory) || error("Bad cat cat")
    obtype = impl_type(cat, ThCategory, :Ob)
    homtype = impl_type(cat, ThCategory, :Hom)
    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
  end
end

@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C}}} begin
  ...
end

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.

Get name of GAT generator expression as a Symbol.

If the generator has no name, returns nothing.

Name of constructor that created expression.

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

Create generator of the same type as the given expression.

Deserialize expression from JSON-able S-expression.

If symbols is true (the default), strings are converted to symbols.

Show the expression in infix notation using LaTeX math.

Does not include $ or \[begin|end]{equation} delimiters.

Show the syntax expression as an S-expression.

Cf. the standard library function Meta.show_sexpr.

Show the expression in infix notation using Unicode symbols.

Julia function for every type constructor, accessor, and term constructor. Term constructors can be overwritten by overrides.

Get syntax module of given expression.

Serialize 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].

@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])
g = Hom{:generator}([:g], [y, x])
h = Hom{:compose}([f, g], [x, x])

1. Methods inside the module (not exported) for all of the term constructors and

field accessors (i.e. stuff like compose, id, dom, codom), which construct terms.

1. A default instance (i.e., without a model parameter) of the theory using the

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

1. Coercion methods of the type constructors that allow one to introduce generators.

x = ThCategory.Ob(FreeCategory.Ob, :x)
y = ThCategory.Ob(FreeCategory.Ob, :y)
f = ThCategory.Hom(:f, x, y)

Note 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

munit() = ...

we have

munit(::Type{FreeSMC.Ob}) = ...

and likewise instead of

ThCategory.Ob(x::Any) = ...

we have

ThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...

Example:

@symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin
  compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end

This generates:

module FreeCategory
export Ob, Hom
using ..__module__

module Meta
  const theory_module = ThCategory
  const theory = ThCategory.Meta.theory
  const theory_type = ThCategory.Meta.T
end

struct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol
  args::Vector
  type_args::Vector{GATExpr}
end

struct Hom{T} <: __module__.HomExpr{T}
  args::Vector
  type_args::Vector{GATExpr}
end

dom(x::Hom) = x.type_args[1]

codom(x::Hom) = x.type_args[2]

function compose(f::Hom, g::Hom; strict=true)
  if strict && !(codom(f) == dom(g))
    throw(SyntaxDomainError(:compose, [f, g]))
  end
  Hom{:compose}([f, g], [dom(f), codom(g)])
end

function id(x::Ob)
  Ob{:id}([x], [x, x])
end
end

# default implementations 

function ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob
  FreeCategory.dom(x)
end

function ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob
  FreeCategory.Ob{:generator}([__value__], [])
end

function ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom
  FreeCategory.id(A)
end

function ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)
  associate_unit(FreeCategory.compose(f, g; strict), id)
end

General-purpose tools for metaprogramming in Julia.

For comparing JuliaFunctionSigs modulo the where parameters

Concatenate two Julia expressions into a block expression.

Wrap Julia expression with docstring.

Generate Julia expression for function definition.

Parse Julia expression that is (possibly) annotated with docstring.

Parse Julia function definition into standardized form.

Parse signature of Julia function.

Replace symbols occuring anywhere in a Julia expression.

Replace symbols occurring anywhere in a Julia function (except the name).

Remove all LineNumberNodes from a Julia expression.