WingNews logo WingNews GitHub [2]

dddbbb's comments

dddbbb | 5 years ago | on: Netflix's Metaflow: Reproducible machine learning pipelines

Maybe it's different in other countries (I am in the UK), but I feel as if there isn't enough content for a recommender system to even be useful. I feel like after browsing through the catalogue a few times, I have a rough idea of most things I would ever possibly be interested in. There's just not that much there. Either that, or the recommender system is working too well and I never see anything beyond what Netflix wants me to.

dddbbb | 5 years ago | on: Amazon hires 427,000 people in 10 months

I would nominally agree with this logic, but surely the exact same applies when voting? Should people not bother voting because they are just one in a sea of many?

dddbbb | 5 years ago | on: Casio F-91W: The strangely ubiquitous watch (2011)

Buying the cheapest Casio can also be a status signal, similar to the CEO of Goldman Sachs wearing a Swatch. Buying a truly cheap watch is a signal of 'I don't care' (which may be true, or may be affected), whereas getting into expensive watches can get very complicated. There's plenty of stories from investment banking about the signals that watches send, from my understanding people are more likely to poke fun at a Tag Heuer than a Casio.

dddbbb | 5 years ago | on: What Gödel Discovered

They didn't set out to explicitly prove 1+1=2, they just got around to it after 2 volumes, it didn't require 2 volumes of background. A direct proof of 1+1=2 is pretty short in most logical systems.

dddbbb | 5 years ago | on: Guido van Rossum joins Microsoft

For many roles at a hedge fund, being able to do mathematics quickly and intuitively is a valuable skill. Not sure why an economist applying for an MD job would need to be tested on that, though.

dddbbb | 5 years ago | on: Building the Mathematical Library of the Future

It seems to me like Lean has a lot of the momentum at the moment. It's clear that other projects like Coq suffer from a lack of traditional mathematicians formalising modern, fashionable topics. Kevin Buzzard's implementation in Lean of perfectoid spaces is a great example of that boundary being broken, as far as I can tell the most advanced Coq proofs are the four colour theorem and Feit-Thompson theorem, which have analogue proofs from the 60s and 70s.

dddbbb | 5 years ago | on: Building the Mathematical Library of the Future

Increased assurance that the proof is correct and the various standard benefits of digital over analogue data. This software automatically checks the validity of the proof (with a very small, manually verified core of code doing so), it does not automatically generate proofs wholesale. The proof itself is written by the mathematician interactively, which is still a manual process that requires skill, creativity and thought.

dddbbb | 5 years ago | on: Turing Incomplete Languages

Totality is optional in Idris. Also, the big dependently-typed languages like Coq, Agda, Idris all support corecursion, so they can run programs infinitely provided the program does something productive.

dddbbb | 5 years ago | on: Turing Incomplete Languages

I'm not sure what Turing completeness has to do with such a problem. There's a theoretical non-Turing complete subset of HTML+JS that has all the problems you claim, meanwhile Markdown with a built-in lambda calculus interpreter is Turing complete yet much less problematic. I think you're overcomplicating things for yourself by bringing terms like 'Turing-complete content' into the discussion, surely it just suffices to explain that the more powerful the system, the more open to abuse it is?

dddbbb | 5 years ago | on: Admitting That Functional Programming Can Be Awkward (2007)

I'd say there is quite an important conceptual difference in that the state monad example exactly desugars to pure functional code. Monads give us a good syntax for sequential computation, but this sequentiality is built out of purely functional components.

dddbbb | 5 years ago | on: Someone has stolen my Instagram account

I find it strange that the Facebook employee wouldn't just forcibly change OP's username to something else (e.g. @danny123) then give the desired name to their friend. Actually stealing someone's account seems like an over the top and unlikely way to go about this.

dddbbb | 5 years ago | on: Things I Was Wrong About: Types

Haskell's Either is a 'true' sum type, it corresponds exactly to the way sums have been defined in the literature for decades, and also is the Curry-Howard representation of logical or. It necessarily must be inside a Either-like wrapper in order to be type safe, String and Int are ultimately different and so at some point we must discriminate between them. foo could call further functions with its argument inside itself accepting Either String Int, but eventually a destructor will be hit somewhere in the call stack.

If String and Int do implement the same behaviour under some circumstance, then a typeclass should be used to define that behaviour. Then foo can have type (Bar baz) => baz -> Int, where String and Int have Bar instances.

page 1
more