/reading

Programming

Parsing

Need to make the parsing stuff I have work on streams of arbitrary tokens rather than just strings (hopefully making it more efficient in the process). Related reading:

I want to be able to associate recursive ADTs with recursive regexen for simple parsing of context free grammars. Here's some relevant resources:

Parallelism

Continuations, monads, continuation monads

Bidirectional programming, optics

Testing

Recursion (schemes)

Zippers

Performance

Metaprogramming

Lisp

Extensible effects

Free(r) monad

Stuff I've played around with so far:

Monad transformers

Higher order effects

What is the theoretical underpinning of the polysemy extensible effects library? My suspicion is that it is a free functor of some kind, probably the free functor from the category of monad transformers to the category of monads.

To answer the question rigorously, I need to do some reading:

Refactoring

Compilation

Fun concepts

Backwards programming

It's fun to program with products:

assoc :: ((x, y), z) -> (x, (y, z))
assoc ((x, y), z) = (x, (y, z))

You can receive everything and throw things away that you don't care about.

It's a little bit tedious to program with coproducts:

assocE :: Either (Either x y) z -> Either x (Either y z)
assocE (Left (Left x)) = Left x
assocE (Left (Right y)) = Right $ Left y
assocE (Right z) = Right $ Right z

You receive things one case at a time, you can't just ignore cases you don't care about.

I suspect that this has something to do with the fact that Hask is cartesian closed, and the product tensor is (,). But of course Hask has a dual, and in the dual category, it's Either that's the product. So maybe if we had some notion of "backwards" pattern matching, it would be fun to use it for coproducts and tedious for products!

After some discussion and googling, I found some promising links:

Probabilistic programming

Type systems

Are ADTs an essential primitive of a sufficiently expressive dependent type system? Based on how things work out computationally in untyped JS, it would be really nice if the answer was "no". Here are some links that seem to provide promising evidence for that hypothesis:

Books

Module systems

Typeclasses (and how to avoid their use because they SUCK)

Curry-Howard correspondence

ADTs

Dependently typed programming

The singletons saga

Containers

I have this big stack of concepts I'm trying to work through at the moment that goes like this:

  • There is this notion of operad with sets of variadic operations, but with no restrictions on how the operations may be composed (hence sets and not categories)
  • I wish to generalize this along two dimensions: I want to describe the arity of a set of operations by a set of input labels instead of a mere natural number, and I want a partial composition operation such that the valid precompositions for a given operation are restricted
  • There is this concept of a "colored operad" (aka multicategory), in which we solve the second problem: there is this set of "colors", and the family of operation sets is no longer indexed by a natural number, but instead by lists of colors. Further, composition is restricted so that "output colors" and "input colors" line up.
  • Now to go beyond lists and to maps (and maybe to other containers), we need some systematic way of abstracting the relationship between lists and natural numbers to maps and strings
  • The theory of "containers" in dependently typed programming elaborates on this relationship between a set of "shapes", each of which corresponds to a set of positions in a container (for lists the set of shapes corresponds to the natural numbers).

Here's some relevant reading:

Linear types

Devops

Nix

Math

Category Theory

Coalgebraic descriptions of systems (state machines)

The theory of "systems" with dynamic behavior is apparently well modeled coalgebraically. So for example a Moore machine is a coalgebra of the signature functor ``, where the carrier represents the state. The terminal coalgebra this unfolds to represents the behavior of the system.

Operads

Monoidal functors

Need to find some information about things that are between lax and strong monoidal functors: the coherence map for the opposite functor is a retraction/section for the coherence map of the functor, but they do not form a full isomorphism. Some promising search results:

There's also some stuff about the interaction of applicatives and alternatives with monads (i.e. the functor composition monoidal structure) a lot of it by Mauro Jaskellioff:

Enrichment

My understanding of enrichment still needs a lot of work. I think a good path forward is to study:

  1. A 2-categories companion (some kind of course material explaining 2-categories and bicategories)
  2. Basic Bicategories (to understand the concept of a bicategory, a weakening of the definition of a 2-category)
  3. ??? (maybe try and represent some monoids objects not in (,) as enriched single object categories, and study how monoidal functors interact with them)

Relationship between (co)monads and monoidal structures

Almost everything by Tarmo Uustalu is relevant, esp. as relates to comonads

Brendan Fong

Traced, compact (bi)categories

