jules

89 ms·

841.
by jules 11y ago
Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependentl
842.
by jules 11y ago
> How the hell does this work? It's easy, since it works as it always did. You check whether the list coming from the database has the correct size n, and then the type system knows that and lets you pass said list to a function tha
843.
by jules 11y ago
The reason is twofold. One, research into dependent types is still ongoing. Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is ex
844.
by jules 11y ago
> and now there are potentially two different instances to choose from in the other module [...] to preserve class coherence I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing.
845.
by jules 11y ago
The requirement to be globally unambiguous is the #1 wart of type classes. Rather than enforcing it with the compiler it would be better to make that restriction unnecessary. It should be possible to define a type class instance local to a
846.
by jules 11y ago
Linus could have chosen to work on improving SVN instead, but he did not. The decision to write a new version control system in the first place is part of what makes makes him so much more effective, not just pure programming ability.
847.
by jules 11y ago
Argument #1 does not really make sense, since by repeatedly applying the same logic it implies that engineers will work an infinite number of minutes each day. A variant of this argument that I've often heard is this: "My decision
848.
by jules 11y ago
While I agree that it's an annoyance, it's a very small annoyance. Since Julia has for loops and Julia ranges use the same 1-based convention you don't run into it often.
849.
by jules 11y ago
What's wrong with the sum of all ways of picking a term from each factor?
850.
by jules 11y ago
For what it's worth, I've ran into this a couple of times. Maybe it's just because I'm more familiar with 0-based indexing, but I think it's not just that. In every case the 0-based indexing had fewer (+1)'s an
851.
by jules 11y ago
Nice, and that generalizes neatly to n-space with exterior algebra / Grassmann coordinates.
852.
by jules 11y ago
The determinant of a linear map is its volume scale factor: any shape of volume V in the input space gets transformed to a shape of volume det(L)V in the output space. This makes a bunch of things easy to understand: - Why you can calculate
853.
by jules 11y ago
Why do you want to write? Do you really want to write? To me it seems strange to want to write about something, anything, but not knowing what to write about. I have the opposite problem: too many things to write about and too little ti
854.
by jules 11y ago
That's what retirement funds are for.
855.
by jules 11y ago
Actually, here in the netherlands most children bike to school by age 5, and continue to bike until they are no longer able to. My grandmother biked until 80, she never had a drivers license. Before age 5 children sit on their parents'
856.
by jules 11y ago
This is a common problem here in the netherlands. We've found some solutions. Buy a bike that doesn't look flashy. Spray paint some stripes of pink paint over it. Buy a big lock. Chances of theft go way down.
857.
by jules 11y ago
Why do you bike on sidewalks?
858.
by jules 11y ago
Those help but the thing that helps me most is to actively engage my rational brain instead of autopilot brain. Try to make it a habit to trigger your rational brain when your autopilot brain is making the decision to procrastinate, and the
859.
by jules 11y ago
Read more information dense texts.
860.
by jules 11y ago
Do you have any tips on the intuition behind the GA product and derivative? I follow the symbols but I can't get any intuition for what it means.
861.
by jules 11y ago
I enjoyed the idea, particularly around the observation that thousands of people are photographing the same statue when you can just look up a much better picture on the internet. I saw the censorship angle as a sidenote, and a warning that
862.
by jules 11y ago
Why is everyone missing the point? Yea sure this doesn't accurately determine whether a picture is original. Of course it's not practical. Of course you would not buy this. That isn't the point. This project is itself art.
863.
by jules 11y ago
> Model checking with 2 acceptors worked, but I gave up on model checking with 3 acceptors since it took more than an hour. Does anyone know how the TLA model checker works? I wasn't able to find this information. Does it use a SAT&
864.
by jules 11y ago
Many people just like to help out their classmates. People already share this information, just inefficiently.
865.
by jules 11y ago
Students want to know lots of info that is in blackboard, on the professor's personal web pages, and things that were said in the lectures, tips for exercises. In each lecture each student writes down: - What homework is due for the ne
866.
by jules 11y ago
The best option for Blackboard higher education is, IMO, fuck the decision makers, ignore the faculty, cater to the students. Let students edit all the info, faculty will get on board when they see students using it, decision makers want co
867.
by jules 11y ago
That looks much better, but most of what I said still applies. Too many pages, info that people actually need is missing or hard to get at. It looks like this is focused on middle/high school though, where that may not apply. For unive
868.
by jules 11y ago
There isn't anything missing, on the contrary, there's too much so that the things that people actually care about are not easy. Nobody cares about an "ecosystem of applications", or "out of classroom experience&quo
869.
by jules 11y ago
I just watched their promo video, and it's still terrible, but with a less ancient looking skin. Interesting how they can so completely miss the point.
870.
by jules 11y ago
Unfortunately this solves the wrong problem. The bottleneck isn't arithmetic, it's data movement. The number of transistors doing arithmetic is already a very tiny fraction of a modern chip. Reducing that tiny fraction to an even

More ›