Decidable is a "Contravariant Alternative".
To have a predictable behaviour, the instance of Decidable must obey some laws.
Divisible lawschoose Either.left x (lose f) = xchoose Either.right (lose f) x = xchoose 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)module type WITH_LOSE_AND_CHOOSE = sig ... endExposes the lose and choose functions, mandatory for each requirement.
module type WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUER = sig ... endMinimal definition using contramap, divide, conquer, lose and choose.
module type CORE = WITH_CONTRAMAP_AND_DIVIDE_AND_CONQUERBasis operations.
module type OPERATION = sig ... endAdditional operations.
module type INFIX = sig ... endInfix operators.
module type API = sig ... endThe complete interface of a Decidable.