Specifying Algebraic Properties¶
Introduction¶
Many datatypes that programmers deal with on a daytoday basis often provide the same set of operations, for example:
 They can be tested for equality to some other value
 They can be ordered (partially or totally)
 They can be composed together
 They can be added or multiplied together
 They have an inverse with respect to some operation
Because those are very common properties, it is often useful to be able to abstract over them. In fact, each of these properties corresponds to an algebraic structure, and is governed by the set of laws which allow the programmer to reason at a higher level of abstraction, and to be able to rely on the behavior specified by the laws associated with the structure.
While these properties can be modeled and implemented using Java interfaces, modern programming languages such as Scala or Haskell provide a better mechanism for expressing the properties: typeclasses.
Typeclasses¶
Typeclasses were introduced by Wadler & Blott [WB89] as an extension to the Hindley/Milner type system to implement a certain kind of overloading, known as adhoc polymorphism.
A typeclass is identified by its name, and is associated with a set of (usually polymorphic) functions signatures, its methods.
It can then be instantiated at various types, given that the user is able to provide a concrete implementation for each method. A user can then apply these methods to any type for which there is a corresponding instance, which essentially corresponds to overloading.
Using typeclasses, one can model algebraic properties of datatypes in a fairly natural way.
Here is for example, the definition and implementation of a Monoid
, ie. a typeclass
for datatypes which can be mashed together associatively, and which have an
identity element w.r.t. to this operation:
abstract class Monoid[A] {
def empty: A
def append(x: A, y: A): A
@law
def law_leftIdentity(x: A) = {
append(empty, x) == x
}
@law
def law_rightIdentity(x: A) = {
append(x, empty) == x
}
@law
def law_associativity(x: A, y: A, z: A) = {
append(x, append(y, z)) == append(append(x, y), z)
}
}
implicit val bigIntAdditiveMonoid: Monoid[BigInt] = new Monoid[BigInt] {
override def empty: BigInt = 0
override def append(x: BigInt, y: BigInt): BigInt = x + y
}
Here, the abstract class specifies the two abstract operations which are required, but also the associated laws that the implementation of these operations must satisfy for the datatype to form a valid monoid.
Stainless will then ensure that the implementation of Monoid
for the BigInt
type satisfy
those laws. In this case, the above definition of bigIntAdditiveMonoid
will generate the
following verification conditions:
┌───────────────────┐
╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════╗
║ └───────────────────┘ ║
║ law_associativity law valid nativez3 ../../test.scala:25:3 0.052 ║
║ law_leftIdentity law valid nativez3 ../../test.scala:25:3 0.037 ║
║ law_rightIdentity law valid nativez3 ../../test.scala:25:3 0.029 ║
╟╢
║ total: 9 valid: 9 (0 from cache) invalid: 0 unknown: 0 time: 0.729 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
Armed with the knowledge that our Monoid
will always be lawful, one can now fearlessly write
the foldMap
function, and get the expected result:
def foldMap[A, M](xs: List[A])(f: A => M)(implicit M: Monoid[M]): M = xs match {
case Nil() => M.empty
case Cons(y, ys) => M.append(f(y), foldMap(ys)(f))
}
def sumBigInt(xs: List[BigInt]): BigInt = {
foldMap(xs)(x => x)
}
Sometimes, Stainless will not be able to automatically prove that an instance is lawful, for example when the property of interest involves a recursive definition over an inductive data type, as in the following code:
sealed abstract class Nat {
def +(m: Nat): Nat = this match {
case Zero => m
case Succ(n) => Succ(n + m)
}
def *(m: Nat): Nat = this match {
case Zero => Zero
case Succ(n) => n * m + m
}
}
final case object Zero extends Nat
final case class Succ(prev: Nat) extends Nat
final val One = Succ(Zero)
implicit def natAdditiveMonoid: Monoid[Nat] = new Monoid[Nat] {
def empty: nat = Zero
def append(x: Nat, y: Nat): Nat = x + y
}
To help Stainless out, one needs to prove that Zero
indeed the right identity of +
,
as well as the associativity of the latter.
@induct
def lemma_rightIdentity_plus(x: Nat): Boolean = {
x + Zero == x
}.holds
@induct
def lemma_associativity_plus(x: Nat, y: Nat, z: Nat): Boolean = {
x + (y + z) == (x + y) + z
}.holds
One can then override the law of interest, and instantiate the lemma over the relevant parameters:
implicit def natAdditiveMonoid: Monoid[Nat] = new Monoid[Nat] {
def empty: nat = Zero
def append(x: Nat, y: Nat): Nat = x + y
override def law_rightIdentity(x: Nat) = {
super.law_rightIdentity(x) because lemma_rightIdentity_plus(x)
}
override def law_associativity(x: Nat, y: Nat, z: Nat) = {
super.law_associativity(x, y, z) because lemma_associativity_plus(x, y, z)
}
}
With these modifications, the example goes through without a hitch.
Typeclass inheritance¶
Some algebraic structures can be defined as some other algebraic structure plus some additional operations and/or laws, eg. a monoid can be seen as a semigroup with identity.
In Scala, typeclasses allow to represent such relationship between algebraic structures by mean of inheritance.
Let’s take for example the Ord
typeclass, which describes totally ordered datatypes.
This class is defined as follows:
trait Eq[A] {
def equals(x: A, y: A): Boolean
}
trait Ord[A] extends Eq[A] {
def lessThanEq(x: A, y: A): Boolean
def lessThan(x: A, y: A): Boolean = lessThanEq(x, y) && !equals(x, y)
}
This can also be read as: if A
is an instance of Ord
, then it also is a instance of Eq
.
Associated methods¶
On top of abstract operations, a typeclass can also introduces concrete methods which
do not need to (but can) be redefined by the programmer at instance declaration time,
just like the lessThan
method of the Ord
class above.
While such methods could be defined as a standalone function with an Ord
constraint,
having it be a part of the class allows users to override it with e.g. a more efficient
implementation specific to the datatype they are instantiating the class for, as shown below:
case object BigIntOrd extends Ord[BigInt] {
def equal(x: BigInt, y: BigInt) = x == y
def lessThanEq(x: BigInt, y: BigInt) = x <= y
override def lessThan(x: BigInt, y: BigInt) x < y
}
Coherence¶
Let’s now look at an issue that might arise when working with typeclasses in Scala.
abstract class Monoid[A] {
def empty: A
def combine(x: A, y: A): A
}
implicit val bigIntAddMonoid: Monoid[BigInt] = new Monoid[BigInt] {
override def empty: BigInt = 0
override def combine(x: BigInt, y: BigInt): BigInt = x + y
}
implicit val bigIntProdMonoid: Monoid[BigInt] = new Monoid[BigInt] {
override def empty: BigInt = 1
override def combine(x: BigInt, y: BigInt): BigInt = x * y
}
def fold[A](list: List[A])(implicit M: Monoid[A]): A = {
list.foldRight(M.empty)(M.combine)
}
val list: List[BigInt] = List(2, 3)
val res: BigInt = fold(list) // ?
Here, the Scala compiler bails out with an ambiguous implicits error but for good reasons this time.
Indeed, depending on which instance of Monoid[BigInt]
it picks, res
can either be equal to 5 or 6.
This issue arise because the two instances above are overlapping, which has the effect of making the
type system incoherent. For a type system to be coherent, “every valid typing derivation for a program
must lead to a resulting program that has the same dynamic semantics”, which is clearly not the case here.
While in this specific example, the compiler will rightfully reject the program, this might always be
possible as one could import a different instance in scope in two different modules, and then a third module
might assume that these modules actually make use of the same instance, silently breaking the program.
Imagine trying to merge two Sets
that have been created with two different Ord
instances in scope.
Haskell partially solves this problem by enforcing that instances defined in the same module do not overlap, that is to say that the compiler would reject the program above. We deem Haskell’s approach only partial as it allows the programmer to define two or more overlapping instances, provided that they are not defined in the same module. A program is then only rejected when the programmer makes imports such overlapping instances in scope and attempts to make use of them. This decision stems from the will to allow linking together two different libraries which both define a class instance for the same type.
Because Stainless operates under a closedworld assumption, we could go further and disallow overlapping instances altogether, but this has not been implemented yet.
One might still want to provide both an additive and multiplicative Monoid
instance for integers.
To this end, one can wrap values of type BigInt
with two different wrapper classes for which
we will define the respective instances:
case class Sum(value: BigInt) extends AnyVal
case class Product(value: BigInt) extends AnyVal
implicit val bigIntSumMonoid: Monoid[Sum] = new Monoid[Sum] {
override def empty: Sum = Sum(0)
override def combine(x: Int, y: Int): Sum = Sum(x.value + y.value)
}
implicit val bigIntProductMonoid: Monoid[Product] = new Monoid[Product] {
override def empty: Product = Product(1)
override def combine(x: Int, y: Int): Product = Product(x.value * y.value)
}
def foldMap[A, B](list: List[A])(f: A => B)(implicit M: Monoid[B]): B = {
list.map(f).foldRight(M.empty)(M.combine)
}
It then becomes possible to unambiguously pick which instance to use depending on the semantics one wants:
val list: List[BigInt] = List(2, 3)
val sum: BigInt = foldMap(list)(Sum(_)).value // 5
val product: BigInt = foldMap(list)(Product(_)).value // 6
Under the hood¶
In this section we describe how laws are encoded within Stainless.
Let’s take as an example the Semigroup+Monoid hierarchy, slightly amended to exercise at once all the features described above.
abstract class Semigroup[A] {
def append(x: A, y: A): A
@law
def law_associativity(x: A, y: A, z: A): Boolean = {
append(x, append(y, z)) == append(append(x, y), z)
}
}
abstract class Monoid[A] extends Semigroup[A] {
def empty: A
@law
def law_leftIdentity(x: A): Boolean = {
append(empty, x) == x
}
@law
def law_rightIdentity(x: A): Boolean = {
append(x, empty) == x
}
override def law_associativity(x: A, y: A, z: A): Boolean = {
// We refine the Semigroup associativity law with a dummy
// predicate `refineLaw` to demonstrate this feature.
super.law_associativity(x, y, z) && refineLaw(x, y, z)
}
}
def refineLaw[A](x: A, y: A, z: A): Boolean = true
Together with a simple implementation for BigInt
:
def bigIntAdditiveMonoid: Monoid[BigInt] = new Monoid[BigInt] {
def empty: BigInt = 0
def append(x: BigInt, y: BigInt): BigInt = x + y
override def law_rightIdentity(x: BigInt): Boolean = {
// no manual proof is needed in this case, but we include
// a dummy one for the sake of this example.
someProof
}
}
def someProof: Boolean = true
Here is the internal Stainless AST pretty much right after extraction from the Scala compiler.
Each symbol (class, method, variable) is annotated with its internal identifier
(ie. the number after the $
sign at the end of its name) which will prove useful
for reading the code after the next phase, as it introduces new symbols with the same
name but different identifiers.
abstract class Semigroup$0[A$85] {
@abstract
def append$3(x$108: A$85, y$24: A$85): A$85 = <empty tree>[A$85]
@law
def law_associativity$0(x$109: A$85, y$25: A$85, z$11: A$85): Boolean = {
this.append$3(x$109, this.append$3(y$25, z$11)) ==
this.append$3(this.append$3(x$109, y$25), z$11)
}
}
abstract class Monoid$0[A$86] extends Semigroup$0[A$86] {
@abstract
def empty$6: A$86 = <empty tree>[A$86]
@law
def law_leftIdentity$0(x$110: A$86): Boolean =
this.append$3(this.empty$6, x$110) == x$110
@law
def law_rightIdentity$0(x$111: A$86): Boolean =
this.append$3(x$111, this.empty$6) == x$111
def law_associativity$1(x$112: A$86, y$26: A$86, z$12: A$86): Boolean =
super.law_associativity$0(x$112, y$26, z$12) && refineLaw$0[A$86](x$112, y$26, z$12)
}
def refineLaw$0[A$87](x$113: A$87, y$27: A$87, z$13: A$87): Boolean = true
case class $anon$0() extends Monoid$0[BigInt] {
def empty$7: BigInt = 0
def append$4(x$112: BigInt, y$26: BigInt): BigInt = x$112 + y$26
def law_rightIdentity$1(x$113: BigInt): Boolean = someProof$0
}
def bigIntAdditiveMonoid$0: Monoid$0[BigInt] = $anon$0()
def someProof$0: Boolean = true
The code above maps in straightforward way to the original code.
Let’s now take a look at the output of the Laws
phase. This is
the phase which desugars the law definitions and their overrides
into methods with explicit postconditions.
abstract class Semigroup$0[A$85] {
@abstract
def append$3(x$108: A$85, y$24: A$85): A$85 = <empty tree>[A$85]
@final
@inlineOnce
@derived(law_associativity$0)
def law_associativity$2(x$120: A$85, y$30: A$85, z$14: A$85): Boolean = {
this.append$3(x$120, this.append$3(y$30, z$14)) ==
this.append$3(this.append$3(x$120, y$30), z$14)
}
@abstract
def law_associativity$0(x$109: A$85, y$25: A$85, z$11: A$85): Boolean = {
<empty tree>[Boolean]
} ensuring {
(res$82: Boolean) => res$82 && this.law_associativity$2(x$109, y$25, z$11)
}
}
abstract class Monoid$0[A$86] extends Semigroup$0[A$86] {
@abstract
def empty$6: A$86 = <empty tree>[A$86]
@final
@inlineOnce
@derived(law_leftIdentity$0)
def law_leftIdentity$1(x$116: A$86): Boolean =
this.append$3(this.empty$6, x$116) == x$116
@abstract
def law_leftIdentity$0(x$110: A$86): Boolean = {
<empty tree>[Boolean]
} ensuring {
(res$77: Boolean) => res$77 && this.law_leftIdentity$1(x$110)
}
@final
@inlineOnce
@derived(law_rightIdentity$0)
def law_rightIdentity$2(x$117: A$86): Boolean =
this.append$3(x$117, this.empty$6) == x$117
@abstract
def law_rightIdentity$0(x$111: A$86): Boolean = {
<empty tree>[Boolean]
} ensuring {
(res$80: Boolean) => res$80 && this.law_rightIdentity$2(x$111)
}
@law
def law_associativity$1(x$112: A$86, y$26: A$86, z$12: A$86): Boolean = {
this.law_associativity$2(x$112, y$26, z$12) && refineLaw$0[A$86](x$112, y$26, z$12)
} ensuring {
(res$84: Boolean) => res$84 && this.law_associativity$2(x$112, y$26, z$12)
}
}
@derived(bigIntAdditiveMonoid$0)
case class $anon$0() extends Monoid$0[BigInt] {
def empty$7: BigInt = 0
def append$4(x$114: BigInt, y$27: BigInt): BigInt = x$114 + y$27
@law
@derived(law_leftIdentity$0)
def law_leftIdentity$2(x$119: BigInt): Boolean = {
true
} ensuring {
(res$84: Boolean) => this.law_leftIdentity$1(x$119)
}
@law
def law_rightIdentity$1(x$115: BigInt): Boolean = {
someProof$0
} ensuring {
(res$79: Boolean) => res$79 && this.law_rightIdentity$2(x$115)
}
@law
@derived(law_associativity$0)
def law_associativity$2(x$120: BigInt, y$29: BigInt, z$13: BigInt): Boolean = {
true
} ensuring {
(res$85: Boolean) => this.law_associativity$1(x$120, y$29, z$13)
}
}
def bigIntAdditiveMonoid$0: Monoid$0[BigInt] = $anon$0()
def someProof$0: Boolean = true
There are a few things going on here:
First of all, each method marked
@law
introduces a new method which holds the original body of the law. The law’s body is then rewritten to be empty, and is provided with a postcondition which refers to the newly introduced method. This desugaring step basically turns the laws into abstract methods which must be overridden at some point with methods whose body can be proven to be true, while also satisfying the law itself.The helper method will be used in subsequent steps to refer to the law’s body, without having to inline it or call the law itself, which is disallowed since it is conceptually an abstract method, as evidenced by its newly added
@abstract
flag.// In class `Semigroup`... // This is the helper method. @final @inlineOnce @derived(law_associativity$0) def law_associativity$2(x$120: A$85, y$30: A$85, z$14: A$85): Boolean = { this.append$3(x$120, this.append$3(y$30, z$14)) == this.append$3(this.append$3(x$120, y$30), z$14) } // This is the original law definition, which now became an abstract method. @abstract def law_associativity$0(x$109: A$85, y$25: A$85, z$11: A$85): Boolean = { <empty tree>[Boolean] } ensuring { (res$82: Boolean) => res$82 && this.law_associativity$2(x$109, y$25, z$11) }
Laws which are overridden into abstract subclasses, are provided with a postcondition that ensures that their body can be proven true, while still satisfying the original law via a call to the helper method introduced in the previous step. This step ensures that laws cannot be fully redefined, and thus potentially weakened, in subclasses.
// In class `Monoid`... @law def law_associativity$1(x$112: A$86, y$26: A$86, z$12: A$86): Boolean = { this.law_associativity$2(x$112, y$26, z$12) && refineLaw$0[A$86](x$112, y$26, z$12) } ensuring { (res$84: Boolean) => res$84 && this.law_associativity$2(x$112, y$26, z$12) }
In the typeclass implementations (eg. class
$anon$0
), methods which override laws are provided with a postcondition which again ensures that their body holds, while still satisfying the law they override, again via a call to the helper method introduced in step 1.// In class `$anon$0`... @law def law_rightIdentity$1(x$115: BigInt): Boolean = { someProof$0 } ensuring { (res$79: Boolean) => res$79 && this.law_rightIdentity$2(x$115) }
If a law is not overridden in a typeclass implementation, a stub override is automatically defined by Stainless, to ensure that a verification condition will be generated. Those stubs just have
true
as a body, and a postcondition which calls to the appropriate law helper introduced in step 1. This expresses the fact that the law holds on its own, without any additional proof steps.// In class `$anon$0` @law @derived(law_leftIdentity$0) def law_leftIdentity$2(x$119: BigInt): Boolean = { true } ensuring { (res$84: Boolean) => this.law_leftIdentity$1(x$119) }
Note
As can be seen above, calling the super method when refining (such as in law_associativity
)
or proving (such as in law_rightIdentity
) a law is superfluous, since it is done anyway
during the encoding as to ensure that laws cannot be weakened. Doing so can nonetheless help
readability, since it makes the code match more closely to the semantics of Scala.
[WB89] 
