-
Notifications
You must be signed in to change notification settings - Fork 51
/
EitherLaws.scala
34 lines (22 loc) · 755 Bytes
/
EitherLaws.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
import stainless.lang._
object EitherLaws {
object FunctorLaws {
def functorLawId[A, B](e: Either[A, B]): Boolean = {
e.map(x => x) == e
}.holds
def functorLawCompose[A, B, C, D](e: Either[A, B], f: B => C, g: C => D): Boolean = {
e.map(x => g(f(x))) == e.map(f).map(g)
}.holds
}
object MonadLaws {
def monadLawIdLeft[A, B](x: B, f: B => Either[A, B]): Boolean = {
Right(x).flatMap(f) == f(x)
}.holds
def monadLawIdRight[A, B](e: Either[A, B]): Boolean = {
e.flatMap(Right(_)) == e
}.holds
def monadLawAssoc[A, B, C, D](e: Either[A, B], f: B => Either[A, C], g: C => Either[A, D]): Boolean = {
e.flatMap(f).flatMap(g) == e.flatMap(x => f(x).flatMap(g))
}.holds
}
}