So if it is preloading everything on a search result page, it means my data bill is going up for things I will not even look at.
A major reason I use Debian is that, as a user, I consider 90% of software lifecycles to be utterly insane and actively hostile to me, and Debian forces them into some semblance of a reasonable, manageable, release pattern (namely, Debian’s). If I get the option to choose between upstream and a Debian package, I will take the latter every single time, because it immediately has a bunch of policy guarantees that make it friendlier to me as a user. And if I don’t get the option, I will avoid the software if I possibly can.
(Firefox is the only major exception, and its excessively fast release cadence and short support windows are by far my biggest issue with it as a piece of software.)
I never really understood why short release cycles is a problem for people, but then I don’t use Debian because of their too long ones. For example, the majority of Firefox’s releases don’t contain user-visible changes.
Could you elaborate what your problems with Firefox on Debian are? Or why software lifecycles can even be hostile to you?
I’m with you. I update my personal devices ~weekly via a rolling release model (going on 10 years now), and I virtually never run into problems. The policies employed by Debian stable provide literally no advantage to me because of that. Maybe the calculus changes in a production environment with more machines to manage, but as far as personal devices go, Debian stable’s policies would lead to a net drain on my time because I’d be constantly pushing against the grain to figure out how to update my software to the latest version provided by upstream.
I’ve had quite a few problems myself, mostly around language-specific package managers that break something under me. This is probably partly my fault because I have a lot of one-off scripts with unversioned dependencies, but at least in the languages I use most (Python, Perl, R, shell, etc.), those kinds of unversioned dependencies seem to be the norm. Most recent example: an update to R on my Mac somehow broke some of my data-visualization scripts while I was working on a paper (seemingly due to a change in ggplot, which was managed through R’s own package manager). Not very convenient timing.
For a desktop I mostly put up with that anyway, but for a server I prefer Debian stable because I can leave it unattended with auto-updates on, not having to worry that something is going to break. For example I have some old Perl CGI stuff lying around, and have been happy that if I manage dependencies via Debian stable’s libdevel-xxx-perl packages instead of CPAN, I can auto-update and pull in security updates without my scripts breaking. I also like major Postfix upgrades (which sometimes require manual intervention) to be scheduled rather than rolling.
Yeah I don’t deal with R myself, but based on what my wife tells me (she works with R a lot), I’m not at all surprised that it would be a headache to deal with!
Every time a major update happens to a piece of software, I need to spend a bunch of time figuring out and adapting to the changes. As a user, my goal is to use software, rather than learn how to use it, so that time is almost invariably wasted. If I can minimize the frequency, and ideally do all my major updates at the same time, that at least constrains the pain.
I’ve ranted about this in a more restricted context before.
My problem with Firefox on Debian is that due to sheer code volume and complexity, third-party security support is impossible; its upstream release and support windows are incompatible with Debian’s; and it’s too important to be dropped from the distro. Due to all that, it has an exception to the release lifecycle, and every now and then with little warning it will go through a major update, breaking everything and wasting a whole bunch of my time.
Due to all that, it has an exception to the release lifecycle, and every now and then with little warning it will go through a major update, breaking everything and wasting a whole bunch of my time.
I had this happen with Chromium; they replaced the renderer in upstream, and a security flaw was found which couldn’t be backported due to how insanely complicated the codebase is and the fact that Chromium doesn’t have a proper stable branch, so one day I woke up and suddenly I couldn’t run Chromium over X forwarding any more, which was literally the only thing I was using it for.
Because you need to invest into upgrading too much of your time. I maintain 4 personal devices with Fedora and I almost manage to upgrade yearly. I am very happy for RHEL at work. 150 servers would be insane. Even with automation. Just the investment into decent ops is years.
For me there is an equivalence between Debian stable releases and Ubuntu LTE ones, they both run at around 2 years.
But the advantage (in my eyes) that Debian has is the rolling update process for the “testing” distribution, which gets a good balance between stability and movement.
We are currently switching our servers from Ubuntu LTE to Debian stable. Driven mostly by lack of confidence in the future trajectory of Ubuntu.
There is also a commentary on this from Joey Hess, one time Debian release manager (I think)
So this creates the function code from the types? I don’t understand how that works.
If I have Int -> Int -> Int how would that know I want the function foo bar baz = bar + baz and not foo bar baz = bar - baz?
It can’t. Your type is too general. Not sure what this specific plugin will do, but it will probably just come up with some expression that will have that type. Possibly the one you want – but probably not. :)
For example of types of functions where the types will only allow one, correct implementation, look up implementations of e.g. length-indexed vectors or red-black trees in dependently typed programming languages. It’s also interesting to look at the interactive modes for languages such as Agda and Idris where you can tell your editor “complete this expression” and it will do that (or tell you that it’s not able to, and what’s missing).
I think it is relying on the free theorems guaranteed by parametricity.
See Philip Wadler’s paper Theorems for Free!
I believe that these tools are not based on parametricity, merely on syntactic proof search (in essence, enumerating possible terms at this type, using techniques from the proof search literature). If you think about it, theorems-for-free does not actually help you generate code at arbitrary types.
Ok, thanks.
But I think the fact that this is possible is a side effect of the free theorems granted by parametricity.
Which explains why it is not possible to do this with a concrete type signature, as per the original question.
Abstract types and parametric polymorphism are a nice language feature that has several consequences. One is the existence of free theorems (technically, a nice denotational semantics in the categoy of relations), another is the possibility of having a restricted enough search space that blind proof search produces sensible/interesting program. Those two consequences are independent, I don’t think that you can claim that one is a “side effect” of the other.
“Theorem for free” is an interesting and thought-provoking and well-written research article, so people will easily share it and think about it. This is great! But it also result in some miscomprehensions (or at least exaggerations) about what the result says, which result in the article sometimes being cited in situations where it is not actually relevant (besides being in the same scientific domain as the work being discussed). I thought you may be interested a slightly more detailed picture of the technical details at play here.
Thanks for the clarification. As you say, this is stuff I know exists, but do not work with it daily so do not understand the full implications and shortcomings.
I am amazed at how many there are.