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!
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 -> f a
() :: f (a -> b) -> f a -> 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.