Proving the Functor Laws with Leon

Leon is a software verification system for Scala. It uses a limited subset of Scala, called Pure Scala, and a nifty online evaluation envrionment to statically verify programs.

Let's see if we can use Leon to prove the functor laws of identity and associativity:

``````fmap id      = id
fmap (p . q) = (fmap p) . (fmap q)``````

To start, we import some standard definitions:

``````import leon.lang._
import leon.collection._``````

Next, we create a simple ADT for which we'll implement a functor:

``````sealed abstract class Amount[A]
case class One[A](a: A) extends Amount[A]
case class Couple[A](a: A, b: A) extends Amount[A]
case class Few[A](a: A, b: A, c: A) extends Amount[A]``````

Now we can implement our functor, which we'll stick inside an object called `AmountFunctor`:

``````def map[A, B](fa: Amount[A])(f: (A) => B): Amount[B] =
fa match {
case One(a) => One(f(a))
case Couple(a, b) => Couple(f(a), f(b))
case Few(a, b, c) => Few(f(a), f(b), f(c))
}``````

It would have been nice to make this type extend an abstract `Functor[F[_]]` class, but I couldn't find a way to do it. Leon doesn't seem to like providing concrete values for higher-kinded type parameters.

Finally, we can implement our functor laws, which Leon will statically check for us. These can go in the `AmountFunctor` object, or their own `AmountFunctorLaws` object with an extra `import AmountFunctor.map`:

``````def identityLaw[A](a: Amount[A]): Boolean = {
map(a)({ x: A => x }) == a
}.holds``````
``````def associativityLaw[A,B,C](p: (B) => C, q: (A) => B, a: Amount[A]): Boolean = {
map(a)({ x: A => p(q(x)) }) == map(map(a)(q))(p)
}.holds``````

Leon then analyzes our program, and gives us some happy green check marks:

Analysis Compiled ✓
Function Verif.
map
identityLaw
associativityLaw

We can also run the analyzer locally via Leon's `leon` script:

``````\$ ./leon FunctorLaws.scala
- Now considering 'postcondition' VC for identityLaw @19:5...
=> VALID
- Now considering 'postcondition' VC for associativityLaw @23:5...
=> VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘                                                                   ║
║ associativityLaw             postcondition            23:5    valid      Z3-f        0.167 ║
║ identityLaw                  postcondition            19:5    valid      Z3-f        0.510 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 2      valid: 2      invalid: 0      unknown 0                                0.677 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝``````

Extended examples

Installing Leon

``````\$ git clone https://github.com/epfl-lara/leon.git
\$ cd leon
\$ sbt clean compile script``````

Make sure `z3` or `cvc4` is also installed.

AmountFunctor.scala

``````import leon.lang._
import leon.collection._

sealed abstract class Amount[A]
case class One[A](a: A) extends Amount[A]
case class Couple[A](a: A, b: A) extends Amount[A]
case class Few[A](a: A, b: A, c: A) extends Amount[A]

object AmountFunctor {

def map[A, B](fa: Amount[A])(f: (A) => B): Amount[B] =
fa match {
case One(a) => One(f(a))
case Couple(a, b) => Couple(f(a), f(b))
case Few(a, b, c) => Few(f(a), f(b), f(c))
}

// fmap id = id
def functorIdentityLaw[A](a: Amount[A]): Boolean = {
map(a)({ x: A => x }) == a
}.holds

// fmap (p . q) = (fmap p) . (fmap q)
def functorAssociativityLaw[A,B,C](p: (B) => C, q: (A) => B, a: Amount[A]): Boolean = {
map(a)({ x: A => p(q(x)) }) == map(map(a)(q))(p)
}.holds

}``````
``````\$ ./leon AmountFunctor.scala
[  Info  ]  - Now considering 'match exhaustiveness' VC for map @12:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for functorIdentityLaw @20:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for functorAssociativityLaw @25:5...
[  Info  ]  => VALID
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                    ║
[  Info  ] ║ AmountFunctor.functorAssociativityLaw  postcondition         25:5  valid  U:smt-z3    0.261 ║
[  Info  ] ║ AmountFunctor.functorIdentityLaw       postcondition         20:5  valid  U:smt-z3    0.256 ║
[  Info  ] ║ AmountFunctor.map                      match exhaustiveness  12:5  valid  U:smt-z3    0.144 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 3      valid: 3      invalid: 0      unknown 0                                 0.661 ║
[  Info  ] ╚═════════════════════════════════════════════════════════════════════════════════════════════╝``````

AmountFunctor2.scala

Trying to use higher-kinded type parameters throws the following, after commenting out a couple lines in leon/purescala/Definitions.scala and leon/purescala/Types.scala:

