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

1.1.1.2 Atomic set elements

1.1.1.3 Mediary sets themselves

1.1.1.4 Utilities based on mediary sets

1.2 Sets

1.3 Categories

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🔗ℹ

(require lathe-morphisms/in-fp/mediary/set)
	package: lathe-morphisms-lib

1.1.1.1 Behavior of well-behaved set elements🔗ℹ

syntax
set-element-good-behavior
syntax
(set-element-good-behavior
  getter-of-value-expr
  getter-of-accepts/c-expr)

   getter-of-value-expr : (-> any/c)
   getter-of-accepts/c-expr : (-> (flat-contract-accepting/c (getter-of-value-expr)))
match expander
(set-element-good-behavior
  getter-of-value-pat
  getter-of-accepts/c-pat)
procedure
(set-element-good-behavior? v) → boolean?
  v : any/c
procedure
(set-element-good-behavior-getter-of-value element-gb)
→ (-> any/c)
  element-gb : set-element-good-behavior?
procedure
(set-element-good-behavior-getter-of-accepts/c element-gb)
→
(->
  (flat-contract-accepting/c
    (set-element-good-behavior-value element-gb)))
  element-gb : set-element-good-behavior?

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.

procedure
(set-element-good-behavior-value element-gb) → any/c
element-gb : set-element-good-behavior?

Given the well-behaved behavior of a well-behaved set element, returns the element.

procedure
(set-element-good-behavior-with-value/c value/c) → contract?
value/c : contract?

Returns a contract that recognizes the well-behaved behavior of a well-behaved set element as long as the given contract recognizes that element.

procedure
(set-element-good-behavior-for-mediary-set-sys/c mss)
→ contract?
mss : mediary-set-sys?

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🔗ℹ

procedure
(atomic-set-element-sys? v) → boolean?
v : any/c
procedure
(atomic-set-element-sys-impl? v) → boolean?
v : any/c
value
prop:atomic-set-element-sys
: (struct-type-property/c atomic-set-element-sys-impl?)

Structure type property operations for atomic set elements, which are well-behaved set elements that can procure their own set-element-good-behavior? values.

procedure
(atomic-set-element-sys-good-behavior element)
→ set-element-good-behavior?
element : atomic-set-element-sys?

Given an atomic set element, returns its well-behaved behavior.

procedure
(atomic-set-element-sys-accepts/c element)
→ (flat-contract-accepting/c element)
element : atomic-set-element-sys?

Given an atomic set element, returns the contract it uses to check for close enough values.

procedure
(make-atomic-set-element-sys-impl-from-good-behavior good-behavior)
→ atomic-set-element-sys-impl?
good-behavior : (-> atomic-set-element-sys? set-element-good-behavior?)

Given an implementation for atomic-set-element-sys-good-behavior, returns something a struct can use to implement the prop:atomic-set-element-sys interface.

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.

procedure
(make-atomic-set-element-sys-impl-from-contract accepts/c)
→ atomic-set-element-sys-impl?
accepts/c :
(->i ([element atomic-set-element-sys?])
[_ (element) (flat-contract-accepting/c element)])

Given an implementation for atomic-set-element-sys-accepts/c, returns something a struct can use to implement the prop:atomic-set-element-sys interface.

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🔗ℹ

procedure
(mediary-set-sys? v) → boolean?
v : any/c
procedure
(mediary-set-sys-impl? v) → boolean?
v : any/c
value
prop:mediary-set-sys
: (struct-type-property/c mediary-set-sys-impl?)

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.

procedure
(mediary-set-sys-element/c mss) → contract?
mss : mediary-set-sys?

Returns a contract which recognizes any element of the given mediary set.

procedure
(make-mediary-set-sys-impl-from-contract element/c)
→ mediary-set-sys-impl?
element/c : (-> mediary-set-sys? contract?)

Given an implementation for mediary-set-sys-element/c, returns something a struct can use to implement the prop:mediary-set-sys interface.

1.1.1.4 Utilities based on mediary sets🔗ℹ

procedure
(ok/c example) → (flat-contract-accepting/c example)
example : any/c

Given a value, returns a contract that recognizes values that are close enough to it in the sense of an atomic set element. When the given value is indeed an atomic-set-element-sys?, this uses its atomic-set-element-sys-accepts/c contract. Otherwise, it considers any value (any/c) to be close enough.

