[Haskell-cafe] something between a QQ and Q Exp?

[Nicolas Frisby]

This message motivates adding support to Template Haskell for code
that can be spliced but can no longer be intensionally analyzed.

I'm trying to use the well-known technique of a hidden constructor in
order to represent values that satisfy a particular predicate.

> module Safe (Safe(), safe, mkSafe) where
>
> newtype Safe a = Hidden a   -- the Hidden constructor is not exported
> safe :: Safe a -> a                -- the safe observer is exported

In my case, the predicate is a restriction on the Haskell syntax used
to define the value. In fact, in order to check my predicate, I need
some of the information that TH embeds in the result of a [| ... |]
quote. Thus I'm using TH to validate the construction of Safe values.

> isSafe :: Exp -> Bool
> isSafe = ... -- uses TH metadata embedded in the Exp
>
> mkSafe :: Q Exp -> Q Exp
> mkSafe m = do
>   e <- m
>   if isSafe e
>     then return (AppE (ConE 'Hidden) e)
>     else fail ("not safe:\n\t" ++ pprint e)

A user's construction of a Safe value then looks like "$(mkSafe [| ...
|])" in some other module. I'd like this to be the only way to build a
Safe value.

Unfortunately, TH is a double-edged sword. In particular, it can be
used to expose the Hidden constructor, thereby invalidating the Safe
type encapsulation of my invariant.

> abuse (AppE con _) = con
>
> uhoh :: a -> Safe a
> uhoh = $(liftM abuse (safe [| ... |]))

On the one hand, I need the user to use TH in order to construct Safe
values. On the other, abuse of TH is capable of breaking my security
kernel all together. If I could get by with a QuasiQuoter such as
"[mkSafe| ... |]", the Hidden constructor would indeed be safe since
the result of mkSafe is spliced in immediately and the user has no
further access to it. Unfortunately, QuasiQuoters don't have access to
the metadata that TH embeds in its quotations, which I need for
validation. This inspires my idea for a solution: something between
the two mechanisms.

My first thought for a solution involved a new core type for Template
Haskell. The Splice type would be completely abstract except for
constructing it from a splicable type and the ability to splice a
Splice into a program. So, TH could splice in either "Q alpha" like
normal or "Q (Splice alpha)", for alpha an element of {Exp, Pat, Type,
[Dec]}. "mkSafe" could be rewritten to generate a Splice instead of
just an Exp, and hence an abusive user could no longer snoop the
generated expression to extract the Hidden constructor. Unfortunately,
if Splice is just another newtype with a hidden constructor, then it
could be subverted in the same way that the "abuse" function exposes
the Hidden constructor. Without further support from the Template
Haskell system itself, it's turtles all the way down, I suspect.

The popularity and convenience of creating a safety kernel by hiding
constructors lends importance to plugging this hole, I think. Template
Haskell is a useful system, but it currently subverts the most common
lightweight approach to enforcing data invariants in the Haskell type
system. It'd be nice if both could be used in the same system --
especially since the user can invoke Template Haskell regardless of
the library author's intent.

Is there already a way to write a security kernel that is robust
against this sort of Template Haskell abuse? Or would we need further
support from the Template Haskell system?

Thanks for your time.