jonlong

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 differentiable and you can compute a piecewise derivative. The Weierstrass function is defined by an infinite series, and you can compute its derivative term-by-term by the usual rules and check that the result does not converge; it is indeed straightforward to calculate its nonexistent derivative, and this is what Weierstrass did!

In general, to even ask what it means to compute a derivative we need to specify some input language which describes functions in finite terms; we are necessarily in the world of constructions rather than (say) arbitrary set-theoretical maps between infinite sets. With this in mind, the claim that differentiation is always a straightforward computation is a strong one.

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 guides for this (e.g., https://support.apple.com/en-us/120768) as does iFixit. Genuine parts are available for purchase and tools are available to rent by individuals (see https://support.apple.com/self-service-repair, which specifically mentions display replacement). Skill and patience are required; replacement by Apple is not.

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

In his article which popularized the idea of The Singularity, Vinge quotes Ulam paraphrasing von Neumann, and states, "Von Neumann even uses the term singularity". As von Neumann surely knew, "singularity" was a term widely used in mathematics well before the idea of black holes (etymonline dates first use to 1893). Vinge does not say anything about black holes.

an object is pulled into the center [of] gravity of a black hole [until] it passes a point beyond which nothing about it, including information, can escape. [...] This disruption on the way to infinity is called a singular event – a singularity.

The point at which "nothing" can escape a black hole is the event horizon, not the singularity. What exactly happens to information and what exactly happens when crossing the event horizon are subjects of debate (see "black hole information paradox" and "AMPS/firewall paradox"); however, it's probably fair to say that the most orthodox/consensus views are that information is conserved through black-hole evaporation and that nothing dramatic happens to an observer passing through the event horizon.

the singularity became a black hole, an impenetrable veil hiding our future from us. Ray Kurzweil, a legendary inventor and computer scientist, seized on this metaphor

While I'm not prepared to go into my personal views in this comment, it's worth noting that the idea that "exponential curves look the same from every point" is not foreign to, e.g., the Kurzweilian view of The Singularity; nevertheless, fitting dramatic, industrial-revolution-sized progress into the fixed scale of a (contemporary) human lifetime would surely be a big deal. This idea, (whether you believe it will happen or not), is obscured by the spurious black hole metaphor.

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 tagged union, and, per above, that function is exactly the one which tags its input as belonging to the left disjunct.

I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.

Well, everything I've said here is standard and widely-taught; go forth and check if you're inclined to. A good introduction is the one by Philip Wadler, https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as... (tagged unions appear in Section 3, though it's all worth reading). A much more to-the-point and programming-focused account is in this OCaml book: https://cs3110.github.io/textbook/chapters/adv/curry-howard.... (very little OCaml syntax is used). You can find countless more.

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 logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...

I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).

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; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B".

However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)

So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct!

Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").)

Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.

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 from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.

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 that says "this work [...] may not be built upon without express permission of the author". To the extent that this refers to derivative works which substantially reuse the text of the paper, this is normal copyright law. To the extent that this refers to the use of scientific ideas or discoveries, this is not enforceable under US copyright law. Copyright cannot prevent anyone from citing or responding to a work. See, e.g., https://www.copyright.gov/circs/circ33.pdf.

(I am an academic, not a lawyer.)

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 qualitative errors have been corrected.

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 dependent types", and it's the things that are less powerful that require qualifiers.

(So when Sail says it has "lightweight dependent types", that seems fine to me (it does seem to do more than it could with simple types or polymorphic types), but if it simply asserted that it "had dependent types" I would feel misled.)

The wording is subtle and language does change, but what I want to push back on is the confusion I see from time to time that "if I can write anything that looks like a function from values to types, I have the same thing that everybody talking about dependent types has". If you think this you don't know what you're missing, or even that there is something you're missing, and what you're missing is very cool!

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 type theory...

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 like Agda, Coq/Rocq, and Lean are well-typed, polymorphic (but not dependent) languages like OCaml, F#, or Haskell ("ML family" or "Hindley-Milner" are related terms). Those are what I'd suggest checking out first!

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 (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history of dependent types is intertwined with the history of formalizing mathematics; dependent types were designed to encode essentially arbitrary mathematical statements.)

