joppy

The other huge benefit to symbols is that they are compact, and recognising patterns or performing symbolic manipulation is much easier when everything is shorter and closer together. Mathematics also uses a two-dimensional layout in some places (integrals, fractions), with very well-chosen and suggestive notation, which would be lost completely going to words.

I agree, as a computer science and maths undergrad, the first rewarding part of category theory was in algebraic topology where we first saw examples of very nontrivial functors (fundamental group, and homology). Up until that point, category theory seemed like a pointlessly abstract way of stating obvious facts.

Even now as a research mathematician, category theory is a good tool for guiding to the “correct” definitions of things, but virtually all the work after that is “category-less” in that it is completely and utterly specialised into the problem domain.

Category theory is still a fantastic way of organising information, stating things like universal properties, and also sometimes making “abstract nonsense” arguments (which often guide you towards some nontrivial observation in a particular category). But it is certainly not the panacea that some make it out to be.

The original text is meant to mean a triple of statements:

x < y if and only if w < z

x = y if and only if w = z

x > y if and only if w > z

This can be tiresome (and obviously confusing) if you need to keep using it in many places, hence some authors define the odd symbol to start with, and then use that in many places.

I’ve seen this used in the context of statements like “x is less than, equal to, or greater than y if and only if w is less than, equal to, or greater than z”. Which might be written “x ⪋ y if and only if w ⪋ z”.

There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own.

There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.

It is pretty common for some pure mathematics papers to be pretty much book length anyway these days, say 80 pages or more.

Arrays are nicer for the IN case because Postgres does not understand an empty list, i.e “WHERE foo IN ()” will error. Using the “WHERE foo = ANY(array)” works as expected with empty arrays.

In C++ you can’t really even separate them if you want to define templates, because (unless I am mistaken) template instantiation can only be done at compile time rather than link time. It’s sad to not be able to cleanly separate the interface from the implementation.

Zig is certainly not weird in the way that something like prolog or scheme are.

There are languages which can automatically transform between a.foo(b) and foo(a, b) - for example the D language. Does this make 2.weeks.from_now more palatable? And if it does, then why worry about whether the code “goes on the class” or not? During execution it doesn’t really matter where the code lives, and during development open classes are doing basically the same thing as defining functions overloaded on the first argument.

Cardinalities of sets do have sensible operations like less than and greater than though - |A| <= |B| if there exists an injective function from A to B. One has to check that this inequality behaves in the ways that you expect, but it is a well-defined concept.

I had to sign back into my computer on my windows install so that I could run the uninstaller, which seemed very odd. I had a one month subscription to in design so I could make some stationery (which went very well), but having to sign in to uninstall a few months later was a bit rude.

Tikz is fantastic if you know exactly what you want to draw. However in the case of many academic papers and presentations, the author doesn’t know exactly what they want to draw until after most of the graphics are made - only then can you observe some changes that can be made to make everything more consistent (not consistent with respect to line widths, colours, and whatever, I mean more consistent as in “tells a consistent story”). Tikz is awful for this - the amount of time one has to spend trying to edit a single graphic is so so much higher than with any other visual vector graphics program (Inkscape, Ipe, Illustrator, etc). It means that for many people, even if something looks out-of-place in the larger context of a paper or presentation, they won’t change it because it’s too hard. If you spent 20 minutes making a graphic with any other tool, then down the road if you feel it would be done better a completely different way, it’s fine to chuck it out and go again. With Tikz, making graphics can take much longer (this is doubly true if your edits are taking place outside of that one week you had Tikz loaded into your brain), and authors are much more reluctant to throw away work to improve a final result.

It’s because of this that I think working with Tikz (or other very-high-friction-for-most-people tools) is to the detriment of the end product. Being able to be agile, especially when displaying technical and complicated graphics, is paramount to those graphics ending up good.

Do you think this is to do with wasm having no threading support at the moment?

