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…
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.)
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…
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…
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…
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…
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…
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…
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…
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…
> 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".
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-ga...
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 "full fat…
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…
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…
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…
> 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…
> 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…
"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 "algebra" might…
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…
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…
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…
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…
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 look at…
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…
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…
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.)
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…
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…
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…
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…
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…
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…
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…
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…
> 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".
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-ga...
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 "full fat…
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…
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…
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…
> 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…
> 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…
"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 "algebra" might…
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…
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…
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…
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…
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 look at…
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…