Retry logic, quantales, lattices

  • I was looking at the retry library we use at work and I suspect that it can be radically simplified by equipping the (roughly) data RetryAction = NoRetry | RetryASAP | RetryIn Int data structure with a monoid data structure.
    • Andre Joyal's recent presentation on polynomial functors at the Topos Institute stream thing had a slide that got me interested in quantales. Specifically, RetryAction might represent a quantale, if we interpret RetryIn Int to be denoting the subset of the real line that is smaller than the specified upper bound. We can freely adjoin whatever monoid we want on Int so long as it distributes over the join.
    • Handy paper about using quantales to model "resource theories" (examples of resources modeled are very close to the exhaustible retry-tolerance we wish to model): Quantitative Foundations for Resource Theories
  • Quantales, Observational Logic and Process Semantics
  • Whitman's solution to the word problem (for lattices, relevant for talking about the free lattice)
  • Free Lattices

Databases

Polynomial functors, monads (stuff from this is also scattered about elsewhere)

Logic

Ehrenfeucht–Fraïssé games

Computability

Geometry

Collision detection

I suspect that finding collisions between shapes (or convex hulls of shapes) has something to do with a lattice of shapes under inclusion as binary relation, intersection as meet, union as join.

The approach I was considering was to only admit circular subsets of points from a given canvas. Then the meet operation and join operation consists of picking a circle inscribed in the intersection of the two provided circles, and a circle just barely enclosing the two provided circles, respectively. Apparently the latter is a "closure operator", which taking convex hulls is also. The operation of taking the convex hull of the superposition of the provided shapes, when taken as the join operation, actually forms a proper join-semilattice. So maybe this wrapping circle business (or an adjustment of it) does too? Someone pointed out there might be problems with associativity.

Anyway here's a paper about closure operators and lattices:

Vector algebra

I want to render a game of life in toroidal coordinates on an actual torus. I started implementing my own vector algebra library using some generalized n-dimensional vector math stuff, but then became intrigued by what the generalization of the cross product to n-dimensions would be. Turns out this is called the Hodge Star operator. In the course of learning about this, I discovered a rabbithole of interesting things to read:

Stuff I've played around with so far:

Graphs

I want to build a 3D git repo visualizer. Need to learn more about graph/tree layout algorithms esp in 3D:

Topology

@monoidmusician suggested https://mathoverflow.net/questions/19152/why-is-a-topology-made-up-of-open-sets as an entrypoint into topology stuff.

Polyomino theory

I suspect that polyominos form a kind of colored operad. Specifically, the colors represent the "contour" of a polyomino-with-holes, and a morphism from a list of contours to a contour is a placement of the input contours such that they respect the boundaries of the output contour and do not overlap. Thus roughly speaking we can think of a multimorphism as a "tiling" of the output polyomino with the input polyominos.

Some fast and loose thinking shows that this appears to be:

  • closed: given a valid tiling of a polyomino, and a valid tiling of each tile, there exists an obviously valid composition (i.e. that respects the contour of the outermost polyomino and avoids overlaps). the composition is roughly given by just deleting the contours of the intermediate tiles polyominos.
  • unital: any polyomino contour P can simply be "tiled" with a single polyomino that occupies its entire surface. this is obviously a valid tiling, has domain [P] and codomain P. when postcomposed with any other tiling, it has no effect. when repeated to fill a list and precomposed with any other tiling, it also has no effect.
  • associative: given a "three level" tiling of a polyomino, it does not matter in what order we forget about the two intermediate levels of contours.

Somewhat interestingly, no discussions appear to have occured on the category theory zulip about polyominos, and nlab also appears to be silent on the subject. Polyominos in general appear to be quite sparsely studied, and in particular their intersection with category theory appears to be completely unstudied.

EDIT: What I might be missing is that this is somehow equivalent to the little disks operad or some other operad of topological embeddings (although AFAIU topology isn't very interested in preventing continuous deformations, which we don't want here)?

"Tilings" seem to have some interesting intersections with dynamic systems (which I'm currently studying from a coalgebraic perspective as part of my work on the cofree-bot stuff) and with algebraic topology and group theory. See for example:

Also need to read more about self-avoiding walks, which are basically the contours of interest.

Some stuff on taxicab geometry that might generally be of use:

Power words: discrete geometry, algebraic topology, polytopes, packing, tiling, covering, incidence structure

Music

Misc. blogs