I guess the problem is that saying "tensor products are spaces of multilinear functions on vector spaces" is tantamount to saying "vector spaces are spaces of multilinear functions on vector spaces", which is simply not true: the second set is strictly smaller than the first. For example, there is no space of linear functions on a vector space which is countably-infinite dimensional: they are all either finite-dimensional or countably infinite dimensional. Said another way, if we're talking about 1-fold tensor products, it is not right to say "a 1-fold tensor product of V is V*", since V itself is a perfectly fine 1-fold tensor product.

In order to have V* = V for an infinite-dimensional vector space V, you need to redefine V^* to some kind of restricted dual, rather than defining it as the set of all linear functions. In the polynomial example, if we take the space of all linear maps g: F[x] -> F such that g(x^n) = g(x^(n+1)) = ... = 0 for some n >> 0, then this restricted dual is isomorphic to F[x] again. But the evaluation map g(f) = f(1) is not in this restricted dual.

There are more reasons why confusing a vector space with its dual is a bad idea. For example you cannot cook up a map V -> V* without extra knowledge, for example a choice of basis of V or something. There are many examples in abstract algebra where there is a perfectly good vector space V, and absolutely no good choice of basis for V, so trying to identify elements of V with V* is unnatural. We may still be able to speak perfectly well of vectors in V or V*, but trying to identify V with V* is still unnatural. A good example is V = (functions R -> R). I can speak easily of elements of V (for example, x + sin(x)), and of elements of V* (for example, f -> integral of xf(x)), but trying to figure out which element in the dual either of these corresponds to is hopeless. We're better off just accepting at some point that there is a real difference between a vector space and its dual.

That’s definitely possible (the function should take two elements in F[x], not in its dual space), the problem is that there are strictly more linear functions on the set of polynomials than there are polynomials. For example you will have trouble finding a polynomial representing the “evaluate at x=1” linear function F[x] -> F, since such a polynomial would have to have infinitely many terms.

So every polynomial could be represented as a linear function on polynomials, but not every linear function on polynomials is itself a polynomial.

There is in fact another definition of “tensor rank” which has everything to do with the rank of a matrix. For a tensor t in a tensor product of vector spaces VxW, define the rank of t to be the least number of summands possible in an expression t = v1xw1 + … + vnxwn.

If t is zero, then it rank is zero. If the tensor product is Vx(dual V), ie of type (n,m)=(1,1), then a tensor t can be considered as a matrix, and its tensor rank is the same thing as its matrix rank. You’re basically looking for the smallest way of writing the matrix as a sum of outer products of row and column vectors.

If you’re into quantum physics, then tensors of rank 0 or 1 are non-entangled, and tensors of rank 2 or more are entangled states.

The easiest way to see it is cardinality: the space of linear functions on a countably-infinite dimensional vector space is uncountably-infinite dimensional. This is the reason why you can’t necessarily swap out vectors with linear functions on an infinite-dimensional vector space (if you restrict to functions with finite support or something, it’s ok).

A familiar example of a tensor product of countably infinite dimensional vector spaces would be polynomials in multiple variables. Say F[x] is the vector space of polynomials in x with coefficients in the field F, and F[x,y] is the space of polynomials in the variables x, y. For example x^2 - x is an element of F[x], and yx^2 - y^2 is an element of F[x,y]. Then it’s not hard to see that as vector spaces, F[x,y] is isomorphic to (F[x] tensor F[y]). A tensor in this new space is precisely a polynomial in two variables.

In the above it’s important to note that a polynomial has finitely many terms, so a power series like 1 + x + x^2 + … is not a polynomial. The space of power series is isomorphic to the space of linear functions on F[x], and is uncountably-infinite dimensional.

I think that tensors have a much more broad meaning to mathematicians. At least in pure mathematics and algebra, there is much more of a focus on the tensor product operation, a way of taking two (or more) vector spaces and producing a new vector space: their tensor product. Tensors are elements of this new space. In particular they don’t need to be multilinear functions on a product of vector spaces (for finite dimensional spaces there is not much difference, but for infinite-dimensional spaces there is a real difference between these two things).

