PKpka·Sep 22, 2016
> What you are doing is claiming types into and out of functions decide if they are functioning correctly. This is not the case at all.
When I say proof, I mean it in the mathematical sense. The Curry–Howard isomorphism [0] formalizes the relationship between (mathematical) logic and type theory. Unless you are saying mathematical logic is inconsistent (and thus every mathematical proof is invalid) this is absolutely the case.
The same way you can construct a mathematical proof that e.g. n is prime, you can can construct a type Prime n that proves that n is prime [1].
> I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong.
This is where your misunderstanding stems from. Continuing with the example from above, if you have a function:
makePrime :: n -> Prime n
the fun
Read the rest
ction can not construct (Prime n) if n is not a prime.
> If I call `get_lottery_number` by your logic it will always provide me with the real winning lottery number since the types check out. That is absolutely incorrect. Types can't prove functionality.
If you give me a specification that constructs predicted lottery numbers I could absolutely turn it into a type :)
> They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case
But you don't have proof that you are handling every case :)
> You can't say a program will have no bugs because the types check out. Is that what you are saying?
Yes, if the types correspond to the specification then there are no bugs. The specification can still have bugs though, but that's unavoidable. The thing is that you've proven the program does what you told it to do.
Once you stop thinking about types in the Java sense and start thinking about them as logical propositions it will all make sense. I provided you with a couple of links in the other comments and here if you are still interested.
[0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
[1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...