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.

making haskell EDSLs shebangable

There's a mindset that says to solve your problem, first write a language to solve your problem in, and then solve your problem in that language. And there's a mindset that says that your language should be an embedded language inside Haskell. In many ways that is appealing.

I wanted to write something that would delete old rsync snapshots. I took the domain-specific language approach, where the language specifies the retention policy for snapshots, like this:

policy = recent <||> weekly <||> monthly

meanings the final policy is to keep 'recent', 'weekly' and 'monthly' backups, with other statements defining what those three other policies mean. I won't write more about the language here - there's more on the webpage for the tool, snaprotate.

One particular piece of this I don't feel terribly comfortable with, and thats how to invoke/run the policy files.

I can imagine two different interfaces:

$ snaprotate -f policyfile

or

$ policyfile

I took the second approach, making policies first order unix executables - commands that can be run like any other command.

In unix tradition the way you indicate the language of a script is with a shebang line (#!/something) at the start of the script.

So then I want my scripts to look like something like this:

#!/usr/bin/snaprotate

policy = recent <||> weekly <||> monthly

This is almost a valid Haskell program, but: i) I need to import the SnapRotate module, and ii) I don't want to specify a main routine (which looks something like:

main = runPolicy policy

).

So the snaprotate commandline looks almost like runhaskell but does some source file rearranging to address the above two points, and to remove the #! shebang line.

#!/bin/bash
FN=$(mktemp /tmp/snaprotateXXXXX).hs
FNHS=$FN.hs
LIBDIR=$(dirname $0)

cat > $FNHS << 32804384892038493284093
import SnapRotate
main = runLevels policy

32804384892038493284093

cat $1 | grep --invert-match '^#!' >> $FNHS
shift
runhaskell -i$LIBDIR $FNHS $@

I wonder if this is the best way to implement such an embedding?

ALTER

I discovered the ALTER command in COBOL, in this note on eliminating that command, allowing self-modifying code. A couple of quotes:

ALTER changes the destination of a GO TO statement elsewhere in the program. It complicates the task of eliminating GO TO, especially if you don't notice that the ALTER is present.

and even worse:

In the presence of segmentation, ALTER can behave in unexpected ways. If an independent segment contains an altered GO TO, and the segment is overlaid and then reloaded, the GO TO is reset to its original destination.
If you ever encounter this form of pathology, proceed with extreme caution. You have found either a bizarre and subtle bug or a vicious marauding style of programming. Quite possibly both.

stack trace in perl

As a user, I hate java stack traces (because they expose the guts of the program, when I don't care about those guts). But as a programmer, I have come to realise how much I like them, when faced with errors like this:

Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.

where the error is actually deep inside the call on line 27.

So googling around I found this line to put at the start of a program:

$SIG{ __DIE__ } = sub { Carp::confess( @_ ) };

which replaces those short die messages with a stack dump produced by Carp:

Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.
 at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 7
 Stupid::C::__ANON__('Can\'t call method "emitCode" on an undefined value at /Users...') called at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27
 Stupid::LanguageWrapper::emitCode('Stupid::LanguageWrapper=HASH(0x8ff9b4)') called at ../src/stupid.pl line 44

which I hope I'll find more useful...

ASCII art C++ constants

I came across Multi-Dimensional Analog Literals in C++. This is an implementation in standard C++ templates that lets you write constants out using ASCII art (in 1, 2 or 3 dimensions):

  unsigned int c = ( o-----o
                     |     !
                     !     !
                     !     !
                     o-----o ).area;

  assert( c == (I-----I) * (I-------I) );

I think the same would be straightforward to implement using Template Haskell's quasiquoting mechanism, which allows you to embed parsers for fairly arbitrary sublanguages inside Haskell source. I wonder what other languages you could also implement something like this in.