There's a mathematician in your compiler

>> my understanding is if you deduce something true from an assumption it means nothing.

> Your understanding is not complete.

> If you start from a set of assumptions and perform a series of logical deductions to reach a conclusion, you have proven that given the assumptions are true, the conclusion is true. You have a proof of correctness under the assumptions.

04091948 is completely correct here.

If you assume P and prove Q, then you've proven that P implies Q.

If you assume P and prove True, then you've proven that P implies True. This is the same thing as proving nothing, since everything implies True.

It's the article that has it backwards. You can deduce true from any premise. In terms of the Curry-Howard isomorphism, I can write a program from any input to the one-element type by throwing away the input and returning the one element.

I think the previous comment was alluding to "resolution", where you prove a statement true by assuming it is false, and then deriving a contradiction. That only works in classical logic, though.

This interpretation is not compatible with the text of the article:

> If you need a quick refresher on logical True and False, here it is: The logical proposition True simply represents something that is true, like the statement 1 < 5. Any true statement like that by definition implies True. If we can start from an assumption and perform a series of logical deductions and reach True, then we know our original assumption is True, that it is provable. Conversely, any statement we know or can prove to be wrong (such as "bananas are a myth") implies False. If we can reach False at the end of a series of logical deductions from an assumption, our assumption is incorrect.

Showing that P implies False is a valid way to show that P is false itself. But showing that P implies True isn't a way to show that P is true. If you run things in the other direction, showing that P is implied by True really is a valid way to show that P is itself true, but showing that P is implied by False is not a way to show that P is false -- everything is implied by False.

> That's not the case, even without axioms if you start at A and deduce B then this proves that "A => B".

As I already pointed out in this thread, you're not right here. It is true that if you start at A and deduce B you've proven A ⟹ B. But if you're deducing something true, it's not necessary to start with A. If B is true, then A ⟹ B for all A, so you've proven nothing you didn't already have. It is quite literally correct to say that "if you deduce something true from an assumption, it means nothing".

You can see a nice visual illustration of the meaninglessness of the premise by completing the proof of "A→B" from "B" at http://incredible.pm (session 2)

Haskell lets you express that types unify: `a ~ b` says that `a` unifies with `b`, and similarly `Int ~ b` or `Bool ~ Char` (though the last one is clearly false).

But there's no equivalent for non-unification - `a /~ b`. You can sort of hack it by asking the compiler "do these types unify right now", and then negating the response you get, but that doesn't work for types which eventually unify, but just fail to at the moment.

A good example is with non-injective type functions. To show `Maybe a ~ Maybe b`, you can exploit the fact that `Maybe` is an injective type constructor to simplify the problem to deciding if `a ~ b`. But if you have an ad-hoc type function which is not injective, say `Foo`, then it's possible that `Foo a ~ Foo b` even if `a /~ b`. It's worse if you have two different type functions - `Foo a ~ Bar b`. Those types fail to unify immediately because `Foo` is definitely different to `Bar` - but depending on the final values of `a` and `b`, the types they result in may unify.