HNHacker News
TopNewBestAskShowJobs

zodiac

1,900 karma · joined November 18, 2012

Just your average fixed point combinator

www.xuanji.li

[ my public key: https://keybase.io/xuanji; my proof: https://keybase.io/xuanji/sigs/YyOVzG7h-Ip1eEcZdfnsvWckOKvnM-6b09PfP3q-9Y0 ]

hi

submissionscomments
zodiac··on Launch HN: machine0 (YC S26) – Persistent CPU and GPU VMs from the CLI
Does snapshot/suspend/resume keep processes/RAM alive - or do you need to re-start processes/reload stuff into RAM? How does that work under the hood (CRIU?) and how fast is it?
zodiac··on “Why not just use Lean?”
We still care about computation and algorithms even when proving theorems in a classical setting!

For e.g., imagine I'm trying to prove the theorem "x divides 6 => x != 5". Of course, one way would be to develop some general lemma about non-divisibility, but a different hacky way might be to say "if x divides 6 then x ∈ {1, 2, 3, 6}, split into 4 cases, check that x != 5 holds in all cases". That first step requires an algorithm to go from a given number to its list of divisors, not just an existence proof that such a finite list exists.

zodiac··on Some Junk Theorems in Lean
Here’s a good document defending the merits of this design. https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
zodiac··on Ladybird passes the Apple 90% threshold on web-platform-tests
No browser passes 100% of WPT, the leader is chrome which has about 1000 failing tests
zodiac··on Trump to impose $100k fee for H-1B worker visas, White House says
1400 x $100,000 is $140 million, not $1.4 billion
zodiac··on Planes in 3D Space
Interesting, in this representation a plane is represented by the point on it closest to the origin, right?
zodiac··on EU Probes Apple's Decision to Shut Down Epic's Developer Account
> Every time you install an open-source app, the developers are extorted by Apple with Core Technology Fee of €0.5 each

I don't think this is true? AIUI a developer can choose to operating using the "old business terms" even in the EU, in which case they don't have to pay the fee. https://developer.apple.com/support/core-technology-fee/ backs this up by stating that the CTF is an element of the "new business terms".

zodiac··on The "missing" graph datatype already exists. It was invented in the '70s
I'm curious about graph algorithms that are "higher order" than what the article describes - e.g. how does Datalog encode the fact that two graphs (given as two relation sets) are isomorphic? How do I write a graph isomorphism algorithm in Datalog, or e.g. enumerate all graphs that have 6 vertices?
zodiac··on Python datetime pitfalls, and what libraries are (not) doing about it
Something like "schedule a reminder to stop using the computer at 10pm so I can sleep by 11pm"? Since I want to sleep at 11pm local time every day
zodiac··on AlphaGeometry: An Olympiad-level AI system for geometry
The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.
zodiac··on A copy-and-patch JIT compiler for CPython
I think there’s syntactic ambiguity whether “faster” modifies “generates” or “code”
zodiac··on Ask yourself dumb questions and answer them (2020)
I read mathematics on screens but when it comes to working out exercises etc I still prefer to do it with pen and paper, so I prefer succinct notation.
zodiac··on Superrational
I didn’t really get that joke, could you explain it?
zodiac··on The Art of LaTeX: Common mistakes and advice for typesetting proofs
The “except for math” part is doing a lot I think. There’s a huge amount of work needed to get rendered math to look as good as latex’s and I’m not sure CSS (as an example) is expressive enough to get this done
zodiac··on Maids trafficked and sold to wealthy Saudis on black market
“Give us your passport or we’ll fire you / won’t give you this job”
zodiac··on Algorithms for competitive programming
I wish discussions of such site didn't inevitably become discussions about software engineer interviews. It's a really nice site created by volunteers and I've often had it been the only decent resource online for a particular topic, if you want to use it as a reference their "terse but accurate" style for the prose and the compact working C++ code is really nice. And it covers some topics (e.g. treaps) which I've never seen appear in software engineer interviews.
zodiac··on Timing of daily calorie loading affects appetite and hunger responses
Could you please define “strategy” such that those people you refer to aren’t “following a strategy” but someone who doesn’t eat breakfast is “following a strategy”?

I eat breakfast when I’m strength training and don’t when I’m not, I’m not obese (16% body fat by dexa scan), so is skipping breakfast a “strategy”?

zodiac··on Timing of daily calorie loading affects appetite and hunger responses
What makes skipping meals a “strategy” while your meal eating habits is (presumably) not a “strategy”?
zodiac··on Edge Case Poisoning (2020)
The article gives one example - find out if a recipe has ingredient X. You could also imagine "find all recipes (from a cookbook) that are vegan", or "find all recipes I could follow given the contents of my fridge", etc.
zodiac··on Mainnet Merge Announcement
I agree with your 3rd, 4th, and 5th sentences, but not with your 1st and 2nd. Assuming a large number of independent validators, the Nash equilibrium is close to "there is no equivocation, hence no slashable evidence, hence no incentive to run a slasher node". (Remember that Nash equilibrium implicitly assumes that agents are not allowed to cooperate with each other). Suppose some fraction of the validators are deviating from this equilibrium by doing lots of equivocation, now there is an incentive to run a slasher node. So what this modelling suggests is that in the real world, we can have a small number of slashers and a large number of validators, and the security comes from the fact that anyone could be a slasher (it's OK that the number of people who actually are is small). But we cannot conclude that "it's OK to have a small number of validators, as long as anyone can be a validator".
zodiac··on Mainnet Merge Announcement
> Which sure sounds like a decentralized process that is ultimately just centralized around the ETH foundation at the end of the day.

The validators need to be decentralized (i.e. prevent "harmful collusion"), but the slashers don't need to be in the same way (as long as the validators are).

zodiac··on All Algorithms Implemented in Rust
Depends on what you mean by "best". For e.g. comparison-based sorting will already cost O(n log n) time but the HashMap solution will run in O(n) HashMap operations.
zodiac··on There’s no speed limit (2009)
The chord is D-flat dominant 7

It’s the same example as on the wiki page for “tritone substitution” - ‘For example, in the key of C major one can use D♭7 instead of G7.’

zodiac··on Python Standard Library changes in recent years
I think the problem is that the first separates words by underscore and the second doesn’t
zodiac··on The big six matrix factorizations
Maybe the_svd_doctor uses flop/s to describe hardware, like you said
zodiac··on MVC frameworks aren't dinosaurs but sharks
50ms is under human detection?

maybe 50ms is under the "conscious detection" threshold (debateable, IMO...) but it will definitely feels "laggy"

zodiac··on Apple must pay a man $1,000 for not including a power adapter with new iPhone
Conversely, I did not like the old system where I would buy a new phone and get a new wall wart which I would proceed to toss into a drawer (since the old wart still works fine)
zodiac··on Ask HN: When did 7 interviews become “normal”?
> This is one of those tricks you just have to memorize and it's very hard to come up with the solution in 30 min.

Maybe that particular solution is hard to come up with, but you can solve the problem without any "tricks", just basic principles. I'll try to explain which principles I'd use using python.

You can start with the trivial O(N^2) solution:

  def has_2sum(lst, target):
    # returns whether there are 2 (not necessarily distinct) elements in `lst` which sum to target
    for a in lst:
      for b in lst:
        if a + b == target: return True
    return False
First principle is runtime analysis. The runtime is O(N^2) because the inner loop is O(N) and runs N times. So we can try to speed up the inner loop. Second principle is to rewrite what the inner loop body as a function of the loop variable b.

  def has_2sum(lst, target):
    for a in lst:
      for b in lst:
        if b == target - a: return True
    return False
Third principle is pattern recognition for common functions: the code is equivalent to

  def has_2sum(lst, target):
    for a in lst:
      return (target - a) in lst
Fourth principle is to know which data structures support membership query. If you thought of hashtables, you get the O(N) solution.

  def has_2sum(lst, target):
    set_lst = set(lst)
    for a in lst:
      return (target - a) in set_lst
If you thought of sorted list, you get an O(N log N) solution.

  import bisect
  def has_2sum(lst, target):
    sort(lst)
    def contains(x):
      # equivalent to `x in lst`
      i = bisect.bisect_left(lst, x)
      return (0 <= i < len(lst)) and (lst[i] == x)
    for a in lst:
      return contains(target - a)
If you thought of `sortedcontainers.SortedList` (a third-party python package), you get an O(N^4/3) solution (analysis: https://grantjenks.com/docs/sortedcontainers/performance-sca...)
zodiac··on Two Vexing Problems in Functional Programming
If you used the State monad for the author's interpreter example, and you did it in Racket (your "state of the world" is a cons-list), what would be the run-time of the resulting interpreter? Similar question for streams (although I'm not that familiar with streams, so I don't know how they would apply here, or if they can be implemented without changes to the base language)
zodiac··on Two Vexing Problems in Functional Programming
That's a good point.

I wonder if the problem is that efficient persistent arrays aren't in racket's standard library (there are some third-party libraries implementing them though). Since racket isn't a "pure FP" language, they include cons-arrays and mutable vectors, and I imagine they felt that there wasn't a need to include efficient persistent arrays in addition to those.

Page 1 of 27Next →