Development With Types
Lots of folk seem to agree that one of the nice things about having a blog is that you can use it as a public whiteboard, to help order your thoughts on any given subject. I don't post all that often myself, but this isn't because my thoughts are already ordered. It's because I've long been in the habit of using a different technology for ordering
( Read more... )
Hah hah hah. Too late. If you don't want me to read it you shouldn't have it syndicated on planet.haskell.org.
I have to say, I'm rather flattered :-). I'm not at all like Dijkstra though! I never prove anything.
But the programming approach is basically right. Start by writing down data types and types of functions without implementations. As this starts to get more complex we check that the 'code' typechecks. So yeah, that level lets you think about the problem fairly abstractly and sketch designs quickly.
Then you can start implementing a few important functions and see that they typecheck. Again without having actual implementations of most functions.
When it comes to the implementations I generally work both bottom up and top down. Bottom up allows you to test things quickly in ghci.
If you're really a good Haskell hacker then at the same time that you're sketching the design you'll be writing the QuickCheck properties that these functions satisfy. This has a great effect on your understanding and will influence your deisgn. It also means you get testing for free when you complete the implementation.
Once you have a program with no more stubs you can check all the QuickCheck properties. Iterate until you've fixed the implementation or your understanding of the properties.
So most of the bugs not caught by the typechecker are caught by the QuickCheck tests.
Next step is to do the benchmarking setup (we need better tools for this - so far we've mostly rewritten this framework for each project). That is you take your initial prototype that passes the QuickCheck testsuite and you benchmark it. It'll probably be terrible since you designed it for clarity. Now with both correctness and performance frameworks in place you start to optimise the code. Each time you check that it made an improvement and that you didn't break anything.
For the binary serialisation lib we did recently we followed this simple methodology and took our initial prototype and made it 600 times faster. This is aproximately 100 times faster than the fastest python serialisation lib, and it's pure, and we know that it correctly roundtrips all the types we cover.
If you're really in the mood for getting things right then you can also write properties about the strictness of your functions and test them using something like StrictCheck. This amounts to something like QuickCheck but for partial values rather than total values.
Reply
Thanks for the stuff on using QuickCheck and benchmarking. Is this hacking methodology written down anywhere on haskell.org? If there are other proto-pozorvlaks out there, perhaps they could be saved some pain by being turned on to typeful prototyping early?
pozorvlak: If this hacking methodology is the sort of thing that you would have liked to have read earlier, what sort of title would it have needed to let you know that it was what you wanted to read? "Haskell hacking methodology"? "Agile development with types"? "Haskell types for perl programmers"?
Reply
I haven't seen anything saying this stuff explicitly on the 'net - I've had to work it out from other things I've read and conversations with you. I think it would be really useful to put it somewhere on Haskell.org - if you were trained in the type-first formal CS style of programming they teach at Oxford, it may seem as natural as breathing, but for largely self-taught programmers like me, I think it's far from obvious. And Haskell can be quite painful to use if you naively apply a hacking style learned on dynamic languages :-(
Reply
Leave a comment