Catlab API

Generalized algebraic theories (GATs) in Julia.

GATs generalize (multisorted) algebraic theories by incorporating a fragment of dependent type theory. They allow type and term constructors to be partially defined. GATs provide a convenient formal syntax for categorical structures.

At present, this module only supports defining the signature of a GAT. In the future we may allow axioms to be expressed as well. Regardless, we will persist in calling this module "GAT". Signatures are defined using the @signature macro.

There are several useful things to do with a GAT signature:

1. Define instances of the signature (models of the theory) in Julia code using the @instance macro
2. Define syntax systems using the @syntax macro (see Syntax module)
3. Define models of the theory by finite presentation using a syntax system and the @present macro (see Present module)

References:

• (Cartmell, 1986, "Generalized algebraic theories and contextual categoies")
• (Pitts, 1995, "Categorical logic", Sec 6: "Dependent types")

Invoke a term constructor by name on an instance.

This method provides reflection for GAT signatures. In everyday use the generic method for the constructor should be called directly, not through this function.

Cf. Julia's builtin invoke() function.

Define an instance of a generalized algebraic theory (GAT).

These are perfectly analagous to instances of a type class in Haskell. See also the Typeclass.jl library for Julia.

Define a signature of a generalized algebraic theory (GAT).

Three kinds of things can go in the signature body:

1. Type constructors, indicated by the special type TYPE, e.g. Hom(X::Ob,Y::Ob)::TYPE
2. Term constructors, e.g., id(X::Ob)::Hom(X,X)
3. Julia functions operating on the term constructors to provide additional functionality

A signature can extend existing signatures (at present only one).

Signature for a generalized algebraic theory (GAT).

Base type for method stubs in GAT signature.

Term constructor in a GAT.

Type constructor in a GAT.

Typeclass = GAT signature + Julia-specific content.

Julia functions for type parameter accessors.

Add a type-valued first argument to a Julia function signature.

We need this to avoid ambiguity in method dispatch when a term constructor has no arguments (e.g., munit()) or more generally has no arguments that are types in the signature (e.g., object generators in a category).

The fundamental reason why these cases must be treated specially is that Julia does not (yet?) support dispatching on return type.

Julia functions for term constructors of GAT.

Implicit equations defined by context, allowing for implicit variables.

Implicit equations for term 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")

Expand context variables that occur implicitly in an expression.

Reference: (Cartmell, 1986, Sec 10: 'Informal syntax').

Expand context variables that occur implicitly in the type expression of a term constructor.

Generate abstract type definition from a GAT type constructor.

Get type constructor by name.

Unlike term constructors, type constructors cannot be overloaded, so there is at most one type constructor with a given name.

Complete set of Julia functions for a type class.

Parse type or term constructor in a GAT.

Parse context for term or type in a GAT.

Parse the body of a GAT instance definition.

Parse a raw expression in a GAT.

A "raw expression" is a just composition of function and constant symbols.

Parse the body of a GAT signature declaration.

Replace names of type constructors in a GAT.

Remove type parameters from dependent type.

General-purpose tools for metaprogramming in Julia.

Append a Julia expression to a block expression.

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.

Finite presentations of a model of a generalized algebraic theory (GAT).

We support two methods for defining models of a GAT: as Julia objects using the @instance macro and as syntactic objects using the @present macro. Instances are useful for casting generic data structures, such as matrices, abstract tensor systems, and wiring diagrams, in categorical language. Presentations define small categories by generators and relations and are useful for applications like knowledge representation.

Add a generator defined by an equation.

Add an equation between terms to a presentation.

Add a generator to a presentation.

Add multiple generators to a presentation.

Get all equations of a presentation.

Retrieve a generator by name.

Get all generators of a presentation.

Does the presentation contain a generator with the given name?

Merge the second presentation into the first.

The first presentation is mutated and returned; the second is not.

Define a presentation using a convenient syntax.

Translate definition of generator in terms of other generators.

Translate declaration of equality between terms.

Translate a single statement in the presentation DSL to Julia code.

Translate declaration of a generator.

Translate a presentation in the DSL to a block of Julia code.

Rewriting for GAT expressions.

The current content of this module is just a stopgap until I can implement a generic term rewriting system.

Simplify unary operation that is an anti-involution on a (typed) monoid.

Simplify associative binary operation.

Maintains the normal form op(e1,e2,...) where e1,e2,... are expressions that are not applications of op()

Simplify associative binary operation with unit.

Reduces a freely generated (typed) monoid to normal form.

Distribute unary operation over a binary operation.

Syntax for a generalized algebraic theory (GAT).

Unlike instances of a theory, syntactic expressions don't necessarily satisfy the equations of the theory. For example, the default syntax operations for the Category theory don't form a category because they don't satisfy the category laws, e.g.,

compose(f, id(A)) != compose(f)

Whether dependent types are enforced at runtime and whether expressions are automatically brought to normal form depends on the particular syntax. In general, a single theory may have many different syntaxes. The purpose of this module to make the construction of syntax simple but flexible.

Base type for expression in the syntax of a GAT.

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.

Show the syntax expression as an S-expression.

Cf. the standard library function Meta.show_sexpr.

Invoke a term constructor by name in a syntax system.

This method provides reflection for syntax systems. In everyday use the generic method for the constructor should be called directly, not through this function.

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. Simply specify a Julia instance type for each doctrine 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.

1. For each doctrine 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.

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 expression in infix notation using Unicode symbols.

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

Define a syntax system for a generalized algebraic theory (GAT).

A syntax system consists of Julia types (with top type GATExpr) for each type constructor in the signature, plus Julia functions for

1. Generators: creating new generator terms, e.g., objects or morphisms
2. Accessors: accessing type parameters, e.g., domains and codomains
3. Term constructors: applying term constructors, e.g., composition and monoidal products

Julia code for all this is generated by the macro. Any of the methods can be overriden with custom simplification logic.

Name of constructor that created expression.

Generate methods for syntax term constructors.

Generate expressions for type parameters of term constructor.

Besides expanding the implicit variables, we must handle two annoying issues:

1. Add types for method dispatch where necessary (see GAT.add_type_dispatch) FIXME: We are currently only handling the nullary case (e.g., munit()). To handle the general case, we need to do basic type inference.

2. Rebind the term constructors to ensure that user overrides are preferred over the default term constructors.

Generate methods for term generators.

Generators are extra term constructors created automatically for the syntax.

Generate syntax type definitions.

Generate accessor methods for type parameters.

Create generator of the same type as the given expression.

Complete set of Julia functions for a syntax system.