Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: positions

Topic: Postdoc position in Chambéry

Tom Hirschowitz (Jun 20 2025 at 07:03):

Hi all,

The LAMA

https://lama.univ-smb.fr

offers a full-time, 18 month postdoc position starting September 2025. The deadline is really soon: July 3!

The details are here

https://univ-smb.nous-recrutons.fr/poste/vk06lqf5ee-chercheur-post-doctorant-fh-shine-guli/

and there

https://www.univ-smb.fr/wp-content/uploads/2025/06/offre-emploi-post-doct_2025_lama-shine-guli2-vf.pdf

but let me give a brief summary.

Most numerical simulation programs compute with very little checks for physical consistency. Typically, adding a length (in metres) to a force (in newtons) is not detected as an error by the programming language. But the very purpose of type systems is to detect inconsistencies of a similar nature. E.g., they prevent addition of numerical values with arrays. Until now, programming language theorists have proposed solutions that are conceptually clear, but too naive to cover all use cases. Typically, physicists sometimes need to use libraries written with different unit systems, in a compatible way. On the other hand, other attempts tried to handle numerous cases independently, but eventually came out as too complex to be usable.

The goal of the present postdoc position is to try and design a conceptually clear solution covering all use cases.

The successful applicant will be based at LAMA, and work with Pierre Hyvernat and me, but also with Vincent Reverdy (who is a numerical physicist and the Particle Physics Laboratory in Annecy).

Relevant skills for the position include: proof assistants, type theory, category theory, programming language theory, implementation of programming languages. It is definitely not necessary to possess all these skills to be successful.

Please don’t hesitate to contact me if you have any question!

John Baez (Jun 20 2025 at 07:45):

@Nathaniel Osgood has long wanted a solution to this problem, and currently together with @Evan Patterson and others we're contemplating one based on the concept of dimensional category.

Tom Hirschowitz (Jun 20 2025 at 11:36):

This looks really nice, thanks for sharing!

I'm probably not getting all the subtleties, though. Is it too early for you to explain how you can simulate physical systems based on these ideas?

Our current approach is very different, which is not surprising given our backgrounds: it's based on what may be called “self-refinement” systems, and combinations thereof. The idea is that your artifically introduce refinements of some types, e.g., of float, which model physical dimensions, together with typing rules that enforce consistency. It's at a very early stage, we've only started playing with the idea in rocq.

John Baez (Jun 20 2025 at 12:22):

Is it too early for you to explain how you can simulate physical systems based on these ideas?

There are lots of ways to simulate physical systems, of course; the only thing dimensional categories provide is a principled type system, or more precisely framework to describe type systems, for dealing with dimensions of all the physical quantities in your physical system. Instead of treating quantities as numbers, we treat them as morphisms in a dimensional category, where the objects are 'dimensions', like

$\text{temperature} \cdot \text{mass}^2 \cdot \text{energy}^{-1}$

John Baez (Jun 20 2025 at 12:24):

The multiplication here is the monoidal structure in the dimensional category, and we get to use negative exponents because all the objects in the dimensional category have inverses with respect to the tensor product.

John Baez (Jun 20 2025 at 12:34):

Technically a dimensional category is a $k$-enriched symmetric monoidal category where all objects are line objects, meaning objects $x$ that

1. have an inverse with respect to the tensor product: there's an object $y$ with $y \otimes x \cong I$
2. have trivial self-braiding: the symmetry $S_{x,x} : x \otimes x \to x \otimes x$ is the identity.

Point 2 is a bit subtle.

Long after James invented dimensional categories, I learned that Grothendieck's student Hoàng Xuân Sính had invented and studied them much earlier in her thesis, under the name Pic-categories. I summarized her work here. She was interested in them for the same reason Jim was: the category of line bundles over a variety (or scheme) is a dimensional category.

I can't emphasize too much: one doesn't need to know or care about algebraic geometry to use dimensional categories for keeping track of units in physical theories! But in the end there's a nice connection, sketched by Jim here: any dimensional category can be seen as a physical theory, and this has a moduli space of models, which is a scheme.

Tom Hirschowitz (Jun 20 2025 at 19:33):

Thanks for the explanation, that's helpful. My question was more about how you would encode the system's dynamics in this framework: how do you specify an initial state, and how do you read out a “next” state?

John Baez (Jun 20 2025 at 20:26):

The ideas I'm talking about merely let you keep track of how quantities have units - that is, they make it impossible to state dimensionally inconsistent equations. There's a vast choice of frameworks for system dynamics - it's really up to you to choose one of those. That's a largely orthogonal issue to keeping track of how quantities have units. But we can look at some particular framework. When you say "next state", does that mean you're doing discrete-time deterministic dynamics?

Tom Hirschowitz (Jun 21 2025 at 06:25):

Oh, I see, thanks. Yes, we're doing discrete-time dynamics, although I guess it doesn't have to be deterministic. That's because we're targeting programming languages.

John Baez (Jun 21 2025 at 08:50):