Tensor products in this generality don’t need to have an (n, m) rank in the sense you’re describing, since they might be put together from completely different spaces. For example it’s perfectly fine to form the tensor product of a 2-dimensional space with a 5-dimensional space, yielding a 10-dimensional space.

It’s not a very high bar though is it, plaintext input and batch processing to produce image files?

How big of a concern is this? Nowhere I’ve ever worked has been concerned with the ability to swap the database for a completely different one, in the same way they are not concerned with the ability to swap whatever programming language is being used for a different one.

People will break fewer rules the fewer rules you have - and people will also use their common sense to interpret the rules. “No pets” doesn’t seem like it precludes “friend drops by with a pet and we stay on the porch”, in the same way that “no parties” doesn’t seem like it precludes “four friends come for dinner one night”.

If you’re renting a house people will expect to use it like one, no matter how many rules are trying to make it into some more restricted experience.

When working with lots of timeseries information I've found it helpful to always order comparisons so that left-to-right is always increasing, so I would write 2180 < week, or even (not 2180 < week) for the negation of the condition. This becomes almost required when there are multiple values being tested: (a <= 10 && 10 <= b && b <= c) is much easier to read than (a <= 10 && b >= 10 && b <= c). As a perspective, it's more focussed on establishing an invariant of the resulting data than writing a single predicate.

The whole async ecosystem in Python seems like a bordering-on-insane duplication of work, given that a huge amount of the benefits can be gained simply by running your application under gevent (which is what many in the WSGI server crowd have been doing for yonks). The fact that every piece of code has to be rewritten (and usually in a very stupid way, like putting 'async' and 'await' in the right spots and otherwise leaving things alone) is just madness.

I'll grant you that aiohttp has a much nicer interface for websockets than I've seen in gevent-based libraries, but that seems like a very small win compared to the huge downside of chucking out most of the web server ecosystem and starting again.

I agree - PNPM supports workspaces, is incredibly fast, and is space-efficient (it more or less builds node_modules out of symlinks back to somewhere central on your local machine). It also structures the node_modules folder correctly unlike NPM and Yarn, making it very difficult to import a library that you haven’t explicitly declared a dependency on.

I would say that the vast majority of "real mathematicians" could not use such a proof system either - this is one of the major obstacles stopping the adoption of proof systems or proof assistants in the mathematical community. I think that even at the moment, what proof systems can prove is far far ahead of what regular users can easily express in those proof systems, and there really needs to be some programming language / human-computer-interaction work or research to bridge the gap there.

This straightforward in the fish shell:

> set array (string split ", " $string)

Afterwards you can also use the fact that arrays and array elements act far more predictably in fish (no implicit splitting on whitespace, for example).

In research maths, there are some results you use as a black box because even though you could re-derive the result, it’s just a ton of work and you’re glad someone else has done it. For example perhaps it involves some very tedious case-by-case checking, or a large and long inductive argument. Then there are some results you use as a black box because it would take you (in this case you already have a PhD in the field, so let’s say at least 8 years of field-specific education) literally years of full-time study to become familiar enough with the underpinning technology to even follow the statement of the proof, let alone deeply understand it yourself.

I think there are very few, if any, things in software development that have an analogue in that second category.

An ID (I’m thinking specifically of a drivers licence in Australia) usually contains virtually all information anyone would ever need to identify themselves as you over the phone - name, address, date of birth, drivers licence number, etc. Having someone scan this and save it is not something you really want anyone to ever do.

There’s a difference between socialising where you can say something dumb, and your friends will say “that was dumb haha” and everyone will move on with their lives, and socialising where you can say something dumb, someone posts it on social media, and the next day everyone at school is talking about what you did.

Ubiquitous socialising can be good but it cuts both ways, especially in an environment where you have no plausible deniability. In my opinion, people should be free to have their own thoughts, potentially get blasted for them, and move on with their lives the next day with minimal consequences. Certainly there should be no consequences coming from people that were not actually there, but just heard about it from some social media platform.