1.2 Sets🔗ℹ

(require lathe-morphisms/in-fp/set)
	package: lathe-morphisms-lib

procedure
(set-sys? v) → boolean?
v : any/c
procedure
(set-sys-impl? v) → boolean?
v : any/c
value
prop:set-sys : (struct-type-property/c set-sys-impl?)

Structure type property operations for sets, which have a type of elements represented by a contract and an ...-accepts/c method.

procedure
(set-sys-element/c ss) → contract?
ss : set-sys?

Returns a contract which recognizes any element of the given set.

procedure
(set-sys-element-accepts/c ss element)
→ (flat-contract-accepting/c element)
ss : set-sys?
element : (set-sys-element/c ss)

Given an element of a given set, returns a contract which recognizes values that are close enough to it.

procedure
(make-set-sys-impl-from-contract element/c
element-accepts/c)
→ set-sys-impl?
  element/c : (-> set-sys? contract?)
   element-accepts/c :
(->i ([ss set-sys?] [element (ss) (set-sys-element/c ss)])
  [_ (element) (flat-contract-accepting/c element)])

Given implementations for set-sys-element/c and set-sys-element-accepts/c, returns something a struct can use to implement the prop:set-sys interface.

procedure
(makeshift-set-sys-from-contract element/c
element-accepts/c) → set-sys?
  element/c : (-> contract?)
   element-accepts/c :
(->i ([element (element/c)])
  [_ (element) (flat-contract-accepting/c element)])

Given implementations for set-sys-element/c and set-sys-element-accepts/c, returns a set.

1.3 Categories🔗ℹ

(require lathe-morphisms/in-fp/category)
	package: lathe-morphisms-lib

procedure
(category-sys? v) → boolean?
v : any/c
procedure
(category-sys-impl? v) → boolean?
v : any/c
value
prop:category-sys : (struct-type-property/c category-sys-impl?)

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.

procedure
(category-sys-object-set-sys cs) → set-sys?
cs : category-sys?

Returns the set of objects in the given category.

procedure
(category-sys-object/c cs) → contract?
cs : category-sys?

Returns a contract which recognizes any object of the given category.

procedure
(category-sys-morphism-set-sys cs s t) → set-sys?
  cs : category-sys?
  s : (category-sys-object/c cs)
  t : (category-sys-object/c cs)

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.

procedure
(category-sys-morphism/c cs s t) → contract?
  cs : category-sys?
  s : (category-sys-object/c cs)
  t : (category-sys-object/c cs)

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.

procedure
(category-sys-object-identity-morphism cs
object)
→ (category-sys-morphism/c cs object object)
cs : category-sys?
object : (category-sys-object/c cs)

Returns the identity morphism which goes from the given object to itself in the given category.

procedure
(category-sys-morphism-chain-two cs
a
b
c
ab
bc)
→ (category-sys-morphism/c cs a c)
  cs : category-sys?
  a : (category-sys-object/c cs)
  b : (category-sys-object/c cs)
  c : (category-sys-object/c cs)
  ab : (category-sys-morphism/c cs a b)
  bc : (category-sys-morphism/c cs b c)

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.

procedure
(make-category-sys-impl-from-chain-two
object-set-sys
morphism-set-sys
object-identity-morphism
morphism-chain-two)
→ category-sys-impl?
  object-set-sys : (-> category-sys? set-sys?)
   morphism-set-sys :
(->i
  (
    [cs category-sys?]
    [s (cs) (category-sys-object/c cs)]
    [t (cs) (category-sys-object/c cs)])
  [_ set-sys?])
   object-identity-morphism :
(->i
  ([cs category-sys?] [object (cs) (category-sys-object/c cs)])
  [_ (cs object) (category-sys-morphism/c cs object object)])
   morphism-chain-two :
(->i
  (
    [cs category-sys?]
    [a (cs) (category-sys-object/c cs)]
    [b (cs) (category-sys-object/c cs)]
    [c (cs) (category-sys-object/c cs)]
    [ab (cs a b) (category-sys-morphism/c cs a b)]
    [bc (cs b c) (category-sys-morphism/c cs b c)])
  [_ (cs a c) (category-sys-morphism/c cs a c)])

Given implementations for category-sys-object-set-sys, category-sys-morphism-set-sys, category-sys-object-identity-morphism, and category-sys-morphism-chain-two, returns something a struct can use to implement the prop:category-sys interface.

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