``````[ Error  ] ssg/FunctorLaws2.scala:13:1: Child classes should have the same number of type parameters as their parent
case object AmountF extends Functor[Amount] {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...``````
``````import leon.lang._
import leon.collection._

sealed abstract class Amount[A]
case class One[A](a: A) extends Amount[A]
case class Couple[A](a: A, b: A) extends Amount[A]
case class Few[A](a: A, b: A, c: A) extends Amount[A]

abstract class Functor[F[_]] {
def map[A, B](fa: F[A])(f: (A) => B): F[B]
}

case object AmountF extends Functor[Amount] {
def map[A, B](fa: Amount[A])(f: (A) => B): Amount[B] =
fa match {
case One(a) => One(f(a))
case Couple(a, b) => Couple(f(a), f(b))
case Few(a, b, c) => Few(f(a), f(b), f(c))
}
}

object AmountFunctor {

def map[A, B](fa: Amount[A])(f: (A) => B): Amount[B] =
fa match {
case One(a) => One(f(a))
case Couple(a, b) => Couple(f(a), f(b))
case Few(a, b, c) => Few(f(a), f(b), f(c))
}

def identityLaw[A](a: Amount[A]): Boolean = {
map(a)({ x: A => x }) == a
}.holds

def associativityLaw[A,B,C](p: (B) => C, q: (A) => B, a: Amount[A]): Boolean = {
map(a)({ x: A => p(q(x)) }) == map(map(a)(q))(p)
}.holds

}``````
``\$ ./leon AmountFunctor2.scala``

AmountFunctorApplicative.scala

``````import leon.lang._
import leon.collection._

sealed abstract class Amount[A]
case class One[A](a: A) extends Amount[A]
case class Couple[A](a: A, b: A) extends Amount[A]
case class Few[A](a: A, b: A, c: A) extends Amount[A]

object AmountFunctor {

def map[A, B](fa: Amount[A])(f: (A) => B): Amount[B] =
fa match {
case One(a) => One(f(a))
case Couple(a, b) => Couple(f(a), f(b))
case Few(a, b, c) => Few(f(a), f(b), f(c))
}

}

object AmountApplicative {

def point[A](a: => A): Amount[A] = Few(a, a, a)

def ap[A, B](fa: => Amount[A])(f: => Amount[A => B]): Amount[B] =
fa match {
case One(a) =>
f match {
case One(g)       => One(g(a))
case Couple(g, _) => One(g(a))
case Few(g, _, _) => One(g(a))
}
case Couple(a, b) =>
f match {
case One(g)       => One(g(a))
case Couple(g, h) => Couple(g(a), h(b))
case Few(g, h, _) => Couple(g(a), h(b))
}
case Few(a, b, c) =>
f match {
case One(g)       => One(g(a))
case Couple(g, h) => Couple(g(a), h(b))
case Few(g, h, i) => Few(g(a), h(b), i(c))
}
}

}

object AmountFunctorLaws {

import AmountFunctor.map

// fmap id = id
def functorIdentityLaw[A](a: Amount[A]): Boolean = {
map(a)({ x: A => x }) == a
}.holds

// fmap (p . q) = (fmap p) . (fmap q)
def functorAssociativityLaw[A,B,C](p: (B) => C, q: (A) => B, a: Amount[A]): Boolean = {
map(a)({ x: A => p(q(x)) }) == map(map(a)(q))(p)
}.holds

}

object AmountApplicativeLaws {

import AmountApplicative.point
import AmountApplicative.ap

// pure id <*> v = v -- Identity
def applicativeIdentityLaw[A](v: Amount[A]): Boolean = {
ap(v)(point({ x: A => x })) == v
}.holds

// pure f <*> pure x = pure (f x) -- Homomorphism
def applicativeHomomorphismLaw[A, B](x: A, f: (A) => B): Boolean = {
ap(point(x))(point(f)) == point(f(x))
}.holds

// u <*> pure y = pure (\$ y) <*> u -- Interchange
def applicativeInterchangeLaw[A, B](u: Amount[(A) => B], y: A): Boolean = {
ap(point(y))(u) == ap(u)(point({ x: ((A) => B) => x(y) }))
}.holds

// pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- Composition
def applicativeCompositionLaw[A,B,C](
u: Amount[B => C], v: Amount[A => B], w: Amount[A]): Boolean = {

// TODO

true
}

}``````
``````\$ ./leon AmountFunctorApplicative.scala
[  Info  ]  - Now considering 'match exhaustiveness' VC for map @12:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'match exhaustiveness' VC for ap @25:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'match exhaustiveness' VC for ap @27:9...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'match exhaustiveness' VC for ap @33:9...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'match exhaustiveness' VC for ap @39:9...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for functorIdentityLaw @54:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for functorAssociativityLaw @59:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for applicativeIdentityLaw @71:5...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for applicativeHomomorphismLaw @76:5...
java.lang.RuntimeException: Only applicable on lambda chains``````