Hi–

Interesting project. I saw this in the docs:

Contracts in the form of preconditions and postconditions are part of the public interface for a module in the same way that function signatures and typespecs are.

Is the intention that pre/post conditions replace traditional typespecs when used or should they be considered supplemental? If they are a replacement, do they interact with Dialyzer at all? Also, the set-theoretic types, assuming they land, also offer a manner of contract with functionality ramifications, are there thoughts about how this library would relate to that future?

I’ve not looked much beyond a quick search through the docs. But these are the questions I’d need to understand for adoption.

Hi @sbuttgereit,

Contracts are not intended to replace typespecs or set-theoretic types; rather, they are complementary mechanisms.

Typespecs are evaluated at compile-time or with a static analysis tool such as Dialyzer, whereas contracts as implemented by Bond are evaluated at run-time (although they are attached to functions at compile-time so must be valid Elixir code).

The closest analogue to contracts in native Elixir is guard expressions for functions, which allow for making rudimentary “assertions” about function arguments. Assertions in Bond are much more powerful and are not limited to the pre-defined set of functions that are allowed in guard expressions.

fun <3

  @post is_hallo: result == :hallo
  def hello do
    :world
  end

in this case dialyzer is screaming at me already … but its MUCH easier to actually get the error in your face … than dialyzer warning about something that SHOULD fail … but never does. ref this thread where dialyzer warns about something that never fails Dialyzer warning from hell: no_return when calling erl_tar.create - #2 by jarlah

iex(1)> TestBond.hello()
** (Bond.PostconditionError) postcondition failed in TestBond.hello/0
|   label: :is_hallo
|   assertion: result == :hallo
|   binding: [result: :world]

    (test_bond 0.1.0) lib/test_bond.ex:6: TestBond.hello/0
    iex:1: (file)
iex(1)> 

its probably more valuable in the ecto example i described above

Thanks for the feedback @dimitarvp.

You might be right about stateful assertions becoming messy. I had been thinking about invariants as inherently stateful, and which describe properties of the state before and after state transitions. But as you point out, there is probably still value in stateless invariants that use only function arguments.

For example, consider a bounded stack with a capacity fixed at creation time. Such stacks do not allow new items to be pushed if the stack is already full. I can think of a few invariants that I would express at the module level, even for a purely functional, stateless version of such a stack (ignore for now how the stack variable binding could be injected into the assertions, I’ll come back to that):

@invariant size_limited_by_capacity: size(stack) <= capacity(stack),
           non_negative_size: size(stack) >= 0,
           fixed_capacity: capacity(stack) == old(capacity(stack)),
           full_implies_at_capacity: full?(stack) ~> (size(stack) == capacity(stack))

Many of these invariant properties could be expressed as postconditions on the relevant functions, but expressing them at the module level as invariants brings to mind a couple of possible advantages:

1. The invariants could be checked at run-time before and after every function call.
2. The invariants could be added to the @moduledoc in a similar way that preconditions and postconditions are already added to the @doc for functions.

The main complication that I can think of is that this scheme would probably only work for 1-arity functions that use the same name for the lone parameter. Otherwise, what would be the value bound to the stack variable in the invariant assertions?

I’m also not sure if the old expression in the fixed_capacity assertion in the invariant makes sense. If invariants are to be checked before and after function calls, the old expression would fail when evaluated before the function call (at least the way that old is currently implemented in Bond). I don’t think Eiffel allows old to be used in invariants, presumably for this reason.

Curious about your thoughts, or if you (or anyone else) have other ideas about invariants for purely functional code.

I added a new “Contracts in a Concurrent World” guide to the Bond docs, which discusses how to eliminate the need for stateful assertions:

https://hexdocs.pm/bond/contracts-and-concurrency.html

TL;DR - It’s the same old trick used for better testability: separate the pure functional code from stateful code.