Contract programming versus static type checking
April 11, 2007
A recurring argument against weakly typed languages is that the risk introduced by their lack of compile time type checking is so tremendous that no mentally sane developer should consider using a weakly typed language (such as Perl) to implement a piece of critical software (like, say, the guidance software of a nuclear warhead).
The common answer of weakly typed language zealots sounds like: static typing is just a special form of testing, and can be compensated with various methods for catching type exceptions at runtime, and they usually mention unit testing and test coverage (See Strong typing vs. strong testing by Bruce Eckel for a discussion on the subject). Aside from developer techniques, the language implementation itself provides some strong means of runtime checking, such as type inference, array boundary checks, etc. Every dynamic language implements a subset of those techniques.
One argument sometimes raised is that static type checker cannot catch all exceptions. Some exceptions will happen at runtime that no static type checker (at least in any of the major languages) could have foreseen, such as crossing array boundaries in C or failing in external code called inline from Python.
Those questions have been central issues at my work over the past year or so.
I develop a large financial accounting software that places pension saving into funds. The core of this software is written in Perl, which gives us all the advantages of high level programming, but at one cost: the lack of static type checking. The lack of types, in fact. Of course, Perl provides some type checking at runtime, especially on objects, but it is rudimentary.
The problem is: this software must not fail. If any technique can help us writing safer code, we try it. We use techniques such as systematic regression testing, test coverage, paranoid design, defensive programming, asserting everything, strict code convention, and more.
But after a while, I started wanting something to compensate for the lack of static type checking in Perl.
This need emerged from a fact: every subroutine in the code tended to start with a bunch of lines that simply asserted the subroutine's input arguments. Sometimes, similar assertions could be seen at the end of the subroutine, upon returning results.
That made the code heavy and hard to read. So I tried to move those assertions outside the subroutine's body, and place them into what in fact was a form of programming contract for subroutines. I would define a syntax for describing outside the subroutine a number of constraints on the subroutine's input arguments and return values. This formed a kind of contract. This contract is compiled at compile time into an anonymous subroutine (a bunch of code generated at runtime) that gets wrapped around the contracted subroutine. Each time the subroutine is called, its input arguments are checked against the constraints defined in the contract. The same happens when the subroutine returns. If an argument fails a constraint, a runtime exception is sent.
The idea has evolved under the pressure of practice and is currently mutating into a Perl module called Sub::Contract, hosted on sourceforge.
Along the way, I realised that I was in fact implementing in Perl5 something like the constraints or refinement types found in other languages like Perl6, Haskell or ML.
In fact, such contracts enforce a stronger form of type checking than static types, since contracts not only specify the type of arguments expected, but even their state.
Consider a function that takes one argument: a date, implemented as strings with the format 'YYYY-MM-DD'.
In Java (statically typed), this argument would have a type ShortDate, specified in the function's signature. In Perl (weakly typed) this argument would just be a scalar and you would have to explicitely check that it has a valid format. Or you would define a contract for this function, and specify in this contract that the functions expects one and only one argument and this argument must validate a constraint. An easy way to implement constraints is by using code references. In Perl, a constraint validating the date format 'YYYY-MM-DD' could therefore look like:
where is_shortdate is a subroutine that returns true if its argument is defined and matches /^\d\d\d\d-\d\d-\d\d$/.
Now, imagine that our function not only expects a date in argument, but further expects this date to be of the year 2006. In Java, you would have to write an assertion for that in the function's body. In Perl too. But if you use contracts, you would just refine the constraint into something like:
Which saves us one line of assertion...
Those *contracts* have proved to be very useful for catching runtime exceptions at earlier development stage. Though to be really efficient, this technique requires that the developer write unit tests and uses code coverage quite systematically.
Curiously, I have not seen contract programming used as an argument in the 'static vs. strong typing' discussion. Hence this post :)
My point here is that I believe that a lack of static type checking does not make a language less safe, provided that you use proper runtime checks. Function contracts are one of them.
Perl is evolving into an interesting direction in this respect: Perl6 will have types and roles (a kind of constraint), all of which enforce safer coding. I won't have to implement pseudo-contracts into the language anymore, they will be implemented in the language core, better, cleaner and safer :)
The common answer of weakly typed language zealots sounds like: static typing is just a special form of testing, and can be compensated with various methods for catching type exceptions at runtime, and they usually mention unit testing and test coverage (See Strong typing vs. strong testing by Bruce Eckel for a discussion on the subject). Aside from developer techniques, the language implementation itself provides some strong means of runtime checking, such as type inference, array boundary checks, etc. Every dynamic language implements a subset of those techniques.
One argument sometimes raised is that static type checker cannot catch all exceptions. Some exceptions will happen at runtime that no static type checker (at least in any of the major languages) could have foreseen, such as crossing array boundaries in C or failing in external code called inline from Python.
Those questions have been central issues at my work over the past year or so.
I develop a large financial accounting software that places pension saving into funds. The core of this software is written in Perl, which gives us all the advantages of high level programming, but at one cost: the lack of static type checking. The lack of types, in fact. Of course, Perl provides some type checking at runtime, especially on objects, but it is rudimentary.
The problem is: this software must not fail. If any technique can help us writing safer code, we try it. We use techniques such as systematic regression testing, test coverage, paranoid design, defensive programming, asserting everything, strict code convention, and more.
But after a while, I started wanting something to compensate for the lack of static type checking in Perl.
This need emerged from a fact: every subroutine in the code tended to start with a bunch of lines that simply asserted the subroutine's input arguments. Sometimes, similar assertions could be seen at the end of the subroutine, upon returning results.
That made the code heavy and hard to read. So I tried to move those assertions outside the subroutine's body, and place them into what in fact was a form of programming contract for subroutines. I would define a syntax for describing outside the subroutine a number of constraints on the subroutine's input arguments and return values. This formed a kind of contract. This contract is compiled at compile time into an anonymous subroutine (a bunch of code generated at runtime) that gets wrapped around the contracted subroutine. Each time the subroutine is called, its input arguments are checked against the constraints defined in the contract. The same happens when the subroutine returns. If an argument fails a constraint, a runtime exception is sent.
The idea has evolved under the pressure of practice and is currently mutating into a Perl module called Sub::Contract, hosted on sourceforge.
Along the way, I realised that I was in fact implementing in Perl5 something like the constraints or refinement types found in other languages like Perl6, Haskell or ML.
In fact, such contracts enforce a stronger form of type checking than static types, since contracts not only specify the type of arguments expected, but even their state.
Consider a function that takes one argument: a date, implemented as strings with the format 'YYYY-MM-DD'.
In Java (statically typed), this argument would have a type ShortDate, specified in the function's signature. In Perl (weakly typed) this argument would just be a scalar and you would have to explicitely check that it has a valid format. Or you would define a contract for this function, and specify in this contract that the functions expects one and only one argument and this argument must validate a constraint. An easy way to implement constraints is by using code references. In Perl, a constraint validating the date format 'YYYY-MM-DD' could therefore look like:
is_shordate($_[0])
where is_shortdate is a subroutine that returns true if its argument is defined and matches /^\d\d\d\d-\d\d-\d\d$/.
Now, imagine that our function not only expects a date in argument, but further expects this date to be of the year 2006. In Java, you would have to write an assertion for that in the function's body. In Perl too. But if you use contracts, you would just refine the constraint into something like:
is_shordate($_[0]) && substr($_[0],0,4) eq "2006"
Which saves us one line of assertion...
Those *contracts* have proved to be very useful for catching runtime exceptions at earlier development stage. Though to be really efficient, this technique requires that the developer write unit tests and uses code coverage quite systematically.
Curiously, I have not seen contract programming used as an argument in the 'static vs. strong typing' discussion. Hence this post :)
My point here is that I believe that a lack of static type checking does not make a language less safe, provided that you use proper runtime checks. Function contracts are one of them.
Perl is evolving into an interesting direction in this respect: Perl6 will have types and roles (a kind of constraint), all of which enforce safer coding. I won't have to implement pseudo-contracts into the language anymore, they will be implemented in the language core, better, cleaner and safer :)
