Type programming: Constraining values

In my last type-programming post, I briefly touched on the topic of recursive type definitions by creating a Peano-encoded integer type. While that and the Boolean type we created in the first post were intriguing, but I haven’t demonstrated the utility of such types. In this post, I will use the PeanoType we developed to perform some type-safe operations on a list of integers by issuing constraints on the size of the lists under consideration. As with the other posts, my goal is to use the simplest possible examples to help us programmatically-imperative simpleton developers transition into an effective functional programming mindset.

In the first two posts, I gently introduced type-level programming by looking at its parallels to value-level programming. We will continue drawing parallels in this post as well, but let’s make a minor adjustment. I will first demonstrate how we will implement our list without type-programming, then compare it to how we can implement the same construct enhanced with type-programming.

So onward to the task at hand. We are going to define an integer-containing list which has a + operation for computing the matrix addition of the two lists. For instance, given list [1, 2, 3], we could add the list [2, 3, 4] and the result is a third list [3, 5, 7]. Our operation is defined only if the two lists are of the same size, hence an attempt to add two lists of differing sizes/lengths results in an error.

We will start by defining a trait for our unsafe integer list. Let’s also do the head/tail thing like Scala’s built-in List, so we will need a Nil object. Since this is prose :: and :: conz, we will definitely define a :: cons operator.

sealed trait UnsafeIntList { self =>
  def ::(head:Int):UnsafeIntList = UnsafeIntListImpl(head, self)
}

case object UnsafeIntNil extends UnsafeIntList 

case class UnsafeIntListImpl
  (head:Int, tail:UnsafeIntList) extends UnsafeIntList 

Now we can define some of our lists. Here are a few illustrative examples.

val empty = UnsafeIntNil
val size1 = 1 :: UnsafeIntNil
val size3 = 1 :: 2 :: size1

Our + operator can now be defined and implemented. Let’s first not worry about our constraint to only allow lists of the same size to by added for the moment.

sealed trait UnsafeIntList { self =>
  def ::(head:Int):UnsafeIntList = UnsafeIntListImpl(head, self)
  def +(other:UnsafeIntList):UnsafeIntList
}

case object UnsafeIntNil extends UnsafeIntList { self =>
  override def +(other:UnsafeIntList) = self
}

case class UnsafeIntListImpl
  (head:Int, tail:UnsafeIntList) extends UnsafeIntList {
  override def +(other:UnsafeIntList) = other match {
    case UnsafeIntListImpl(h, t) => (head + h) :: (tail + t)
  }
}

Now for a few examples of our new operator taken from the test code.

val sum0 = UnsafeIntNil + UnsafeIntNil
sum0 should equal (UnsafeIntNil)

val sum1 = (1 :: UnsafeIntNil) + (2 :: UnsafeIntNil)
sum1 should equal (3 :: UnsafeIntNil)

val sum2 = (1 :: 2 :: UnsafeIntNil) + (3 :: 4 :: UnsafeIntNil)
sum2 should equal (4 :: 6 :: UnsafeIntNil)

Without equipping our list with types, we will have to validate this size constraint at run time. Let’s give our unsafe integer list a size property and require it to be equal when calling +.

sealed trait UnsafeIntList { self =>
  def ::(head:Int):UnsafeIntList = UnsafeIntListImpl(head, self)
  def +(other:UnsafeIntList):UnsafeIntList
  def size:Int 
}

case object UnsafeIntNil extends UnsafeIntList { self =>
  override def +(other:UnsafeIntList) = {
    require(other == UnsafeIntNil, 
      "argument 'other' must be the UnsafeIntNil object")
    self
  }
  override val size = 0
}

case class UnsafeIntListImpl
  (head:Int, tail:UnsafeIntList) extends UnsafeIntList {
  override def +(other:UnsafeIntList) = {
    require(other.size == size, 
      "argument 'other' must have the same size as "+
      "this UnsafeIntList")
    other match {
      case UnsafeIntListImpl(h, t) => (head + h) :: (tail + t)
    }
  }
  override val size = 1 + tail.size 
}

We can also test this with ScalaTest thanks to intercept.

