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
In other words: boilerplate that wouldn’t even have to be in there.