Fail better

I have tried to use Idris a number of times in the past. I never got much further than copy & pasting the definition of Vect and writing append : Vect n t -> Vect m t -> Vect (n + m) t and zip : Vect n s -> Vect n t -> Vect n (s, t).

I have glanced at Agda and its ternary mixfix operators and dabbled in Coq, where you can write all the fancy dependent types, but none of the functions.

It never clicked, but I guess I must have learned something.

Last week I started another toy project in Idris. I had problems with types, and solved them by adding proofs of properties and using them. I even made Idris generate some proofs for me. It is so much fun!

Watch this space for an upcoming series on a tiny language with traced evaluation.

What’s my point? Not sure. Persistence pays off in learning?

My computer science teacher in high school had this quote from Worstward Ho by Samual Beckett on his door and I liked it even then.

Ever tried. Ever failed. No matter. Try again. Fail again. Fail better.

We did so much cool stuff. Program Turing Machines and microcode for some simulated CPU, write a meta-circular evaluator in Racket (which was called PLT Scheme back then), discuss the Entscheidungsproblem and proofs by diagonalisation. I did not appreciate it at the time. I wanted to write real programs™, in a real language, like Java™. 🤦