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 `Vect`

s 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.