The interesting feature of Ada here seems to be what it calls "subtype predicates". As you've explained, these come in a "dynamic" flavor, which are a nice syntax for runtime assertions, and a static flavor, which are compile-time checked but restricted to certain static expressions (per https://ada-lang.io/docs/arm/AA-3/AA-3.2#p15_3_3.2.4).

An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count!

I do believe (having heard from multiple sources) that Ada's type system was ahead of its time and its success in creating practical programs that are likely to be correct is probably underrated. But I'm not here just to legislate semantics; one should be aware that there is something vastly more powerful out there called "dependent types" (even if that power is not likely to come into most people's day-to-day).

(Unfortunately Wikipedia is quite poor on this topic; you will see, for example, that on the Talk page someone asked "Is Ada really dependently typed?" two years ago; no reply. And it makes no sense to say that Ada has "tactics" but not "proof terms"; tactics are a way of generating proof terms. There are many better resources out there (especially ones associated with the languages Agda, Coq (currently being renamed Rocq), and Lean, e.g. https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...). But be warned, there is no "short version": dependent types cannot be explained in a sentence, and they are not something you will arrive at with enough "hacking away".)

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.

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 glyphs and juxtaposition of existing people-emoji to describe families in detail.

You can read about it here: https://www.unicode.org/L2/L2022/22276-family-emoji-guidelin...

"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 be the most overloaded term in mathematics.

(The article says in the second paragraph: "the name comes from universal algebra". The wiki article you linked disambiguates itself with universal algebra right at the top.)

"Algebraic data type" in this sense is synonymous with "inductive data type".

The values of an algebraic data type do not form a free ring or any ring. You cannot generally add or multiply them. You may write a particular type with constructors intended to serve this purpose, but the laws defining a ring will not hold.

A separate fact is that types (not their values) belong to a free semiring "up to isomorphism" (where sum and product are the categorical coproduct and product). It is this fact that seems to have been conflated with the "algebra" of "algebraic data types". The disambiguation of this with the sense from universal algebra is the very purpose of the article.

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, geometric meaning given by Euler's rotation theorem) is the right starting point for thinking about distances in this space.

(Your reference [2] supports this point of view: read "simplest" as "canonical". Your reference [1] claims five distinct bi-invariant metrics, but this is wrong. The argument given is that any metric related to a bi-invariant metric by a "positive continuous strictly increasing function" is itself bi-invariant, which is not true.)

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 phone flat, so that the rotation away from you is about a horizontal axis; then you should experience the noncommutativity.

(The resulting orientations are 180 degrees apart, which indeed makes it difficult to say that any one orientation should be the unique average. But this is due to the geodesic structure of the space of rotations, not the noncommutative product that happened to construct these points, see above.)

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 sense (not always uniquely).

Commutativity has nothing to do with this; do not confuse the typical formula for averaging with the reason for doing so! Of course, there are other senses of "average" (which generally do continue to apply to the space of rotations as well).

The application for this given by GreedCtrl's reference is to spline interpolation. Another is in robotics, when combining multiple noisy observations of the orientation of an object.

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 in older books.

That said ∇× is what I've seen most commonly overall.

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 how much the sum of the interior angles of an n-sided polygon exceeds the usual sum π(n - 2). It's most common to think about triangles, but we can also think about 2-gons... these are usually degenerate shapes with a sum of interior angles of zero.

But on the two disc-sphere, draw two lines, each from the center of one disc to the center of the other disc, passing straight through the glued boundary. These form a 2-gon with sum of interior angles (and also excess over the usual value) equal to twice the angle between the lines. To get the total curvature of the whole sphere, let each of the two interior angles be 2π, for a total of 4π... two circles, the Euler characteristic.

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 the expected 2πr is a measure of the curvature at that point.

In the two-discs sphere construction, a circle centered on the disc boundaries will appear half in each disc. But it will be short of the usual circumference due to the shape of the discs. All the curvature has been pushed to these boundaries.

In the cube, a circle centered at a vertex will appear on three sides; its circumference will be three-quarters of the usual value. Note that all the curvature of the cube is at the vertices, not the edges!

For the portal-torus, try drawing a circle anywhere, passing through the portals... it will have the usual circumference, zero curvature everywhere.