Okay. Suppose we're studying an object that's accelerating at a constant rate, where for each integer $i$ there is a position $x(i)$ and velocity $v(i)$, obeying

$x(i+1) = x(i) + v(i) \Delta t$
$v(i+1) = v(i) + a \Delta t$

In a naive approach we treat $x(i), v(i), a$ and $\Delta t$ as real numbers. But now we want to incorporate dimensional analysis. So we introduce a dimensional category: an $\mathbb{R}$-linear symmetric monoidal category where every object is a line object. We pick one whose objects are generated by objects $L$ and $T$ (length and time), and we give our quantities dimensions, making them into morphisms

$x(i) : I \to L$
$v(i) : I \to L/T$
$a: I \to L/T^2$
$\Delta t: I \to T$

Here $L/T$ is short for $L \otimes T^{-1}$, where $T^{-1}$ is the object that's a tensor inverse to $T$. Similarly $L/T^2$ is short for $L \otimes T^{-2}$.

Now something like $v(i) \Delta t$ is short for the tensor product of morphisms $v(i) : I \to L/T$ and $\Delta t : I \to T$, which is a morphism $v(i) \Delta t: I \to L$.

Note that in our equations we are only adding morphisms with the same source and same target:

$x(i+1) = x(i) + v(i) \Delta t$
$v(i+1) = v(i) + a \Delta t$

This means our equations are dimensionally consistent. If we tried to write

$x(i+1) = x(i) + v(i)^2 \Delta t$

this would give a type error because we're trying to add two morphisms that aren't in the same homset. (Each homset is a real vector space, since our category is $\mathbb{R}$-linear.)

John Baez (Jun 21 2025 at 08:52):

Anyway, I won't apply for the postdoc, but I've been talking to @Evan Patterson and @Nathaniel Osgood about building dimensional analysis into software in this way.

Tom Hirschowitz (Jun 22 2025 at 08:01):

Nice! Thanks for explaining.

In fact, we could even view the initial conditions as a morphism $I \to L \oplus L/T$, and the increment as an endomorphism of $L \oplus L/T$, right? This makes the system a kind of automaton internal to the ambient category. Except that the use of $\oplus$ makes us step outside the realm of dimensional categories. Maybe we should consider categories in which all objects are generated by line objects, direct sums, and tensors?

Anyway, I'm not sure how to handle the concurrency issue here. Would you guys be willing to join forces? Let's call @Pierre Hyvernat and @Vincent Reverdy so that they at least read the current discussion, to start with. It might also be the case that both strands can happily live independently of each other. As I said, we're working with the rocq prover for now: do you know already which kind of software you have in mind?

John Baez (Jun 22 2025 at 10:01):

@Evan Patterson is using Catcolab, a modeling system he has been developing based on double categorical doctrines. @Nathaniel Osgood might use either that or AlgebraicJulia, a framework for using category theory in Julia.

Nathaniel is the most eager to get dimensional analysis going, because he uses our AlgebraicJulia software for agent-based models and stock-flow models in his work on epidemiology, and getting dimensional analysis going should be helpful there.

By the way, please note that dimensional categories are equivalent to abelian-group-graded algebras, which are often a more lightweight and practical means to the same end. Given a skeletal dimensional category, its set of objects forms an abelian group $A$ under tensor product, and the set of morphisms $f: I \to a$ where $a$ ranges over all objects $a$ forms an $A$-graded algebra. Conversely from any algebra graded by an abelian group we can reconstruct a dimensional category.

John Baez (Jun 22 2025 at 10:12):

Tom Hirschowitz said:

In fact, we could even view the initial conditions as a morphism $I \to L \oplus L/T$, and the increment as an endomorphism of $L \oplus L/T$, right? This makes the system a kind of automaton internal to the ambient category. Except that the use of $\oplus$ makes us step outside the realm of dimensional categories. Maybe we should consider categories in which all objects are generated by line objects, direct sums, and tensors?

That sounds like it should work - nice idea. It might eventually work well in Catcolab, which is designed for working with different doctrines - e.g. the doctrine of dimensional categories, the doctrine of symmetric monoidal categories with coproducts, etc.

Kevin Carlson (Jun 22 2025 at 20:03):

In our modeling work around CatColab we would tend to keep the dimensional category, which is a model of your unit system, separate from the dynamics of particular physical systems with laws of motion (say) expressed in units from that dimensional category. From a PL perspective, surely you wouldn’t want to put the operational semantics of your programming language right into the type theory? And your programs will be approximating smooth phenomena in many cases, whereas I’m sure you don’t want to start putting differential equations directly into your unit system. We’d tend to suggest picking functors out of your nice trim syntactic dimensional category into any number of categories of dynamical systems (including automata modeling operational semantics), a move which should feel familiar from lots of places in categorical logic and PL.

Kevin Carlson (Jun 22 2025 at 20:04):

I’m very glad to see this is happening, anyway! I talked to Vincent about it two years ago but it trailed off at that time.