jonlong

11 ms·

1.
by jonlong 10d ago
What I would add here is that the property of left-cancellation is exactly equivalent to injectivity, i.e., f : A -> B is injective iff, for any g, h : C -> A, f o g = f o h implies g = h. If A = {} then f is injective and left-canc
2.
by jonlong 3mo ago
It's important to know that (in the usual setting of analysis) not every function is everywhere (or even anywhere) differentiable, but this is more orthogonal to the author's point than opposed to it. A square wave is piecewise di
3.
by jonlong 4mo ago
Fwiw, you can use the "Modern English" language setting to banish the long s. Reproducing Byrne's original typography is a stated goal of the author. (You can certainly debate the value of that goal.)
4.
by jonlong 7mo ago
Apple may not design for repairability, but what you are saying is not true. I have personally purchased and installed genuine replacement displays on MacBooks with no involvement from Apple. Apple publishes repair guides for this (e.g., h
5.
by jonlong 8mo ago
The etymology and physical metaphor of "The Singularity" are a bit confused here, and I think it muddles the overall point. > the singularity is a term borrowed from physics to describe a cataclysmic threshold in a black hole I
6.
by jonlong 9mo ago
It's true that in intuitionistic logic "A implies (A or B)"; the usual computational interpretation of that is that "there is a function taking a value of type A and returning a value of type A + B", where + is the
7.
by jonlong 9mo ago
I suppose I erroneously assumed some familiarity with the correspondence between product types (i.e., types of pairs) and the constructive logical interpretation of "and". Suffice it to say for now: there is an interpretation of l
8.
by jonlong 9mo ago
Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical. Now I do see where you are coming from; unde
9.
by jonlong 9mo ago
While others have addressed the programming case for tagged unions, I want to add that, to a logician, tagged unions are the natural construct corresponding to "logical or". In intuitionistic logic (which is the most basic kind
10.
by jonlong 1y ago
I agree with your point, but it's worth noting that scientific papers are normally and by default copyrighted works. (In some cases the author may assign the copyright to a publisher.) Eric's draft contains an unusual statement th
11.
by jonlong 1y ago
For late arrivals to this thread: note that the illustration being discussed has been updated (see the Wayback Machine for the old version). The new version probably still does not show the best second-order approximations, but the obvious
12.
by jonlong 2y ago
> They likely misjudged the plane due to assuming it was a large jet but it was a regional jet Maybe this is possible, but it seems implausible given that ATC explicitly refers to the jet as a "CRJ".
13.
by jonlong 2y ago
Indeed -- for a more detailed, incisive, and entertaining take, check out Season 1 of the "Opinionated History of Mathematics" podcast by Viktor Blåsjö https://intellectualmathematics.com/blog/the-case-against
14.
by jonlong 2y ago
Well, "dependently typed" is widely used to mean something like "derived from Martin-Löf type theory, including arbitrary dependent sums and dependent products"; in other words, "dependent types" means "fu
15.
by jonlong 2y ago
Ah, very interesting. It does seem that the Ada community has done serious engineering work to build in powerful formal verification, in a way that is somehow parallel to the (much slower, for practical purposes, if more elegant) arc of typ
16.
by jonlong 2y ago
I would say dependent types are going into the deep end; unless you have a real need to prove things, it may be hard to see the motivation to learn such abstractions. In between ad hoc types like TypeScript and dependently-typed languages
17.
by jonlong 2y ago
Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf
18.
by jonlong 2y ago
> The astute reader will notice that float operations are not communicative Presumably this was meant to read "commutative". IEEE 754 addition and multiplication are commutative (ignoring NaN values), but not associative.
19.
by jonlong 2y ago
> you're not going to be able to cover all valid families that way In fact the emoji committee backpedaled on family permutations for exactly this reason, and now recommends (exactly as you suggest) "symbolic" family glyph
20.
by jonlong 2y ago
"Free algebra" here comes from universal algebra/category theory, which is quite distinct from the "free algebra" of ring theory (having nothing in particular to do with sums and products). Unfortunately "algeb
21.
by jonlong 2y ago
The bi-invariant metric as pointed out by chombier is what I have in mind. I agree that a non-canonical metric may be the right one for some applications, but those are the exceptional ones. The bi-invariant metric (which has a simple, ge
22.
by jonlong 2y ago
If you start with the phone upright and rotate the screen away from you by turning the phone around the vertical axis, then both rotations are around the same axis and of course they do commute. My guess is that romwell is holding the p
23.
by jonlong 2y ago
The most widely-used concept of "average" is surely a point that minimizes the sum of squared distances to each of a list of input points. Distances are canonically defined in the space of rotations, and so are averages in this se
24.
by jonlong 2y ago
Wiki says that curl is standard in North America, while rot is common in "the rest of the world, particularly in 20th century scientific literature". As a North American I can confirm that I was always taught curl and only saw rot
25.
by jonlong 2y ago
Yes! For the two-disc sphere, I can't think of an intuitive way to "see" the "circles lost" integral. But here's a different intuitive way to see the total curvature. Another way to measure the curvature is to
26.
by jonlong 2y ago
Here's an easy way to test the curvature of these examples. Draw a circle (all points equidistant to a given one) centered at a point on one of the "glue" edges. The amount that the circumference of that circle is short of th