4 ms·
There's a mathematician in your compiler
- ivanbakel 7y agoSuper impressed that you can develop type inequality in Scala. Haskell, the logical darling, can't do it in the general case.
- tiborsaas 7y agoCan you ELI5 type inequality?
- ivanbakel 7y agoHaskell 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.
- philzook 7y agoYou can achieve a certain amount of type disequality in Haskell. It isn't necessarily easy or sufficient for all purposes. There is a type family that returns a type level Bool for equality here. https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Equality.html https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-... There are some older techniques here http://okmij.org/ftp/Haskell/typeEQ.html http://okmij.org/ftp/Haskell/typeEQ.html
- Tarean 7y agoYou can do `(A == B)~ False` but that won't affect type variable unification. Pretty sure `/~` would break type class coherence under haskell's open world assumption?
- 04091948 7y ago> 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 is this a difference between mathematical and natural language? my understanding is if you deduce something true from an assumption it means nothing. you need to deduce something false and thus the negation of your assumption is true.
- auggierose 7y agoYeah, that's what you get when you let computer scientists do math :-D I hope it's just a typo, otherwise you should throw the article straight into the garbage.
- bregma 7y ago> 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. If you can go on to demonstrate your conclusion is false (say, with a single counterexample) then it will prove that at least one of your original assumptions is false. You now have some provably reliable knowledge .
- thaumasiotes 7y ago>> 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.
- deleted 7y ago[deleted]
- m23khan 7y agothis is a very interesting read.