julesh

julesh, 6 months ago to random

70 years ago, the people who designed languages like Cobol, Algol and Fortran made the questionable choice that the semantics of an argument to a function is determined entirely by its position within an ordered list of arguments. Since their compilers had to run on a potato and grab arguments directly from registers it probably made sense at the time, but it's a language choice that's definitely overstayed its welcome by 50 years. Named arguments are better in every conceivable way, and so many languages that ought to know better are still beholden to the caveman languages.

Meanwhile, type theorists decided that their contexts are lists equipped with explicit commutativity, not bags - and category theorists characterising free symmetric monoidal categories did exactly the same thing. There is an obvious and totally reasonable way of making a selection of variables from a bag-like scope, namely, names. Is there an actually good reason to stick with argument lists, or have type theorists and category theorists also been hyptonised by Algol and Cobol?

julesh, 4 months ago to random

The fact that quantum algebra was originally developed without string diagrams is no less mind blowing to me than what mathematicians did in the Islamic Middle Ages without having algebraic notation

julesh, 9 months ago to random

With topological invariants of lax functors now en route to being understood, I think only one of my old grand challenge problems for applied category theory remains standing: How to talk about continuous time processes

You can definitely do it by mapping a monoid of time into your category (for example Toby Smithe does it a lot), but to me that feels like potentially not the right way to do it

Instead of composing a list of morphisms, I want to be able to integrate a bunch of infinitesimal morphisms along a path

julesh, 7 months ago to random

In our work on dependent optics we're following an idea of @bgavran that there's an extra hidden dimension: dependent lenses = morphisms of containers = natural transformations of polynomial functors are secretly connected components with respect to a lower dimension, and revealing it is very useful. But I was also just reminded by @zanzi that the 0-cells of this category are really functors so there's also another dimension upwards. This category is naturally 4-dimensional !!! 😰

julesh, 8 months ago to random

Why do we care about dependent optics?

• We must pursue our white whale

• There's a huge amount of theory done in parallel by David Spivak et al using polynomial functors and by us using optics which is transparently the same stuff, and we'd like to be able to unify it both for mathematical and sociological reasons

• We would like to be able to solve obvious analogies like "lenses are to prisms as dependent lenses are to what?"

• We would like to be able to talk about external/demonic choice of open games and other classes of cybernetic processes over categories which are topologically nontrivial, such as measurable spaces - what does it mean for a game's structure to change depending on an earlier state which is a point in a measurable space?

