syntactically correct type-checkable /* NOTIMPL */

Agda, a dependently typed programming langauge Agda has a neat feature for partially written code.

Often I'll flesh out code and write something like a TODO inline. I'm sure lots of other people do to.

(For example, in C:

  int x;
  x = TODO_CALCULATEX();

This won't compile, so you don't get the benefit of compile time checking on your code until you've fixed up all your TODOs into something that makes sense to the compiler: either implementing it, or implementing a stub (an extreme case of which might be to replace the whole function call above by the constant 0).

In C and other languages which don't do much in the way of correctness checking at compiler time, thats ok.

For a lot of uses of Agda, the compile time checking is where all the interesting stuff is, though: for example, Agda types are where you put proofs like "this sort function really does sort".

Its a bit more awkward to make up stubs that claim in their comment or name to do something, whilst not doing it, because there is usually a lot more stuff in the type signature (such as the assertion that this sort function really does sort). You can't just put a return 0; and have it type check ok.

So, Agda uses a special extra bit of syntax: _ (an underscore) to mean "I have no value for this; but please pretend to all intents and purposes that you do." That way, compile time checking can carry on. Agda understand that its a TODO that you'll get to later on. Or even in some circumstances figure out the value for you.