Type programming: Constraining values with equivalent types

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.

But what about all of those interesting operations we defined on BoolType and SizeType (originally named PeanoType)? Were those just for show, but otherwise useless? Well it turns out that those can be quite handy too. In our + operation, we didn’t take the other list’s size type as an argument. Instead we pinned it down to match Size of the list being operated on.

sealed trait IntList[Size <: SizeType] { 
  def +(that:IntList[Size]):IntList[Size]
}

Just as we can pass values to our methods as parameters, we can pass types as parameters. These types can be combined to produce the return type. For instance, we could define a ++ which accepts another list but with a different list size.

sealed trait IntList[Size <: SizeType] { 
  def ++[ThatSize <: SizeType](that:IntList[ThatSize]):Unit
}

Let’s define ++ to mean “concatenate”. Given this list and that list, the concatenation should be a list with size equal to the sum of the two lists. If you recall from when we developed PeanoType/SizeType, we had an add type operator. Hence, our return type for ++ should be the length of this list added to the link of that list.

sealed trait IntList[Size <: SizeType] {
  def ++[ThatSize <: SizeType](that:IntList[ThatSize]):
    IntList[Size#add[ThatSize]]
}

Unfortunately, I want to rename something once again. To me, add implies an action to be taken. On the other hand, if I rename it to plus I believe it feels more like an expression. In this case, I’m not adding as much as I am expressing the resulting type is the sum of the two. So bear with me as I change our name from two posts ago to plus

sealed trait IntList[Size <: SizeType] {
  def ++[ThatSize <: SizeType](that:IntList[ThatSize]):
    IntList[Size#plus[ThatSize]]
}

Let’s now implement our ++ concatenate in our IntNil object. It’s trivial because any list concatenated with the empty list is the same list.

case object IntNil extends IntList[Size0] {
  override def ++[ThatSize <: SizeType](that:IntList[ThatSize]) = 
    that
}

It should not take much to be convinced that this will pass the type checker. That is to say, Size0#plus[ThatSize] is equivalent to ThatSize, hence the return type needs to be equivalent to IntList[ThatSize]. Since we are returning that we’re good to go. You can fork it and compile it for yourself if need be.

Now we should consider how to implement ++ in our IntListImpl case class. We’ll just a little dab of recursion. We can define the result as a new IntListImpl, where our head element is the head element of the resulting list, and the tail is our tail concatenated with the argument.

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

  private type Size = SizeN[TailSize] // defined for clarity

  override def ++[ThatSize <: SizeType](that:IntList[ThatSize]) = 
    IntListImpl(head, tail ++ that)
}

If you are uncomfortable with recursion, it may take a few thoughtful moments to see how this one works. The main thing to keep in mind is that you assume the recursive call is correct. Hence you can trust that the expression tail ++ that correctly concatenates the two lists. Given that concatenation and our own head element, you have the resulting list you wanted.

The first thing that is interesting here is that our recursive expression does not yield the type Size#plus[ThatSize]. Instead, it is SizeN[TailSize#plus[ThatSize]]. However, because those two types are equivalent (that is, implicitly[Size#plus[ThatSize]] =:= SizeN[TailSize#plus[ThatSize]]], the code compiles! The compiler is able to perform the logic to deduce that the types are equivalent and therefore passes the check.

Now I’ll be the first to admit that all of this code is kinda ugly, especially coming from a language which prides itself in elegance. While it may be unsightly, code which utilizes our list bears no witness to it. Given the compile checks this gives us, I think it is well worth the ugliness. Let’s take a look at some of the test cases.

(IntNil ++ IntNil) should equal (IntNil)
((1 :: IntNil) ++ IntNil) should equal (1 :: IntNil)
((1 :: IntNil) ++ (2 :: IntNil)) should equal (1 :: 2 :: IntNil)
((1 :: IntNil) ++ (2 :: 3 :: IntNil)) 
  should equal (1 :: 2 :: 3 :: IntNil)

Ok, nothing special there, right? It’s just lists concatenated together. Checkout what happens when we combine our two operators for matrix sum and concatenation.

(((1 :: 2 :: IntNil) ++ (3 :: IntNil)) + 
  (4 :: 5 :: 6 :: IntNil))
  should equal (5 :: 7 :: 9 :: IntNil)

Recall last time that the + sum operator disallowed two lists of differing sizes. Notice that this code compiles because the types are equivalent as you would logically deduce. Fortunately, the compiler likewise deduces this equivalence and gives us the type safety we wanted.

These last few blog posts have really opened my eyes to the capabilities of the Scala type system. At this point I feel much more confident in my ability to follow more advanced blog posts and projects which extensively utilize the Scala type system, and I hope my readers feel the same way. In the coming weeks, I plan to prepare this blog series into a presentation I’ll be giving at the local functional programming meetup HuntFunc. I’m not sure where I’ll go next with my exploration of the Scala type system. Have any recommendations? Post them below or hit me up on twitter. Thanks as always for reading!

About these ads
Tagged with: , , ,
Posted in Software Development
2 comments on “Type programming: Constraining values with equivalent types
  1. mikolaj says:

    One thing I’ve observed is that if I put this in the body of IntListImpl:

    implicitly[ SizeN[Size0]#add[SizeTail] =:= SizeTail#add[SizeN[Size0]] ]

    it fails with:

    [error] wtf.scala:27: Cannot prove that SizeN[SizeTail] =:= SizeTail#add[SizeN[Size0]].
    [error] implicitly[ SizeN[Size0]#add[SizeTail] =:= SizeTail#add[SizeN[Size0]] ]

    So what I was trying to prove that SizeN[Size0]#add[SizeTail], which is 1 + SizeTail, was equal to SizeTail#add[SizeN[Size0]], that is SizeTail + 1, in the context of IntListImpl. I guess it doesn’t work because we don’t know if SizeTail is SizeN or Size0, SizeTail#add is abstract here. Still it means that addition is not commutative in this case, while with values I was free to write

    def size = 1 + tail.size
    or
    def size = tail.size + 1

    I’ve been trying to come around this somehow but I’ve failed so far. I might be missing something very obvious though. Do you have any ideas?

    Thanks!

    • barnesjd says:

      At first glance I do not see any problems with your code or logic. I’ll try it out myself to see if I find anything. It’s unfortunate that it doesn’t “just work”, but kudos for exploring commutativity like this!

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 569 other followers

%d bloggers like this: