« Just what the funk is a Functor anyway?
Implicits for the Fearless »

Applicative Functor laws using Reductio (Scala)

Here is the Applicative functor type-class (see Applicative Programming with Effects, Conor McBride, Ross Paterson):

class Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

Here are the laws for the Applicative functor type-class:

  • identity
    pure id <*> u == u
  • composition
    pure (.) <*> u <*> v <*> w == u <*> (v <*> w)
  • homomorphism
    pure f <*> pure x == pure (f x)
  • interchange
    u <*> pure x == pure (\f -> f x) <*> u

Here are those laws stated using Reductio. I have changed pure to unit and the language is Scala:

 
object ApplicativeLaws {
  def identity[A[_], X](implicit a: Applicative[A],
                                 aax: Arbitrary[A[X]],
                                 e: Equal[A[X]]) =
    prop((apx: A[X]) => apx === a(a.unit((x: X) => x), apx))
 
  def composition[A[_], X, Y, Z](implicit a: Applicative[A],
                                aayz: Arbitrary[A[Y => Z]],
                                aaxy: Arbitrary[A[X => Y]],
                                aax: Arbitrary[A[X]],
                                e: Equal[A[Z]]) =
    prop((apyz: A[Y => Z], apxy: A[X => Y], apx: A[X]) =>
            a(apyz, a(apxy, apx)) ===
            a(a(a(a.unit((f: Y => Z) => (g: X => Y) => f compose g), apyz), apxy), apx))
 
  def homomorphism[A[_], X, Y](implicit a: Applicative[A],
                                        ax: Arbitrary[X],
                                        axy: Arbitrary[X => Y],
                                        e: Equal[A[Y]]) =
    prop((f: X => Y, x: X) => a(a.unit(f), a.unit(x)) === a.unit(f(x)))
 
  def interchange[A[_], X, Y](implicit a: Applicative[A],
                                       ax: Arbitrary[X],
                                       apxy: Arbitrary[A[X => Y]],
                                       e: Equal[A[Y]]) =
    prop((f: A[X => Y], x: X) =>
      a(f, a.unit(x)) === a(a.unit((f: X => Y) => f(x)), f))
}

Pretty neat eh? :) Let’s test the Applicative instance for List:

List(identity[List, Int],
     composition[List, Int, Long, String],
     homomorphism[List, Int, String],
     interchange[List, Int, String]).
  foreach(p => summary println p)

This runs 100 unit tests per property, so 400 unit tests altogether. Here is the output:

OK, passed 100 tests.
OK, passed 100 tests.
OK, passed 100 tests.
OK, passed 100 tests.

Woot woot!

This entry was posted on Thursday, July 3rd, 2008 at 4:42 pm and is filed under Programming. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

One Response to “Applicative Functor laws using Reductio (Scala)”

  1. Stefan Wagner Says:
    July 4th, 2008 at 7:16 am

    Apropos functor, funky, …
    Is it just me, who has a funky layout (in Linux/Firefox 3.0)
    See a screenshot .

    To the topic!
    How do I read that:

    class Applicative f where
    pure :: a -&gt; f a
    () :: f (a -&gt; b) -&gt; f a -&gt; f b

    ‘… where pure “is defined as” function, which maps a to f of a … (and where)
    zorong “is defined as” a matching such that the function on ey* match a to b implies ey* function on a which is matched to ey* function on b.

    ey* is used for a, where a (the indefinite article) could collide with a (the variable named ‘a’)
    zorong () is something I don’t have much of an idea on. Some kind of foobar.
    Well - the asterix looks much like an universal something or anything, but those two kinds of brackets show that there is some kind of restriction.

Leave a Reply