(#:for-all
  cs category-sys?
  a (category-sys-object/c cs)
  b (category-sys-object/c cs)
  ab (category-sys-morphism/c cs a b)

  (#:should-be-equal
    (morphism-chain-two cs a a b
      (object-identity-morphism cs a)
      ab)
    ab))

(#:for-all
  cs category-sys?
  a (category-sys-object/c cs)
  b (category-sys-object/c cs)
  ab (category-sys-morphism/c cs a b)

  (#:should-be-equal
    (morphism-chain-two cs a b b
      ab
      (object-identity-morphism cs b))
    ab))

(#:for-all
  cs category-sys?
  a (category-sys-object/c cs)
  b (category-sys-object/c cs)
  c (category-sys-object/c cs)
  d (category-sys-object/c cs)
  ab (category-sys-morphism/c cs a b)
  bc (category-sys-morphism/c cs b c)
  cd (category-sys-morphism/c cs c d)

  (#:should-be-equal
    (morphism-chain-two cs a c d
      (morphism-chain-two cs a b c ab bc)
      cd)
    (morphism-chain-two cs a b d
      ab
      (morphism-chain-two cs b c d bc cd))))

procedure
(functor-sys? v) → boolean?
v : any/c
procedure
(functor-sys-impl? v) → boolean?
v : any/c
value
prop:functor-sys : (struct-type-property/c functor-sys-impl?)

Structure type property operations for functors, structure-preserving transformations of objects and morphisms from a source category to a target category.

procedure
(functor-sys-source fs) → category-sys?
fs : functor-sys?

Returns a functor’s source category.

procedure
(functor-sys-replace-source fs new-s) → functor-sys?
fs : functor-sys?
new-s : category-sys?

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.

procedure
(functor-sys-target fs) → category-sys?
fs : functor-sys?

Returns a functor’s target category.

procedure
(functor-sys-replace-target fs new-t) → functor-sys?
fs : functor-sys?
new-t : category-sys?

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.

procedure
(functor-sys-apply-to-object fs object)
→ (category-sys-object/c (functor-sys-target fs))
fs : functor-sys?
object : (category-sys-object/c (functor-sys-source fs))

Transforms an object according to the given functor.

procedure
(functor-sys-apply-to-morphism fs a b ab)
→
(category-sys-morphism/c (functor-sys-target fs)
  (functor-sys-apply-to-object fs a)
  (functor-sys-apply-to-object fs b))
  fs : functor-sys?
  a : (category-sys-object/c (functor-sys-source fs))
  b : (category-sys-object/c (functor-sys-source fs))
  ab : (category-sys-morphism/c (functor-sys-source fs) a b)

Uses the given functor to transform a morphism that originally goes from the given source object a to the given target object b.

procedure
(make-functor-sys-impl-from-apply source
replace-source
target
replace-target
apply-to-object
apply-to-morphism)
→ functor-sys-impl?
  source : (-> functor-sys? category-sys?)
  replace-source : (-> functor-sys? category-sys? functor-sys?)
  target : (-> functor-sys? category-sys?)
  replace-target : (-> functor-sys? category-sys? functor-sys?)
   apply-to-object :
(->i
  (
    [fs functor-sys?]
    [object (fs)
      (category-sys-object/c (functor-sys-source fs))])
  [_ (fs) (category-sys-object/c (functor-sys-target fs))])
   apply-to-morphism :
(->i
  (
    [fs functor-sys?]
    [a (fs) (category-sys-object/c (functor-sys-source fs))]
    [b (fs) (category-sys-object/c (functor-sys-source fs))]
    [morphism (fs a b)
      (category-sys-morphism/c (functor-sys-source fs) a b)])
  [_ (fs a b)
    (category-sys-morphism/c (functor-sys-target fs)
      (functor-sys-apply-to-object fs a)
      (functor-sys-apply-to-object fs b))])

Given implementations for the following methods, returns something a struct can use to implement the prop:functor-sys interface.

functor-sys-source
functor-sys-replace-source
functor-sys-target
functor-sys-replace-target
functor-sys-apply-to-object
functor-sys-apply-to-morphism

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

(#:for-all
  fs functor-sys?
  #:let s (functor-sys-source fs)
  #:let t (functor-sys-target fs)
  a (category-sys-object/c s)

  (#:should-be-equal
    (apply-to-morphism fs a a
      (category-sys-object-identity-morphism s a))
    (category-sys-object-identity-morphism t
      (apply-to-object fs a))))

(#:for-all
  fs functor-sys?
  #:let s (functor-sys-source fs)
  #:let t (functor-sys-target fs)
  a (category-sys-object/c s)
  b (category-sys-object/c s)
  c (category-sys-object/c s)
  ab (category-sys-morphism/c s a b)
  bc (category-sys-morphism/c s b c)

  (#:should-be-equal
    (apply-to-morphism fs a c
      (category-sys-morphism-chain-two s a b c ab bc))
    (category-sys-morphism-chain-two t
      (apply-to-object fs a)
      (apply-to-object fs b)
      (apply-to-object fs c)
      (apply-to-morphism fs a b ab)
      (apply-to-morphism fs b c bc))))

procedure
(functor-sys/c source/c target/c) → contract?
source/c : contract?
target/c : contract?

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.

procedure
(makeshift-functor-sys s
t
apply-to-object
apply-to-morphism)
→ (functor-sys/c (ok/c s) (ok/c t))
  s : category-sys?
  t : category-sys?
  apply-to-object : (-> (category-sys-object/c s) (category-sys-object/c t))
   apply-to-morphism :
(->i
  (
    [a (category-sys-object/c s)]
    [b (category-sys-object/c s)]
    [ab (a b) (category-sys-morphism/c s a b)])
  [_ (a b)
    (category-sys-morphism/c t
      (apply-to-object a)
      (apply-to-object b))])

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

(#:for-all
  a (category-sys-object/c s)

  (#:should-be-equal
    (apply-to-morphism a a
      (category-sys-object-identity-morphism s a))
    (category-sys-object-identity-morphism t
      (apply-to-object a))))

(#:for-all
  a (category-sys-object/c s)
  b (category-sys-object/c s)
  c (category-sys-object/c s)
  ab (category-sys-morphism/c s a b)
  bc (category-sys-morphism/c s b c)

  (#:should-be-equal
    (apply-to-morphism a c
      (category-sys-morphism-chain-two s a b c ab bc))
    (category-sys-morphism-chain-two t
      (apply-to-object a)
      (apply-to-object b)
      (apply-to-object c)
      (apply-to-morphism a b ab)
      (apply-to-morphism b c bc))))

procedure
(functor-sys-identity endpoint)
→ (functor-sys/c (ok/c endpoint) (ok/c endpoint))
endpoint : category-sys?

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.

procedure
(functor-sys-chain-two ab bc)
→
(functor-sys/c
  (ok/c (functor-sys-source ab))
  (ok/c (functor-sys-target bc)))
  ab : functor-sys?
  bc : (functor-sys/c (ok/c (functor-sys-target ab)) any/c)

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.

procedure
(natural-transformation-sys? v) → boolean?
v : any/c
procedure
(natural-transformation-sys-impl? v) → boolean?
v : any/c
value
prop:natural-transformation-sys
: (struct-type-property/c natural-transformation-sys-impl?)

Structure type property operations for natural transformations, transformations of morphisms that relate a source functor (functor-sys?) to a target functor.

procedure
(natural-transformation-sys-endpoint-source nts)
→ category-sys?
nts : natural-transformation-sys?

Returns a natural transformation’s endpoint functors’ source category.

procedure
(natural-transformation-sys-replace-endpoint-source nts
new-es)
→ natural-transformation-sys?
nts : natural-transformation-sys?
new-es : category-sys?

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.

procedure
(natural-transformation-sys-endpoint-target nts)
→ category-sys?
nts : natural-transformation-sys?

Returns a natural transformation’s endpoint functors’ target category.

procedure
(natural-transformation-sys-replace-endpoint-target nts
new-et)
→ natural-transformation-sys?
nts : natural-transformation-sys?
new-et : category-sys?

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.

procedure
(natural-transformation-sys-endpoint/c nts) → flat-contract?
nts : natural-transformation-sys?

Returns a flat contract that recognizes any functor that goes from the natural transformation’s endpoint functors’ source category to their target category.

procedure
(natural-transformation-sys-source nts)
→ (natural-transformation-sys-endpoint/c nts)
nts : natural-transformation-sys?

Returns a natural transformation’s source functor.

procedure
(natural-transformation-sys-replace-source nts
new-s)
→ natural-transformation-sys?
nts : natural-transformation-sys?
new-s : (natural-transformation-sys-endpoint/c nts)

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.

