Tainnor

12 ms·

91.
by Tainnor 1y ago
> Physics is sloppy. :) This is not a general description of a vector, where vector is an element of a general vector space. Not all vector spaces have a norm, which is required for magnitude to make any sense. Fine, then let's be p
92.
by Tainnor 1y ago
You're arguing for including historical motivation in order to make a definition seem more immediately useful and intuitive. I agree with that. What the person you replied to is suggesting, however, is that this can only get you so far
93.
by Tainnor 1y ago
In the mathematical sense, a vector is nothing but an object that can be added to other objects and scaled by some field (with some reasonable properties attached). In physics, a vector is often more specifically something with magnitude an
94.
by Tainnor 1y ago
Codomain is not an obscure term. One second of Googling would have helped.
95.
by Tainnor 1y ago
Yes we can. Several people have tried explaining this to you. Maybe you should sit down and work through the material.
96.
by Tainnor 1y ago
> Vectors need to emanate from the same origin to be considered as part of the same vector space. That's absolutely not the case.
97.
by Tainnor 1y ago
Functions with arbitrary codomains are not vectors, but when your codomain is some field, they are. This is what the article is very explicitly about. I guess you can quibble that the title is imprecise, but it's just a title and the a
98.
by Tainnor 1y ago
I think you are confused about the analogies at the beginning at the article (although there is nothing technically wrong about them). Here's the definition of a vector space which agrees with the one everyone in mathematics use: http
99.
by Tainnor 1y ago
> The general theme is that I am interested in the metaphysical concept of vectors, not the thing that human mathematicians have labeled vectors. That's fine but then you shouldn't be surprised that you can't read higher l
100.
by Tainnor 1y ago
> So I had to repair my intuition again: a vector is a local linearization of something that might be macroscopically, and the linearity is what makes it possible to add and scalar-multiply it. And also that there is functionally no diff
101.
by Tainnor 1y ago
Have you seen: https://leanprover-community.github.io/mathematics_in_lean/
102.
by Tainnor 1y ago
> When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the result I need to obtain and then think about how to build it using my library. fw
103.
by Tainnor 1y ago
> Monad is a weird type that a lot of languages can't properly represent in their type system. While true, a lot of FP-inspired libraries in the majority of languages that don't have HKT will just implement one or several speci
104.
by Tainnor 1y ago
> In my experience, people new to Haskell focus way too much on getting the "a-ha" moment for monads in general, [...] I feel this is true in general for mathematics (and therefore by languages whose design is heavily inspired
105.
by Tainnor 1y ago
> There's a lot of stuff where, I know how to do it but I can't remember the parameter order or the exact method name and the LLM absolutely knows. And I really get nothing out of trying to remember/look up the exact way t
106.
by Tainnor 1y ago
Just today I had a "communication 101" training session that was telling me, among other things, to be concise and targeted . I don't know what's either concise or targeted about an 1h session that doesn't differ
107.
by Tainnor 1y ago
> Here in EU, if not stated in your work agreement, it's pretty common people work full time job and also as a self-employed contractor for other companies. Absolutely not a common thing in my corner of the EU.
108.
by Tainnor 1y ago
Checked errors are not categorically better than runtime exceptions. There are lots of things that should never be checked exceptions: division by zero, illegal array access, OOM, and everything that can't be (at least not locally) rec
109.
by Tainnor 1y ago
To me, it feels like Kotlin for the backend isn't really all that popular in the US from what I read on HN, but here in Europe there are a lot of companies (big and small) using it. Maybe it's the geographic proximity (JetBrains b
110.
by Tainnor 1y ago
> I really miss Java’s exception safety in Kotlin. Java is the only language that I'm aware of with checked exceptions (Swift has "throws" which I guess goes in that direction but is untyped) and it's in my experience
111.
by Tainnor 1y ago
Java also has to maintain backwards compatibility at (almost) all cost, so it has a lot of warts that it can't or won't remove. For example, I think there are like 4 or 5 different types of switch statements/expressions. I al
112.
by Tainnor 1y ago
No. Unlike Ruby, Kotlin is compiled and you can't monkeypatch things, so unless you go out of your way to do reflection magic (something that is unfortunately common in the Java community), you won't get weird runtime surprises li
113.
by Tainnor 1y ago
A language without dependent types wouldn't even let you write down the statement of the theorem, so no.
114.
by Tainnor 1y ago
There's a subset of people in the Japanese learning community that claim to have found the "one true way" of understanding Japanese and sometimes this amounts to making very grandiose claims about how to think like a Japanese
115.
by Tainnor 1y ago
I absolutely adore Sufjan Stevens but at least around here barely anyone's heard of him.
116.
by Tainnor 1y ago
One person who comes to my mind who is a) arguably a creative boundary-breaking genius and b) has some degree of success within mainstream pop is Rosalía. But she's more of an "artist's artist". A lot of modern pop icons
117.
by Tainnor 1y ago
Gaussian elimination (for square matrices) is O(n^3) arithmetic operations and it's one of the most important algorithms in any scientific domain.
118.
by Tainnor 1y ago
As it says on that page, the project was discontinued in 2017 - although they did later make another U-turn and committed to open source without, in my understanding, fully going back to LiMux.
119.
by Tainnor 1y ago
> By the compactness theorem this is guaranteed to work. I think you mean completeness, but essentially yes.
120.
by Tainnor 1y ago
First of all, I should have written "recursively enumerable theory" or "theory with decidable axioms". But I think it's clear that I'm referring to things like ZFC, first-order PA or any other similar system. W

More ›