A Maybe Dictionary on S7
In s7contract: Behavioral Contracts and Generative Laws for 'S7'

knitr::opts_chunk$set(collapse = TRUE, comment = "#>")
knitr::read_chunk(
  system.file("examples", "maybe-laws.R", package = "s7contract")
)

This S7 dictionary stores pure and bind as functions. Just(value) carries a value; Nothing() represents absence. An interface checks operation availability, while laws state the required behavior.

The dictionary

pure wraps a value in Just. bind passes a Just payload to a function returning Maybe, and propagates Nothing without calling that function.

Binding Nothing leaves the second callback unevaluated:

Generated values and functions

The input domain is Nothing or Just containing one integer from -10 to 10, with equal constructor probabilities. Functions come from three equally likely families: always return Nothing, add an integer from -5 to 5, or retain values at least a generated threshold in that range. Integer ranges expand with size. These functions are total on the tested inputs and intermediate values, which stay between -20 and 20.

Function descriptions remain data in counterexamples. Shrinking tries earlier constructors and function families, then moves integer parameters toward zero. The interpreter constructs each function independently of the dictionary under test. Equality compares the observable constructor and uses identical() for payloads, so integer and double payloads differ.

Three laws, one suite

The Haskell 2010 Report, §6.3.6 gives the three monad equations. Writing pure for the unit operation and >>= for bind:

pure(a) >>= f              = f(a)
m >>= pure                 = m
(m >>= f) >>= g            = m >>= (x -> f(x) >>= g)

maybe_laws(dictionary) returns three ordinary laws. Each equation uses the same interpreted functions on both sides. Coverage labels describe reference outcomes of those functions, including absence at the input or after either function in a composition.

These laws test the generated families of functions and integer payloads. dict_bind() calls the dictionary under test; gen_bind() composes generators and their shrink trees.

A default that breaks the laws

This dictionary replaces every Nothing result with Just(0L). Its operations still satisfy the structural interface:

Associativity fails because the default allows a later function to run on one side of the equation. The reduced input keeps both function descriptions:

The same law and recorded parameters reproduce the failure:

The Haskell monad tutorial develops the distinction between type-class operations and their laws.