waluigi

3 ms·

1.
by waluigi 1y ago
It’s even more counterintuitive than you let on! If you are working in ZFC along with the axiom “ZFC is consistent” then there’s no issue: just a normal number[1]. Where things get really strange is in ZFC plus the axiom “ZFC is inconsist
2.
by waluigi 2y ago
Defining x/0 as 0 doesn’t break anything mathematically; all the relevant field axioms have an x != 0 hypothesis so this really is undefined behavior. Moreover, it’s actually pretty common for proof assistants to adopt the x/0 = 0
3.
by waluigi 5y ago
I think what the poster above is saying is that by saying "the pentagon" the author is referring to the (unique) 5 sided regular polygon, as opposed to some random, potentially non-regular 5 sided polygon.
4.
by waluigi 6y ago
I would push back against this. There is definitely a pretty steep learning curve, but once you are over it you really start to reap the benefits of being able to rapidly add niche functionality that exactly fits your workflows.
5.
by waluigi 8y ago
The way I would approach this is to write what essentially amounts to a declarative specification of what computation needs to be run, and then define an interpreter that handles the caching of intermediate values. The "Embedded DSL +
6.
by waluigi 8y ago
Monad Transformers aren't _that_ bad, the MTL style of doing things makes it all pretty painless. It also provides a huge opportunity for testing. At a very high level, you describe all of your effects as a series of embedded, composta
7.
by waluigi 8y ago
F#'s object model is very different from OCaml's. F# is basically the same as C# when it comes to objects, but OCaml has some sense of structural subtyping that F# lacks. On top of that, OCaml has a very powerful module system, wh
8.
by waluigi 8y ago
This owns. It's important to realize that a lot of at-risk populations that would most benefit from medication are often the most economically disadvantaged, and that our current healthcare system often excludes them from the help they
9.
by waluigi 8y ago
Thank you for pointing this out. It seems that "Governments are ineffective" is taken as a universal truth around here, without considering the fact that pro-privatisation governments have a very strong incentive to make programs
10.
by waluigi 8y ago
Its a common misconception that proofs by contradiction are not constructive. Take the proof that √2 is irrational. What you are trying to prove is that √2 is not rational, or, constructively speaking, `√2 ∈ ℚ => ⊥`. So a proof that cons
11.
by waluigi 8y ago
Yeah, effect systems in general are a really cool idea that I wish we saw more of. Haskell and its derivatives are the only semi popular languages that have some sort of system, and those are just a few points in the design space that admit