Proving the functor laws with Leon

July 25, 2015

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 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