procedure
(natural-transformation-sys-target nts)
→ (natural-transformation-sys-endpoint/c nts)
nts : natural-transformation-sys?

Returns a natural transformation’s target functor.

procedure
(natural-transformation-sys-replace-target nts
new-t)
→ natural-transformation-sys?
nts : natural-transformation-sys?
new-t : (natural-transformation-sys-endpoint/c nts)

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.

procedure
(natural-transformation-sys-apply-to-morphism nts
a
b
ab)
→
(category-sys-morphism/c
  (natural-transformation-sys-endpoint-target nts)
  (functor-sys-apply-to-object
    (natural-transformation-sys-source nts)
    a)
  (functor-sys-apply-to-object
    (natural-transformation-sys-target nts)
    b))
  nts : natural-transformation-sys?
   a :
(category-sys-object/c
  (natural-transformation-sys-endpoint-source nts))
   b :
(category-sys-object/c
  (natural-transformation-sys-endpoint-source nts))
   ab :
(category-sys-morphism/c
  (natural-transformation-sys-endpoint-source nts)
  a
  b)

Uses the given natural transformation to transform a morphism that originally goes from the given source object a to the given target object b.

procedure
(make-natural-transformation-sys-impl-from-apply
endpoint-source
replace-endpoint-source
endpoint-target
replace-endpoint-target
source
replace-source
target
replace-target
apply-to-morphism)
→ natural-transformation-sys-impl?
  endpoint-source : (-> natural-transformation-sys? category-sys?)
   replace-endpoint-source :
(-> natural-transformation-sys? category-sys?
  natural-transformation-sys?)
  endpoint-target : (-> natural-transformation-sys? category-sys?)
   replace-endpoint-target :
(-> natural-transformation-sys? category-sys?
  natural-transformation-sys?)
   source :
(->i ([nts natural-transformation-sys?])
  [_ (nts) (natural-transformation-sys-endpoint/c nts)])
   replace-source :
(->i
  (
    [nts natural-transformation-sys?]
    [s (nts) (natural-transformation-sys-endpoint/c nts)])
  [_ natural-transformation-sys?])
   target :
(->i ([nts natural-transformation-sys?])
  [_ (nts) (natural-transformation-sys-endpoint/c nts)])
   replace-target :
(->i
  (
    [nts natural-transformation-sys?]
    [s (nts) (natural-transformation-sys-endpoint/c nts)])
  [_ natural-transformation-sys?])
   apply-to-morphism :
(->i
  (
    [nts natural-transformation-sys?]
    [a (nts)
      (category-sys-object/c
        (natural-transformation-sys-endpoint-source nts))]
    [b (nts)
      (category-sys-object/c
        (natural-transformation-sys-endpoint-source nts))]
    [ab (nts a b)
      (category-sys-morphism/c
        (natural-transformation-sys-endpoint-source nts)
        a
        b)])
  [_ (nts a b ab)
    (category-sys-morphism/c
      (natural-transformation-sys-endpoint-target nts)
      (functor-sys-apply-to-object
        (natural-transformation-sys-source nts)
        a)
      (functor-sys-apply-to-object
        (natural-transformation-sys-target nts)
        b))])

Given implementations for the following methods, returns something a struct can use to implement the prop:natural-transformation-sys interface.

natural-transformation-sys-endpoint-source
natural-transformation-sys-replace-endpoint-source
natural-transformation-sys-endpoint-target
natural-transformation-sys-replace-endpoint-target
natural-transformation-sys-source
natural-transformation-sys-replace-source
natural-transformation-sys-target
natural-transformation-sys-replace-target
natural-transformation-sys-apply-to-morphism

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

