Module Preface_specs.Decidable

Decidable is a "Contravariant Alternative".

Laws

To have a predictable behaviour, the instance of Decidable must obey some laws.

  1. All Divisible laws
  2. choose Either.left x (lose f) = x
  3. choose Either.right (lose f) x = x
  4. choose f (choose g m n) o
=
let f' =
  Either.(case (case id (right % left) % g) (right % right) % right)
in
choose f' m (choose Fun.id n o)

Minimal definition

module type WITH_LOSE_AND_CHOOSE = sig ... end

Exposes the lose and choose functions, mandatory for each requirement.

module type WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUER = sig ... end

Minimal definition using contramap, divide, conquer, lose and choose.

Structure anatomy

Basis operations.

module type OPERATION = sig ... end

Additional operations.

module type INFIX = sig ... end

Infix operators.

Complete API

module type API = sig ... end

The complete interface of a Decidable.

Additional references