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!

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!

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!