That's again a myth. There is no dbus dependency. You can use dbus to do activation but you don't have to. Now, there is a dependency on libdbus which just means systemd is using the dbus serialisation format for its ipc (which, I repeat, don't have to happen over dbus).
It's because I'm not really precise (but neither is Lennart). Technically, libdbus is a part of dbus. It allows two applications to communicate with each other using the dbus serialisation and abstracts the transport layer. You can use it over a Unix socket and then it's just a serialisation format like any application using IPC would need. Then, using dbus is no more stupid than anything else. Actually, it's pretty clever as there already is quite a lot of tools understanding this format.
However, libdus is not what people usually talk about when they talk of dbus. The core part of dbus and what could bother server administrator is the message bus daemon which allows any applications to expose their functionalities and talk to any others. Now, systemd can use the message bus to allow applications to ask for service activation. But, it's not required and you can run the init system without it.
No, prices are not stupid. You didn't think through the whole problem.
The issue of cost and incentive with this kind of revolutionary innovation is real. The problem is simple. When you innovate, you bear alone the fixed cost of development while your competitors can copy and bear only the marginal cost. That's the reason the patent system exists and normally that's fine.
But, for a revolutionary invention, patents might not be feasible. Imagine you find a cure to cancer. Do you really think every governments and public opinion are going to let you be the sole producer for 30 years while people are dying ? Impossible. This creates a disincentive to push money towards a cure for private investor. Now, the idea behind a price is that if you find the cure, the price is going to cover your fixed cost (ideally more) thus investing is competitive again. Technically, as it fosters competition and you will only reimburse the finder, it supposed to generate more research than just spending the price money. Putting money aside for this kind of price was one of the main goal of the Bill and Monica Gates Foundation when it was founded (I think, they went back a bit because people wrongly assume its wasted money).
>Imagine you find a cure to cancer. Do you really think every governments and public opinion are going to let you be the sole producer for 30 years while people are dying ?
Isn't this the way medical patents work currently?
1 Bitcoin today and 1 Bitcoin in six months is not the same at all because you lose all the value you could have add from this Bitcoin during the six months so you have to discount it. That's called present value of money and that's one of the way companies manage their investments.
Theoretically, you have to use the real rate of return of your money and discount it on the time period. Of course, estimating the real rate of return is an art in itself. Considering value of bitcoin has been shown to be highly volatile, doing any semi-long term investment with it is basically gambling.
That's true, but you're talking "just" about time value (interest), sig's comment was about the volatility of BTC in terms of USD, different things. You'd also lose the interest if the product was denominated in USD or another major currency.
Most people are completely unaware of what CS researchers are doing in France because they don't work on things which the public finds ultra-sexy. Most of what they do and are good at has direct industrial application.
They made some pretty interesting things in type theory, language design (OCaml), proof (Coq), static analysis and certification (B-method, Frama-C, CompCert).
All of these is useful if you want to do safe embedded softwares for your planes, flight control softwares, automatic metros or nuclear reactor monitoring systems (which they do) but it isn't really easy to explain to the general public.
There is also a supposedly quite strong numerical modelling group working on nuclear deterrence but most of this stuff is classified. Let's also not forget that France still is a major arm dealer so you have some R&D done by private defence companies. Nothing comparable to the USA but you still apparently have some development in targeting, surveillance and interception (well, France has a world covering array network, I hope they at least try to use it).
Now, there is nothing particularly exceptional here. The situation is mostly the same in all publicly founded laboratories around the world. What France doesn't have very much is people doing frivolous stuff like email sorting or social network aka start-ups but that's another problem.
> It's a top-5 program internationally, so I take it to be quite good.
Most of the international rankings are heavily biased in favour of English speaking countries and particularly the USA (especially ARWU). It's mostly fine in sciences where all the important publications are in English. It's clearly dubious in the humanities. Beware this kind of claim.
Does someone have read the original article ?
I am curious about how the reader evaluation of potential risk was assessed.
Was there a control group which didn't see any comment to compare variance amongst this group to the other groups variances ?
How was the sampling done ? Were people with knowledge of science equitably balanced amongst groups ? How many of them was there ?
At which level is the variance difference amongst groups significant ? 2000 subjects can lead to average results depending of the sampling.
The jsonline article does quite a lousy job with details.
The title of the original article is "Science, new media, and the public" published in the Science Magazine. https://www.sciencemag.org/content/339/6115/40.
If you google the title you can find the full text.
I think you should probably read the links you post. They are close to claim exactly the contrary of what you say. As the Wikipedia article rightfully points, the difference is far less obvious than you make it seem.
The definition of an interpreter is generally broader than a main loop running instructions one at a time. For example, everyone seem to agree that Python is an interpreted language while python interpreter transforms the source code into an IR before passing that to its main loop. Truth is the line between what is a VM, an interpreter and a compiler is rather fuzzy.
The implementation of a process virtual machine clearly is an interpreter of a bitcode. Now, it's not entirely absurde to consider the couple JIT and VM taken together as an interpreter. Actually, this is clearly encompassed by the third point of the definition of an interpreter provided by Wikipedia : "explicitly execute stored precompiled code[1] made by a compiler which is part of the interpreter system".
To come back to the article discussion, I agree with the previous poster than the expression "source code VM" is kind of meaningless. Actually, the paragraph following is even plain wrong. The Dart VM executes bitcode not source file and Dart is JITed.
In the same way, I find it quite surprising that forty years after Hindley paper, people still confuse type annotated and statically typed but well, c'est la vie.
Have a read about V8 and the DartVM's architecture. V8, and the DartVM have a different architecture than IE's Chakra and Firefox's monkeys. They use a method JIT which initially generates very simple native machine code directly from the AST. The machine code includes instructions to identify hot code, which is re-compiled again from the AST. The optimizing compiler converts the source into an SSA form, and IR, but this is not byte/bitcode. This is what Bak et al are referring to when they call this architecture a "source code vm".
Lars Bak on channel 9:
Bytecodes are a silly thing in my mind.
They can be used for different things interpretation. But interpreters are really slow.
But they can also be used as a wire format, for instance in .net or java where that's what you ship over the wire.
In javascript the wire format is sourcecode, and for each function you have, inside the running javascript program, you have to cook up the source code again. So that is the primary representation.
So we just decided why not generate native code right away because the CPU is pretty fast.
[Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).
No, this nonequivalence applies directly to the typing of the lambda-calculus which was the topic of the original papers by Hindley and proven by Damas.
On the contrary, the value restriction is a part of the extended rules used for the typing of ML. It was introduced because ML isn't pure, it supports references. The value restriction is there to prevent them having polymorphic type. The rule is simple : syntactic values are the only things receiving a polymorphic type. What is a syntactic value ? To quote Geoffrey Smith notes on SML97 "Basically, a syntactic value is an expression that can be evaluated without doing any computation".
All this iss done in order to ensure type safety. Actually, if references could have a polymorphic type, the type system would accept incorrect programs such as :
let r : 'a list ref = ref []
let r1 : int list ref = r
let r2 : string list ref = r
r2 := "a"
let v : int = 1 + !r1
Which does not work because r, r1 and r2 are references to the same value.
Value restriction is a bit overkill. It rejects program which could be safely typed. Other solution to this problem exists. Actually, Standard ML used a different solution at the beginning (carrying information about the typed hold in a cell along) but it has other drawbacks. MLTon has a really good page about all that : http://mlton.org/ValueRestriction
You may be interested to know that the value restriction is not there to protect against unsafe programs. Rather, it is because polymorphic values get elaborated to functions after type inference, which produces some exceptionally unintuitive (but safe) behavior.
You could elaborate polymorphic values to type functions; and if you were compiling ML to System F or System F-omega, that is certainly what you would do. But in practice this might produce performance problems (I shouldn't have to call a function every time I use the empty list just because it has polymorphic type!). I must admit I'm not sure what SML and Haskell compilers actually do.
So in some sense the value restriction is there to prevent us from having to make the ugly choice between unsafety on the one hand, and inefficiency and unintuitive behavior on the other.
In the presence of polymorphism and mutable cells, value restriction (or a restriction thereof) is necessary to establish type soundness (ie that typed programs are safe), so I'd argue that it achieves this goal.
As for this explanation, I'm not entirely convinced. In the first example, seeing x as two different cells depending on the type is interesting, but I have trouble seeing how it is possible to express its semantics without keeping runtime type information. Is System F compatible with type erasure?
I'm getting a few detailed responses :) Unfortunately, I'm getting conflicting answers. I'm having trouble wrapping my head around why App+Abs couldn't be equivalent to Let in the absence of the value restriction.
It's because of the way the premises are written in regard to the type environment in the rules and how things are unified. It's directly linked to free and bound type variables and yes, it's complicated to understand.
If you look at the [Abs] rule, you will see in the premise "x : tau". Here, by definition, tau is non qualified. It represents a unique type. It's necessary monomorphic. Concretely, it means x will be bound to a type variable in the type environment and this type variable will uniquely be unified.
On the other hand, the premise for [Let] is e0 : sigma, x : sigma. Contrary to tau, sigma is qualified (polymorphic). So, it can be unified to a different type variable in different expressions.
I completely understand why it fails you. The way qualifier affects the unification process is quite complicated. I finally understood it only after having to write my own rules when I was implementing a type checker for my master thesis.
If you don't mind the formalism, read carefully the Wikipedia article paying particular attention to how tau and sigma are defined and to the paragraph about free and bound type variables. If you want something more practical, look at the Peyton Jones book I gave a link to in this thread. Part 9.5 is the important part but it's difficult to get without having read the whole chapter (eventually chapter 8 too). It 's still complex but far less abrupt than the Wikipedia article.
I understand the notation, but I don't understand the reasoning behind the Abs+App restriction (why does it have to be that way). I've been working on my own language and haven't gotten to the type inference yet, so maybe I'll finally understand once I go through it.
If the SPJ book is the one about implementing functional languages, then I've got a copy on my laptop I can peruse when I get home from work.
The difference between abstraction bindings and let bindings is that let variables are only ever bound to the value of a single expression, whereas the argument of a function may be bound to the value of any number of expressions.
This causes difficulties because the set of free type variables needs to be calculated in order for generalisation to produce safe type schemes, and that is tough to do for an unknown set of expressions.
I was not totally right in the my "uncle" comment. It has to do with the value restriction in the sense that it is where the distinction occurs (lambdas are never genezalized ; let-bindings are generalized for values), but the original HM system (without refs) indeed made this distinction.
I believe that if you don't do it and generalize everywhere, unification of types is harder or even impossible because everything has a type scheme.
This would look a lot like System F, for which type inference is undecidable, for example.
Yes. For example, if you generalize reference values, you can type ref [] as ∀a. (a list) ref, then store [4] to it, then retrieve a float from the head of the stored list, thus breaking the type system. It is a bit similar to array type variance problem that struck Java. One solution is to distinguish between syntactic forms that may allocate memory (eg, function applications) and the ones that can not (eg, abstractions, constants, variables), and only generalize the latter ones.
(Operationally speaking, the two forms (let and abs+app) are always equivalent, though).
I tend to disagree with you in the sens that Damas-Milner seems to me as the typical exemple of an algorithm which seems simple but actually have subtle implication and trade-off. Robinson's unification which is at the center of the algorithm is already made a bit tricky by quantification as soon as you have polymorphism. Then, some rules have actually deeper implication and trade-off than it seems (especially let).
For people interested in type checkers, there is a couple of really good chapters by written by Peter Hancock in a book available online : The Implementation of Functional Programming Languages by Simon Peyton Jones. They entirely cover the theory and there is a complete implementation in Miranda. Here is the link :
http://research.microsoft.com/en-us/um/people/simonpj/papers...
