Liskov Substitution Principle is Contravariance

The Liskov Substitution Principle is a much cited result by those who believe in the myth of “object-oriented programming”. But the LSP is like many things in the OO mythos that become “invisible or simpler” when looked at from the perspective of the properties of functions (which is what programming really is about).

Let’s remind ourselves of the LSP:

Let q(x) be a property provable about objects x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T.

Let Q[A] be a property provable about objects of type A. By Curry-Howard, a proof of this property is a program, and the property that it proves is a type.

So we translate “let q(x) be a property provable about objects x of type T” to just Q[T]. We translate “q(y) should be true for objects y of type S” to Q[S].

We write X => Y to mean “X implies Y”, or “if X, then Y”. Let’s translate “S is a subtype of T” into these terms. It means that the set of all values in S is a subset of the values in T. So if you have a value s in S, then s is also in T. More loosely, we will say that every object s in S corresponds to exactly one object t in T. In other words, S implies T, or S => T. This is precisely the type of functions from S to T, and we will consider every function of this type to be a proof that S => T.

We’re now ready to state the Liskov Substitution Principle:

For all T, S. Q[T] => (S => T) => Q[S]

Read it as: If the property Q holds for all values of type T, then if every object of type S maps to exactly one object of type T, the property Q holds for all values of type S.

This is exactly the type of comap for a contravariant functor. So LSP just says “predicates are contravariant”. And what’s more, comap literally boils down to function composition in practise. So it’s almost completely trivial.

More on Monoids and Monads

In a previous post on monoids, we established that Monoids are List-Algebras. In other words, a monoid A essentially models a function of type List[A] => A. We saw how the unit and associativity laws for monoids model the fact that we can fold left and right, and that the empty list doesn’t count.

Monoids for Free

We defined a monoid as a category with one object. Now, let’s generalize this notion. Before, we represented Monoid as having a binary function and an identity element for that function. But by our categorical definition, we could just restrict the Scala category (where types are the objects and functions are the arrows) and define Monoid in terms of that:

class Endo[M] {
  def compose(m1: M => M, m2: M => M): M => M = m1 compose m2
  def identity: M => M = m => m
}

A function from some type to itself is called an endomorphism. Endo[M] for any type M, is a monoid, by our previous definition. It is a category with one object M whose only arrows are endomorphisms on M.

We know already that lists and monoids are intimately connected. Now notice that M => M is exactly the form of the right-hand side of foldRight. Let’s remind ourselves of the type of foldRight:

def foldRight[A,B]: (List[A], A => (B => B)) => (B => B)

Read this with an eye to endomorphisms and the fact that they form monoids. FoldRight, then, is saying that a List[A] together with a function from a value of A to an endomorphism on B, allows us to collapse all those As into a single endomorphism on B. Here’s a possible implementation:

