Posted: Mar 12, 2012 5:49 pm
by VazScep
mizvekov wrote:Yes. I came to use Fusion because of another boost lib, called Spirit, which is basically a Scanner / Parser library.
With it, you can very seamlessly create a parser from a BNF grammar, and have it generate an AST from the input with very little effort. It will normally build this AST from stl containers (or their boost equivalents) and tuples. And here Fusion helps because then you can use your own custom structs instead of tuples.
That's awesome. Even though they're such a simple concept, tuples are something I miss immediately when I go back to Java and C#.

VazScep wrote:Well it does get used implicitly in the cases where this would have no user visible effects, such as any assignment which would obliterate the original value anyway.
Or it can be used explicitly with std::move. In this case, you would be exposed to the original 'moved from' object.
There isn't much in the way of guarantees of in what state this object will be, except that they must be in a destructible state, ie the destructor will not segfault when it is called. Everything else is up to whoever implements the class to define what happens. But the STL classes are guaranteed by the standard to be left in sensible states, so for example a moved vector will be left in an empty state.
So as it is up to whoever implements it to define, you as a user at least will have the guarantee that the 'moved to' object will be in the intended state. You can assume that whoever wrote the class you are using either did not provide a move constructor or provided one which works.
Ugh. I misread you and thought the move semantics was something particular to lambda expressions. I think it makes sense now!

VazScep wrote:Well that depends on what you mean by "destructive member".
You can easily see what happens in the lambda case if you think about it's equivalent Functor.
So for example if you have this lambda:
Code: Select all
[b]() { b.destructive_method(); }

It's equivalent Functor will be something like:
Code: Select all
struct Lambda {
    const B b;
    Lambda(B &b_) : b(b_) {}
    void operator()() { b.destructive_method(); }

Whereas if you had:
Code: Select all
[b]() mutable { b.destructive_method(); }

The equivalent one is:
Code: Select all
struct Lambda {
    B b;
    Lambda(B &b_) : b(b_) {}
    void operator()() { b.destructive_method(); }

Notice how the constness of b differs between these two.

Now, if you had B defined as something like this:
Code: Select all
struct B {
      int val;
      void b.destructive_method() { val = 0; }

The first lambda example and it's equivalent Functor would both fail to compile, because destructive_method is not a "const" method.
What happens here is basically that methods in a class take a hidden parameter that is passed implicitly, called the 'this' parameter.
It is as if you had the below in C:
Code: Select all
void destructive_method(struct B *this) { this->val = 0; }

And when you try to call it by passing a const pointer to the 'this' parameter, it fails to compile because the parameters type cannot be implicitly casted.
You can fix it by doing the below instead:
Code: Select all
void b.destructive_method() const { val = 0; }

which is equivalent to:
Code: Select all
void destructive_method(const struct B *this) { this->val = 0; }

And then it will continue compilation, but fail again on "val = 0", because it will try to do "this->val = 0;" with 'this' being a const pointer, which is not allowed.
But the question then becomes, can this method be destructive even if it's pointer to it's own instance is const?
The answer is absofuckinglutelly yes, that method still has access to global data, which can be and is usually declared as non-const, it can still call OS APIs and such.
And it can even do something evil like:
Code: Select all
void b.destructive_method() const { const_cast<B*>(this)->val = 0; }

So anyway, it is up to whoever writes the class to decide what happens, and if that person wants to be a raving lunatic, the type system will not stop him.
But in general, no sane library will do something like this.
Great stuff! Cheers for the explanation. I had a feeling it had something to do with constness, which is another thing that I think C++ gets right compared to its "successors". Of course, since I started functional programming, my attitude has been towards const and immutability by default :grin:

Okay great, much better, anyway thank you again, I will try playing with it a little.
You'll find it a real pain to do any proofs. The biggest headache is the fact that you can't write things like:

Code: Select all
1) P  (assumption)
2) P => Q  (assumption)
3) Q  (MP 1,2)
4) P => (P => Q) => Q (1-3)

There's just nothing in the formal system which allows you to make assumptions like this and then discharge them at the end of a proof. And yet being able to do this makes things so much easier.

So the first thing you encounter in the proof theory of this sort of formal system is the "Deduction Theorem", which shows that any proof with explicit assumptions can always be translated into a proof which doesn't make explicit assumptions. And after writing my utilities module, the first thing I did was define a new proof language which allows for explicit assumptions, and then I wrote a "Deduction Function", which mirrors the Deduction Theorem exactly except that it is recursive where the theorem is inductive. This function transforms a proof in the new proof language into a true theorem from the logical kernel.