8.12
Lathe Morphisms🔗ℹ
Lathe Morphisms for Racket isn’t much yet, but it’s going to be a library centering around category theory and foundational mathematics. We recognize not everyone is going to want to wade through specialized mathematical terminology, so as we design and document Lathe Morphisms, we hope to first consider the needs of those people who have little choice.
This goal of writing a category theory library for Racket can take many forms. Even within the field of category theory, it’s common to investigate alternative ways of formalizing the basic concepts. Then when trying to represent category theory concepts in a programming language, it’s possible to approach that task with varying degrees of fidelity to the matematical concepts. Finally, Racket is a programming language that embraces language extension and polyglot programming, and different ways of programming in Racket (especially different #langs) may justify different API design approaches.
In Lathe Morphisms for Racket, we choose our naming conventions to make room for a number of different approaches all at once. In particular, we’re making room for approaches that have support for a form of classical reasoning, even though for now we just have a couple of approaches based on a constructive form of category theory without proof witnesses.
Throughout this library, we sometimes need to ensure that more than one value passed to a function are all close enough together. For functions like these, we consider one of the values v to be the source of truth, and we check that the others are (ok/c v). This calls the value’s atomic-set-element-sys-accepts/c method if it has one, and otherwise it just uses any/c.
At its strictest, the implementation of a value’s ...-accepts/c method will tend to use match/c around some recursive calls to ok/c. At its most lenient, it can simply return any/c. Even for programs where the strictness of contracts is a priority, it’s advisable to be at least a lenient enough to allow for any impersonators that program’s contracts produce. Generally, concepts Lathe Morphisms offers like categories and functors can’t be impersonated in a way that’s actually an impersonator-of? the original, so they’ll be a kind of pseudo-impersonator. Lathe Morphisms doesn’t currently offer any pseudo-impersonators of its own, but programmers should watch out for at least the pseudo-impersonators they define themselves.
1 Functional-programming-based theories🔗ℹ
1.1 Functional-programming-based theories that are "mediary" for open extensibility🔗ℹ
1.1.1 Mediary sets and their elements🔗ℹ
1.1.1.1 Behavior of well-behaved set elements🔗ℹ
Struct-like operations which construct and deconstruct a value that represents the behavior that makes a set element well-behaved. Namely, this behavior consists of a way to get the value itself (
getter-of-value-expr) and a way to get a contract that recognizes values that are
close enough to it (
getter-of-accepts/c-expr).
Two set-element-good-behavior values are equal? if they contain equal? elements.
Given the well-behaved behavior of a well-behaved set element, returns the element.
Returns a contract that recognizes the well-behaved behavior of a well-behaved set element as long as the given contract recognizes that element.
Returns a contract that recognizes the well-behaved behavior of a well-behaved set element as long as the given mediary set system recognizes that well-behaved element as one of its (not necessarily well-behaved) elements.
1.1.1.2 Atomic set elements🔗ℹ
Structure type property operations for atomic set elements, which are well-behaved set elements that can procure their own
set-element-good-behavior? values.
Given an atomic set element, returns its well-behaved behavior.
Given an atomic set element, returns the contract it uses to check for
close enough values.
When good-behavior is called with an element element to obtain a set-element-good-behavior? value, the result of calling the set-element-good-behavior-getter-of-value getter of that value should be element.
Most of the time, make-atomic-set-element-sys-impl-from-good-behavior is more general-purpose than necessary, and make-atomic-set-element-sys-impl-from-contract can be used instead.
While this is more convenient, make-atomic-set-element-sys-impl-from-good-behavior is technically more general-purpose. That alternative gives more comprehensive control over things like the eq? identity of various values, the timing of side effects, the particular prop:procedure-implementing structs that implement the procedures, the presence of impersonators in various places, and whether the set-element-good-behavior-getter-of-value getter returns element (which it should) or some other value (which it shouldn’t). For an API-compliant pure FP style with little use of impersonators, there’s virtually no need for that extra generality.
1.1.1.3 Mediary sets themselves🔗ℹ
Structure type property operations for mediary sets, which are sets where not all the elements have to be well-behaved.
The only thing that makes an element well-behaved is that it can recognize when another value is close enough to it.
The behavior of a mediary set itself is limited to recognizing its values.
Returns a contract which recognizes any element of the given mediary set.
1.1.1.4 Utilities based on mediary sets🔗ℹ
Structure type property operations for sets, which have a type of elements represented by a contract and an ...-accepts/c method.
Returns a contract which recognizes any element of the given set.
Given an element of a given set, returns a contract which recognizes values that are
close enough to it.
Structure type property operations for categories, which have a set (
set-sys?) of objects and for every two objects, a set of morphisms from one to the other.
Returns the set of objects in the given category.
Returns a contract which recognizes any object of the given category.
Returns the set of morphisms that go from the given object s (the source) to the given object t (the target) in the given category.
Returns a contract which recognizes any morphism that goes from the given object s (the source) to the given object t (the target) in the given category.
Returns the identity morphism which goes from the given object to itself in the given category.
Returns the morphism which is the composition of two given morphisms fenceposted by three given objects in the given category.
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each morphism. Composition in category theory literature is most often written with its arguments the other way around.
The given method implementations should observe some algebraic laws. Namely, the morphism-chain-two operation should be associative, and object-identity-morphism should act as an identity element for it. In more symbolic terms (using a pseudocode DSL):
Structure type property operations for functors, structure-preserving transformations of objects and morphisms from a source category to a target category.
Returns a functor’s source category.
Returns a functor like the given one, but with its source category replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
functor-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Returns a functor’s target category.
Returns a functor like the given one, but with its target category replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
functor-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Transforms an object according to the given functor.
Uses the given functor to transform a morphism that originally goes from the given source object a to the given target object b.
Given implementations for the following methods, returns something a struct can use to implement the
prop:functor-sys interface.
When the replace methods don’t raise errors, they should observe the lens laws: The result of getting a value after it’s been replaced should be the same as just using the value that was passed to the replacer. The result of replacing a value with itself should be the same as not using the replacer at all. The result of replacing a value and replacing it a second time should be the same as just skipping to the second replacement.
Moreover, the replace methods should not raise an error when a value is replaced with itself. They’re intended only for use by functor-sys/c and similar error-detection systems, which will tend to replace a replace a value with one that reports better errors.
The other given method implementations should observe some algebraic laws. Namely, the apply-to-morphism operation should respect the identity and associativity laws of the category-sys-object-identity-morphism and category-sys-morphism-chain-two operations. In more symbolic terms (using a pseudocode DSL):
Returns a contract that recognizes any functor whose source and target categories are recognized by the given contracts.
The result is a flat contract as long as the given contracts are flat.
Returns a functor that goes from the source category s to the target category t, transforming objects and morphisms using the given procedures.
This may be more convenient than defining an instance of prop:functor-sys.
The given procedures should satisfy algebraic laws. Namely, the apply-to-morphism operation should respect the identity and associativity laws of the category-sys-object-identity-morphism and category-sys-morphism-chain-two operations. In more symbolic terms (using a pseudocode DSL):
Returns the identity functor on the given category. This is a functor that goes from the given category to itself, taking every object and every morphism to itself.
Returns the composition of the two given functors. This is a functor that goes from the first functor’s source category to the second functor’s target category, transforming every object and every morphism by applying the first functor and then the second. The target of the first functor should match the source of the second.
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each functor. Composition in category theory literature is most often written with its arguments the other way around.
Structure type property operations for natural transformations, transformations of morphisms that relate a source functor (
functor-sys?) to a target functor.
Returns a natural transformation’s endpoint functors’ source category.
Returns a natural transformation like the given one, but with its endpoint functors’ source category replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
natural-transformation-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Returns a natural transformation’s endpoint functors’ target category.
Returns a natural transformation like the given one, but with its endpoint functors’ target category replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
natural-transformation-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Returns a flat contract that recognizes any functor that goes from the natural transformation’s endpoint functors’ source category to their target category.
Returns a natural transformation’s source functor.
Returns a natural transformation like the given one, but with its source functor replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
natural-transformation-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Returns a natural transformation’s target functor.
Returns a natural transformation like the given one, but with its target functor replaced with the given one. This may raise an error if the given value isn’t similar enough to the one being replaced. This is intended only for use by
natural-transformation-sys/c and similar error-detection systems as a way to replace a value with one that reports better errors.
Uses the given natural transformation to transform a morphism that originally goes from the given source object a to the given target object b.
When the replace methods don’t raise errors, they should observe the lens laws: The result of getting a value after it’s been replaced should be the same as just using the value that was passed to the replacer. The result of replacing a value with itself should be the same as not using the replacer at all. The result of replacing a value and replacing it a second time should be the same as just skipping to the second replacement.
Moreover, the replace methods should not raise an error when a value is replaced with itself. They’re intended only for use by natural-transformation-sys/c and similar error-detection systems, which will tend to replace a replace a value with one that reports better errors.
The other given method implementations should observe some algebraic laws. Namely, applying the apply-to-morphism operation to a composed morphism should be the same as applying it to just one composed part of that morphism and applying the source and target functors to the other parts so that it joins up. In more symbolic terms (using a pseudocode DSL):
Using an infix notation where we infer most arguments and write (ab ; bc) for the category-sys-morphism-chain-two operation, these laws can be written like so:
| s ab ; nts bc = nts (ab ; bc) = nts ab ; t bc |
Using more math-style variable name choices:
| F f ; alpha g = alpha (f ; g) = alpha f ; G g |
In category theory literature, it’s common for natural transformations’ component functions to go from objects to morphisms, not morphisms to morphisms. We consider a natural transformation to act on an object by applying to its identity morphism. In that case the usual naturality square law looks like this:
| F f ; alpha (id y) = alpha (id x) ; G f |
We can derive that law like so:
| F f ; alpha (id y) |
| = alpha (f ; id y) |
| = alpha f |
| = alpha (id x ; f) |
| = alpha (id x) ; G f |
Returns a contract that recognizes any natural transformation for which the source and target functors and their source and target categories are recognized by the given contracts.
The result is a flat contract as long as the given contracts are flat.
Returns a natural transformation that goes from the source functor s to the target functor t, transforming morphisms using the given procedure.
This may be more convenient than defining an instance of prop:natural-transformation-sys.
The given procedure should satisfy algebraic laws. Namely, applying the apply-to-morphism operation to a composed morphism should be the same as applying it to just one composed part of that morphism and applying the source and target functors to the other parts so that it joins up. In more symbolic terms (using a pseudocode DSL):
For a little more discussion about how our choice of natural transformation laws relates to the more common naturality square law, see the documentation for make-natural-transformation-sys-impl-from-apply.
Returns the identity natural transformation on the given functor. This is a natural transformation that goes from the given functor to itself, taking every morphism to itself.
Returns the vertical composition of the two given natural transformations. This is a natural transformation that goes from the first natural transformation’s source functor to the second natural transformation’s target functor. The target functor of the first natural transformation should match the source functor of the second.
If all the algebraic structures involved obey their laws, then the way this natural transformation transforms a morphism that’s composed from two morphisms is equivalent to applying the first natural transformation to the first part of the morphism, applying the second natural transformation to the second part of the morphism, and composing the results. Moreover, every morphism is the composition of itself and an identity morphism, so this specification determines the behavior on all morphisms. However, if any of the algebraic structures involved doesn’t obey its laws, this operation may leak some Lathe Morphisms implementation details that are subject to change.
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each natural transformation. Composition in category theory literature is most often written with its arguments the other way around.
Returns the horizontal composition of the two given natural transformations. This is a natural transformation that goes from the composition of their source functors to the composition of their target functors, transforming every morphism by applying the first natural transformation and then the second. The first natural transformation’s endpoint functors’ target category should match the second’s endpoint functors’ source category.
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the endpoint source to the endpoint target of each natural transformation. Composition in category theory literature is most often written with its arguments the other way around.