def foldRight[A,B] = (as: List[A], f: A => B => B) => {
  val m = new Endo[B]
  as match {
    case Nil => m.identity
    case x :: xs => m.compose(f(x), foldRight(as, f))
  }

That’s slightly different from what you might be used to seeing, but equivalent.

A Theory of Monoids

This gives rise to a further theory. If we had a List[List[A]] such that A is a monoid, so we know we can go from List[A] to A, then it’s safe to say that we could fold all the inner lists and end up with List[A] which we can then fold. Another way of saying the same thing is that we can pass the list constructor :: to foldRight. It has the correct type for the f argument, which is not a coincidence (namely A => List[A] => List[A]). That in turn gives us another function (List[A] => List[A] => List[A]) which, as it turns out, appends one list to another. If we pass that to foldRight, we get List[List[A]] => List[A] => List[A]. That again has the proper type for foldRight, and so on. The pattern here is that we can keep doing this to turn an arbitrarily nested list of lists into an endofunction on lists, and we can always pass an empty list to one of those endofunctions to get an identity.

So the types of arbitrarily nested lists are monoids. Our composition for such a monoid appends one list to another, and the identity for that function is the empty list.

Let’s call this our “theory of monoids”, so we can refer to it by name later on.

Monoids of a Higher Kind

But there’s something more general going on here. For a moment, let’s denote List[A] as A*, meaning “zero or more values of type A“. If A is a monoid, then this gives us the function A* => A (since monoids are list-algebras). Now note what happened with arbitrary nesting of List. Let’s notate this as List*[A] meaning “lists of A nested to zero or more levels”. It seems that we can go from List*[A] => List[A]. So the List type constructor itself seems to be a sort of monoid of a higher kind.

And this turns out to be true. Let’s look at our monoid trait again:

trait Monoid[M] {
  val identity: M
  def append(a: M, b: M): M
}

With an eye towards M* => M, we can see that the Monoid provides a way of turning a list-of-M of arbitrary length (M*) into a list-of-M of length 1 (M¹). The identity takes care of the case where we have an empty list (M⁰), and the append reduces M² to M¹. By induction, we know that this is enough to collapse any number of Ms into a single M.

For our higher-kinded monoid, which we’ll call M as well, we need the same thing–a way of going from M⁰ to M¹, and from M² to M¹. “Higher-kinded monoid” is a bit long-winded. Since it’s a triad (a type constructor with identity and append), and also a sort of monoid, we’ll contract this to “Monad”:

trait Monad[M[_]] {
  def map[A,B](f: A => B): M[A] => M[B]
  def unit[A](a: A): M[A]
  def join[A](m: M[M[A]]): M[A]
}

The Obvious Axioms

Now recall the monoid laws from before. We can infer the monad laws from those. Monad’s unit is the identity of our higher-order monoid, and should be an identity for the join method, which is Monad’s equivalent of Monoid’s append. So join(unit(m)) == m (left identity) and join(map(unit)(m)) == m (right identity).

The join method should be associative, meaning that if you have M[M[M[A]]], it doesn’t matter whether you join the inner or outer Ms first. That is, join(map(join)(m)) should equal join(join(m)).

This is pretty much a straight translation from the monoid laws, except that we needed map to apply a function “on the right” (or on the inside) of an M.

The Monad for Monoids

OK, so remember our theory of monoids from above? We can encode that theory in Scala, using a monad:

val listMonad = new Monad[List] {
  def map[A,B](f: A => B) = (xs: List[A]) => xs.map(f)
  def unit[A](a: A) = a :: Nil
  def join[A](xs: List[List[A]]) = xs.flatten
}

So List is a monad that represents a theory about monoids. What is this thing saying about monoids? The map method says that if we can fold a List[A] with a monoid, and we can turn every A into a monoid B, then we can fold a List[B]. The unit and join methods, together with the monad laws above, are saying the following:

If we have an expression of some monoid-type A, like (a1 + a2 + a3), where a1, a2, and a3 are values of type A and + is the append function of the monoid, then we can insert the identity into that expression wherever we want, and we can add and remove parentheses at will, and the order in which we add and remove them doesn’t matter.

Monads Are Not Just About Monoids

Alright, so the List monad is all about monoids, but this is just one use case for the Monad trait. I.e. List is the monad for monoids.

We could write a Monad instance that means something totally different. For example we might write Monad[Future], to encode a theory of concurrent processes. What would that theory be saying? Well, map would say that we can extend a running process by giving its continuation. And the unit and join functions with the monad laws would say that we can arbitrarily fork subexpressions of a program, and arbitrarily join with forked processes, and that the order in which we fork and join doesn’t matter to the result of the program.

We can perfectly well write an implementation of Monad[Option], or Monad[Reader[A]#->] where trait Reader[A] { type ->[B] = A => B }. I’ll leave these implementations as an exercise for the reader. See if you can come up with an explanation for the monad laws in each case.

I hope you’ve enjoyed this deep dive into monoids, monads, and their relationship.

Type-Level Programming in Scala, Part 6d: HList Zip/Unzip

For zip and unzip, we need to define some type classes. First, we will define an HZip type class that accepts two HLists and produces a zipped HList.

sealed trait HZip[A <: HList, B <: HList, Result <: HList] {
   def apply(a: A, b: B): Result
}

We implement the type class with two main cases hzipNil0 and hzipCons.

Zipping two HNils produces an HNil.

   implicit def hzipNil0 =
      new HZip[HNil, HNil, HNil] {
         def apply(a: HNil, b: HNil) = HNil
      }

Zipping two HCons cells combines their heads into a tuple, zips their tails, and creates a new HCons cell from the tuple and zipped tails.

   implicit def hzipCons[HA, HB, TA <: HList, TB <: HList, TR <: HList](implicit hzipTail: HZip[TA, TB, TR]) =
      new HZip[HA :: TA, HB :: TB, (HA, HB) :: TR] {
         def apply(a: HA :: TA, b: HB :: TB) = HCons( (a.head, b.head), hzipTail(a.tail, b.tail) )
      }

Two additional cases, hzipNil1 and hzipNil2, handle mismatched lengths by simply truncating the longer list.

   implicit def hzipNil1[H, T <: HList] =
      new HZip[HCons[H,T], HNil, HNil] {
         def apply(a: HCons[H,T], b: HNil) = HNil
      }

   implicit def hzipNil2[H, T <: HList] =
      new HZip[HNil, HCons[H,T], HNil] {
         def apply(a: HNil, b: HCons[H,T]) = HNil
      }

We hook this into our HListOps type class and we can call zip directly on an HList.

Examples:

   // a heterogeneous list of length 3 and type
   //  Int :: String :: List[Char] :: HNil
   val a = 3 :: "ai4" :: List('r','H') :: HNil

   // a heterogeneous list of length 4 and type
   //  Char :: Int :: Char :: String :: HNil
   val b = '3' :: 2 :: 'j' :: "sdfh" :: HNil

   // the two HLists zipped
   val c = a zip b

   // zipped again.
   val cc = c zip c.tail

   // verify proper types
   // note that the fourth element of b is dropped, like when zipping a homogeneous List
   val checkCType : (Int, Char) :: (String, Int) :: (List[Char], Char) :: HNil = c

   val checkCCType : ((Int, Char), (String, Int)) :: ((String, Int), (List[Char], Char)) :: HNil = cc

   // verify proper values
   val (3, '3') :: ("ai4", 2) :: (List('r', 'H'), 'j') :: HNil = c

   val ((3,'3'),("ai4",2)) :: (("ai4",2),(List('r', 'H'),'j')) :: HNil = cc

Next, we’ll define an unzip type class that accepts an HList of tuples and separates it into two HLists by components:

trait Unzip[H <: HList, R1 <: HList, R2 <: HList] {
   def unzip(h: H): (R1, R2)
}

Unzipping HNil produces HNil.

   implicit def unzipNil =
      new Unzip[HNil, HNil, HNil] {
         def unzip(h: HNil) = (HNil, HNil)
      }

For HCons, we unzip the tail, separate the head components, and prepend the respective head component to each tail component.

   implicit def unzipCons[H1, H2, T <: HList, TR1 <: HList, TR2 <: HList]
      (implicit unzipTail: Unzip[T, TR1, TR2]) =

      new Unzip[(H1,H2) :: T, H1 :: TR1, H2 :: TR2]  {
         def unzip(h: (H1,H2) :: T) = {
            val (t1, t2) = unzipTail.unzip(h.tail)
            (HCons(h.head._1, t1), HCons(h.head._2, t2))
         }
      }

   def unzip[H <: HList, R1 <: HList, R2 <: HList](h: H)(implicit un: Unzip[H, R1, R2]): (R1, R2) =
      un unzip h
}

Again, we just need to hook this into our HListOps type class.

Building on the example from above,

   // unzip the zipped HLists
   val (cc1, cc2) = cc.unzip

   val (ca, cb) = cc1.unzip

   // check types
   val checkCC1 : (Int, Char) :: (String, Int) :: HNil = cc1

   val checkCC2 : (String, Int) :: (List[Char], Char) :: HNil = cc2

   val checkCa: Int :: String :: HNil= ca

   val checkCb: Char :: Int :: HNil = cb

We will look at applying functions to HList values next.