(#:for-all
  nts natural-transformation-sys?
  #:let es (natural-transformation-sys-endpoint-source nts)
  #:let et (natural-transformation-sys-endpoint-target nts)
  #:let s (natural-transformation-sys-source nts)
  #:let t (natural-transformation-sys-target nts)
  a (category-sys-object/c es)
  b (category-sys-object/c es)
  c (category-sys-object/c es)
  ab (category-sys-morphism/c es a b)
  bc (category-sys-morphism/c es b c)

  (#:should-be-equal
    (apply-to-morphism nts a c
      (category-sys-morphism-chain-two es a b c ab bc))
    (category-sys-morphism-chain-two t
      (functor-sys-apply-to-object s a)
      (functor-sys-apply-to-object s b)
      (functor-sys-apply-to-object t c)
      (functor-sys-apply-to-morphism s a b ab)
      (apply-to-morphism nts b c bc)))

  (#:should-be-equal
    (apply-to-morphism nts a c
      (category-sys-morphism-chain-two es a b c ab bc))
    (category-sys-morphism-chain-two t
      (functor-sys-apply-to-object s a)
      (functor-sys-apply-to-object t b)
      (functor-sys-apply-to-object t c)
      (apply-to-morphism nts a b ab)
      (functor-sys-apply-to-morphism t b c bc))))

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

procedure
(natural-transformation-sys/c endpoint-source/c
endpoint-target/c
source/c
target/c) → contract?
  endpoint-source/c : contract?
  endpoint-target/c : contract?
  source/c : contract?
  target/c : contract?

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.

procedure
(makeshift-natural-transformation-sys es
et
s
t
apply-to-morphism)
→ (natural-transformation-sys/c (ok/c es) (ok/c et) (ok/c s) (ok/c t))
  es : category-sys?
  et : category-sys?
  s : (functor-sys/c (ok/c es) (ok/c et))
  t : (functor-sys/c (ok/c es) (ok/c et))
   apply-to-morphism :
(->i
  (
    [a (category-sys-object/c es)]
    [b (category-sys-object/c es)]
    [ab (a b) (category-sys-morphism/c es a b)])
  [_ (a b ab)
    (category-sys-morphism/c et
      (functor-sys-apply-to-object s a)
      (functor-sys-apply-to-object t b))])

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-all
  a (category-sys-object/c es)
  b (category-sys-object/c es)
  c (category-sys-object/c es)
  ab (category-sys-morphism/c es a b)
  bc (category-sys-morphism/c es b c)

  (#:should-be-equal
    (apply-to-morphism a c
      (category-sys-morphism-chain-two es a b c ab bc))
    (category-sys-morphism-chain-two t
      (functor-sys-apply-to-object s a)
      (functor-sys-apply-to-object s b)
      (functor-sys-apply-to-object t c)
      (functor-sys-apply-to-morphism s a b ab)
      (apply-to-morphism b c bc)))

  (#:should-be-equal
    (apply-to-morphism a c
      (category-sys-morphism-chain-two es a b c ab bc))
    (category-sys-morphism-chain-two t
      (functor-sys-apply-to-object s a)
      (functor-sys-apply-to-object t b)
      (functor-sys-apply-to-object t c)
      (apply-to-morphism a b ab)
      (functor-sys-apply-to-morphism t b c bc))))

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.

procedure
(natural-transformation-sys-identity endpoint)
→
(natural-transformation-sys/c
  (ok/c (functor-sys-source endpoint))
  (ok/c (functor-sys-target endpoint))
  (ok/c endpoint)
  (ok/c endpoint))
  endpoint : functor-sys?

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.

procedure
(natural-transformation-sys-chain-two ab
bc)
→
(natural-transformation-sys/c
  (ok/c (natural-transformation-sys-endpoint-source ab))
  (ok/c (natural-transformation-sys-endpoint-target ab))
  (ok/c (natural-transformation-sys-source ab))
  (ok/c (natural-transformation-sys-target bc)))
  ab : natural-transformation-sys?
   bc :
(natural-transformation-sys/c
  (ok/c (natural-transformation-sys-endpoint-source ab))
  (ok/c (natural-transformation-sys-endpoint-target ab))
  (ok/c (natural-transformation-sys-target ab))
  any/c)

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.

procedure
(natural-transformation-sys-chain-two-along-end ab
bc)
→
(natural-transformation-sys/c
  (ok/c (natural-transformation-sys-endpoint-source ab))
  (ok/c (natural-transformation-sys-endpoint-target bc))
  (ok/c
    (functor-sys-chain-two
      (natural-transformation-sys-source ab)
      (natural-transformation-sys-source bc)))
  (ok/c
    (functor-sys-chain-two
      (natural-transformation-sys-target ab)
      (natural-transformation-sys-target bc))))
  ab : natural-transformation-sys?
   bc :
(natural-transformation-sys/c
  (ok/c (natural-transformation-sys-endpoint-target ab))
  any/c
  any/c
  any/c)

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.