3.1 Dimension Systems🔗ℹ

3.1.1 Dimension Systems in General🔗ℹ

The maximum of zero dimension numbers is well-defined; it’s the least dimension number of the dimension system. Typically this is 0, representing the dimension of 0-dimensional shapes. We recommend to use dim-sys-dim-zero in that case for better clarity of intent.

This is equivalent to calling dim-sys-dim-max without passing in any dimension numbers. We provide this alternative for better clarity of intent.

This is equivalent to calling dim-sys-dim-max without exactly two dimension numbers. We provide this alternative to clarify how make-dim-sys-impl-from-max-of-two works. It may also be good for catching errors.

The given method implementations should observe some algebraic laws. Namely, the dim=? operation should be a decision procedure for equality of dimension numbers, and the dim-max-of-two operation should be associative, commutative, and idempotent with dim-zero as its identity element.

3.1.2 Category-Theoretic Dimension System Manipulations🔗ℹ

• dim-sys-morphism-sys-source

• dim-sys-morphism-sys-replace-source

• dim-sys-morphism-sys-target

• dim-sys-morphism-sys-replace-target

• dim-sys-morphism-sys-morph-dim

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 dim-sys-morphism-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 implementation (dim-sys-morphism-sys-morph-dim) should observe some algebraic laws. Namely, it should preserve the relatedness of dimension numbers by the dim-sys-dim=? and dim-sys-dim-max operations (not to mention operations like dim-sys-dim-zero, which are derived from those). In more symbolic terms (using a pseudocode DSL):

(#:for-all

ms dim-sys-morphism-sys?

#:let s (dim-sys-morphism-sys-source ms)

#:let t (dim-sys-morphism-sys-target ms)

(#:should-be-equal

(morph-dim ms (dim-sys-dim-zero s))

(dim-sys-dim-zero t)))

(#:for-all

ms dim-sys-morphism-sys?

#:let s (dim-sys-morphism-sys-source ms)

#:let t (dim-sys-morphism-sys-target ms)

a (dim-sys-dim/c s)

b (dim-sys-dim/c s)

(#:should-be-equal

(morph-dim ms (dim-sys-dim-max s a b))

(dim-sys-dim-max t

(morph-dim ms a)

(morph-dim ms b))))

(#:for-all

ms dim-sys-morphism-sys?

#:let s (dim-sys-morphism-sys-source ms)

#:let t (dim-sys-morphism-sys-target ms)

a (dim-sys-dim/c s)

b (dim-sys-dim/c s)

(#:should-be-equal

(dim-sys-dim=? s  a b)

(dim-sys-dim=? t (morph-dim ms a) (morph-dim ms b))))

The result is a flat contract as long as the given contracts are flat.

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 transformation. Composition is often written with its arguments the other way around (e.g. in Racket’s compose operation).

Every two dim-sys-category-sys values are equal?. One such value is always an ok/c match for another.

This is equivalent to (functor-sys-apply-to-morphism fs (dim-sys-morphism-sys-source dsms) (dim-sys-morphism-sys-target dsms) dsms).

This is equivalent to (natural-transformation-sys-apply-to-morphism fs (dim-sys-morphism-sys-source dsms) (dim-sys-morphism-sys-target dsms) dsms).

• functor-sys-apply-to-object

• functor-sys-apply-to-morphism

These method implementations should observe the same algebraic laws as those required by make-functor-sys-impl-from-apply.

This is essentially a shorthand for calling make-functor-sys-impl-from-apply and supplying the appropriate source- and target-determining method implementations.

3.1.3 Commonly Used Dimension Systems🔗ℹ

The dim-sys-dim/c of a nat-dim-sys is a flat contract.

Every two nat-dim-sys values are equal?. One such value is always an ok/c match for another.

Two extended-with-top-dim-finite values are equal? if they contain equal? elements.

Every two extended-with-top-dim-infinite values are equal?.

The resulting contract has the same contract obstinacy as the given one.

If the given function is not the decision procedure of a decidable equivalence relation, then neither is this one. In that case, this one merely relates two finite dimension numbers if they would be related by original-dim=? in the unextended dimension system.

The resulting dimension system’s dim-sys-dim-max operation corresponds with the original operation on the extended-with-top-dim-finite? dimension numbers, and it treats the extended-with-top-dim-infinite? dimension number as being greater than the rest.

Two extended-with-top-dim-sys values are equal? if they contain equal? elements. One such value is an ok/c match for another if the first’s element is ok/c for the second’s.

Two extended-with-top-dim-sys-morphism-sys values are equal? if they contain equal? elements. One such value is an ok/c match for another if the first’s element is ok/c for the second’s.

Every two extended-with-top-dim-sys-morphism-sys values are equal?. One such value is always an ok/c match for another.

Two extend-with-top-dim-sys-morphism-sys values are equal? if they contain equal? elements. One such value is an ok/c match for another if the first’s element is ok/c for the second’s.

This is primarily used as the source of unextend-with-top-dim-sys, which otherwise would have to have an error-handling case if it encountered the extended-with-top-dim-infinite value. (TODO: Consider passing an error handler to unextend-with-top-dim-sys-morphism-sys. Perhaps that would be a better approach than this, since we would be encouraged to write errors where the error messages make the most sense, not rely indirectly on the error messages of the contracts of the behaviors we invoke. On the other hand, perhaps that error-handling should take place in a morphism (or natural transformation) from extended-with-top-dim-sys to extended-with-top-finite-dim-sys.)

Two extended-with-top-finite-dim-sys values are equal? if they contain equal? elements. One such value is an ok/c match for another if the first’s element is ok/c for the second’s.

Note that the source is an extended-with-top-finite-dim-sys? value, not an extended-with-top-dim-sys? value, so this operation can’t encounter a extended-with-top-dim-infinite value and get stuck.

Two extend-with-top-dim-sys-morphism-sys values are equal? if they contain equal? elements. One such value is an ok/c match for another if the first’s element is ok/c for the second’s.