Opened 3 years ago

#12561 new bug

Scope extrusion in Template Haskell

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 8.0.1
Keywords: TemplateHaskell Cc: goldfire, oleg@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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 QQ has more limited effects. This would work, and has the merit of simplicity. We can read stuff (reification), report errors, and even catch those exceptions -- provided that we don't include 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."

Change History (0)

Note: See TracTickets for help on using tickets.