Catlab API

Catlab API

Catlab.GATModule.

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")
source

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.

source

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.

source

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

source

Signature for a generalized algebraic theory (GAT).

source
Catlab.GAT.StubType.

Base type for method stubs in GAT signature.

source

Term constructor in a GAT.

source

Type constructor in a GAT.

source

Typeclass = GAT signature + Julia-specific content.

source

Julia functions for type parameter accessors.

source

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.

source

Julia functions for term constructors of GAT.

source

Implicit equations defined by context, allowing for implicit variables.

source

Implicit equations for term constructor.

source

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")
source

Expand context variables that occur implicitly in an expression.

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

source

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

source

Generate abstract type definition from a GAT type constructor.

source

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.

source

Complete set of Julia functions for a type class.

source

Parse type or term constructor in a GAT.

source

Parse context for term or type in a GAT.

source

Parse the body of a GAT instance definition.

source

Parse a raw expression in a GAT.

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

source

Parse the body of a GAT signature declaration.

source

Replace names of type constructors in a GAT.

source

Remove type parameters from dependent type.

source
Catlab.MetaModule.

General-purpose tools for metaprogramming in Julia.

source

Append a Julia expression to a block expression.

source

Concatenate two Julia expressions into a block expression.

source

Wrap Julia expression with docstring.

source

Generate Julia expression for function definition.

source

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

source

Parse Julia function definition into standardized form.

source

Parse signature of Julia function.

source

Replace symbols occuring anywhere in a Julia expression.

source

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

source

Remove all LineNumberNodes from a Julia expression.

source
Catlab.PresentModule.

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.

source

Add a generator defined by an equation.

source

Add an equation between terms to a presentation.

source

Add a generator to a presentation.

source

Add multiple generators to a presentation.

source

Get all equations of a presentation.

source

Retrieve a generator by name.

source

Get all generators of a presentation.

source

Does the presentation contain a generator with the given name?

source

Merge the second presentation into the first.

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

source

Define a presentation using a convenient syntax.

source

Translate definition of generator in terms of other generators.

source

Translate declaration of equality between terms.

source

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

source

Translate declaration of a generator.

source

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

source
Catlab.RewriteModule.

Rewriting for GAT expressions.

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

source

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

source

Simplify associative binary operation.

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

source

Simplify associative binary operation with unit.

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

source

Distribute unary operation over a binary operation.

source
Catlab.SyntaxModule.

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.

source

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.

source

Show the syntax expression as an S-expression.

Cf. the standard library function Meta.show_sexpr.

source

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.

source

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.

source

Deserialize expression from JSON-able S-expression.

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

source

Show the expression in infix notation using LaTeX math.

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

source

Show the expression in infix notation using Unicode symbols.

source

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

source

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.

source

Name of constructor that created expression.

source

Generate methods for syntax term constructors.

source

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.

source

Generate methods for term generators.

Generators are extra term constructors created automatically for the syntax.

source

Generate syntax type definitions.

source

Generate accessor methods for type parameters.

source

Create generator of the same type as the given expression.

source

Complete set of Julia functions for a syntax system.

source