From: Patrick Browne
Sent: Sun, April 3, 2011 9:04:22 AM
...
2)My second question is more theoretical. It is stated by the author that type checking and excitability provide verification.
I don't know what "excitability" has to do with verification. Type checking in Haskell provides some degree of verification. Besides the basic guarantees that the function will actually return a value of the type the signature claims, more complicated types (often involving parametric polymorphism) can be used to enforce some higher level properties. Also, because Haskell is a pure language, which means all the arguments and results are explicit. In a language like Java, methods might also change variables elsewhere. This does not show up in the type, so just checking the types tells you less about whether a Java function might be correct.
In this case verification probably means checking that an instance is consistent with its type class. Does verification using these techniques in Haskell have any firmer logical foundation than say doing the verification in Java?
Yes. The type system in Java lacks parametric polymorphism, for one. The Haskell type system can often provide some guarnatees about correct operation of a function, especially through "free theorems" http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi There are stronger type systems in languages/proof assistants such as Coq or Agda, which really do let you prove anything you like about functions.
I am aware that Haskell uses inference for type checking, but is the net result superior to compilers that do not use inference?
It's the design of the type system which produces good results. It would still tell you just as much about your program if there was no type inference, but it would be annoying to have to write out so many types. Even languages like C or Java do some type inference so you don't have to write down the type of every subterm of an expression - it's int x = f(12 * y + z); not int x = (int)f((int)((int)((int)12*(int)y)+(int)z);
Also, is Haskell execution based purely on logic?
I'm not entirely sure what this means either. Evaluation expressions is pure and functional and can be done by rewriting or graph reduction. There are also things like threads and IO which are more imperative. Evaluation is certainly not based on logic in the same sense as Prolog - there's no unification or backtracing. Brandon