mrkgnao

Great, Haskell away!

> a long, hard ಠ_ಠ to make sure it doesn't deserve a (╯°□°)╯︵ ┻━┻

Truly an idiom for our age.

Frustrated by trompe l'oeils, a defiant Hackernews uses concentration and focus tricks to hack his biological GPU to dump raw eye input while waiting for his Idris proof of the commutativity of addition to finish compiling. Optical illusions disappear. But to his horror, the rest of the world is actually naturally blurry. Another Hackernews shows up to satirise said idiot's "experience", as massing clouds of Strikeforces of all sorts loom darkly in the distance, smelling neural buffer overflows.

(Honestly, though, that website is amazing. The "idiot" was purely for effect.)

It's better to use

    stack --install-ghc $whatever_command

which gets you the version of GHC you need to be able to run $whatever_command into ~/.stack if you don't have it. Much less brittle than a system-wide installation, and perfect for working with multiple GHCs. Anecdotally: I setup the Arch Linux machine I'm typing this on yesterday. I installed[1] Stack/GHC before xorg :)

[1]: It was so that I could run Aura: https://github.com/aurapm/aura

"Does [[1]] have type [Int] or type [[Int]]?", I'm guessing.

It was worth trying:

    class Effable t where
      f :: forall d. Effable d
        => t -> d

    instance intsAreEffable :: Effable Int where
      f x = ???

(This is PureScript, though. Excuse the bad pun.)

Is that the famous TV tax?

I'm writing an NaaS in Idris as we speak.

    .bs-equalheight .bs-responsive .col-md-3

Checkmate, TSA. /s

> DINE<GO>, FLY<GO>, and POSH<GO>

Can you ... can you order takeout from a Bloomberg terminal?

What are their "SJW credentials"?

I'm sorry, but "PR crisis" continues the worrying (if thankfully rare) trend of people talking about this whole ... situation like it's an unfortunate but incidental bug that just needs to be ironed over, akin to some kind of "cost of doing business". There is a very important category difference between, say, Cloudbleed, and allegations of sexual harassment.

Bounds-checking errors and the like do happen, and in rare cases reach catastrophic proportions, as we saw today. Downplaying what happened in that kind of situation isn't quite right, but it's still victimless in a certain sense -- you're minimizing the PR damage to yourself while not exactly hurting any other party. But Uber's behaviour here is essentially an attempt to apply the kind of "mitigation" that a situation report for a security vulnerability documents to a human conflict. (Non-serious aside: do they have an in-house "Fowler incident report" being edited every ten minutes?) It'd be far more admirable if they could go the completely Homo economicus route and declare "We don't honestly care, as long as we're profitable, and we're going to do everything possible to combat this eventuality." or something along those lines that actually reflects what they think of this, but obviously that would be ... suboptimal.

Yes, Uber management may be (in fact, from the emails they're sending out to people "deleting Uber", they definitely are) suffering as a result, but the lack of a contrite "Yes, this happened, it shouldn't have" instead of the "This is contrary to our values, our ethos, and a few other words that conjure associations of fine, upstanding citizenship in our communities and such" (read "Lies!"), together with the obviously impartial steps they're taking to "investigate" the matter, make it difficult to find empathy for their pain here.

(Any strawmen or logically suspect arguments in the above are unintentional and I'd love being told about them. Damn, I'd use that for an HN signature if those were supported.)

I'd say it's not so much as impressive as it is fortunate (providential, even) for someone with a certain kind of mind: I would definitely have benefited if I'd found HN a few years earlier than I did (rather than Reddit, ha).

You can work in the ring of dual numbers, where ε is a nilpotent and hence noninvertible (which is okay, because it's not a field!) and it's a perfectly rational (hehe) number system to work in.

https://en.wikipedia.org/wiki/Dual_number

But you can use those 12 bits as a key into some pre-arranged set of information, each of which carries more information.

Yeah, that's when they're fresh.

I think using dried leaves saves the trouble of having to pick them off the tree because they just fall to the ground, but I'm a city boy and wouldn't know for sure. Might have to ask my father! :)

You surely mean "revisionist scholarship"?

Isn't evil-mode more well-known?

There are plenty of Vim emulator plugins for "GUI editors" like Atom (or even the Visual Studio family, as a comment in this thread mentions) that do just that!

Again, that was just an example. F is just one possible sheaf on the real line, and in the case of F, yes, continuous functions can be stitched together.

You could define A(I) = { } for a trivial example of a different sheaf A where the "data" (always an empty set, regardless of I) is very different from what it was in the case of F (the set of continuous functions on I).

The "sheaf axioms" define what it means for a "rule" associating "data" to open subsets to be a sheaf, and I was just trying to illustrate them with the example of "F". (Perhaps calling them "properties" or "laws" -- or even an interface or typeclass! -- might help?)

In general, proving that something that looks like a sheaf really is one may be nontrivial. :)

