h-cobordism

I'm pretty sure you're right on all counts; I'm not even sure that shared immutable borrows would work under the very simple transform given in the README.

Edit: Also, the user-facing language doesn't seem to have linearity at all, i.e. all values may be cloned. But linearity is something that people use to guarantee certain invariants all the time in Rust (and ATS, I've heard), so this seems like a misstep. It also means that memory allocation is implicit, which makes things less predictable for users.

> hey "ECMA script is portable and accessible"! So lets "browserify" all the things

It's not because JavaScript is portable or accessible (it's definitely not portable, and if you wanted accessibility you could do much better), it's simply because it's the most popular language.

I skimmed the Eloquent docs[0] but I couldn't see anything that sets it apart from other ORMs. What makes it special?

[0]: https://laravel.com/docs/7.x/eloquent

(1) That sounds like a recipe to unintentionally miss a ton of concurrency. Having to put an `await` there is a great indicator that you're forcing an order of execution.

(2) Can you give an example of an async and a non-async subroutine that have "the same semantics"?

> embarrassingly knotty around its ObjC bridging (there’s a basic impedance mismatch between those two worlds)

I think they've done an incredible job with their ObjC interop, given said mismatch.

But you're right — the person above who said that

> The world has enough cookie cutter procedural and OOP languages.

definitely isn't looking for Swift.

Tangential: How would the function `first :: &(Vec a) -> Option &a` (which, given a non-exclusive reference to a vector, returns a non-exclusive reference to the first item of the vector, with the same lifetime) be typed using linear and / or dependent types?

I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.

> - how much of the burden of writing the proof falls on me, and how much falls to the compiler?

The compiler in Idris can do some magic, but usually the burden is mostly on you to write proofs. Idris (and similar languages) have assistance in editors to help you automatically write code and proofs.

> What are the full range of things I can express?

Dependent types as present in Idris, Coq, Agda, etc. can serve as a foundation for mathematics, so… pretty much anything!

For your example, most such languages don't have quotient types, so you'll still need to use setoids or similar to model quotients.

> - how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through?

It's pretty much the same situation as Haskell or Rust, but I think having to write fromJust / unwrap is great. It tells you when you're reading the code exactly what assumption has been made, and it doesn't seem awfully burdensome.

> yet for programming I have to front-load all this complexity to express something so utterly trivial.

What's "all this complexity" that you're referring to?

See this thread.

https://news.ycombinator.com/item?id=23127741

There's nothing wrong if, as an interviewer, you get bored of interviewing candidate after candidate. The process is pretty repetitive by nature.

> Does such a thing exist at higher dimensions?

Yes, everything in your first paragraph extends to any number of dimensions (replacing "quaternion" with "rotor").

> I vaguely recall something about having complex numbers for 2D rotation, quaternions for 3D rotation, and octonions for (I'm guessing) 4D rotation

Bivectors and rotors faithfully represent rotations in any number of dimensions. The octonion product can't, because as you said, it's not associative, but rotations obviously have to compose associatively.

Luckily the WOFF2 itself is only around 18KB.

It still seems like an inferior solution to just using SVG, but it's not insanely bulky.

> clearly other people do as well

I don't think most people understand how the content they post to Reddit is licensed.

I assume most people run the code they compile on the very machine they compile it on, so how does preventing compile-time system calls help stop malware?

You're referring to raw string literals, right?

Does HTML5 even let you read a file without loading it all into memory?

Edit: Looks like this is it. https://developer.mozilla.org/en-US/docs/Web/API/ReadableStr...

Edit 2: And yes, this is using it. https://github.com/saljam/webwormhole/blob/master/web/main.j...

And the cross product is used with vectors, which are either symbols like u or v, or written with an underscore / arrow on top, so there's zero risk of confusion.

(Also, the cross product is always a less elegant alternative to the exterior product, but I guess this isn't the place for that rant.)

And also make sure to distinguish between your pi's and your n's! I can't count the number of times I've mixed the two up while finding Fourier coefficients.

> There's no such thing as 'MIDI music'. MIDI is a communications protocol to transfer encoded performance data between electronic sources and sinks.

Why can't I just as easily say that

> There's no such thing as 'sheet music'. Sheets are a communications protocol to transfer encoded performance data between human sources and sinks.

1. Isn't an infinite universe consistent with observations?

2. Yes, real numbers, much like complex numbers, were "invented". But complex numbers lay hidden, waiting to be discovered, as the algebraic closure of the reals, and similarly, the reals can be discovered from the "simpler" ideas of ordered field and Dedekind-completeness.

3. That's the weird thing about mathematics --- when you invent things, you leave a world of discoveries for others to make, and sometimes those discoveries are that your invention has inside it a perfect mirror image of another invention.

4. Once you leave classical logic, you suddenly have a lot more room for invention, because there are several competing definitions of "real number", and none is definitively better.

> It's silly to think that the sqaure root of negative one is something real to be discovered.

As you said, the complex numbers are the unique (up to isomorphism) algebraic closure of R. Given that they arise as the unique solution to (in my opinion) a pretty fundamental question about the real numbers, I think it's fair to say that they've been "discovered", not "invented".

I think in your first paragraph you're confusing intuitionistic logic and linear logic --- intuitionistic logic still lets you "clone" and "delete" propositions freely.

The second paragraph is somewhat true --- at its base, the modern use of the term "intuitionistic logic" refers merely to not accepting the law of the excluded middle. However, there are varieties of intuitionism that are very, very inconsistent with classical logic, like those adopting the idea that "every function between real numbers is continuous".