Consequence

Overview

A consequence is a typeclass close to the material conditional. It allows to verify the implication of a consequence B2, assuming B1: B1 => B2

Usage

Taking a value of type A / B1, when passing it to a method or a variable asking for a A / B2, an implicit conversion using a given Consequence[A, B1, B2] will be invoked:

val x: Double < 10d = 3d
val y: Double < 20d = x

desugars to

val x: Double < 10d = 3d
val y: Double < 20d = refineConstrained(x)(using Consequence[Double, Less[10d], Less[20d]])

Note: If no consequence is found, a default Consequence instance will be passed instead.

Creating a consequence

The creation of a Consequence instance is analogous to Constraint instances:

class ConsequenceImpl[A, B1, B2] extends Consequence[A, B1, B2] {

  override inline def assert(value: A): Boolean = ???

  override inline def getMessage(value: A): String = ???
}

transparent inline given[A, B1, B2]: Consequence[A, B1, B2]
= new ConsequenceImpl

For further information, check this page

Verified implications

Some relations are assumed and don't need to be verified. You can use Consequence.verified in this case.

/**
 * B1 => B1 | B2
 */
transparent inline given[A, B1, B2]: Consequence[A, B1, Or[B1, B2]] = Consequence.verified

Al-contrario, you can use Consequence.invalid to express an always-invalid consequence.

/**
 * (B => !B) => false
 */
transparent inline given [A, B]: Consequence[A, B, Not[B]] = Consequence.invalid

Binary relations

Since 1.2.0, Iron provides traits to characterize your binary relations and apply default consequences including:

• Reflexive: aRa is true
• Symmetric: aRb <=> bRa
• AntiSymmetric: aRb & bRa => a = b
• Transitive: aRb & bRc => aRc
• Equivalence: Reflexive, transitive and symmetric
• Order: Reflexive, transitive and antisymmetric

Example from iron-numeric:

trait Divisible[V] extends Order[V, Divisible]

//By transitivity, Divisible[10d] => Divisible[5d] (no extra evaluation required)

For further information, check the Scaladoc