Embedded unit-tested examples in source code

[cdsmith]

If we can get Template Haskell working, we should add a TH-based unit test system that can be embedded into the code. Though, this might be complicated to do with staging restrictions.

[cdsmith]

I think the better way to do this would be to use a source plugin to:

1. Parse the module with some stolen syntax for examples.
2. Extract the stolen example syntax, stash examples in a global IORef, and remove them from the parse tree.
3. In a later stage, inject code to check the condition at runtime, before calling the user's main.

Perhaps this would look something like:

f :: Number -> Number
f(x) = 8 * x + 2

Examples
    | f(0) = 2
    | f(5) = 42

That's a little ugly, as all stolen syntax is. Notice that the source syntax is initially parsed as a definition with guards, but it can be rewritten into a comparison for equality by a source plugin that runs after parsing or renaming.

I'd really want a colon instead of |, but that would be a syntax error because f(5) isn't a pattern. I suppose one could start out with a colon there in the original source, and then do something hacky to replace it with | before GHC sees the code. But I need to decide exactly how far down that path I'm willing to go.

[cdsmith]

Of course, the other option is:

f :: Number -> Number
-- Example: f(5) = 42
f(x) = 8 * x + 2

A plugin could just as easily parse this and make it execute at runtime. It's just a little hokey because it's a comment, and students are taught that those don't matter... but now this becomes "except for this one!"

[cdsmith]

Another alternative bit of stolen syntax is to add a generic assert with ==:

f :: Int -> Int
f(x) = 8 * x + 2
Example: f(0) == 2
Example: f(5) == 42

This parses as a TH splice whose value is a list with first element Example and the rest of the list as f(0) = 2. Obviously a type error, but if you enable TemplateHaskell syntax, it is a valid parse, so a source plugin can steal it. The advantage here is that you can be more flexible and write something like:

Example: all([ f(x) > 0 | x <- [0..10] ]

I think I like this one best.

[cdsmith]

Status: I have started to build a GHC plugin for this. It's fairly easy to find and extract the assertions according to this rule. The remaining tasks are less clear:

• Injecting code into main to run the example tests. It seems like doing this in a source plugin is the wrong place, especially when one deals with the existence of things like:

module Main (main) where
(main, foo) = (putStrLn "Hello", 5)

• Writing the code for the assertion checking, which includes some non-type-checked code that was extracted after parsing and munged, and now needs to be resolved and type-checked and incorporated into other synthetically generated code.

• Producing helpful error messages in the example checking, which means pulling out and describing subexpressions of the assertion to describe why it failed. I feel like we want something similar to the assert-explainer plugin here.

When I have a decent story for making this work, I'll check in the code and see where it goes.