• We would like to combine the denotational expressiveness of dependent leneses with the operational sensitivity of optics (see https://arxiv.org/abs/2209.09351), for example to talk about manifold learning (which is denotationally about dependent lenses over the category of differentiable manifolds with submersions as display maps) in a way that is aware of operational aspects; the long term goal is to be able to develop a static type theory for differentiable programming

• Probably some other reasons that I forgot right now

julesh, 7 months ago to random

It's curious that the category Cat is only prevented from being an object of itself for set-theoretic reasons, there are no category-theoretic reasons preventing it. You might think that Cat can only be seen as an object of 2Cat, that you're forced to go up a dimension as well as up a universe size, but magically functor composition is strictly associative so Cat is still a perfectly good 1-category

julesh, 7 months ago to random

What the heck is really going on with foldl and foldr?

The first take is that folding is about the universal map from a free monoid (ie. lists) to some other monoid. That says you can fold something that's (1) a binary operation on a single set, (2) unital on both sides, and (3) associative, aka a monoid. In that case foldl and foldr are different implementations of the same function

I think the next step of abstraction is that foldl and foldr deal with left and right monoid actions (or possibly the other way round), which gives up (1), and weakens (2) and (3) while keeping them morally intact

But, like, foldl and foldr appear to work perfectly well with no associativity whatsoever. It doesn't even feel like a programming hack to me - left-folding or right-folding a non-associative operation over terms of a free monoid feels to me like a perfectly reasonable thing to do mathematically speaking. But I have no idea whether they have universal properties or if it's just a thing

I idly wonder, if you go from monoids to commutative monoids, ie. from lists to finite multisets, what happens to foldl and foldr? Intuitively I feel like left and right folds are no longer well defined, but why would imposing commutativity suddenly also require associativity as well?

julesh, 4 months ago to random

Today's hell journey: Basingstoke -🚍-> Reading -🚄-> London -🚄-> Glasgow

julesh, 4 months ago to random

Knives are cutlery, forks are stabblery, spoons are scooplery

julesh, 9 months ago to random

Since last week I'm feeling my periodic inspiration to get some stuff written down. This inevitably leads to me getting bogged down in a bunch of details before putting it all aside again. But maybe this time is different.

julesh, 2 months ago to random

We've known about this for a couple of months but it finally hit the news today. Basically every university in the UK is incredibly financially dependent on scamming kids all over the world out of their families' life savings, sorry, "tuition fees”. Things are about to get really rough around here.

julesh, 8 months ago to random

Committing crimes against haskell, purely for shits and giggles (I wanted to see if I could implement some functions without using any function types)

type family Length xs type instance Length Empty = Zero type instance Length (Cons x xs) = Succ (Length xs) type family Snoc xs x type instance Snoc Empty x = Cons x Empty type instance Snoc (Cons x xs) y = Cons x (Snoc xs y) type family Reverse xs type instance Reverse Empty = Empty type instance Reverse (Cons x xs) = Snoc (Reverse xs) x

julesh, 10 months ago to random

"No, the Yoneda lemma doesn't solve the problem of qualia" by @mc
https://matteocapucci.wordpress.com/2023/07/15/no-the-yoneda-lemma-doesnt-solve-the-problem-of-qualia/

julesh, 4 months ago to random

Today's task: fighting Jekyll

julesh, 2 months ago to random

Just realised that the purely economic case for UBI is basically identical to the case for VCs, just on a different scale: when people can absorb risks, innovation happens

julesh, 2 months ago to random

Blind reviewing: author doesn't know who the reviewer is, reviewer knows who the author is (eg. most peer review)
Double blind reviewing: author doesn't know who the reviewer is, reviewer doesn't know who the author is (eg. some peer review)
Reverse blind reviewing: author knows who the reviewer is, reviewer doesn't know who the author is (eg. some assessment marking)

julesh, 1 month ago to random

I always thought that storm drains in the street mainly went down to the same sewer as your toilet. Turns out that's called a "combined sewer" and they exist, but most built since around the 30s have 2 completely separate sewer systems in parallel, with the one for "urban runoff" mainly just going into rivers. The more you know.

julesh, 6 months ago to random

My new catchphrase with grantwriting is "find the catnip", ie. the bit that's irresistible to the funder

julesh, 7 months ago to random

Things I instinctively feel:

• no language has successfully isolated the true essence of OOP yet
• the true essence of state machines is not state
• monads are not the one true way of sequencing access to a state machine
• one of the most important abstractions of programming is still waiting to be discovered

julesh, 7 months ago to random

Mario Román's PhD thesis, Monoidal Context Theory
https://mroman42.github.io/notes/papers/monoidal-context-theory.pdf
[156 page pdf download link]

julesh, 3 months ago to random

Haskell hot take: Prelude should make Float and Double non-instances of Eq, and then provide functions unsafeFloatEq and unsafeDoubleEq for those cases when you really do want to compare them for equality

julesh, 3 months ago to random

Apparently MS Word now uses AI to add alt text to images, so an extensive form game in my exam model solutions is now labelled "a diagram of a train"

julesh, 9 months ago to random

Watching an absolute spherical chonk of a pigeon sitting on a wire outside the window and suddenly wondering how do birbs balance?.... it sure doesn't look like it's actively balancing, it's twisting around preening itself with its beak and feet… but it's so chonky its centre of gravity surely isn't very low down... how do birbs break the laws of physics?

julesh, 2 days ago to random

Old people, not content with merely destroying the economy for young people, are now trying to actively murder young people

image/png

julesh, 7 days ago to random

It's not just imagination, Englandandwales really is a conservative religious country compared to Scotland