Post #1815119

2026-04-26 21:07 UTC

Something it took me many years to appreciate is this: a lot of constructions in algebra can be interpreted as figuring out what you can precompute when you&#39;re not sure what&#39;s coming next. The first example I was taught may have been the free group on some generators. You&#39;re basically saying &quot;well I don&#39;t know how to multiply these things so I&#39;ll just record whatever I need now so when I do learn how to multiply elements I&#39;ve already done as much work as possible&quot;. Sometimes there&#39;s even a kind of cost model. As I&#39;ve mentioned before, a tensor product is basically what you need to store from x and y when you know that at some point in the future you&#39;re going to compute many bilinear functions f(x,y), but you don&#39;t know what f actually is, arbitrary multiplication is expensive, but memory is cheap along with addition and multiplication by a constant. In a sense everything I said here is wrong. For example in mathematics you have considerable freedom to choose what sets actually represent a tensor product so it makes no sense to identify a construction with a particular &quot;implementation&quot;. Nonetheless the definition of the tensor product corresponds well to the sort of interface you might attach to an obvious precomputation for the bilinear function scenario. (I think this is basically summarising what a Left Kan extension is.)

Replies (6)

@sjb@mstdn.io 2026-04-26 21:18

@dpiponi@mathstodon.xyz Algebra is based on unknowns: e.g. x being a variable instead of writing 3. These examples are what happens when multiplication operator is an "unknown", and when a bilinear function is an unknown. They're just more complex unknowns.

Open ##2346185
@iblech@mathstodon.xyz 2026-04-27 05:44

@dpiponi@mathstodon.xyz Very nice point of view! Also neatly visible in the construction of the free functor on a type constructor t :: Type → Type: data FreeF t a = MkFreeF (exists r. (t r, r → a)) A value of type FreeF t a consists of a type r, a value x :: t r and a function f :: r → a. We're recording which function r → a we'd like to apply to x via functorial lift at some point in the future, once we have a map from t to an actual functor.

Open ##2346189
@ohad@mathstodon.xyz 2026-04-27 06:51

@dpiponi@mathstodon.xyz Yup, I'm planning to pursue this perspective in my short course Algebra and Normalisation at this year's Scottish Proframming Languages and Verification summer school in Glasgow https://spli.scot/splv/2026-glasgow/ This is also the perspective we take in the various frex papers and abstracts (ICFP18, PEPM20+23, ICFP25).

Open ##2346190
@theohonohan@graphics.social 2026-04-27 07:54

@dpiponi@mathstodon.xyz it's funny, i thought of Kan extensions when reading the first part of this. My understanding/example is that in a "tech tree" setting where morphisms describe which technologies depend on which, and everything maps to its year of invention, a left Kan extension to some new set of inventions will take a limit of the new invention's dependencies – which might look like a product (the set of years in which the prerequisites were invented), or the max of the dates if they're ordered.

Open ##2346193
@mjd@mathstodon.xyz 2026-04-27 08:27

@dpiponi@mathstodon.xyz This reminds me of the observation that there's a representation of numeric quantities that can perform both addition and multiplication of numbers in constant time, but it's useless for numeric calculation because there's no corresponding algorithm for the ≤ relation. (The representation being expression trees with numbers at the leaves.)

Open ##2346194
@mjd@mathstodon.xyz 2026-04-27 16:02

@dpiponi@mathstodon.xyz This also fits in well with nebulous ideas I've had about the fundamental purpose of mathematical notation in general. Often we solve problems by writing an expression and then transforming it into a different expression. To take the first example that comes to mind, consider \[ \sum_{i=1}^n = \frac{n^2+n}2 \] And this is interesting because, as you put it, it has precomputed as much as possible when n is still unknown.

Open ##2346198