Typechecker-directed epiphanies

As I get more experience with powerful type systems like that of Idris and Mercury, I’m noticing a strange phenomenon. These type checkers deal with powerful logics, but the checkers themselves are not very smart; they can only verify a property if it’s syntactically obvious. And if you don’t have much experience with such a type checker, and haven’t learned the quirks of exactly what “syntactically obvious” means, programming in that language can be a chore. It’s been a while since I felt lost in Idris, but since lately I’ve been learning Mercury, I’m getting reacquainted with the despair of “Why won’t you accept this obviously-correct code, compiler?”

But as you get more familiar with what exactly the compiler checks, your relationship with it starts to change. The question changes from “Why can’t the stupid compiler see this?” to “Well, how do I know my code is correct?” And something that very often happens is, once I’ve thought for a few moments about how I know what’s going on, it’s immediately clear how to rewrite the code so that the compiler knows what’s going on.

But more importantly: sometimes, when I’ve taken a moment to think rigorously, I realize that my code isn’t correct. Maybe the Mercury predicate that is supposed to be deterministic actually has multiple solutions — not just the way I wrote it but the way I meant it, and I have to come up with a different plan for writing the predicate because my old one is flawed. And I would never have noticed it before because as far as I can tell, the code is obviously correct.

I admit that stupid typecheckers verifying complicated properties is a bit of a usability problem for people inexperienced with the typechecker. I have felt that pain and frustration, and I know it isn’t pleasant.

But I think it might be worth it. Once the pain goes away, you’re left with an obligation to strengthen your understanding of your code — to go from “This obviously does what I want it to do” to “Here, Stupid Compiler, you can’t understand my higher level thought processes, so let me walk you through it.”

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s