Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
creata
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
54 ms
·
721.
▲
Wadler: Type Classes
(homepages.inf.ed.ac.uk)
2 points
by
creata
5y ago
|
0 comments
722.
▲
by
creata
5y ago
Judging by the getting started guide[0], they thankfully haven't forked Rust or anything, this is all about windows-rs[1], a Rust library for conveniently accessing the Windows API. [0]: https://docs.microsoft.com/en-
723.
▲
by
creata
5y ago
> contrary to what they blowhard they response time to keys is very large They state explicitly on their README that they're measuring throughput, not latency. Besides that, all three of your complaints are true as far as I'm a
724.
▲
by
creata
5y ago
> Blaming technicians for the negative externalities of their industries is a dark path. Disagree. > Are we going to blame lawyers who defend rapists? No, because I want there to be someone who defends that rapist's rights. In co
725.
▲
by
creata
5y ago
> but what about all those sites that don't have a strong commercial tie-in? Surely it's okay for sites that "don't have a commercial tie-in" to stick with untargeted ads? I just think that building a giant stalk
726.
▲
by
creata
5y ago
And the site seems to be written with Scribble[0], so that's at least two interesting choices of tools. [0]: https://docs.racket-lang.org/scribble/
727.
▲
by
creata
5y ago
Looks like that that's not a valid monad in general.[0] And also, I feel like it's a stretch to say that "almost all specific monads" are traversable. [0]: https://stackoverflow.com/questions/4228487
728.
▲
by
creata
5y ago
Ha, sorry, my comment was way too sarcastic. And yes, that looks to be what happened here.
729.
▲
by
creata
5y ago
You're right. To be clearer, the emphasis was on making it too easy to specialize: people don't just stop at maps and filters, they specialize everything , and that can have a significant impact on compilation times. For exampl
730.
▲
by
creata
5y ago
> It doesn't compose with other abstractions But monads don't compose with each other, do they? I thought you needed something more (monad transformers, algebraic effects, etc.) to get things to compose. Or maybe you meant some
731.
▲
by
creata
5y ago
Nice! Out of curiosity, if the iterators weren't of the same type (e.g. one was an iterator over the values of a hashmap and the other was over the items in a list) what would you have used instead of for _, m := range maps { .
732.
▲
by
creata
5y ago
> switched to external because that was much more conducive to optimisations Source? I thought conventional wisdom was that internal iteration was much easier for compilers to digest.
733.
▲
by
creata
5y ago
Might you be looking for https://doc.rust-lang.org/std/iter/fn.from_fn.html ?
734.
▲
by
creata
5y ago
Alright, if it's not too much trouble, can you show me what the equivalent of the following code would be in Go? I think this is extremely clear as-is, but I'd love to see how you can apparently make it even clearer by avoiding it
735.
▲
by
creata
5y ago
> Java doubling down on the collection APIs without introducing monads explicitly for users. I'm not necessarily disagreeing with you, but how has that backfired for Java? It seems as popular as ever, and I don't hear many peop
736.
▲
by
creata
5y ago
Here's my understanding: to get higher-order function calls to compile to fast code, you need some kind of compile-time code expansion: templates in C++, specialization in Haskell, monomorphization in Rust, etc. But if you make it t
737.
▲
by
creata
5y ago
> the site’s deliberate inaccessibility to visually impaired people Can you expand? I naively thought that a site with markup as simple as HN's (zooming is flawless and it even works without JavaScript) would be very accessible to
738.
▲
by
creata
5y ago
Don't SMT solvers output proof objects so that the results can be easily independently verified?
739.
▲
by
creata
5y ago
Believe it or not, sometimes you want to raise awareness about something that would otherwise be hidden behind a kebab menu and rendered entirely clinical. I don't think this is the sound criticism you intend it to be.
740.
▲
by
creata
5y ago
Mind explaining (a) precisely whom you're talking to in your second paragraph, (b) how you inferred that they're running from their problems, and (c) what those problems are?
741.
▲
by
creata
5y ago
Sorry, I haven't really thought about the specifics. Are you insinuating that these questions are insurmountable?
742.
▲
The Programming Languages Zoo
(plzoo.andrej.com)
147 points
by
creata
5y ago
|
13 comments
743.
▲
by
creata
5y ago
> Are you thinking of something else? I think the point is to contrast them with dynamic arrays --- linked lists, unlike arrays, are persistent data structures, which does make them easier to reason about. > Also, the common definitio
744.
▲
by
creata
5y ago
Why not just set an arbitrary threshold on how big you need to be before interoperability law applies to you? After all, people are only forced to interoperate with you when you're sufficiently big. > I just don’t see how the law ca
745.
▲
by
creata
5y ago
Let's read the original comment: > Some years back, I used to be the proud owner of "libgoliath.so", but then they suddenly decided to hike the price to IIRC Euro 80,- per year (either that, or prove that I have a Somalian
746.
▲
Compiling Tree Transforms to Operate on Packed Representations (2017) [pdf]
(engineering.purdue.edu)
6 points
by
creata
5y ago
|
0 comments
747.
▲
by
creata
5y ago
Wrt your update, > The idea that you can formally verify such a sequence of claims is .. mind boggling. Eh, if you're convinced that something's correct, it's not too mind-boggling that you can also explain it to a compute
748.
▲
by
creata
5y ago
This is all a bit vague, so I may be misinterpreting here. But in the given example, the proof must also prove that at each step the set is getting strictly smaller, so the computer still only has to check that the proof is correct. That is
749.
▲
by
creata
5y ago
> Every program can be made into a proof I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to
750.
▲
by
creata
5y ago
> Why should there be a tool to verify a general theorem? We want to verify proofs, not theorems. And that's far from "theoretically impossible."
More ›