Ah, interesting. That last paper demonstration seems promising. I like that it lets you state laws like the monad law. I see it's also Core driven. I'll try it out. I've got a type I want to prove is Applicative and Alternative.
Andy, what's your assessment on the difficulty of working with plain Haskell?
For example, what if you took your HOOD project and used HSE or TH to annotate a whole source tree from expressions to patterns (with view patterns)? One thing I pondered was, e.g. if you have this program:
\x -> x
01234678 -- these are the columns
you could transform it to:
observe "(0,0)-(1,8)"
(\(observe "(0,1)-(0,2)" -> x) ->
observe "(0,7)-(0,8)" x)
Which would allow you to map back to the original source. But now instead of storing just locations, you want rather than just to see what things are being forced, you want to produce a series of valid source programs. So maybe you store kind of diff instructions, like this:
http://lpaste.net/114511 You get something like:
orig_ex = (\x -> (\y -> x * y)) 5 7
translated_ex =
seq (push (Reset "(\\x -> (\\y -> x * y)) 5 7")
((\x ->
(push (Set 0 25 ("(\\y -> " ++ show x ++ " * y)"))
(\y ->
push (Set 0 13 (show x ++ " * " ++ show y))
(x * y)))) 5 7))
stack
λ> readIORef translated_ex >>= mapM_ putStrLn . interpret
(\x -> (\y -> x * y)) 5 7
(\y -> 5 * y)
5 * 7
I think the problem I encountered was that I'd need alpha conversion, which would need something like haskell-names to resolve names. A little more involved as a project to pursue. There's probably some fatal flaw that means it's a terrible idea.
Presumably you've already considered things like this in your research.
Ciao