intercept[IllegalArgumentException](
  (1 :: UnsafeIntNil) + UnsafeIntNil
)
intercept[IllegalArgumentException](
  (1 :: 2 :: UnsafeIntNil) + UnsafeIntNil
)
intercept[IllegalArgumentException](
  (1 :: 2 :: UnsafeIntNil) + (3 :: UnsafeIntNil)
)
intercept[IllegalArgumentException](
  (UnsafeIntNil) + (3 :: UnsafeIntNil)
)

One thing worth noting is that if you compile this code (and you’re welcome to go fork it), you will get this warning:

[warn] UnsafeIntList.scala:20: match may not be exhaustive.
[warn] It would fail on the following input: UnsafeIntNil
[warn]     other match {
[warn]     ^

You can alleviate this warning by adding a case for UnsafeIntNil, but I really don’t want to because I know that case will never happen. We know that our require will always eliminate the possibility of an empty list, yet the compiler is unaware. This is because we are enforcing this constraint at run time, unbeknownst to the compiler. Spoiler alert: This won’t happen when we use types later.

So this all works, right? We can certainly use this class to write some very useful software that will satisfy customers and make us all rich. Yet we can still make it better, and always improving is quintessential to living this agile life. Note that like all good data structures in software, our UnsafeIntList is immutable. You cannot add elements to a list. Doing so yields a new list. Hence the size/length is always known at compile time. Theoretically we can encode this knowledge via types into our integer list and validate our + operation at compile time. It turns out this theory is demonstrable in Scala.

What we need first is a way to encode the size of a list as a type. We’ll use the PeanoType we developed last time. For clarity in this blog post, I renamed PeanoType, Type0, and TypeN to SizeType, Size0, SizeN, respectively. Help yourself to the code if needed.

Let’s start from scratch with our new and improved IntList.

sealed trait IntList[Size <: SizeType] { 
  def ::(head:Int):IntList[SizeN[Size]] = ???
}

What we have here looks much like our UnsafeIntList. The difference is we have a type parameter Size which is a SizeType. Notice that our cons operator will return a list of size one greater than the size of our list, also known as SizeN[Size].

Let’s now take a quick look at our IntNil

case object IntNil extends IntList[Size0] 

It’s an IntList of Size0. And now for our case class.

case class IntListImpl
  [SizeTail <: SizeType]
  (head:Int, tail:IntList[SizeTail]) 
  extends IntList[SizeN[SizeTail]] 

Let’s break this one down. Our class is a function of a head element and a tail IntList, hence line 3 is much like the argument definition given in UnsafeIntListImpl. Because the tail argument has a type associated with it, namely SizeTail, we have to pass that type as a parameter to the class in line 2. Finally, our class extends IntList as you should expect. Here we give the size type as SizeN[SizeTail] because our new list is precisely one element larger than the previous. Now we can go back to our IntList trait and implement the cons operator.

sealed trait IntList[Size <: SizeType] { self =>
  def ::(head:Int):IntList[SizeN[Size]] = IntListImpl(head, self)
}

Our usage looks the same as before, where 1 :: IntNil constructs the list containing only the element 1 for instance. Now let’s begin adding our + to each of our constructs. The declaration in IntList is very straight forward. The signature just takes a list with our size and returns another list with the same size.

sealed trait IntList[Size <: SizeType] { self =>
  def ::(head:Int):IntList[SizeN[Size]] = IntListImpl(head, self)
  def +(other:IntList[Size]):IntList[Size]
}

Thanks to the Size type on our trait, we are able to constrain the other argument and the returned IntList to conform to the same size as our list. Because the size must be the same and our IntNil is an object, the implementation of + on IntNil is trivial.

case object IntNil extends IntList[Size0] { self =>
  override def +(other:IntList[Size0]) = self
}

To conform to the parent trait’s definition of +, we provide the Size0 type for the argument list and we simply return our self reference since we are the singleton Nil object.

Now the implementation of + on the case class IntListImpl is where things get quite interesting. Let me show you then I’ll discuss the key features.

case class IntListImpl
  [SizeTail <: SizeType]
  (head:Int, tail:IntList[SizeTail]) 
  extends IntList[SizeN[SizeTail]] 
{ self =>
  private type Size = SizeN[SizeTail] // defined for clarity
  override def +(other:IntList[Size]) = other match {
    case IntListImpl(h, t) => (head + h) :: (tail + t)
  }
}

First I added the type definition on line 6 for clarity. Now we can refer to our size as simply Size rather than our size we calculated as SizeN[SizeTail]. Just as with the trait definition of +, we see that our argument has its size type constrained to equal our own. The function body is simply a pattern match on our argument as before to let us extract the head and tail of the argument. Given the head and tail of our argument, the sum is simply the sum of the heads constructed with the sum of the tails.

Remember that compiler warning about a non-exhaustive match? Even though we are not including the IntNil as a potential match, we don’t get that any more. The compiler is able to infer that this is not a possibility, unlike with our run time value-level programming check from before. As a matter of fact, we cannot include IntNil as a case. Try it, and you’ll get the following compiler error.

[error] IntList.scala:17: pattern type is incompatible with expected type;
[error]  found   : com.joescii.typed.IntNil.type
[error]  required: com.joescii.typed.IntList[IntListImpl.this.Size]
[error] Note: if you intended to match against the class, try `case _: <none>`
[error]     case IntNil => self
[error]          ^

Now let’s take a look at some usages of our type-safe IntList. The legal cases look the same.

val sum0 = IntNil + IntNil
sum0 should equal (IntNil)

val sum1 = (1 :: IntNil) + (2 :: IntNil)
sum1 should equal (3 :: IntNil)

val sum2 = (1 :: 2 :: IntNil) + (3 :: 4 :: IntNil)
sum2 should equal (4 :: 6 :: IntNil)

As we’ve seen in previous posts, the most interesting thing in type programming isn’t so much what can be compiled, but what doesn’t compile. Once again, I used illTyped from shapeless to make repeatable negative compilation test cases.

illTyped("(1 :: IntNil) + IntNil")
illTyped("(1 :: 2 :: IntNil) + IntNil")
illTyped("(1 :: 2 :: IntNil) + (3 :: IntNil)")
illTyped("IntNil + (3 :: IntNil)")

So for good measure, I also implemented size as with the UnsafeIntList so they will have the same features. I would argue that in most regards, this type-safe list is preferable to the unsafe list, yet interestingly enough it is fewer lines of code! The source for UnsafeIntList is 25 LOC while the source for IntList is 20 LOC. But to be fair… I probably should include the SizeType source which is 11 LOC.

This exercise reinforced something that occurred to me while watching the lectures in Principles of Reactive Programming course covering the Future monad. In statically-typed functional programming, we want to promote the maximal amount of information from run time calculations to compile time calculations. In this exercise, we moved the length constraint from run time to compile time. This has several compelling advantages. First is perhaps the most obvious, which is it helps us to produce a more valid or correct program. Secondly, it documents the program. We no longer rely on the developer of the IntList to be diligent and provide scaladoc caveats for what inputs will result in an error. Instead we simply read the type. Even if we misunderstand the type, the compiler will be sure to get it right. Finally I see an advantage in run time efficiency. Our code no longer needs to make a length check at run time to validate the arguments. They were validated a long time ago by the compiler. Many folks like to complain about how slow the Scala compiler is, but I suspect those folks don’t realize how much stuff like this it could be doing for them.

It’s the end of type-unsafe programming! Well, I don’t know. When I look at this, I don’t understand how we could use this list to store arbitrary data input. Maybe that’s okay. Perhaps it just means that a list is the wrong construct for storing arbitrary data if you want maximum type safety. I’m willing to bet that all of the Haskell guys long ago abandoned my pedestrian walk down type-programming lame, so I’m not counting on wiser counsel to help me here.

In the next week or so I plan to write another post on this topic. I have another example in mind which could be really interesting involving type equivalence. Stay tuned!

About these ads
Tagged with: , , ,
Posted in Software Development
2 comments on “Type programming: Constraining values
  1. […] my next post (UPDATE: posted) I have in mind to play around with these types in value-level programming. Now that we’ve […]

  2. […] Last time we explored how we can use the Peano-encoded natural number type to define constraints on on values. In particular, we created an IntList type which has a + operator to perform the matrix sum of two like-sized lists. We used our SizeType to instruct the compiler to constrain the arguments to only allow lists of the same size/length. We accomplished this by simply declaring our argument for + with the same SizeType as declared for the containing class. […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 623 other followers

%d bloggers like this: