3.1 Dimension Systems
(require punctaffy/hypersnippet/dim) | |
package: punctaffy-lib |
3.1.1 Dimension Systems in General
procedure
v : any/c
procedure
(dim-sys-impl? v) → boolean?
v : any/c
value
procedure
(dim-sys-dim/c ds) → flat-contract?
ds : dim-sys?
procedure
(dim-sys-dim-max ds arg ...) → (dim-sys-dim/c ds)
ds : dim-sys? arg : (dim-sys-dim/c ds)
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.
procedure
(dim-sys-dim-zero ds) → (dim-sys-dim/c ds)
ds : dim-sys?
This is equivalent to calling dim-sys-dim-max without passing in any dimension numbers. We provide this alternative for better clarity of intent.
procedure
(dim-sys-dim-max-of-two ds a b) → (dim-sys-dim/c ds)
ds : dim-sys? a : (dim-sys-dim/c ds) b : (dim-sys-dim/c ds)
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.
procedure
(dim-sys-dim<? ds a b) → boolean?
ds : dim-sys? a : (dim-sys-dim/c ds) b : (dim-sys-dim/c ds)
procedure
(dim-sys-dim<=? ds a b) → boolean?
ds : dim-sys? a : (dim-sys-dim/c ds) b : (dim-sys-dim/c ds)
procedure
(dim-sys-dim=? ds a b) → boolean?
ds : dim-sys? a : (dim-sys-dim/c ds) b : (dim-sys-dim/c ds)
procedure
(dim-sys-dim=0? ds d) → boolean?
ds : dim-sys? d : (dim-sys-dim/c ds)
procedure
(dim-sys-dim</c ds bound) → flat-contract?
ds : dim-sys? bound : (dim-sys-dim/c ds)
procedure
(dim-sys-dim=/c ds bound) → flat-contract?
ds : dim-sys? bound : (dim-sys-dim/c ds)
procedure
(dim-sys-0<dim/c ds) → flat-contract?
ds : dim-sys?
procedure
(make-dim-sys-impl-from-max-of-two dim/c dim=? dim-zero dim-max-of-two) → dim-sys-impl? dim/c : (-> dim-sys? flat-contract?)
dim=? :
(->i ( [ds dim-sys?] [a (ds) (dim-sys-dim/c ds)] [b (ds) (dim-sys-dim/c ds)]) [_ boolean?]) dim-zero : (->i ([ds dim-sys?]) [_ (ds) (dim-sys-dim/c ds)])
dim-max-of-two :
(->i ( [ds dim-sys?] [a (ds) (dim-sys-dim/c ds)] [b (ds) (dim-sys-dim/c ds)]) [_ (ds) (dim-sys-dim/c ds)])
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
procedure
v : any/c
procedure
v : any/c
value
: (struct-type-property/c dim-sys-morphism-sys-impl?)
procedure
(dim-sys-morphism-sys-source dsms) → dim-sys?
dsms : dim-sys-morphism-sys?
procedure
(dim-sys-morphism-sys-replace-source dsms new-s) → dim-sys-morphism-sys? dsms : dim-sys-morphism-sys? new-s : dim-sys?
procedure
(dim-sys-morphism-sys-target dsms) → dim-sys?
dsms : dim-sys-morphism-sys?
procedure
(dim-sys-morphism-sys-replace-target dsms new-s) → dim-sys-morphism-sys? dsms : dim-sys-morphism-sys? new-s : dim-sys?
procedure
→ (dim-sys-dim/c (dim-sys-morphism-sys-target ms)) ms : dim-sys-morphism-sys? d : (dim-sys-dim/c (dim-sys-morphism-sys-source ms))
procedure
(make-dim-sys-morphism-sys-impl-from-morph source replace-source target replace-target morph-dim) → dim-sys-morphism-sys-impl? source : (-> dim-sys-morphism-sys? dim-sys?) replace-source : (-> dim-sys-morphism-sys? dim-sys? dim-sys-morphism-sys?) target : (-> dim-sys-morphism-sys? dim-sys?) replace-target : (-> dim-sys-morphism-sys? dim-sys? dim-sys-morphism-sys?)
morph-dim :
(->i ( [ms dim-sys-morphism-sys?] [object (ms) (dim-sys-dim/c (dim-sys-morphism-sys-source ms))]) [_ (ms) (dim-sys-dim/c (dim-sys-morphism-sys-target ms))])
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))))
procedure
(dim-sys-morphism-sys/c source/c target/c) → contract?
source/c : contract? target/c : contract?
The result is a flat contract as long as the given contracts are flat.
procedure
(dim-sys-morphism-sys-identity endpoint)
→ (dim-sys-morphism-sys/c (ok/c endpoint) (ok/c endpoint)) endpoint : dim-sys?
procedure
(dim-sys-morphism-sys-chain-two ab bc)
→
(dim-sys-morphism-sys/c (ok/c (dim-sys-morphism-sys-source ab)) (ok/c (dim-sys-morphism-sys-target bc))) ab : dim-sys-morphism-sys?
bc :
(dim-sys-morphism-sys/c (ok/c (dim-sys-morphism-sys-target ab)) any/c)
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).
syntax
syntax
match expander
procedure
v : any/c
Every two dim-sys-category-sys values are equal?. One such value is always an ok/c match for another.
procedure
(functor-from-dim-sys-sys-apply-to-morphism fs dsms)
→
(category-sys-morphism/c (functor-sys-target fs) (functor-sys-apply-to-object fs (dim-sys-morphism-sys-source dsms)) (functor-sys-apply-to-object fs (dim-sys-morphism-sys-target dsms))) fs : (functor-sys/c dim-sys-category-sys? any/c) dsms : dim-sys-morphism-sys?
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).
procedure
v : any/c
procedure
(make-dim-sys-endofunctor-sys-impl-from-apply apply-to-dim-sys apply-to-dim-sys-morphism-sys) → functor-sys-impl? apply-to-dim-sys : (-> dim-sys-endofunctor-sys? dim-sys? dim-sys?)
apply-to-dim-sys-morphism-sys :
(->i ( [es dim-sys-endofunctor-sys?] [ms dim-sys-morphism-sys?]) [_ (es ms) (dim-sys-morphism-sys/c (ok/c (functor-sys-apply-to-object es (dim-sys-morphism-sys-source ms))) (ok/c (functor-sys-apply-to-object es (dim-sys-morphism-sys-target ms))))])
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
syntax
syntax
match expander
procedure
(nat-dim-sys? v) → boolean?
v : any/c
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.
syntax
syntax
(extended-with-top-dim-finite original)
match expander
(extended-with-top-dim-finite original)
procedure
v : any/c
procedure
d : extended-with-top-dim-finite?
Two extended-with-top-dim-finite values are equal? if they contain equal? elements.
syntax
syntax
match expander
procedure
v : any/c
Every two extended-with-top-dim-infinite values are equal?.
procedure
v : any/c
procedure
(extended-with-top-dim/c original-dim/c) → contract?
original-dim/c : contract?
The resulting contract has the same contract obstinacy as the given one.
procedure
(extended-with-top-dim=? original-dim=? a b) → boolean?
original-dim=? : (-> any/c any/c boolean?) a : extended-with-top-dim? b : extended-with-top-dim?
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.
syntax
syntax
(extended-with-top-dim-sys original)
original : dim-sys?
match expander
(extended-with-top-dim-sys original)
procedure
v : any/c
procedure
ds : extended-with-top-dim-sys?
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.
syntax
syntax
(extended-with-top-dim-sys-morphism-sys original)
original : dim-sys-morphism-sys?
match expander
(extended-with-top-dim-sys-morphism-sys original)
procedure
v : any/c
procedure
→ dim-sys-morphism-sys? dsms : extended-with-top-dim-sys-morphism-sys?
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.
syntax
syntax
match expander
procedure
v : any/c
Every two extended-with-top-dim-sys-morphism-sys values are equal?. One such value is always an ok/c match for another.
syntax
syntax
(extend-with-top-dim-sys-morphism-sys source)
source : dim-sys?
match expander
(extend-with-top-dim-sys-morphism-sys source)
procedure
v : any/c
procedure
(extend-with-top-dim-sys-morphism-sys-source dsms) → dim-sys?
dsms : extend-with-top-dim-sys-morphism-sys?
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.
syntax
syntax
(extended-with-top-finite-dim-sys original)
original : dim-sys?
match expander
(extended-with-top-finite-dim-sys original)
procedure
v : any/c
procedure
ds : extended-with-top-dim-sys?
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.
syntax
syntax
target : dim-sys?
match expander
procedure
v : any/c
procedure
(unextend-with-top-dim-sys-morphism-sys-target dsms) → dim-sys?
dsms : extend-with-top-dim-sys-morphism-sys?
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.