Scope extrusion in Template Haskell
With typed quotes [|| e ||]
and splices $$(e)
, Template Haskell is supposed guarantee to generate type-correct code. But a conversation with Oleg following my talk at the Cambridge Metaprogramming Summer School (Aug 16) made me realise that it isn't.
The problem is that
[|| e ||] :: Q (TExp ty)
So a typed quote is still monadic. That is useful because it means that a function returning code can fail gracefully:
f :: Int -> Q (TExp Bool)
f n | n < 0 = fail "Argument less than zero"
| otherwise = ....
yielding a civilised error in the type checker's monad.
But giving ALL the power of Q is too much. Below is a program cooked up by Oleg that demonstrates the problem concretely.
{-# Language TemplateHaskell #-}
module T where
import Language.Haskell.TH
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Ppr
import Data.IORef
show_code cde = (runQ . unTypeQ $ cde) >>= putStrLn . pprint
t1 = do
c1 <- [|| (1::Int) + 2 ||]
c2 <- [|| 3 + $$(return c1) ||]
return c2
t2 :: Q (TExp Int)
t2 = do
r <- runIO $ newIORef undefined
c1 <- [|| \x -> (1::Int) +
$$(do
xv <- [||x||]
runIO $ writeIORef r xv
return xv) ||]
runIO $ readIORef r
t1s = show_code t1
ts2 = show_code t2
Possible solutions.
- Give typed quotes access to only an emasculated Q monad, thus
[[| e ||] :: QQ (TExp ty)
where
TExp
values in exceptions (not sure how we prevent that!).
- Do what Meta OCaml does. Oleg writes "But you can go all the way and allow any effects. Q becomes no special (and possibly redundant). The stress is not on precluding scope extrusion statically but catch it immediately when it occurs (and report it with detailed error information: which variable has escaped, on which line of the source code was its intended binder, etc). This is what MetaOCaml does. I should stress it reports the scope extrusion even for open code, if one (of many) free variables in that code cannot eventually be bound. So the problem is not a scope extrusion per se: it is waiting until the whole code is generated to report it, at which time lots of information is already lost and it becomes very difficult to find the error. But reporting the error requires quite a bit of internal changes, to track free variables in any TH code fragment. Anyway, if you want to write the Wiki page, you can refer to my BER MetaOCaml paper, which describes the process."
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Template Haskell |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire, oleg@okmij.org |
Operating system | |
Architecture |