Categorical programming with functorial strength
Dwight Spencer · 2020
This work demonstrates industrial-strength categorical programs can be computed applicatively using only a category's commutative diagrams for reduction. Categorical initial and final datatypes can be declared incrementally and parametrically in the Hagino-Wraith style to build the programmer's toolkit. These datatypes arrive bundled with structurally-natural constructive or destructive operators ready for programming purposes. Environmental is freely distributed throughout the computation (first-order functorial strength) to achieve expressiveness within a confluent terminating reduction system that obviates hard-to-manage exponential datatypes. Such data types are termed strong. These category-theoretical results arise within split fibrations and are lifted to a term logic (programming language) precisely consistent with this categorical construction. The initiality and finality universal properties for strong datatype construction within the split fibration setting generates a strongly normalizing weak-head categorical combinator reduction engine that distributes throughout data structure interiors. Both eager initial datatype usage and lazy final datatype usage permit coding of complex algorithms, such as indexed database access and Ackermann's function, by using context actions over strong datatypes dictated by programmer-specified state transformations over component datatypes.