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)

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]

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

Extended examples

Installing Leon

Analysis	Compiled ✓
Function	Verif.
map	✓
identityLaw	✓
associativityLaw	✓

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

}

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:

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

}

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
  }

}