In the special case that I outlined above, it certainly is easy to show that F satisfies those axioms, as you point out. And it is a sheaf (the sheaf of continuous real-valued functions on R) precisely because it does.

Le Monde, mais Die Welt. :)

(Right?)

That's what the timer reading froze at, but is that the same as the time when an abort sequence was initiated?

This is the first time that I saw a livestream where an abort happened, so I'm curious. Is the timer freeze standard?

So, I can probably try to provide the beginnings of an ELI5 from a math point of view, since the heading really caught my eye: a sheaf is a way of assigning some data to subsets of a space which satisfied some commonsense axioms.

For instance, suppose you have a sheaf F that assigns to every open interval I on the real line the set[1] F(I) of real-valued functions defined on it. If I write F(a,b) for F((a,b)):

* f(x) = x is in all the F(a,b), since it's defined everywhere on the real line

* f(x) = 1/(x-3) isn't in F(2.9, 3.1) or even F(1,5), but it is in F(4,5)

And so on. There's an axiom that says that if you have

* f in F(I)

* g in F(J)

such that f = g everywhere on the intersection of I and J, then there is in fact some function h defined all over I ∪ J (i.e. h ∈ F(I ∪ J)) which you can restrict to I and J to get f and g respectively. So "compatible functions can be stitched together", where "compatible" means "agree on overlaps".

Sheaves give you a language to coherently[0] talk about "partially-defined" functions such as 1/(x-3) above, to stitch them together, and go from the "local" to the "global" picture and back comfortably. This last point is actually a hallmark of mathematics in the last one or two centuries: for instance, consider some equation which you want to find integer solutions for. If you want to show it has no solutions, you can reduce both sides modulo some number and show that there are no solutions mod n, which means it is impossible to find any solutions to begin with. It is a much more deep fact (the Hasse principle) that if you can find solutions mod all n (and a real one), you can always solve the original equation! (I'm fudging a bit here: see [2] for details.)

(Quick plug: I have a short post that talks about these things here[3], as well as another on the "p-adic" numbers that appear in the Hasse principle.)

Sheaves are general enough ("data" can mean[4] almost anything!) that Paul Cohen used them to prove the independence of the axiom of choice[5] from the Zermelo-Fränkel axioms (which is hard set theory) even though they were created for geometry, broadly speaking: in particular, they were one of the tools with which Grothendieck and his collaborators powerfully recast algebraic geometry in the 20th century, giving birth to "scheme theory"[6], which is e.g. vital in modern number theory. (I should probably mention the standard example of Wiles' proof of the Taniyama-Shimura conjecture that settled FLT.)

Cool stuff.

[0]: excuse the pun

[1]: ring, really

[2]: https://en.m.wikipedia.org/wiki/Hasse_principle

[3]: https://mrkgnao.github.io/schemes-i/

[4]: Well, a sheaf can be defined as a certain kind of contravariant functor into a category, which one can think of as the "type" of our data.

[5]: https://en.wikipedia.org/wiki/Forcing_(mathematics)

[6]: https://en.wikipedia.org/wiki/Scheme_(mathematics)

> Loon engineers turned to the computing power of Google to improve the navigational system

That earned a chuckle.

You just reminded me of something I've learned about in school:

https://en.wikipedia.org/wiki/Survivorship_curve

Street phuchka vendors in Kolkata (they are what you call golgappas in Delhi) will hand you bowls made out of sal leaves. I wonder if that's the same as what you came across?

https://billandpaige.files.wordpress.com/2014/06/dsc_6462.jp...

That makes sense, in which case someone who's already had some experience thinking about liars-and-truthtellers puzzles gets nothing out new of it, and those are probably the overwhelming majority anyway.

Isn't this a spoiler? I haven't seen the puzzle in a while.