Haskell programs as specifications
Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs: 1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2. 2)My second question is more theoretical. It is stated by the author that type checking and excitability provide verification. 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? I am aware that Haskell uses inference for type checking, but is the net result superior to compilers that do not use inference? Also, is Haskell execution based purely on logic? Regards, Pat This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
On Sunday 03 April 2011 16:04:22, Patrick Browne wrote:
Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs:
1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2.
Only took a short look, but that'd probably be because it's wrong, t1 should give True for both. You have a road r from a to b and a car c at a. Then after you move the car along the road, it will be located at b, regardless of whether it's a one- way road or traffic may flow in both directions.
Daniel, I think that the definition of other in Link makes bi-directional travel possible in prog1. The function other takes an edge and the first node and returns the other (second) node of that edge. So we can begin our journey at the end and arrive at the start other (Edge (Node "end") (Node "start")) (Node "end") =gives=> Node "start" Or we can begin at the start and end at the end. other (Edge (Node "start") (Node "end")) (Node "start") =gives=> Node "end" So prog1 allows a car to go in both directions. Pat On 03/04/2011 15:39, Daniel Fischer wrote:
On Sunday 03 April 2011 16:04:22, Patrick Browne wrote:
Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs:
1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2.
Only took a short look, but that'd probably be because it's wrong, t1 should give True for both. You have a road r from a to b and a car c at a. Then after you move the car along the road, it will be located at b, regardless of whether it's a one- way road or traffic may flow in both directions.
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
On Sunday 03 April 2011 21:25:34, Patrick Browne wrote:
Daniel, I think that the definition of other in Link makes bi-directional travel possible in prog1. The function other takes an edge and the first node and returns the other (second) node of that edge. So we can begin our journey at the end and arrive at the start
other (Edge (Node "end") (Node "start")) (Node "end") =gives=> Node "start"
Or we can begin at the start and end at the end.
other (Edge (Node "start") (Node "end")) (Node "start") =gives=> Node "end"
So prog1 allows a car to go in both directions.
If you have edges in both directions, yes. But that's not the point for t1. In t1, you only have (Edge start end), and a car located at start. Then you (try to) move the car along that edge and check whether it is afterwards located at end. other (Edge start end) start =gives=> end, for both, one-way and two-way roads, so the move yields (Car end), its location is end and t1 == True.
Pat
On 03/04/2011 15:39, Daniel Fischer wrote:
On Sunday 03 April 2011 16:04:22, Patrick Browne wrote:
Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs:
1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2.
Only took a short look, but that'd probably be because it's wrong, t1 should give True for both. You have a road r from a to b and a car c at a. Then after you move the car along the road, it will be located at b, regardless of whether it's a one- way road or traffic may flow in both directions.
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
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
participants (3)
-
Brandon Moore -
Daniel Fischer -
Patrick Browne