[eru]

If you wrote an S-Expression syntax on top of Agda (or Haskell), you gain all of Lisps anti-boilerplatitude for free. There's of course also Template Haskell.

As it is, the static typing helps to avoid some boilerplate, too, indepedent of macros. In some sense, static typing removes, among other things, boilerplate tests.