3 ms·
> This is wrong because it depends on the language. The behavior depends on the implementation but if you are meant to return the first character in the string
by pka 10y ago
> This is wrong because it depends on the language. The behavior depends on the implementation but if you are meant to return the first character in the string and the string has no characters then you should return an empty string if provided a string with no characters.
How? The type is:
takeFirstChar :: String -> Char
There's no such thing as an empty char. Your get_first_letter essentially has the type:
get_first_letter :: Either Null String -> Either Null String
Which doesn't guarantee anything and is arguably a lot worse than just:
get_first_letter :: NonEmptyString -> Char
This is why you can't have proven code in a lot of languages, because they permit you to lie about the actual types. From there, any proof is invalid because it is based on invalid propositions.
Dependently typed and other languages do not allow you to lie about the types (for example, a value can't be null unless this is reflected in the type; you can't throw exceptions or do IO unless this is reflected in the type, etc), hence a well typed program in such a language is a valid proof. You can not implicitly cast between types, i.e. a function like:
cast :: a -> b
doesn't exist.
A function like print actually has the type:
print :: String -> IO ()
Which tells you that it is doing IO. You can't call such a function from a pure function for example, the types wouldn't permit it.
> Also, you are assuming the implementation of neString is correct. What if that has a bug? Again, just because your passing your data around the correct way doesn't mean the correct things are happening with it.
I was simplifying, but neString would actually have a type similar to:
neString :: String n -> Maybe (String (n != 0))
where n is the length of the string. Notice, the length is encoded in the type! A wrong implementation (one that returns i.e. Maybe (String 0)) will not type check.
But yes, you can have errors in your proof, no doubt. But these are specification errors, which there's no way to get around. What a proof guarantees is that there are no errors in the implementation of your specification.
- gravypod 10y agoOk so if you are given a specification and you use formal methods throughout and it doesn't conform to the specification you were provided with at the end you have made an error. The specification is not at fault here. 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. I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong. Implementations cannot be judged just because they accept the correct types. For instance, if I am told to write a function to predict lottery numbers and do the following LoteryNumberType get_lottery_number :: LotteryNumberType 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. They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case that a function can return which was already being done before formal methods where an idea. You can't say a program will have no bugs because the types check out. Is that what you are saying? Your code's types match in all uses -> this means there are no bugs -> this means I don't need to test my code? Is that really what you think?
- pka 10y ago> 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 function 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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Primality.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...