During the last episode, we built a structure called Vect whose size is encoded in the type. There were some shortcomings however, which we will fix in this article. The goal still being to write, a zip function whose calls compile only with Vect of the same size.

A pinch of dependent types

Remember that when we called the plus3 function, we had to specify the size of the vector in the parameter : plus3[[X] =>> Vect[X, 4]](vect). First, wouldn't it be nice if we could write this without hardcoding the 4 type ? And using plus3[[X] =>> Vect[X, vect.size]](vect) instead ? The answer is to simply capture the type corresponding to the size. This can be done with this simple type alias:

enum Vect[+A, S<:Int]{
    /*
    ...
    definitions given in the first part
    ...
    */

    // Capturing S as a type 
    type Size = S

    def size(using V: ValueOf[S]) = V.value
    
}

The zip function

Having the size encoded in the type is an interesting feature as it gives an ability to let the compiler check things at runtime. In this regard, the compiler acts as a proof checker. Our zip function can explicitly be implemented for Vects which have the same size. The implementation is straightforward:

  • zipping two empty Vect result in the empty Vect
  • zipping two Vect result in a Vect of the same size as the inputs.

In Scala 3, it translates as this:

def [A, B, S <: Int] (v: Vect[A, S]) zip (w: Vect[B, S]): Vect[(A, B), S] = (v, w) match {
    case (Empty, Empty) => Empty
    case (Cons(a, ta), Cons(b, tb)) => Cons(a -> b, ta zip tb)
}

Once again we can see how to use the extension method syntax and how clearly the function takes as input two Vect with the same size S.

Perspectives

Our implementation of Vect is nice enough to have an overview of the future but has some issues associated with it. To begin with, it is absolutely not stack safe. Yet it was a nice example to start messing around with Dotty/Scala3.