1. 19
  1.  

  2. 6

    Great article. However, whenever anyone talks about contracts I feel compelled to add that, although testing their enforcement is valuable, their primary value comes from a couple of other things:

    1. Documentation. Contracts should be seen as part of the function signature. When you decide to use a function, you should immediately be thinking how you know, for instance, whether the value you are passing to a function is non-negative.

    2. Aid to a static checker. Sometimes a checker can tell you for certain that a value can never be negative.

    3. An invitation to simplify. If the preconditions start getting complicated, it’s worth revisiting your factoring to see if you can simplify them. Sometimes that leads to an easier to understand solution.

    Apologies for the rant. I just feel that this gets lost sometimes when people start to use contracts as tests. Great article.

    1. 3

      Funnily enough, I’ve seen the exact same objection brought up with tests! A lot of TDD advocates say that it’s nice to have a regression suite, the real value of TDD comes from the documentation and improved design. I’ve seen it also with formal methods: it’s important to have the verification, but a lot of the value comes from the documentation and system understanding.

      Not saying that contracts don’t also have huge benefits for documentation and design, or even that those are more beneficial than the testing benefits. Just find it interesting how, in general, people are antsy thinking about correctness tools as being about correctness vs being about holistic design techniques.

      Apologies for the rant. I just feel that this gets lost sometimes when people start to use contracts as tests.

      I wish more people ranted like you do.

      1. 2

        Thanks. I really think both are important. I’m just doing the typical thing of providing counterpoint. Re correctness, I did this talk which kind of points to some dynamics of correctness and the ways we can arrive at. Really enjoy your posts. Great to see the ones related to J in particular.

    2. 2

      I’m glad you wrote this post! I’ve been wanting to find the time to do this, but just haven’t had a chance to do it yet. The idea looks soo promising – about the only thing wrong with it is the lack of good contract support in most languages.

      1. 2

        I’ve been meaning to play with the runtime contracts in frama-c for C code, seems like it might work nicely at least on the C end.

        1. 2

          Yes! ACLS looks amazing. I think the biggest problem might be the fact that you can’t take advantage of contracts for the code you integrate with. This seems to be not unique, though.

          Additionally, I guess it’s the case that contracts can’t really take the place of memory safety lnguage features in all cases. In the simplest case, in dev mode (where contracts are checked), you ensure that malloc returns a valid pointer. But in production mode, that assertion would be gone. Additionally, since malloc doesn’t have a standard place to store information about the size that was allocated, you can’t assert bounds checks.

          You can, importantly, check for overlapping pointers, which is cool.

          Do the ACLS contracts work with var args?

      2. 2

        I’m a big fan of property checking, but find it a little painful in dynamically typed languages, since we need to pass around generators explicitly. One reason Haskell’s QuickCheck is really nice to use is that a few rather simple things end up complementing each other:

        • A “default” random generator can be defined for any type (e.g. instance Arbitrary Customer where ...)
        • Default generators can be defined for composite datatypes, e.g. a generator for List t which automatically uses the generator for t (e.g. instance (Arbitrary t) => Arbitrary (NonEmptyList t) where ...)
        • Type inference can figure out what type a value has to have, and the type class mechanism will figure out the default generator to use for that type

        This means our properties are often as simple as e.g. printParseInverse x = parse (print x) == x

        The other annoyance of property based testing is crafting generators to satisfy some precondition. This isn’t so difficult in Haskell due to the culture/best-practice of trying to write total functions: if a function needs the input data to have some particular structure, that should be encoded in the type. On the other hand, if the input type doesn’t encode some precondition (e.g. because it would be too tricky to represent) then, culturally, we’d usually say that values violating the precondition are still valid, since the function’s type claims to accept them, and hence it’s up to the function to handle them in some way (e.g. with a Maybe result).

        Hence with QuickCheck we can normally make do with the default generators, and have Haskell do all of the plumbing to make that work. The only reason to avoid default generators are those times when they give poor coverage of the cases we care about.

        1. 3

          On the other hand, if the input type doesn’t encode some precondition (e.g. because it would be too tricky to represent) then, culturally, we’d usually say that values violating the precondition are still valid, since the function’s type claims to accept them, and hence it’s up to the function to handle them in some way (e.g. with a Maybe result).

          I think there’s some cases where what you want isn’t easily specifiable in many type systems, for example “two numbers that are not equal”. If it’s on a helper function, the main function should have already taken care of the invalid case, such as by returning an error instead of going through with the computation. In that case, violating the helper’s precondition is definitely a bug in the main function, and we should error.

          1. 2

            I think there’s some cases where what you want isn’t easily specifiable in many type systems, for example “two numbers that are not equal”.

            Of course. The reason I mentioned “culture” is about how we handle violations, and where we place the blame. In my experience, the “Haskell culture” would be the following:

            If it’s a function which can be imported from elsewhere, then it should never “go wrong”. The function is responsible for checking that the precondition is satisfied, and if it doesn’t check then it’s a bug. The easiest way to handle blame is to have a Maybe return type, and return the value Nothing if the check failed. Since the caller gave us dodgy arguments, they have to deal with the Nothing case. Callers might use a partial function like fromJust to extract the answer if they’re confident that the arguments they give will always work.

            If the function isn’t part of the public API, but it is widely used inside a library/application, then it should usually follow the rules above.

            If the function has a very narrow scope, e.g. it’s a helper defined in a let or where block, then it’s fine to be partial and assume valid arguments will be given. Any problems are the fault of the enclosing function (of which the partial function is just one part).

            For example, we might have the following function which requires non-equal arguments:

            dodgyCalc :: Int -> Int -> Rational
            dodgyCalc x y = 2 % (x - y)
            

            We could expose this with a Maybe:

            safeCalc :: Int -> Int -> -> Maybe Rational
            safeCalc x y = if x == y then Nothing else Just (2 % (x - y))
            

            Or we might give it a narrow scope:

            outerFunc :: Int -> Rational
            outerFunc n = dodgyCalc n (n + 1)
              where dodgyCalc x y = 2 % (x - y)
            

            There are of course exceptions, like when checks are expensive. Even in these situations it might make sense to come up with a “safer” API over the top, e.g. providing a bunch of callbacks and having them plumbed together in a way which either guarantees the precondition, or only checks it once instead of repeatedly.