Exercises for proving functor laws in Leon. http://www.meetup.com/Scala-Study-Group/events/223073122/

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:

[ 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

}

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
  }

}