As a follow up to my essay about Lambda the Ultimate copilot and boilerplate, Csepp over on Merveilles Town kindly pointed me to this lecture by Edwin Brady.

The idea is that a strong type system can help you do development automatically.

In the example, Brady is showing how to make a two-dimensional matrix transpose, M-wide and N-high.

First, Brady types in:

```
transpose : (matrix : Vect n (Vect m ty)) -> Vect m (Vect n ty))
```

The type-aware bot turns that into:

```
transpose : (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose matrix = ?transpose_rhs
```

He moves his cursor to the `matrix`

in the second line, hits another key, and the bot makes it:

```
transpose : (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = ?transpose_rhs_1
transpose (x :: xs) = ?transpose_rhs_2
```

He manually changes `?transpose_rhs_1`

to `?empties`

, hits another chord and the bot then generates this:

```
empties : Vect m (Vect Z ty)
transpose : (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = ?transpose_rhs_1
transpose (x :: xs) = ?transpose_rhs_2
```

Stepping his cursor up to the `empties`

line, he hits a key and we now have:

```
empties : Vect m (Vect Z ty)
empties = ?empties_rhs
transpose : (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = ?empties
transpose (x :: xs) = ?transpose_rhs_2
```

He sees that this is gonna bork somehow, so he deletes the two `empties`

lines, leaving him with the three `transpose`

lines, typing eleven characters the first one to read:

```
transpose : {m : _} -> (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = ?empties
transpose (x :: xs) = ?transpose_rhs_2
```

So when he then again “lifts” the `empties`

, he gets a more complete version:

```
empties : (m : Nat) -> Vect m (Vect Z ty)
```

And his bot can then turn that into:

```
empties: (m: Nat) -> Vect m (Vect Z ty)
empties Z = []
empties (S k) = [] :: empties k
```

He then by hand edits the last line of his `transpose`

function so he has:

```
transpose : {m: _} -> (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = empties m
transpose (x :: xs)
= let xs_trans = transpose xs in
?transposeHelper
```

Lifting the `transposeHelper`

gives him (in addition to the empties function):

```
transposeHelper : Vect m ty -> (1 xs_trans : Vect m (Vect k ty)) ->
Vect m (Vect (S k) ty)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
transposeHelper (x :: xs) [] zs = []
transposeHelper (x :: xs) (y :: ys) zs = transposeHelper (x :: xs) x zs
transpose : {m: _} -> (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = empties m
transpose (x :: xs)
= let xs_trans = transpose xs in
?transposeHelper xs x xs_trans
```

He sees that this is gibberish, because he doesn’t have a termination checker (like we’ve got in brev with `define-some`

or `descend`

)

He undoes this “lift and generate, going back to:

```
transpose : {m: _} -> (matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = empties m
transpose (x :: xs)
= let xs_trans = transpose xs in
?transposeHelper
```

Examines the vars in the env, thinks a bit… and the solution to type trouble is more types! It’s not enough to specify what it is, let’s also specify how many it is. He changes `matrix`

to `1 matrix`

. And now it works:

```
transposeHelper : Vect m ty -> (1 xs_trans : Vect m (Vect k ty)) ->
Vect m (Vect (S k) ty)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
transpose : {m: _} -> (1 matrix: Vect n (Vect m ty)) -> Vect m (Vect n ty)
transpose [] = empties m
transpose (x :: xs)
= let xs_trans = transpose xs in
transposeHelper x xs_trans
```

So, he types… let’s see, 74, 7, 32, 16… a total of 129 characters to
generate eleven lines of code across three functions (`transpose`

,
`empties`

, and `transposeHelper`

). And note that he has to write the
actual logical body of `transpose`

himself (and even then it didn’t
work until he changed the types and re-generated the helper).

Coincidentally, I needed a 2d matrix transpose the other day for something and you know how that looks in brev?

```
(over args)
```

That’s it.

Here’s an example:

```
(apply (over args) '("lime"
"idea"
"psst"))
```

returns

```
("lip"
"ids"
"mes"
"eat")
```

And here’s a port of his generated code to brev so any Haskell-averse readers can see how his works:

```
(define (transpose-helper (x . xs) (y . ys)) (cons (cons x y) (transpose-helper xs ys)))
(define (transpose-helper (x . xs) '()) (cons (cons x '()) (transpose-helper xs '())))
(define (transpose-helper '() '()) '())
(define (transpose (x . xs)) (transpose-helper x (transpose xs)))
(define (transpose '()) '())
```

And OK, to us nerds of the ML family and Haskell, we can follow along with what’s going on when we read the generated code, but I’m sure that to most people, this style of code is kinda… ivory tower?

Compared to how it would look like expressed in R5RS:

```
(define (transpose lis) (apply map list lis))
```

I just don’t get the type hype. I just don’t. I’m keeping an open mind that that camp might one day create something useful but I’m watching from afar, I’m not eager to dive in.

The so called “auto-generation” is him

- taking a function name, reading the types of its argument from the env (since those vars were annotated previously), and lifting it to a typed prodecure spec (a contract, for y’all Eiffel fogeys) with annotations
- expanding a procedure spec into the standard cons recursion

In other words: boilerplate that wouldn’t even have to be in there.